Program Extraction Info
Yevgeniy Makarov
Where can I find documentation on program extraction in Isabelle? I am
interested in producing a lambda term with constructors corresponding to
conjunction, disjunction, and other connectives via Curry-Howard isomorphism,
for the purpose of manipulating this term by my own program (currently
written in Scheme). I am also interested in just producing ML programs.
Thank you,
Yevgeniy
--------
Send messages to isabell...@cl.cam.ac.uk
Conference announcements should be relevant and brief
Stefan Berghofer
> Hello,
>
> Where can I find documentation on program extraction in Isabelle? I am
> interested in producing a lambda term with constructors corresponding to
> conjunction, disjunction, and other connectives via Curry-Howard isomorphism,
> for the purpose of manipulating this term by my own program (currently
> written in Scheme). I am also interested in just producing ML programs.
Unfortunately, there is currently no documentation for the program extraction
module in the Isabelle user manual. More theoretical background information
on program extraction in Isabelle can be found in my PhD thesis available at
http://www4.in.tum.de/~berghofe/papers/phd.pdf
in particular in chapter 4 and 5. Isabelle's program extraction mechanism can
be invoked via the "extract" command. For example, if you have proved
the theorem
theorem pred: "x ~= 0 ==> EX y. x = Suc y"
by (cases x) simp_all
you can extract a program computing the predecessor of a natural number x
using the command
extract pred
This command does two things:
1. It adds a definition of the function "pred" to the current theory.
The definition can be inspected by the command
thm pred_def
which yields the output
pred == nat_case arbitrary (%nat. nat)
2. It proves a correctness theorem called "pred_correctness" for the
above function and stores it in the theorem database. This theorem
can be inspected by the command
thm pred_correctness
which yields the output
x ~= 0 ==> x = Suc (pred x)
When extracting programs from theorems containing predicate variables,
the user also needs to specify which of the predicate variables is
computationally relevant (this is similar to the Set / Prop distinction
in Coq). The relevant variables can be given to the extract command as
a comma-separated list in parentheses. As an example, consider the theorem
theorem or_commute: "P | Q ==> Q | P" by rules
An invocation of
extract or_commute (P, Q)
yields the program
or_commute_P_Q == %H. case H of Inl p => Inr p | Inr q => Inl q
whereas
extract or_commute
yields
or_commute == %H. case H of Left => Right | Right => Left
Note that relevant predicate variables only need to be specified at the
"top level": When or_commute is used in some other proof, the program
extraction module automatically figures out from the context, which
of the variables are computationally relevant.
More examples for program extraction can be found in the directories
HOL/Extraction or HOL/Lambda in the Isabelle distribution.
When adding new logical operators and basic inference rules for a logic,
one needs to do the following:
1. Specify corresponding programs (so-called realizers) and correctness
proofs for basic inference rules. This can be done via the
"realizers" command.
2. For every operator, specify what it means for a program (i.e. a term)
to "realize" a given formula involving this operator. This can be done
via the "realizability" command.
3. For every operator, specify the type of the program extracted from
a proof of a formula involving this operator. This can be done via
the "extract_type" command.
To get an idea how the above commands are used to set up program extraction
for a new logic, you can have a look at the file HOL/Extraction.thy in
the Isabelle distribution.
In order to use the program extraction module for a particular logic,
it must be compiled with proof objects switched on. This can be achieved
by adding
ISABELLE_USEDIR_OPTIONS="-p 2"
which switches on proof objects for all sessions, or
HOL_PROOF_OBJECTS="-p 2"
which switches on proof objects just for the HOL image. Moreover,
when working with ProofGeneral, make sure to switch on proof objects
for the current session by selecting the menu item
Isabelle -> Settings -> Full Proofs
Executable ML code can be generated from Isabelle terms using the
"generate_code" command, which is documented in section
"2.9. Executable specifications" of the Isabelle/HOL manual.
For example,
generate_code ("test.ML")
test = "or_commute_P_Q"
generates code for or_commute_P_Q and bind the result to the
ML identifier test. The generated code will be written to the file
test.ML. In contrast, the command
generate_code
test = "or_commute_P_Q"
directly loads the generated code into the Isabelle session.
Greetings,
Stefan
--
Dr. Stefan Berghofer E-Mail: berg...@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