Re: [isabelle] proofterms incomplete wrt beta reduction



Sean McLaughlin wrote:
It is thus difficult, when translating these proof terms,
 to know with precision when to apply beta reduction and when not to.
I realize there is no beta axiom, as in HOL Light.  Is there a  general way
to tell when beta reduction should be applied?  Currently I apply it

One of the reasons why beta-conversion is not recorded in the proof object is
that Isabelle's central inference rule - higher-order resolution - works modulo
beta-conversion, too.
Interestingly, the Coq theorem prover goes even further and not only leaves
beta-conversion, but also iota-conversion (i.e. unfolding of recursive
definitions) implicit in proof terms. The ability to elide such
computations in proof terms turns out to be essential for applications
such as proof-carrying code, where the size of the transmitted proofs
needs to be kept as small as possible. One of my colleagues, who built
a proof-carrying code system based on Isabelle, noticed that even proof
terms for relatively simple safety properties of programs can reach an
enormous size just because of the numerous calls to Isabelle's simplifier
that are recorded in the proof term.

wildly everywhere I can and it seems to work most of the time, but I'd like to be precise about it.

This is exactly what the proof replaying function in Pure/Proof/proofchecker.ML
does as well. It uses only very primitive inference rules such as Thm.implies_elim,
which are *not* modulo beta-conversion (unlike higher-order resolution). Note
that eta-conversion needs to be done as well.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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