The classical extraction module for Coq |
The classical extraction module for Coq enriches the Coq proof assistant [4] with a set of commands to extract programs from classical proofs built in the Coq environment. The target language of the extraction mechanism is the λc-calculus, an extension of λ-calculus with control primitives introduced by Jean-Louis Krivine to realize provable formulæ of classical logic. Extracted programs are stored in lambda-calculus object files (.lco) that can be inspected, loaded and evaluated using the jivaro toplevel that is distributed on the author's web page.
The classical extraction module for Coq is copyright © 2009 Alexandre Miquel.
The classical extraction module for Coq is free software: you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation, either version 3 of the License, or any later version. You should have received a copy of the GNU Lesser General Public License along with this program. If not, see http://www.gnu.org/licenses/.
The classical extraction module for Coq is distributed on the author's
web page at
http://perso.ens-lyon.fr/alexandre.miquel/kextraction/
The classical extraction module has been designed and written by Alexandre Miquel (Alexandre.Miquel@ens-lyon.fr) using ideas developped in [1] and [3].
The classical extraction module for Coq comes as a bunch of ML files that can be statically or dynamically linked with Coq (version 8.2 or higher). The installation procedure is described in the file INSTALL in the archive.
When compiled as a dynamically linked module, the classical extraction module is loaded into the Coq environment using the command
Require ClassicalExtraction.
(typing ClasssicalExtraction as one word). The classical extraction commands described in section 3 are then available in the Coq toplevel.
When compiled as a statically linked module, the classical extraction commands are immediately available, without the invocation above.
The classical extraction module provides the following commands:
This command extracts λc-terms from the objects denoted by the qualified identifiers qualid1 … qualidn as well as from all the objects they may depend on in the current environment. The result is stored in a lambda-calculus object file "file", with extension .lco added if necessary. This file can be inspected, loaded and executed in the jivaro toplevel.
The command Classical Extraction "file" qualid1 … qualidn is equivalent to the sequence of commands
Classical Extraction Reset.Classical Extract qualid1 … qualidn.
Classical Extraction Save "file".
This command clears the current list of λc-definitions. All the λc-definitions contained in the list before the command was executed are lost.
This command stores the current list of λc-definitions in a lambda-calculus object file "file", with extension .lco added if necessary. This file can be inspected, loaded and executed in the jivaro toplevel.
This command extracts λc-terms from the objects denoted by the qualified identifiers qualid1 … qualidn as well as from all the objects they may depend on in the current environment. The result is added to the list of λc-definitions already built by former extraction commands.
During extraction, global identifiers are turned into λc-symbols formed from the corresponding absolute section paths. For instance, the constructor S of type nat → nat is mapped to the λc-symbol `Coq.Init.Datatypes.S'.
This command extracts a function that computes a witness (possibly depending on parameters) from an existence proof in Prop given by qualid1 using a decidability proof given by qualid2. Both qualified identifiers qualid1 and qualid2 have to be declared in the current environment with types of the form:
|
The extracted function is a λc-term t such that for every sequence of semantical objects x→:T→ and for every sequence of realizers u→ that represent the objects x→, the term tu→ computes a realizer representing a semantical object y:U such that P x→ y.
The extracted function is added to the current list of λc-definitions under the name path1%witness, where path1 is the λc-symbol associated to the qualified identifier qualid1 during extraction.
From a technical point of view, the classical extraction mechanism is a projection of pCIC-terms1 onto λc-terms where all types are collapsed onto a special constant .type that is computationally meaningless. (Classical extraction is not intended to build interesting programs from types or type formers.) The translation M↦ M* from pCIC to λc is defined on the underlying PTS as follows:
|
Note that unlike constructive extraction (such as implemented in Coq by Pierre Letouzey [2]), classical extraction treats the terms of sort Prop (a.k.a. proof-terms) the same way as the terms of sort Set or Type. Sorts of pCIC objects are actually not considered during classical extraction.
The Coq environment allows the user to introduce many constants to represent (co)inductively defined type families, constructors, definitions and axioms. Each pCIC-constant c is translated as a λc-constant with the same full name
| c* ≡ c |
For instance the constructor S in the inductive definition of the type nat is translated as the λc-constant Coq.Init.Datatypes.S corresponding to the full name of this constructor in the Coq environment. As an exception, every constant I representing a (co)inductive type or type family is translated as the computationally meaningless λc-constant .type, like every type former:
| I* ≡ .type . |
The case analysis of a pCIC-term M belonging to a (co)inductive type family I with constructors c1,…,ck of arities n1,… nk (excluding parameters) is translated as follows
| ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ |
| ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ |
| ≡ |
|
where I%case is a special λc-constant associated to the type family I. Intuitively, this λc-constant implements the case analysis of the extracted term M* against the terms λx1⋯λxni Ni* (1≤ i≤ k) extracted from the branches of the match construct. Note that the elimination predicate of the match construct and the parameters of the corresponding (co)inductive definition are lost during extraction.
Fixpoints and cofixpoints are translated the very same way in the λc-calculus, regardless of problems of structural decreasing/production. Formally, this translation is defined by
| ⎛ ⎜ ⎜ ⎝ |
| ⎞ ⎟ ⎟ ⎠ |
| ≡ |
|
where .fix_n_i (for 1≤ i≤ n) is a λc-constant implementing the fixpoint combinator defined by the reduction rule
| .fix_n_i F1 ⋯ Fn ≻ Fi (.fix_n_1 F1⋯ Fn) ⋯ (.fix_n_n F1⋯ Fn) |
(Note the mutual dependency of the combinators .fix_n_1, …, .fix_n_n.) During the extraction process, these fixpoint combinators are automatically generated when needed, their definition being stored in the resulting object file.
The λc-representation of the data structures pertaining to a given (co)inductive type family I is defined by the implementation of the λc-constants c1,…,ck associated to the constructors of I and by the implementation of the λc-constant I%case that governs case analysis for the type family I. Since the objects of the family I are only accessed via the λc-constants c1,…,ck and I%case during the extraction process, changing the implementation of these constants is sufficient to change the λc-representation of all objects of the family I in the whole extracted program.
By default, (co)inductively defined data structures of pCIC are projected onto the λc-calculus using the standard impredicative encoding. Formally, if I is a (co)inductive type family depending on p parameters that is defined from k constructors c1,…,ck of arities n1,…,nk (excluding parameters), then, by default, every λc-constant ci (1≤ i≤ k) associated to the corresponding constructor is defined in the λc-calculus as an alias for the λ-term
| ci := |
|
|
| ei x1⋯ xni | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Case analysis is then implemented as the application of the matched value to all the branches of the match construct, so that the λc-constant I%case is simply defined as an alias for the identity function:
| I%case := λz z |
For some data types, it is desirable to replace the default representation described above by a more efficient representation. The typical example is the type nat of natural numbers, whose default representation with the λc-constants
|
is even more inefficient than the traditional encoding à la Church.
For this purpose, the classical extraction module introduces a special set of λc-definitions to override some of the λc-definitions that would be normally produced during extraction. These λc-definitions are stored in an object file override.lco (in the kextraction directory) that is automatically loaded at the first invocation of a classical extraction command. Each time the extraction procedure produces a new λc-constant (representing a constructor, a case combinator, a definition, an axiom, etc.) the extractor first looks whether this constant is defined in the list of overriding definitions. If it is, the definition is taken from the list; otherwise, the constant is given its default definition using the mechanism described above.
The object file override.lco containing the list of overriding definitions is compiled from a source file override.lc in the kextraction directory (using the jivaro toplevel). Before loading the object file override.lco, the extractor looks for the source file override.lc in the kextraction directory. When this file exists and appears to be newer than the object file—or when the object file is missing—the extractor silently invokes the jivaro toplevel to (re)compile the list of overriding definitions before loading them.
The file override.lc accompanying the classical extraction module for Coq takes advantage of the presence of (unbounded) machine integers in the jivaro toplevel to redefine the representation of natural numbers as follows:
|
With these definitions, every natural number n∈ℕ is represented in the extracted code as a lazy integer, that is, as a term t that passes the machine representation of the integer n to its first argument (formally: tk evaluates to kn for all terms k, still writing n the machine representation of the integer n).2
Although the (re)definitions above are sufficient to change the representation of natural numbers in the whole extracted code—thus changing the underlying space complexity—they do not change the fact that the code extracted from Coq functions still works with numerals on a unary basis, through the λc-constants implementing the constructors O, S and case analysis. To improve time complexity as well, this redefinition of natural numbers has to be accompanied with redefinitions of functions manipulating natural numbers in the extracted code. In this direction, the file override.lc redefines some of the λc-constants corresponding to arithmetic functions of the standard library of Coq, such as addition
|
and multiplication, as well as the bounded predecessor and subtraction functions.
By default, each pCIC-axiom is extracted as a λc-constant (with the same full name) that is declared in the resulting object file as an undefined symbol (similarly to the special constant .type representing types).
Again, it is possible to override this behaviour by redefining the corresponding λc-constant in the file of overriding definitions. The file override.lc that comes with the classical extraction module for Coq contains a redefinition of the λ-constant that implements the axiom of excluded middle
| classic : forall P : Prop, P ∨ ¬P |
as well as of some other λc-constants associated to other results of the library for classical logic. (For instance, the λc-constant corresponding to Peirce's law is redefined as an alias for λP .cc, where .cc is the constant for call/cc.)
In this way, it is possible to extract programs from classical proofs formalized in Coq using the library of classical logic in Prop, and to experience the fascinating computational behaviour of extracted programs working with continuations.
This document was translated from LATEX by HEVEA.