Email Gateway (Aug 18 2022 at 20:14): Email Gateway (Aug 18 2022 at 20:14):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 18 2022 at 20:15):From: Tobias Nipkow <nipkow@in.tum.de>
There is Haskabelle for translating Haskelle to HOL. But data types become eager
in the process. One would need a similar translation to HOLCF.
Of course I agree that code generation for HOLCF would be very nice to have. We
had this on the agenda at some point - maybe we should get back to it.
Tobias
Email Gateway (Aug 18 2022 at 20:15):From: Till Mossakowski <till@informatik.uni-bremen.de>
we have implemented a translation of Haskell into Isabelle HOLCF as part
of the Heterogeneous Tool Set, see www.dfki.de/cps/hets. This has been
done some years ago and probably would need to be adapted to the latest
Isabelle version, though.
Best, Till
Email Gateway (Aug 18 2022 at 20:17):From: Brian Huffman <huffman@in.tum.de>
On Wed, Jun 27, 2012 at 7:36 AM, Christian Sternagel
<c-sterna@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.
Email Gateway (Aug 19 2022 at 08:04):From: Makarius <makarius@sketis.net>
Sorry, this does not make any sense. Things are more consistent now,
because the full responsibility is to the packages, which fulfill that
easily by handing over to standard Isabelle operations to introduce terms
with mixfix syntax and specifications in the standard way. So it all
works out uniformly in the post-Isabelle2005 era.
In contrast, the old scheme where 'consts' where separate had several
conceptual problems. The one that might still be remembered is the "unify
consts" problem: since an earlier 'consts' declaration would already be
polymorphic, a subsequent 'defs' (or derived form) would often get an
unexpected type, or different types for different equations.
Historically, this has led to some packages trying to "repair"
type-inference in different ways. So old 'primrec', 'recdef', 'inductive'
could give the user different versions of type-inference.
As already observed, abbreviations handle alternative syntax views better,
but users need to write them down themselves.
Some packages like 'inductive_set' allow the user to include such
abbreviations simultaneously into the specification -- they are recognized
by the Pure == form. Thus old idioms like pretending that "(x, y) : R" is
actually a judgement "x -R-> y" could be supported with reasonable add-on
functionality to that particular package. This is not exceedingly
elegant, but better than the old scheme based on 'translations', which
does not quite fit into the local theory specification concept.
Makarius
Email Gateway (Aug 19 2022 at 08:04):From: Makarius <makarius@sketis.net>
In principle the 'definition' package has a filter to convert between the
specification given by the user, and the actual definition of the strict
form "f == RHS". It is rather simplistic, though, so it can probably not
be stretched that far.
How about non-recursive 'fixrec'? That would be analogous to using 'fun'
in HOL to get pattern matching, instead of trying to add this
functionality to the basic 'definition' package.
Makarius
Email Gateway (Aug 19 2022 at 08:05):From: Makarius <makarius@sketis.net>
This is a consequence of the way greek letters were added to the
identifier syntax in 2003. \<lambda> was treated as a special case, and
you loose in all other situations, such as \<Lambda> here, or \<mu>,
\<iota> etc. that occurr occasionally in applications.
I have some ideas in the pipeline to address this problem and some others
wrt. sub/superscripts within identifiers, but I did not manage to try that
out yet, to see how it impacts existing theories. There is some renewed
motivation to do it soon, because I don't want to imitate slightly odd
identifier treatment of Proof General in Isabelle/jEdit.
Makarius
Email Gateway (Aug 19 2022 at 08:05):From: Makarius <makarius@sketis.net>
This is specific to HOLCF. Any global modification of the input method is
apt to cause annoyances in other situations, where $ or \<cdot> are used
differently / independently.
Until some better configuration for Isabelle/jEdit input methods becomes
available, you can add the following line to your
$ISABELLE_HOME_USER/etc/symbols file:
\<cdot> code: 0x0022c5 abbrev: $
Note that etc/symbols allows to change the "code" assignment as well, but
this should be done with great care, or not at all, to avoid chaos in the
communication with other users.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC