*To*: Sean McLaughlin <seanmcl at cmu.edu>*Subject*: Re: [isabelle] proofterms incomplete wrt beta reduction*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Tue, 10 Jan 2006 11:50:32 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1819E108-5B75-4803-A8E3-CD76D9650195@cmu.edu>*Organization*: Technische Universität München*References*: <1819E108-5B75-4803-A8E3-CD76D9650195@cmu.edu>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

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'dlike 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

**References**:**[isabelle] proofterms incomplete wrt beta reduction***From:*Sean McLaughlin

- Previous by Date: [isabelle] IJCAR 2006: Call For Papers (CFP)
- Next by Date: [isabelle] SFM-06:HV - International School on Formal Methods
- Previous by Thread: [isabelle] proofterms incomplete wrt beta reduction
- Next by Thread: [isabelle] access axclass data
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list