*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] HOLCF*From*: Brian Huffman <huffman at in.tum.de>*Date*: Fri, 29 Jun 2012 09:09:40 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FEA9BC8.8070602@jaist.ac.jp>*References*: <4FEA9BC8.8070602@jaist.ac.jp>

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

**References**:**[isabelle] HOLCF***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] jEdit: -l flag
- Next by Date: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Previous by Thread: Re: [isabelle] HOLCF
- Next by Thread: [isabelle] Quickcheck ML
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list