Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Berghofer's program extraction mechanism and c...


view this post on Zulip Email Gateway (Feb 23 2021 at 17:57):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear all,

I'm interested to understand if/how Stefan Berghofer's program
extraction mechanism
for Isabelle as developed in his PhD thesis (in the sense of obtaining
realizers)
https://www21.in.tum.de/~berghofe/papers/phd.pdf

is related to the current approaches for code generation from
Isabelle/HOL.

It would be great if you could share your insights.

Many thanks in advance!
Angeliki

view this post on Zulip Email Gateway (Feb 23 2021 at 18:09):

From: Manuel Eberl <eberlm@in.tum.de>
I don't know terribly much about Berghofer's work, but I'm fairly
certain it has absolutely nothing to do with how the code generator works.

I think Berghofer's approach is closer to what people do e.g. in Coq:
using the Curry–Howard isomorphism to get code from the proof terms.

My impression from a distance that Berghofer's implementation is a very
impressive accomplishment, but one that has not been used for anything
but small examples so far.

One big problem is that (unless I misunderstood something) it only works
as long as you don't use any non-constructive reasoning (i.e. no axiom
of choice, no proof by contradiction).

However, one of the big strengths of Isabelle/HOL is automation, and
none of the automation cares about constructive vs non-constructive, nor
does it care about keeping proof terms small (because normally proof
terms are not stored anyway). Thus, if you use automation, Berghofer's
approach will either not work at all (because the automation used
something non-constructive somewhere) or run into performance problems
or give you horribly bloated code (because the automation produced huge
and overly complicated proof terms).

And these problems only become bigger if you apply it to bigger examples.

The code generator, on the other hand, works by having very tight
control over what code is produced: things like equational and recursive
definitions work out of the box, anything else (quantifiers, choice,
inductive predicates, abstract types, quotient types) requires some
extra work (e.g. proving code equations, running "code_pred", …).

Basically, the code generator works by translating equations in HOL into
"equations" in ML/Haskell/Scala/etc. and "pretending" that the meaning
is the same (which is somewhat justified). And anything constant that
isn't specified by a simple equation has to be brought into that form by
the user (by supplying code equations).

Hope that helps – if I said anything wrong, I'm sure someone will
correct me.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 24 2021 at 01:00):

From: Tjark Weber <tjark.weber@it.uu.se>
This is ameliorated by the fact that lemmas often have no
"computational content": their proofs do not affect the extracted
program. Therefore Isabelle's automation may still be useful in
(possibly large) parts of a formalization intended for program
extraction.

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

view this post on Zulip Email Gateway (Feb 25 2021 at 15:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Note that code generation using extraction from proofs works in two steps:

a) The extraction part: Turning a proof into a set of definitions and
corresponding equational theorems in Isabelle/HOL

b) The code generation part: Turning those theorems into executable
programs.

Hence there is no fundamental difference: both approaches rely on a
regular code generator, although that has been replaced in the meantime.

Personally I tend to view proof terms in Isabelle as a device to bolster
the logical foundations. The code generation examples in the
distributions are nice demonstrations – but the mechanism so far has no
impact on practical applications.

Cheers,
Florian
signature.asc


Last updated: Dec 08 2021 at 09:20 UTC