[isabelle] HOLCF



Dear Brian,

I'm currently experimenting with HOLCF (and reading your thesis in parallel), and I have to say, really nice work!

Some tiny things I noticed:
------------------------------------------------------------------
Domain Package:

* syntax annotations are allowed for constructors but do not work if given separately with "notation", e.g.,

  domain 'a list = Nil | Cons (lazy 'a) (lazy "'a list") (infixr ":" 65)

works, but

  notation Cons (infixr ":" 65)

doesn't (due to being a continuous function)


Fixrec Package:

* does not allow mixfix annotations (due to continuous function type), e.g.,

  fixrec append :: "'a list -> 'a list -> 'a list" (infixr "++" 65) where
    "Nil ++ ys = ys" |
    "(Cons$x$xs) ++ ys = Cons$x$(xs ++ ys)"

does not work. We have to introduce an intermediate abbreviation:

abbreviation append_syn :: "'a list => 'a list => 'a list" (infixr "++" 65) where
    "xs ++ ys = append$xs$ys"

General:

* definitions do not allow "natural" equations like "f$x$y = P x y", we have to use "f = Lambda x y. P x y" instead.

* a space after the unicode symbol for "Lambda" is mandatory, otherwise we get an inner syntax error
------------------------------------------------------------------

Shouldn't it be possible to reuse the same machinery that allows to give mixfix annotations for domain constructors at all other locations that allow for mixfix annotations?

Concerning usage of HOLCF in jEdit (I guess, this is for Makarius): could a translation from $ to the unicode cdot be added to the default "translation table", since typing "<space> c d o t" and then moving back in order to remove the space is slightly odd.

The more I read about HOLCF and its intended use to verify functional programs, the more I feel that it is a pity that code generation does not work for it. Currently if we want to verify Haskell code, we have to take the sources, translate them (manually?) into Isabelle, and verify the desired properties. However the original sources are still used for compilation and if those change, we might not even notice. It would be much more reliable to generate Haskell code (e.g., the Standard Prelude) from its Isabelle/HOLCF formalization automatically.

cheers

chris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.