Benjamin Gr
email: benjamin.gregoire@inria.fr

Xavier Leroy
email: xavier.leroy@inria.fr

A Compiled Implementation of Strong Reduction

Keywords: D.3.1 [Programming Languages]: Language Classificationsapplicative (functional) languages, D.3.4 [Programming Languages]: Processors-compilers, interpreters, F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages-operational semantics, partial evaluation, F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-lambda calculus and related systems, proof theory, I.1.3 [Symbolic and Algebraic Manipulation]: Languages and Systems-evaluation strategies, I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving Languages, Theory, Experimentation, Verification Strong reduction, beta-equivalence, normalization by evaluation, abstract machine, virtual machine, Calculus of Constructions, Coq

Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and βequivalence checker for the λ-calculus with products, sums, and guarded fixpoints. Our approach is based on compilation to the bytecode of an abstract machine performing weak reductions on non-closed terms, derived with minimal modifications from the ZAM machine used in the Objective Caml bytecode interpreter, and complemented by a recursive "read back" procedure. An implementation in the Coq proof assistant demonstrates important speedups compared with the original interpreter-based implementation of strong reduction in Coq.

Introduction

It is folklore that β-reduction in the λ-calculus is the computation model underlying functional programming languages. Actually, functional languages implement only weak β-reduction, whereby reductions are not performed on function bodies until functions are applied to actual arguments. Efficient compiled implementations of weak reduction are widely known and deployed, based either on environments and closures or on graph reduction, and implemented either as abstract machines or by direct machine code generation.

In contrast, this paper focuses on strong reduction, where βreductions are also performed on function bodies. The practical need for strong reduction appears in two areas. The first area is partial evaluation, also known as program specialization: specializing a function applied to some known arguments (the other arguments remaining unknown) amounts to strongly normalizing a partial application of the function. The other area where strong reduction is required, which prompted the work presented here, is type checking / proof checking in type systems / logics based on dependent types, such as LF or the Calculus of Constructions [START_REF] Harper | A framework for defining logics[END_REF][START_REF] Coquand | The calculus of Constructions[END_REF][START_REF] Pfenning | Inductively defined types in the Calculus of Constructions[END_REF], which are at the basis of proof assistants such as Alf, Coq, Elf, Lego and NuPRL. In these systems, dependent types may contain arbitrary terms, and types are compared up to β-equivalence of the terms they contain, as captured by the following conversion rule:

E a : τ τ β ≈ τ (conv)
E a : τ Thus, type checking in these systems, or equivalently proof checking, involve performing strong β-reductions inside the types to be compared, until the reducts are syntactically equal.

Most, if not all, proof assistants of the Coq/HOL family implement these strong reductions in a purely interpretative way, by walking over a tree-based representation of terms. Despite various implementation tricks involving explicit substitutions, this interpretative approach can become a performance bottleneck when developing and checking proofs with large computational content, such as proofs based on reflection. Proof by reflection is characterized by the use of efficient decision procedures, proved correct once and for all, to replace long proof derivations. A typical example is the use of computations on binary decision diagrams to prove results on boolean formulas [START_REF] Verma | Reflecting BDDs in Coq[END_REF]. Another example is Appel and Haken's famous proof of the 4-color theorem [START_REF] Appel | Every planar map is four colorable[END_REF], which involves checking colorability of a finite, but large, number of well-chosen planar graphs: rather than developing a proof of 4-colorability for every such graph, a proved decision procedure is invoked on all of them. The present paper reports on the design and implementation of a strong evaluator and equivalence tester for the Coq proof assistant that eliminates most of the interpretive overhead via compilation to the byte-code of a virtual machine. In sections 2 and 3, we first show how strong reduction can be implemented by a recursive combination of weak symbolic reduction (weak reduction of terms containing free variables) and readback (reconstruction of a term in normal form from the head normal form returned by the weak symbolic evaluator). While developed independently, this combination is similar to online type-directed partial evaluation [START_REF] Danvy | Online type-directed partial evaluation[END_REF][START_REF] Sumii | Online type-directed partial evaluation for dynamically-typed languages[END_REF]; however, we give a new presentation of this approach that paves the way to an implementation of weak symbolic reduction that avoids explicit run-time tests "is this term symbolic or not?".

In section 4, we develop one such efficient implementation of weak symbolic reduction, as an abstract machine and its associated compilation scheme. The abstract machine is a minor extension of the ZAM abstract machine [START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF] that is at the heart of the Objective Caml bytecode interpreter [START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF], and reuses all the work that has been expended in making the latter efficient.

Both the abstract machine and its compilation scheme have been proved correct with respect to the weak reduction semantics, and the proof was mechanically checked by Coq; section 5 reports on this proof development. Performance figures obtained on a modified version of the Coq proof assistant are reported in section 6. We end this paper by a discussion of related work in section 7, and some concluding remarks in section 8.

Strong Reduction for the Pure λ-calculus

We first present our strong reduction technique on the simplest functional language of all: the pure λ-calculus.

The Pure λ-calculus

The syntax of the calculus is given by Terms: a ::= x | λx.a | a 1 a 2 Terms are identified up to renaming of λ-bound variables (αconversion). The strong reduction relation ⇒ consists of the familiar β-reduction rule, plus a context rule allowing reduction in arbitrary subterms, including below a lambda:

(λx.a) a ⇒ a{x ← a } (β) Γ(a) ⇒ Γ(a ) if a ⇒ a (context) with Γ ::= λx.[ ] | [ ] a | a [ ].
We write * ⇒ for the reflexive and transitive closure of ⇒. In the following, we assume that all λ-terms a considered are strongly normalizing: there are no infinite reduction sequences starting from a. In our setting, this property is guaranteed by the type system of the Calculus of Constructions.

We are interested in two computational problems. The first is to compute the normal form N (a) of a closed, strongly normalizing term a. This is the unique term such that a * ⇒ N (a) and N (a) does not reduce. The second problem is to decide whether two closed, strongly normalizing terms a 1 and a 2 are β-equivalent, written a 1 ≈ a 2 . This equivalence is defined by a 1 ≈ a 2 if and only if there exists a term a such that a 1 * ⇒ a and a 2 * ⇒ a.

Strong Reduction by Iterated Symbolic Weak Reduction and Readback

To compute the normal form of a closed term a, our approach is first to compute the head normal form (also called value) of a using an off-the-shelf weak evaluator. Such an evaluator performs β-reductions anywhere in the term except under a λ-abstraction. Thus, the value of a is of the form λx.a , where a is, in general, not in normal form. To obtain the normal form of a, all that remains to do is recursively compute the normal form N (a ) of a ; then, we will have N (a) = N (λx.a ) = λx. N (a ).

A slight difficulty arises here: a is not necessarily closed, since the formal parameter x may occur free in a . Thus, we cannot just run our off-the-shelf weak evaluator on a , since such evaluators work only on closed terms. To circumvent this problem, we enrich the term algebra with the ability to represent and manipulate free variables during weak reduction. More formally, we inject the pure λ-terms a into the following algebra of extended terms b:

Extended terms: b ::= x | λx.b | b 1 b 2 | [ x v 1 . . . v n ] Values: v ::= λx.b | [ x v 1 . . . v n ]
Here, x is a constant, uniquely associated with the identifier x, but not subject to alpha-conversion. The extended term [ x] is a runtime representation of the free variable x. Since free variables can be applied during weak reduction, we also need run-time representations [ x v 1 . . . v n ] for applications of a free variable x to arguments v 1 , . . . , v n .

We now formalize the symbolic weak reduction of extended, closed terms b. ("Symbolic" here means that this weak reduction knows how to handle free variables as represented by [. . .] terms.) To be more specific, and to match exactly the implementation of symbolic weak reduction by an abstract machine presented in section 4, we impose a call-by-value, right-to-left evaluation strategy. The symbolic weak reduction relation → is defined by the following three rules:

(λx.b) v → b{x ← v} (β v ) [ x v 1 . . . v n ] v → [ x v 1 . . . v n v] (β s ) Γ v (a) → Γ v (a ) if a → a (context v ) with Γ v ::= [ ] v | b [ ].
Rule (β v ) is the familiar call-by-value function application rule. It handles the case where the function part of an application evaluates to a known function. Rule (β s ) ("symbolic" beta reduction) handles the case where the function part evaluates to the representation of a free variable [ x] or of an application of a free variable

[ x v 1 . . . v n ].
Finally, our choice of contexts Γ v precludes reductions under function abstractions, and forces the argument part of an application to be evaluated to a value before starting evaluation of the function part (right-to-left strategy).

As usual, we write * → for the transitive and reflexive closure of →. We define the value V (b) of an extended closed term b as the normal form of b for the relation * →. Notice that such a normal form is necessarily a value: reduction cannot get stuck. Now that we know how to reduce weakly terms containing free variables, we can express precisely the strong normalization procedure outlined earlier: first, normalize weakly; second, read back the resulting value as a normalized term, recursing over the bodies of functions if needed.

N (b) = R (V (b)) (1) R (λx.b) = λy. N ((λx.b) [ ỹ]) (y fresh) (2) R ([ x v 1 . . . v n ]) = x R (v 1 ) . . . R (v n ) (3)
The readback function R transforms values v into normalized source terms a. For function values λx.b (equation 2), reading back consists in applying the value to the run-time representation of a fresh free variable [ ỹ]. ("Fresh", here, means that y does not occur at all in b; the freshness condition can be made fully precise by using negative de Bruijn indices.) We then compute the value of this term, or equivalently of the term b{x ← [ ỹ]}, and read it back as a normalized term a. The normal form of λx.b is then λy.a. The two forms are equivalent, since the first step of weak reduction of (λx.b) [ ỹ] transforms this term into b{x ← [ ỹ]}. However, by writing (2) as a function application rather than a direct substitution, we make it clear that the readback procedure does not need to "look inside" function values: it remains applicable even if function values are represented as opaque closures of compiled code, like our abstract machine-based weak evaluator of section 4 does. The only requirement that the readback function R puts on the representation of values used by the weak evaluator V is that the representations of functions λx.b and of "accumulators" [ x v 1 . . . v n ] can be distinguished at run-time, and that the components x, v 1 , . . . , v n of the latter can be recovered from the latter.

Reading back the value

[ x v 1 . . . v n ] (equation

Correctness of the Normalization Procedure

We now proceed to show the correctness of the function N defined above. We start with partial correctness: assuming the computation of N (a) terminates, we show that it is indeed the normal form of the pure term a.

x = x λx.b = λx.b b 1 b 2 = b 1 b 2 [ x v 1 . . . v n ] = x v 1 . . . v n
LEMMA 3. If N (b) is defined, then b * ⇒ N (b). If R (v) is defined, then v * ⇒ R (v).
PROOF. Both statements are proved simultaneously by "course of value" induction (induction on the number of recursive calls to N and R ). The last case to consider is R ([ x v 1 . . . v n ]). Applying the induction hypothesis to the v i , we obtain that We now turn to proving that N always terminates when given a strongly-normalizing argument. LEMMA 5. If b is strongly normalizing, then V (b) is defined.

v i * ⇒ R (v i ) for i = 1, . . . , n. Thus, [ x v 1 . . . v n ] = x v 1 . . . v n * ⇒ x R (v 1 ) . . . R (v n ) = R ([ x v 1 . . . v n ]).
PROOF. By way of contradiction, consider an infinite weak reduction sequence starting at b and performing infinitely many β v and β s reductions (possibly under context). There can only be a finite number of β s reductions in a row, without an intervening β v step, since the number of application nodes in the term decreases by one during a β s reduction. Thus, the infinite weak reduction sequence contains infinitely many β v reductions. As shown in lemma 2, each such β v reduction corresponds to a β reduction on translated terms. Thus, we can construct an infinite sequence of β reductions starting at b. This contradicts the hypothesis that b is strongly normalizing. LEMMA 6. If v is strongly normalizing, then R (v) is defined.

PROOF. Consider the ordering on pure terms defined as the transitive closure of the following two cases:

• a a if a ⇒ a ;
• a a if a is a strict subterm of a up to a renaming of free variables.

It is easy to see that is well-founded on strongly normalizing terms, in the sense that there exists no infinitely decreasing chains a a 1 . . . starting with a strongly normalizing term a. (From such a chain, we could trivially construct an infinite reduction sequence starting with a.)

The result then follows by well-founded induction using the ordering. For the function case, we have We can therefore apply the induction hypothesis to R (V (b )), and obtain the expected result.

R (λx.b) = λy.R (V (b )) with b = b{x ← [ ỹ]})). Since b = b{x ← y}
For the case R ([ x v 1 . . . v n ]) = x R (v 1 ) . . . R (v n ), it is obvious that v 1 , . . . , v n are strict subterms of [ x v 1 . . . v n ] = x v 1 . . . v n ,

and the result follows by induction hypothesis.

As a corollary of lemmas 4, 5 and 6, we obtain the (total) correctness of the strong normalization procedure: THEOREM 1. If a is a closed, strongly normalizing pure λ-term, then N (a) is defined and is the normal form of a.

Deciding β-equivalence

The previous results give a naive procedure to decide the βequivalence of two strongly normalizing terms a 1 and a 2 : compute N (a 1 ) and N (a 2 ) and compare the normal forms for syntactic equality. However, it is often not necessary to go all the way to normal forms to find a common reduct. The following more efficient procedure E(a 1 , a 2 ) reduces weakly the terms a 1 and a 2 , compares their values, and recurses only if syntactically different functions are obtained.

• E(b 1 , b 2 ) if and only if E v (V (b 1 ), V (b 2 )). • E v (v 1 , v 2 ) if v 1 ≡ v 2 . • E v (λx 1 .b 1 , λx 2 .b 2 ) if E v ((λx 1 .b 1 ) [ ỹ], (λx 2 .b 2 ) [ ỹ]) where y is a fresh variable. • E v ([ x v 1 . . . v n ], [ x w 1 . . . w n ]) if E v (v i , w i ) for all i = 1, . . . , n. • E v (v 1 , v 2 ) is false otherwise.
In this definition, the ≡ relation stands for any relation that is finer than β-convertibility and can be computed cheaply, so that the "early return" test (second case above) can be profitably applied at each step. Syntactic equality up to α-conversion is an obvious candidate for ≡ in an interpreted setting. In a compiled implementation such as that of section 4, syntactic equality might not be easily decidable, in which case ≡ can be equality of machine representations.

The correctness of the E predicate defined above can easily be proved along the lines of section 2.3, and we omit the proofs.

Extension to the Calculus of Constructions

We now progressively extend the approach presented in section 2 with the additional features of the (type-erased) term language of the Calculus of Constructions: inductive types (a generalization of products and sums) and fixpoints.

Booleans and Conditional

Before considering inductive types in their full generality, it is helpful to present a familiar special case: booleans and the if. . . then. . . else. . . construct. The syntax of the source calculus becomes:

Terms: a ::= x | λx.a | a 1 a 2 | true | false | if a 1 then a 2 else a 3
The associated reduction rules are:

(λx.a) a ⇒ a{x ← a } if true then a else a ⇒ a if false then a else a ⇒ a Γ(a) ⇒ Γ(a ) if a ⇒ a with Γ ::= λx.[ ] | [ ] a | a [ ] | if [ ] then a 2 else a 3 | if a 1 then [ ] else a 3 | if a 1 then a 2 else [ ].
We must also add booleans and the conditional construct to the algebra of extended terms. However, a new case arises: the run-time representation of a free variable [ x] can now appear in the if part of a conditional. Just like rule (β s ) simply "remembers" the arguments to an application of a free variable, we need to "remember" the if. . . then. . . else. . . construct that could not be reduced because the condition was a free variable. To capture this phenomenon, we introduce a new syntactic category k of accumulators, or run-time representations of non-closed, non-reducible terms.

Extended terms: b

::= x | λx.b | b 1 b 2 | true | false | if b 1 then b 2 else b 3 | [k] Accumulators: k ::= x | k v | if k then b else b Values: v ::= λx.b | true | false | [k]
Symbolic weak reduction is then defined by the following rules:

(λx.b) v → b{x ← v} [k] v → [k v] if true then b else b → b if false then b else b → b if [k] then b else b → [if k then b else b ] Γ v (a) → Γ v (a ) if a → a with Γ v ::= [ ] v | b [ ] | if [ ]
(λx.b) v → b{x ← v} [k] v → [k v] case C( v) of (C i ( x i ) → b i ) i∈I → b j { x j ← v} if C = C j and | v| = | x j | case [k] of (C i ( x i ) → b i ) i∈I → [case k of (C i ( x i ) → b i ) i∈I ] Γ v (a) → Γ v (a ) if a → a N (b) = R (V (b)) R (λx.b) = λy. N ((λx.b) [ ỹ]) (y fresh) R (C(v 1 , . . . , v n ) = C(R (v 1 ), . . . , R (v n )) R ([k]) = R (k) R ( x) = x R (k v) = R (k) R (v) R (case k of (C i ( x i ) → b i ) i∈I ) = case R (k) of (C i ( y i ) → N (b (C i ( -→ [ ỹi ])))) i∈I where b = λx. case x of (C i ( x i ) → b i
N (b) = R (V (b)) R (λx.b) = λy. N ((λx.b) [ ỹ]) (y fresh) R (true) = true R (false) = false R ([k]) = R (k) R ( x) = x R (k v) = R (k) R (v) R (if k then b else b ) = if R (k) then N (b) else N (b )

Inductive Types

Inductive types in the Calculus of Constructions [START_REF] Pfenning | Inductively defined types in the Calculus of Constructions[END_REF] are similar to datatypes in ML and Haskell: they consist in one or several alternatives, identified by unique constructors C, each constructor carrying zero, one or several terms as arguments. A built-in case construct allows shallow pattern-matching on terms of inductive types. Once enriched with inductive types, the source calculus becomes:

Terms: a ::= x | λx.a | a 1 a 2 | C( a) | case a of (C i ( x i ) → a i ) i∈I
We write z for a sequence of elements of the syntactic class z, and | z| for the number of elements in such a sequence.

The reduction rules for inductive types are:

(λx.a) a ⇒ a{x ← a } case C( a) of (C i ( x i ) → a i ) i∈I ⇒ a j { x j ← a} if C = C j and | a| = | x j | Γ(a) ⇒ Γ(a ) if a ⇒ a
Extended terms and weak symbolic reduction are modified accordingly, taking into account the fact that a case construct can be applied to an accumulator, and needs to be remembered unevaluated as a whole in this case.

Extended terms:

b

::= x | λx.b | b 1 b 2 | [k] | C( b) | case b of (C i ( x i ) → b i ) i∈I Accumulators: k ::= x | k v | case k of (C i ( x i ) → b i ) i∈I Values: v ::= λx.b | C( v) | [k]
Reduction contexts:

Γ v ::= [ ] v | b [ ] | C( b, [ ], v) | case [ ] of (C i ( x i ) → b i ) i∈I
Figure 1 defines the weak reduction rules and the normalization and readback procedures in the presence of inductive types. As in the case of the conditional construct in section 3.1, there are two weak reduction rules for case, depending on whether the argument is a constructed value C( v) or an accumulator [k]. In the former case, reduction proceeds with the appropriate arm of the case construct. In the latter case, an accumulator is built that "remembers" the whole case statement.

The readback functions are as in section 3.1, with the treatment of case generalizing that of if. . . then. . . else: we recursively normalize each arm of the case, after replacing the pattern-bound variables x i by run-time representations of fresh free variables; then, a case statement is reconstructed from the normal forms of the arms and the readback of the accumulator being matched upon. To emphasize the fact that the case construct can be compiled, and thus its arms are not necessarily recoverable from the code, we present the recursive normalization of each arm C i ( x i ) → b i as an application of the matching function λx.case x of . . . to the argument

C i ( -→ [ ỹi ]
), composed of the constructor of the i th arm applied to the correct number of fresh free variables. The compiled code for the matching function then selects the i th arm and perform the substitution x i ← -→

[ ỹi ] all by itself.

Fixpoints

The Calculus of Constructions supports the definition of recursive functions via fixpoints. Fixpoints are introduced by a family of operators fix n , where the positive integer n indicates the position of the argument that is used to guard the recursion and prevent infinite unrolling:

Writing b = λ f .λx 1 . . . λx n .b , fix n (b) v 1 . . . v n-1 (C( v)) → b { f ← b, x 1 ← v 1 , . . . , x n-1 ← v n-1 , x n ← C( v)} fix n (b) v 1 . . . v n-1 [k] → [fix n (b) v 1 . . . v n-1 k] R (fix n (b) v 1 . . . v i ) = N (fix n (b)) R (v 1 ) . . . R (v i ) if i < n R (fix n (b) v 1 . . . v n-1 k) = N (fix n (b)) R (v 1 ) . . . R (v n-1 ) R (k) N (fix n (b)) = fix n (λg.λy 1 . . . λy n .N (b [ g] [ ỹ1 ] . . . [ ỹn ])
where g, y 1 , . . . , y n are fresh The reduction rule for the fix n operators is not the standard unrolling rule

fix n (λ f .a) ⇒ a{ f ← fix n (λ f .a)}
since such a rule would allow infinite unrolling, and thus render type-checking undecidable. Instead, the calculus provides a guarded unrolling rule, allowing unrolling of the recursive definition only if the n th argument is a constructed term: writing a = fix n (λ f .λx 1 . . . λx n .a ), we have

a a 1 . . . a n-1 (C( a n )) ⇒ a { f ← a, x 1 ← a 1 , . . . , x n-1 ← a n-1 , x n ← C( a n )}
Further statically-checked restrictions on the body a of the recursive definition ensures that it recursively applies f only to strict subterms of the n th argument C( a n ). This ensures that all recursive definitions proceed by structural induction, and are thus guaranteed to normalize strongly. At first sight, this restriction might appear to restrict severely the expressiveness of the logic, but this is not so: the guard argument over which the function is structurally recursive can also be an inductive proof term such as a proof of accessibility in a well-founded ordering, guaranteeing the termination of the function. Thus, general recursive definitions can also be handled, as long as they are provably total in the logic.

As a consequence of the guarded unrolling rule, applications of

Values: v ::= . . . | fix n (λ f .λx 1 . . . λx n .b) v 1 . . . v i if 0 ≤ i < n Accumulators: k ::= . . . | fix n (λ f .λx 1 . . . λx n .b) v 1 . . . v n-1 k
The additional reduction rules and readback rules for fixpoints are shown in figure 2. The main point to notice is that in the source calculus, the normal form of a non-applied fixpoint fix n (λ f .λx 1 . . . λx n .a) is simply fix n (λ f .λx 1 . . . λx n .a ) where a is the normal form of a. In other terms, we normalize a without assuming anything known on the function name f nor on the parameters x i , and in particular without assuming that f unrolls to fix n (. . .): the guarded unrolling rule does not apply here. For the same reason, an application of fix n (a) to fewer than n arguments in normal form, or to n -1 normal forms and one normal form that is not a constructor application, is itself in normal form.

An Abstract Machine for Weak Symbolic Reduction

We now turn to implementing weak symbolic reduction by compilation to a suitable abstract machine. This abstract machine is a slight extension of the ZAM, which underlies the bytecode interpreter of Objective Caml [START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF][START_REF] Leroy | The Objective Caml system. Software and documentation available on the Web[END_REF], In the terminology of [START_REF] Peyton | Implementing lazy functional languages on stock hardware: the spineless tagless G-machine[END_REF], the ZAM is an environment-and closure-based abstract machine following the "push-enter" model, and implementing a call-by-value evaluation strategy.

The purpose of this section is to demonstrate that minor modifications of an existing abstract machine for weak reduction suffice to turn it into an abstract machine for weak symbolic reduction, without impacting significantly the evaluation speed for closed terms. Consequently, we present a minimal subset of the ZAM, omitting several aspects of the real ZAM that are irrelevant for our purposes, such as the optimization of tail-calls, the use of a register to cache the top of the stack, and the actual representation of environments (as a stack-allocated part and a heap-allocated part) and closures (single block, minimal environments). These omitted aspects are discussed in [START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF] and in the first author's forthcoming dissertation.

Machine States and Machine Values

The machine state has four components:

• A code pointer c representing the code being executed as a sequence of instructions.

(λ f .λx 1 . . . λx n .b) v 1 . . . v n-1 .
The transitions of the abstract machine are shown in figure 3, and the halting configurations in figure 4.

Compilation and Execution of Functions

The compilation scheme for the ZAM is presented as a function

[[b]] c
, where b is an expression and c an instruction sequence representing the continuation of b. It returns an instruction sequence that evaluates b, leaves its value at the top of the stack, and continues in sequence by executing the code c. For the pure λ-calculus, the compilation scheme is defined as follows:

[[x]] c = ACCESS(i); c where i is the de Bruijn index of x [[λx 1 . . . x m .b]] c = CLOSURE(GRAB; . . . ; GRAB m times ; [[b]] RETURN); c [[b b 1 . . . b m ]] c = PUSHRETADDR(c); [[b n ]] . . . [[b 1 ]] [[b]] APPLY(m)
A reference to a variable x is compiled to an ACCESS instruction carrying the de Bruijn index of the variable. The execution of ACCESS(i) looks up the i th entry in the machine environment and pushes it on the stack.

A curried function λx 1 . . . x m .b compiles to a CLOSURE instruction, which at run-time builds a closure of its argument (a piece of code) with the current environment, and pushes the closure on the stack. The argument of CLOSURE is the code for the body b of the function, preceded by m GRAB instructions and followed by a RETURN instruction.

As its name suggests, GRAB attempts to pop one function argument from the stack and add it in front of the current environment. (This corresponds exactly to a β v reduction step.) This is possible only if the count n of available arguments is non-zero, and causes n to be decremented. If n = 0, all arguments have been consumed already by previous GRAB instructions, hence the curried function is partially applied. The virtual machine then returns a closure of the current code (including the aborted GRAB) and the current environment to the caller of the function.

The RETURN instruction is the dual of GRAB: if all arguments have been consumed (n = 0), the value of the function body is returned to its caller; if some arguments remain (n > 0), the curried function was "over-applied", and its result, which must be a function, is to be applied to the remaining argument. The latter is achieved by tailcalling the closure found on the top of the stack with the remaining arguments.

The At this point, the reader is probably wondering how we treat the β s reduction rule, corresponding to the application of an accumulator [k]. Recall that such an accumulator is represented by a pseudoclosure [0 : ACCU, k]. Thus, the APPLY instruction will cause the ACCU instruction to be executed with k being moved to the environment register of the machine. The ACCU instruction simply pops all provided arguments v1 , . . . , vn off the stack, constructs an accumulator [0 : ACCU, [1 : k, v1 , . . . , vn ]] representing the application of k to these arguments, and returns this accumulator to the caller. Thus, the effect of the β s reduction rule is achieved without testing at runtime whether the function part of an application is a real closure or an accumulator. In other terms, we implement symbolic weak reduction of function applications without any run-time overhead on applications of regular functions.

Inductive Types

Inductive types lead to the addition of the following two compilation rules:

[[C(b 1 , . . . , b n )]] c = [[b n ]] . . . [[b 1 ]] MAKEBLOCK(n, #C); c [[case b of (C 1 ( x 1 ) → b 1 . . . C n ( x n ) → b n )]] c = PUSHRETADDR(c); SWITCH([[b 1 ]] RETURN, . . . , [[b n ]] RETURN)
In the latter rule, we assume that the arms of the case are ordered so that #C i = i for i = 1, . . . , n. No generality is lost since the type system of the Constructions guarantees the exhaustiveness of case statements.

The compilation and execution of constructor applications is straightforward: the arguments of the constructor are evaluated, and the MAKEBLOCK instruction then creates the representation of the constructed term, tagged with the constructor number.

For the case statement, a return frame to the continuation c is pushed first. The SWITCH instruction then discriminates on the tag of the matched value, and branches to the code of the corresponding case arm, after adding the fields of the matched value to the envi- If the matched value has tag 0, denoting a case on an accumulator k, the SWITCH instruction builds the accumulator [0 : ACCU, [2 : k, c 0 , e]] where c 0 is the code consisting of the SWITCH instruction and the code for the arms of the case. Later, the readback procedure can restart the abstract machine with code c 0 , environment e, stack v.ε and number of arguments 0, where v is the machine representation of C i ( ˜ y i ). The code for the i th arm will evaluate, then stop on its final RETURN instruction, since a final configuration is reached (first case in figure 4). Thus, this achieves the effect of computing the value of b i { x i ← ˜ y i }.

k, v 1 , . . . , v n ]].s n MAKEBLOCK(T, m); c e v 1 . . . v m .s n c e [T : v 1 , . . . , v m ].s n SWITCH(c 1 , . . . , c m ) e [T : v 1 , . . . , v p ].s n if 1 ≤ T ≤ m c T v p . . . v 1 .e s 0 c 0 = SWITCH(c 1 , . . . , c m ) e
This "replay" facility is the reason why a PUSHRETADDR-RETURN pair is used to implement the control-flow merging of the arms of the case, rather than a more standard GOTO instruction. Apart from the slightly higher cost of the PUSHRETADDR-RETURN combination compared with a GOTO, this compilation scheme support symbolic execution and readback for case statements without impacting the evaluation speed on non-symbolic, closed terms. (The actual implementation uses a jump table for the SWITCH instruction, covering both the case tag = 0 and tag ≥ 1, so that an additional test for tag = 0 is not required.)

Fixpoints

The compilation of fixpoint definitions is as follows:

[[fix n (λ f .λx 1 . . . λx n .b)]] c = CLOSUREREC(GRAB; . . . ; GRAB n-1 times ; GRABREC; [[b]] RETURN); c
The CLOSUREREC instruction constructs a closure for a recursive function. In the simplified presentation given in this paper, this is a cyclic closure v = [T λ : c, v.e] where the first slot of the environment, corresponding to the recursive variable f in the source term, points back to the closure itself [START_REF] Cousineau | The categorical abstract machine[END_REF]. (The actual implementation uses the scheme described in [START_REF] Appel | Compiling with continuations[END_REF] instead of cyclic closures.)

The code part of the recursive closure consists of the compilation of the body b of the definition, preceded by n -1 GRAB instructions and one GRABREC instruction. The n -1 GRAB instructions absorb the first n -1 parameters, which are not subject to a guard condition. The last parameter, however, is guarded: evaluation should not proceed if it is bound to an accumulator. Hence, GRABREC checks whether the argument is an accumulator, and if so, constructs and returns an accumulator representing the suspended application of the fixpoint.

A Mechanically-checked Proof of Correctness

The first author has developed a fully formal specification and proof of correctness of the approach described in this paper, using the Coq proof assistant. Such a mechanically-checked correctness proof is required to ensure that we do not compromise the logical consistency of the Coq system by plugging a buggy evaluator in it. (The correctness of the kernel of the Coq proof-and type-checker has previously been mechanically proved in Coq by Barras [START_REF] Barras | Coq in Coq[END_REF][START_REF] Barras | Auto-validation d'un système de preuves avec familles inductives[END_REF].) We now give a high-level overview of this 5000-line development; a detailed presentation is beyond the scope of this paper and will be published separately.

The bulk of the development consists of proving that the modified ZAM machine and its compilation scheme (including the optimizations that we left out in section 4) faithfully implement the weak symbolic reduction semantics. The remainder of the proof shows the correctness of the readback, strong normalization and equivalence testing procedures; this part of the proof is much shorter and easier, and follows the lines of section 2.3, using de Bruijn indices instead of variable names.

Following [START_REF] Hardin | Functional runtimes within the lambda-sigma calculus[END_REF], the correctness of the modified ZAM and its compilation scheme is established by proving a simulation result between the reductions of the source term and the transitions of the abstract machine executing the compiled code for the term. First, we set up a decompilation relation S ⇑ b between machine states S = (c, e, s, n) and source terms b, and also between machine values and source values v ⇑ v. This decompilation relation can be viewed as a left inverse of the compilation function: if we compile a term and build an initial machine state with this code, the decompilation of this initial state gives us back the original term. However, decompilation is also defined for intermediate machine states, reached after one or several transitions, and where the code part of the state is not the image of a source term by the compilation function. Several examples of decompilation relations for different, simpler abstract machines are shown in [START_REF] Hardin | Functional runtimes within the lambda-sigma calculus[END_REF]. Ours is broadly similar, with the exception that [START_REF] Hardin | Functional runtimes within the lambda-sigma calculus[END_REF] uses explicit substitutions in the source language, while we perform classical substitution as part of the decompilation predicate in order to keep the source language unchanged.

Once the decompilation relation is set up, we can show the main simulation result: one transition of the abstract machine corresponds to zero, one or several reductions on the source term. We also show that initial states of the machine decompile to the original term. There are two kinds of initial states of interest:

([[b]] RETURN, ε, ε, 0), corresponding to executing the code of a closed term b, and (APPLY(n), ε, f . v1 . . . vn .ε, 0), corresponding to applying the closure f to the arguments v1 , . . . , vn during the readback procedure.

LEMMA 8 (INITIAL STATES).

([[b

]] RETURN, ε, ε, 0) ⇑ b if b is closed. 2. (APPLY(n), ε, f . v1 . . . vn .ε, 0) ⇑ f v 1 . . . v n if f ⇑ f and vi ⇑ v i for i = 1, . . . , n.
Symmetrically, final machine configurations decompile to values.

LEMMA 9 (FINAL STATES). If S is a final machine configuration and v the associated return value, as defined in figure 4, then there exists a source value v such that S ⇑ v and v ⇑ v.

To show the correctness of the abstract machine and its compilation scheme, it remains to show two properties. First, the machine does not get stuck when executing the compiled code of a term that is not stuck.

LEMMA 10 (PROGRESS). If S ⇑ b, and S is not a final state, and Second, the abstract machine always terminates when given the code for a term that evaluates to a value. Given the simulation lemma 7, the only way the machine could fail to terminate is by performing an infinite number of consecutive "silent" transitions, that is, transitions between two states that decompile to the same term. To show that this cannot happen, we define a non-negative integer measure |S| on machine states S, and show that it strictly decreases at each silent transition. Again, [START_REF] Hardin | Functional runtimes within the lambda-sigma calculus[END_REF] gives examples of such measures for other machines. As a corollary of the previous lemmas, we obtain the total correctness of the abstract machine and its compilation scheme:

Experimental Results

The first author has implemented the approach presented here in the context of the Coq proof assistant, version 7. The implementation consists of a bytecode compiler and a readback procedure and equivalence tester written in OCaml, and an abstract machine interpreter written in C. The Coq proof checker was modified to use our equivalence tester. Synthetic tests. Figure 5 gives the time it takes to strongly normalize or to decide the equality of various artificial test terms. For comparison purposes, we also give timings for the current interpreterbased normalization and equivalence testing procedures of the Coq system. For normalization, Coq supports both call-by-value and lazy call-by-name strategies, while only the latter is supported for equivalence testing. When the example does not require normalization under λ, we also give the times for the OCaml bytecode interpreter. The timings for our system include compilation times in addition to evaluation times, in order to make the comparison with Coq's interpreter fairer.

Overall, our compiled implementation is 10 to 100 times faster than Coq's lazy call-by-name interpreter, and 1.1 to 100 times faster than Coq's call-by-value interpreter.

Example 1 computes factorial 9 using Peano integers. This involves no normalization under λ. The result of the weak evaluation is 362880 applications of the constructor Succ to the constant Zero, which is then transformed into an isomorphic source term during readback. Example 2 computes the parity of factorial 9. Compared with example 1, example 2 involves more work during weak reduction, but much less work during readback, since its result is an atomic constant. It therefore normalizes much faster than example 1 in our system, approaching the speed of the OCaml bytecode interpreter.

Example 3 computes 256 × 64 using Church integers. Normalization under λ is required, and the normal form is quite large, requiring significant readback effort. Example 4 computes λx.λy. (128 + x) × (128 + y) using Peano arithmetic; it requires not only normalization under λ, but also large amounts of normalization of case and fix constructs applied to the free variables x, y. In both cases, we observe significant speed-ups compared with Coq's lazy callby-name interpreter, but only a 10% to 30% improvement compared with Coq's call-by-value interpreter.

Examples 5 and 6 perform equivalence testing instead of strong normalization. In both cases, we compare two terms that evaluate to the same (large) normal form, but are syntactically different enough to force full reduction to determine their equivalence. Again, we observe speedups of 20 to 100 compared with Coq's original equivalence test.

Proof checking. Figure 6 gives total proof checking times obtained with the original Coq implementation and with our modified implementation. The efficiency of our implementation depends greatly on whether the proofs being checked involve significant amount of computation. For proofs that involve few computations, such as the standard library of theories distributed with the Coq system, our im-plementation actually leads to a 3% slowdown compared with the original Coq implementation. This was to be expected, since the beta-equality tests performed are trivial: the terms to be compared are often in normal form already, thus requiring very little computation to show that they are equal. This is the least favorable case for our implementation, since we pay the price of compiling the terms down to bytecode, yet gain essentially nothing in return. However, this compilation overhead is low enough to be acceptable.

At the other end of the spectrum, proofs that involve significant amounts of computation exhibit speedups by one order of magnitude. As a representative example, we used Gonthier and Werner's Coq proof of the 4-color theorem, and more precisely the part of the proof that checks 4-colorability of a large number of elementary planar graphs. This part of the proof consists mostly in evaluating a function deciding 4-colorability on the elementary graphs. Here, our implementation is 33 to 45 times faster than the original Coq system. Owing to its more efficient use of memory, our implementation is able to complete the checking of the whole proof, while the original Coq runs out of memory on the largest configurations (of perimeter 14).

To compare the performances of our reducer with those of the OCaml system, we used Coq's extraction facility to extract from the Coq development the Caml code that defines the decision procedure and applies it to the elementary graphs. As figure 6 shows, our reducer runs about as fast as OCaml's bytecode interpreter; the speed ratio varies between 1.4 and 0.95. Compiling the extracted Caml code with the OCaml native-code compiler results in speed ratios between 3.5 and 5.6, which is typical of the speed-ups obtained by going from bytecode interpretation to native-code generation.

Related Work

Implementations of strong reduction. The work most closely related to us is Crégut's abstract machine for strong reduction [START_REF] Crégut | An abstract machine for lambda-terms normalization[END_REF][START_REF] Crégut | Machines à environnement pour la réduction symbolique et l'évaluation partielle[END_REF]. This machine is derived from Krivine's machine and implements a lazy evaluation strategy. The code is executed by expansion to Motorola 68000 assembly code. Like ours, Crégut's machine can handle terms containing free variables. However, reductions under lambdas are not performed by a separate readback phase as in our approach, but directly by the abstract machine: when encountering a term λx.b in head position, Crégut's machine immediately proceeds to reducing b (with a free x variable). This is potentially faster than our readback scheme when the goal is to compute the normal form of a term, but prevents early stopping when the goal is to compare two terms for β-equality. Also, strong reduction of case statements and recursive definitions is mentioned in [START_REF] Crégut | Machines à environnement pour la réduction symbolique et l'évaluation partielle[END_REF] but not formalized. Some of the mechanisms we use can be found in optimized interpreters performing strong reduction. Barras' reducer [START_REF] Barras | Programming and computing in HOL[END_REF] uses environments and closures, and a reduction strategy based on Crégut's machine. Nadathur and Wilson [START_REF] Nadathur | A notation for lambda terms: A generalization of environments[END_REF] represent terms in such as way that reduction can be easily stopped at weak head normal form, while keeping enough information to restart strong evaluation later. Still, these approaches remain essentially based on interpretation of a tree-based data structure, without compilation to bytecode.

Online partial evaluation.

The connections between strong normalization and partial evaluation (program specialization) [START_REF] Jones | Partial Evaluation and Automatic Program Generation[END_REF] are well known: specializing a function λx.λy.a for x = b amounts to strongly normalizing the partial application (λx.λy.a) b. Classical partial evaluation comes in two flavors: offline partial evaluation, where a preliminary binding-time analysis classifies sub-terms into dynamic and static terms; and online partial evaluation, where the tests "static or dynamic?" are performed on the fly during specialization. Our approach does not rely on binding-time analysis, and therefore is a form of online partial evaluation.

Our decomposition of strong normalization into (compiled) weak symbolic reduction and (interpreted) readback is non-standard in traditional online partial evaluation. However, a similar decomposition is used in the online type-directed partial evaluation of Danvy [START_REF] Danvy | Online type-directed partial evaluation[END_REF] and Sumii and Kobayashi [START_REF] Sumii | Online type-directed partial evaluation for dynamically-typed languages[END_REF]. (The "type-directed" qualifier is a bit of a misnomer, since this approach does not exploit static typing information, unlike the original type-directed partial evaluation discussed below.) The main difference between online TDPE and our work is that online TDPE, like traditional online partial evaluation, operates on a standard two-level language, and instruments elementary operations of the language (function applications, case statements, etc) with run-time tests "static or dynamic?". In contrast, our presentation in terms of accumulators instead of a 2level language allows implementing function application and case statements without explicit run-time tests "proper value or accumulator?", thus entailing essentially no additional cost compared with a standard, non-symbolic weak evaluator. However, our approach requires a specially adapted virtual machine, while online TDPE can be implemented on top of any functional language using only source-level transformations.

TDPE and normalization by evaluation. Type-directed partial evaluation (TDPE), also known as normalization by evaluation, computes normal forms by combining a standard weak evaluator with a type-directed reification procedure that reconstructs normalized terms from values [START_REF] Danvy | Type-directed partial evaluation[END_REF][START_REF] Berger | An inverse of the evaluation functional for typed λ-calculus[END_REF]. A function value is reified by applying it to a generic argument derived from the type of the function domain (an η-long form of a free variable, where all dynamic application nodes are replaced by static application nodes), and recursively normalizing this application. This alternation between evaluation and reification looks superficially similar to our approach, but differs in several key aspects. First, TDPE uses η-expansions and produces an η-long βη normal form, while our approach does not perform η-expansions and produces pure β normal forms. Since η conversion is not valid in the Calculus of Constructions, TDPE is not applicable in our context.

The second difference between TDPE and our approach is that the reification procedure of TDPE is based on the types of the terms to be normalized, while our readback procedure proceeds by examination of the shape of their values, without needing type information. While the recursion on the type structure that underlies TDPE is extremely elegant, it has been worked out only for simply-typed lambda calculus and for system F [START_REF] Vestergaard | The polymorphic type theory of normalisation by evaluation[END_REF]. Extending TDPE to a type system as rich as that of the Constructions is an open issue.

By abandoning the guidance of the type system, our approach loses one of the advantages of TDPE: the ability to reuse an existing weak evaluator unchanged. Indeed, we had to modify the abstract machine so that it deals correctly with free variables (accumulators). However, our modifications are minimal, and this advantage of TDPE holds only when the language contains only functions and products: to handle sums, TDPE requires a weak evaluator that features control operators (prompts or call/cc), which few do; in contrast, our approach requires a few more modifications for sums, but the total of these modifications still requires less implementation work than adding control operators to a weak evaluator that does not have them initially.

Conclusions and Future Work

We have shown how minimal modifications to an existing abstract machine-based weak evaluator, combined with a simple, typeoblivious readback procedure, lead to an efficient implementation of strong reduction and equivalence testing for a purely functional language featuring products, sums, and guarded recursion.

We have presented this approach in the context of call-by-value weak evaluation and an environment-based abstract machine. It would be interesting to investigate their applicability to other weak evaluators, such as lazy evaluation and graph reduction.

The application of this work to the Coq proof assistant raises interesting type-theoretic issues. First, we test equivalence between type-erased terms, while the Calculus of Construction performs conversion between type-annotated terms. The logical consistency of the former approach follows from Miquel's model-theoretic results [START_REF] Miquel | Le Calcul des Constructions implicite: syntaxe et sémantique[END_REF] in the case of the core Calculus of Constructions, but remains to be extended to inductive types.

A related issue is the treatment of proof terms during equivalence checking. The types being compared for equivalence can contain arbitrary proof terms. Proof terms are often large and costly to normalize. However, the general principle of proof irrelevance suggests that it might not be necessary to normalize them, since a proof of a given proposition is (morally) just as good as any other proof of this proposition. This suggests replacing all proof terms contained in types by a single constant P (a nullary constructor) before testing the equivalence of two types. Again, more work is needed to prove that the corresponding relaxed conversion rule is logically consistent.

Finally,N

  (a) = R (v) = λu. u (λw.w) Remark: The readback of functional values (equation 2) could alternatively be written as R (λx.b) = λy. N (b{x ← [ ỹ]})

REMARK 1 .

 1 For all extended terms b, N (b) and R (b), if defined, are terms that belong to the following grammar: n ::= λx.n | x n 1 . . . n k Hence, they are pure λ-terms in normal form. Now, define the following translation b from an extended term b to a pure λ-term, obtained by erasing the distinction between run-time representations of free variables and the free variables themselves:

LEMMA 2 .

 2 If b → b , then b * ⇒ b . PROOF. By cases on the reduction rule used. If b → b by rule (β v ), then b ⇒ b by rule (β). If b → b by rule (β s ), then b = b . Finally, for context reductions, notice that translations of callby-value contexts Γ v are a subset of Γ contexts, and conclude by induction on the number of context rules used.

  Since N (b) = R (V (b)), we have b * ⇒ V (b) by lemma 2, and V (b) * ⇒ R (V (b)) by induction hypothesis. It follows that b * ⇒ N (b). Consider now the case R (λx.b). Write b = (λx.b) [ ỹ]. By induction hypothesis, b * ⇒ N (b ). Since N (b ) is in normal form by remark 1, and b ⇒ b{x ← y}, confluence of the λ-calculus ensures that b{x ← y} * ⇒ N (b ). Hence, λy. b{x ← y} * ⇒ λy.N (b ). Since λy. b{x ← y} = λx.b up to alpha-conversion, the expected result λx.b * ⇒ N (b ) follows.

LEMMA 4 .

 4 For all pure λ-terms a, if N (a) is defined, then it is the normal form of a.PROOF. Since a is a pure λ-term (containing no [. . .]), we have a = a. By lemma 3, a * ⇒ N (a). Moreover, N (a) is in normal form by remark 1.

  , b is a strict subterm of λx.b up to renaming of x by y. Hence, b is strongly normalizing, and lemma 5 establishes the termination of V (b ). Moreover, V (b ) is a reduct of b by lemma 2. Hence, λx.b b V (b ).

  then b else b . It only remains to extend the readback procedure to booleans and the new syntactic class of accumulators. The only point worth noticing is that reading back a suspended conditional if k then b else b involves normalizing both arms b and b of the conditional, and reconstructing an if. . . then. . . else with the readback of k and the normal forms of b and b .

Figure 1 .

 1 Figure 1. Symbolic weak reduction and readback for inductive types

Figure 2 .

 2 Figure 2. Symbolic weak reduction and readback for fixpoints

  fix n (b) to fewer than n values are values (weak normal forms), while applications of fix n (b) to n -1 values and an accumulator are themselves accumulators: Extended terms: b ::= . . . | fix n (λ f .λx 1 . . . λx n .b)

  code for a multiple application b b 1 . . . b m first pushes a return frame c, e, n containing the code c to be executed when the applied function returns, as well as the current environment and argument count (instruction PUSHRETADDR). Then, the arguments b m . . . b 1 and the function b are evaluated right-to-left, and their values pushed on the stack. Finally, the APPLY(m) instruction branches to the code of the closure obtained by evaluating b, setting the argument count to m. The "push-enter" nature of the ZAM is apparent in the fact that we compile curried functions and multiple applications as a whole, and evaluate arguments right-to-left. For an application b b 1 . . . b m , this avoids the construction of intermediate closures representing the applications b b 1 , (b b 1 ) b 2 , . . . , like an "eval-apply" machine such as the SECD would do. The compilation scheme given above remains correct if applied to non-maximal curried functions and applications (e.g. if we treat b b 1 b 2 as two applications, (b b 1 ) b 2 ), but becomes less efficient at run-time.

[ 0 :Figure 3 .Figure 4 .

 034 Figure 3. Transitions of the abstract machine. Each two-line entry represents a transition; the first line is the machine state before the transition, and the second line is the state after.

LEMMA 7 (

 7 SIMULATION). If S ⇑ b and the machine performs a transition from state S to state S , then there exists a source term b such that S ⇑ b and b * → b .

Figure 6 .

 6 Figure 6. Benchmark results for the checking of actual proofs (on a Pentium III 1Ghz, 256 Mb)

LEMMA 11 (

 11 NO STUTTERING). If the machine performs a transition from S to S , and S ⇑ b and S ⇑ b, then |S | < |S|.

THEOREM 2 .

 2 Let S be a machine state that decompiles to b. If b * → V (b), then the abstract machine started in state S terminates with a return value v that decompiles to V (b). If b diverges (reduces infinitely), the abstract machine started in state S performs an infinite number of transitions.

  3) simply consists in extracting the variable x from x, reading back the values to which it is applied, and reconstructing the application x R (v 1 ) . . . R (v n ).Weak symbolic evaluation reduces it to v = λy. (λz.z) y (λt.t). Readback of λt.t triggers the evaluation of (λt.t) [ w],which returns [ w]. Thus, R (λt.t) = λw.w. Then, R (v ) = u (λw.w).

	Example: Consider the following source term
	a = (λx.x)(λy. (λz.z) y (λt.t))
	This is a functional value, hence the readback procedure R restarts
	weak symbolic evaluation on b = (λy. (λz.z) y (λt.t)) [ ũ]. The
	value returned by the second round of weak symbolic evaluation is
	v = [ ũ (λt.t)].

•

  An environment e: a sequence of machine values v1 . . . vn associating the value vi to the variable having de Bruijn index i. • A stack s (a sequence of machine values and return contexts) holding function arguments, intermediate results, and function return contexts. • An integer n counting the number of function arguments available on the stack. The machine-level values v manipulated by the abstract machine are pointers to heap blocks, written [T : v1 . . . vn ], where T is a tag attached to the block (a small integer), and v1 . . . vn are the values contained in the block. We use tag 0 for representations of accumulator terms [k], tags 1 . . . n to encode the constructor C of constructed terms C( v), and a distinct tag T λ for function closures. The values of the calculus are represented by heap blocks as follows: For inductive types, we assume that the constructors of an inductive type are numbered consecutively starting at 1 when the type is declared. We write #C for the tag number associated with constructor C. The value C( v) is then represented by the heap block [#C : v], where v are the representations of v. • Finally, an accumulator [k] is represented by the heap block [0 : ACCU, k]. This is a pseudo-closure with the single machine instruction ACCU as code part, and an encoding k of k as environment part. This encoding is as follows: -[0 : x] represents the free variable x. : k, c, e] represents the suspended case statement case k of (C i ( x i ) → b i ), where c and e are the code and the environment for the function λx.case x of (C i ( x i ) → b i ). -[3 : c, e, k] represents the suspended fixpoint application fix n (λ f .λx 1 . . . λx n .b) v 1 . . . v n-1 k, where c and e are the code and the environment for the partially applied fixpoint fix n

• A function value is represented by a closure [T λ : c, e] of the compiled code c for the function body, and an environment e associating values to the variables free in λx.b. • -[1 : k, v1 , . . . , vn ] represents the suspended application k v 1 . . . v n .

-[2

Benchmark results for the synthetic tests (on a Pentium III 1Ghz, 256 Mb)

	Test		Our system Coq CBV Coq Lazy OCaml bytecode
	1. Normalization of factorial(9) (Peano integers)	14.2s	61.6s	466s	0.347s
	2. Normalization of is even(factorial(9)) (Peano integers)	0.447s	46.9s	4.82s	0.357s
	3. Normalization of 256 × 64 (Church integers)		0.106s	0.116s	1.99s	n/a
	4. Normalization of λx.λy. (128 + x) × (128 + y) (Church integers)	0.082s	0.107s	1.81s	n/a
	5. Equivalence of factorial(8) and factorial (8) (Peano integers)	0.096s	n/a	9.02s	0.085s
	6. Equivalence of 256 × 64 and 64 × 256 (Church integers)	0.094s	n/a	2.00s	n/a
	Figure 5. Proof	Our system	Coq OCaml bytecode OCaml native
	Coq's standard theories	135s	131s	n/a	n/a
	4-color theorem, perimeter 11	1.68s	56.7s	1.18s	0.30s
	4-color theorem, perimeter 12	6.50s	259s	6.18s	1.92s
	4-color theorem, perimeter 13	14.8s	680s	15.5s	4.11s
	4-color theorem, perimeter 14	69.6s out of memory	73.1s	19.8s

Acknowledgments

Henri Laulhère conducted preliminary experiments on modifying the Objective Caml compiler to implement strong normalization circa 1998; the results of these experiments were communicated and explained to us by Alexandre Miquel, and partly inspired this work. We thank Bruno Barras and Benjamin Werner for their expertise on Coq and the Calculus of Constructions, and the anonymous reviewers for pointing us to the work on online TDPE.