Re: [isabelle] HOLCF



On Wed, Jun 27, 2012 at 7:36 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> Dear Brian,
>
> I'm currently experimenting with HOLCF (and reading your thesis in
> parallel), and I have to say, really nice work!

Thanks!

> 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)

Yes, you would need to define this syntax using an abbreviation, like
you do below for your fixrec functions.

Way back when we used to define functions with separate "consts",
"syntax", and "defs" commands, HOLCF used to provide a replacement
"syntax" command that knew about the continuous function type.
Unfortunately things are less consistent now, when each command is
responsible for handling its own syntax declarations.

> 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"

Like most other function definition commands in Isabelle now, Fixrec
uses a standard Isar specification parser (Specification.read_spec) to
process its input; it handles both parsing and type inference. This
parser of course expects infix functions to have ordinary function
types. Adding support for infix with continuous function types would
probably require a complete reimplementation of specification.ML.

> 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.

This shouldn't be surprising, since definitions like "f$x$y = P x y"
are not sound in general; continuity checks are required.

Equations like this work fine with Fixrec. (Although you might want to
declare the equation with [simp del] if you don't want it unfolded
automatically.)

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

You also need spaces after alphanumeric quantifiers like "ALL",  "EX",
"THE", and "SOME", right? The same reasoning applies here, because
Isabelle's lexer considers \<Lambda> to be a letter; \<lambda> is an
oddball in that the lexer considers it to be a non-letter.

> ------------------------------------------------------------------
>
> 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?

Not easily. (See above about specification parser.) It used to be
easier in the old days with a single "syntax" command.

> 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.

I don't expect that all Isabelle users will want "$" to be replaced by
"\<cdot>", and anyway, shouldn't the input translations for jEdit be
customizable? It seems ridiculous to have to ask a developer to change
the distribution every time somebody wants to add a new input
translation.

In ProofGeneral, I have it set up to replace ",." with "\<cdot>"; this
shortcut works very well for me.

> 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.

John Matthews and I have occasionally discussed an old idea that could
help with all of the problems that you mentioned: Have HOLCF use
ordinary function types ("=>" instead of "->") in many more places,
e.g. constructor functions for domains, and user-defined fixrec
functions. (The continuous function type would still be needed for
some higher-order constructions.) At the same time, the various HOLCF
packages would need to generate continuity theorems for each new
constant. With ordinary function types, code generation would work,
infix declarations would work, and you wouldn't even need to type all
those \<cdot>s.

- Brian





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