Email Gateway (Aug 22 2022 at 16:15): Email Gateway (Aug 22 2022 at 16:15):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
based on repeated discussions and confusion when interacting with
functional programmers and type-theory based theorem prover users, I
wrote a blog post explaining how functions in Isabelle are different
than functions in Haskell/Coq/etc, and what the deal is about
undefined:
http://www.joachim-breitner.de/blog/732
Please let me know if I say something wrong that should not be said
like that on the Internet. Otherwise, feel free to share when you have
trouble explaining these things to someone.
Regards,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 16:15):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Joachim,
Many people will probably agree with you when you declare
Isabelle functions do not compute (unlike, say, Coq functions)
However, I think stopping at this declaration means giving up too easily on what Isabelle/HOL (and HOL in general) have to offer w.r.t. certified programming.
True, you can get non-computable behavior for the specifications of functions. But rather than saying that you cannot program in HOL, I would rather say that
the traditional machinery developed in HOL-based provers includes a functional programming language, but currently does not (bother to) clearly single it out, as a subset
of what can be specified. (Of course, singling that out would mean committing to intensional, extra-logical aspects -- which is always necessary when connecting logic with programming -- likewise, the termination property of a function written in Coq does not dwell in the Coq logic.)
To see my point, consider the same OCaml program in the following two scenarios:
1) generated from an Isabelle/HOL function
2) extracted from a Coq function
Say you prove something about the source functions in each of these provers. Is the fact proved in Coq more relevant for the OCaml program than that proved in Isabelle?
The answer is: No, provided some minimal precautions are taken about the specification and the code extraction setup. One can of course go into a discussion about the partial correctness restriction stemming from the additional flexibility of Isabelle/HOL's code generator (discussed by Haftmann and Nipkow), but this can be alleviated by removing that flexibility. Btw, for adequacy, both Coq and Isabelle would need to carefully consider that one reasons in a total logic about a program written in a "partial" environment, and rely on a form of "moral correctness" result (http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html).
Andrei
Email Gateway (Aug 22 2022 at 16:15):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
Am Donnerstag, den 12.10.2017, 19:40 +0000 schrieb Andrei Popescu:
Many people will probably agree with you when you declare
Isabelle functions do not compute (unlike, say, Coq functions)
However, I think stopping at this declaration means giving up too
easily on what Isabelle/HOL (and HOL in general) have to offer w.r.t.
certified programming.
Good point. I should add section
Say you prove something about the source functions in each of these
provers. Is the fact proved in Coq more relevant for the OCaml
program than that proved in Isabelle?The answer is: No, provided some minimal precautions are taken about
the specification and the code extraction setup. One can of course go
into a discussion about the partial correctness restriction stemming
from the additional flexibility of Isabelle/HOL's code generator
(discussed by Haftmann and Nipkow), but this can be alleviated by
removing that flexibility.
How can you achieve that?
Coq users stress the point that when you extract from Coq to Haskell,
you know it terminates. And similarly, when you translate Haskell to
Coq, and Coq accepts it, then this is in a way a termination proof of
the Haskell code.
Can we say the same for Isabelle code extraction?
(I guess we can say the same for Haskabelle translation from Haskell to
Coq, because fun requires well-founded recursion.)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 16:15):From: Makarius <makarius@sketis.net>
I generally like it. Yes, HOL is first and foremost classical
mathematics; the functional specifications give an appearance of
functional programming, without restricting it to a computational
world-view. The "programming" in HOL is good enough for most applications.
BTW, if you take the literal meaning of the word "undefined", it means
"not defined". So it fits well into your story. People who think of
"undefined" as "halt and catch fire" instruction are wrong :-)
Minor note: some ASCII => have sneaked in, but you appear to use Unicode
rendering of Isabelle symbols uniformly.
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 16:16):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Joachim,
See £££ below..
From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Joachim Breitner <joachim@cis.upenn.edu>
Sent: 12 October 2017 20:57
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
Hi,
Am Donnerstag, den 12.10.2017, 19:40 +0000 schrieb Andrei Popescu:
Many people will probably agree with you when you declare
Isabelle functions do not compute (unlike, say, Coq functions)
However, I think stopping at this declaration means giving up too
easily on what Isabelle/HOL (and HOL in general) have to offer w.r.t.
certified programming.
Good point. I should add section
Say you prove something about the source functions in each of these
provers. Is the fact proved in Coq more relevant for the OCaml
program than that proved in Isabelle?The answer is: No, provided some minimal precautions are taken about
the specification and the code extraction setup. One can of course go
into a discussion about the partial correctness restriction stemming
from the additional flexibility of Isabelle/HOL's code generator
(discussed by Haftmann and Nipkow), but this can be alleviated by
removing that flexibility.
How can you achieve that?
£££ E.g., refraining from using that flexibility. :- )
Coq users stress the point that when you extract from Coq to Haskell,
you know it terminates. And similarly, when you translate Haskell to
Coq, and Coq accepts it, then this is in a way a termination proof of
the Haskell code.
Can we say the same for Isabelle code extraction?
(I guess we can say the same for Haskabelle translation from Haskell to
Coq, because fun requires well-founded recursion.)
£££ We could achieve that, in principle, if we went through the trouble of automatically tracking executable specifications. In practice, I believe this is not such a big issue,: we can make sure this is the case by inspecting the definitions. Staying executable is easy -- the hard part is proving properties of the functions....
Andrei
-
Email Gateway (Aug 22 2022 at 16:16):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Joachim,
Just two pointers on this.
CakeML has a linkup from HOL4 function definitions to their deeply embedded CakeML
semantics. This linkup is used for code generation and ensures that the generated code
terminates.
Lars Hupel has been working on a link from Isabelle/HOL functions to CakeML's
semantics, using similar ideas. He is also able to generate CakeML code out of
Isabelle/HOL function definitions. I'm not sure, though, whether he has also shown that
all generated programs terminate. But the theory would definitely allow you to track that
fairly easily. He has a draft paper on his homepage:
https://www21.in.tum.de/~hupel/pub/isabelle-cakeml.pdf
Andreas
Email Gateway (Aug 22 2022 at 16:16):From: Lars Hupel <hupel@in.tum.de>
I only show that all the functions that I compile terminate (a side
effect of the dictionary construction), but I haven't show total
correctness of the resulting CakeML program.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:16):From: Joachim Breitner <joachim@cis.upenn.edu>
Hi,
you have a deep embedding of the extracted code equations, right? So
you could state termination, and (at least in theory) prove it in
Isabelle, couldn’t you?
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 16:16):From: Lars Hupel <hupel@in.tum.de>
The initial semantics (plain HO term rewriting) has no notion of
evaluation order or normal forms.
Instead one would need to define an alternative semantics that
prescribes an evaluation order and prove its correctness wrt original
semantics, or run my compiler to CakeML (which does precisely that).
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joachim,
based on repeated discussions and confusion when interacting with> functional programmers and type-theory based theorem prover users, I>
wrote a blog post explaining how functions in Isabelle are different>
than functions in Haskell/Coq/etc, and what the deal is about>
undefined:> > http://www.joachim-breitner.de/blog/732> > Please let me
know if I say something wrong that should not be said> like that on the
Internet. Otherwise, feel free to share when you have> trouble
explaining these things to someone.
thanks for that blog post, which does indeed cover the essence of the
relationship of Isabelle/HOL and functional programming.
Let me add some remarks:
a) Terminology
You are mixing Isabelle and Isabelle/HOL quite freely. IMHO it should
read Isabelle/HOL throughout.
b) Section »Not all function specifications are ok«
Notation »S« stands beside »Suc«. You might want to consolidate that.
c) Section »You can still compute with Isabelle functions«
You might want to add the key idea of the “moral reasoning” foundation:
interpret HOL equations as a shallow embedding of corresponding programs.
The approach still has its advantages, e.g. you get datatype abstraction
(almost) for free.
Lars' work goes beyond that by constructing a deep embedding of
equations into HOL itself.
d) Section »Termination is a property of specifications, not functions«
Speaking about »termination« for function specifications is illusive,
since the logic itself does not know about a concept called
»termination«. But you can utilize typical termination arguments (e.g.
well-founded relations) to automate the derivation of equations from a
primitive, abstract definition.
e) Why there is nothing but a quite loose characterization of the
»executable« sublanguage of Isabelle/HOL.
It is the sheer complexity of the system itself: The sublanguage is not
built into the logic, but appears by a elaborate stack of tools:
Tools to introduce concepts known from FP in a suitable manner:
datatype, function.
Tool to generate programs for sets of equations: code generator.
Both layers are highly customizable. Of course you can do some kind of
FP while you use, but you are always free to make it crumble down doing
some – apparent according to common sense but difficult to characterize
precisely – »nonsense«, e.g. non-terminating simp rules for the
termination prover.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 16:18):From: Lawrence Paulson <lp15@cam.ac.uk>
Surely the point is that Coq (or rather its underlying calculus, and similar type theories) have an operational semantics. The semantics of higher-order logic is set-theoretic. Therefore higher-order logic has no definitive operational semantics at all. Rather we identify an executable sublanguage.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC