Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Stefan Berghofer <berghofe@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC