From Operational Semantics to Abstract Machines

John Hannan

Department of Computer Science, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen East, Denmark.

hannan@diku.dk

Dale Miller

Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104-6389, USA.

dale@cis.upenn.edu

Received 16 October 1992

We consider the problem of mechanically constructing abstract machines from operational semantics, producing intermediate-level specifications of evaluators guaranteed to be correct with respect to the operational semantics. We construct these machines by repeatedly applying correctness-preserving transformations to operational semantics until the resulting specifications have the form of abstract machines. Though not automatable in general, this approach to constructing machine implementations can be mechanized, providing machine-verified correctness proofs. As examples we present the transformation of specifications for both call-by-name and call-by-value evaluation of the untyped λ-calculus into abstract machines that implement such evaluation strategies. We also present extensions to the call-by-value machine for a language containing constructs for recursion, conditionals, concrete data types, and built-in functions. In all cases, the correctness of the derived abstract machines follows from the (generally transparent) correctness of the initial operational semantic specification and the correctness of the transformations applied.

1. Introduction

The correctness of programming language implementations is an important issue confronting language designers and implementors. Traditionally, such implementations are first built “by hand” and only then proved correct. Unfortunately, the resulting implementations may have little relationship to the language’s semantic specifications and so correctness may be difficult to show. For realistic languages, such correctness proofs become unwieldy because of the overwhelming amount of implementation-level information that must be correlated. In an alternative approach, a language implementation is constructed from the semantic specification in such a way that the resulting implementation is guaranteed to satisfy correctness requirements: no independent proof being necessary. This approach may provide a mechanical, if not automatic, process allowing the correctness to be machine checked. This latter point is important when considering the sizes of correctness proofs for realistic languages. Of course the choice of semantic specification and target language greatly influences the practicality of this approach.

We use operational semantics to specify the meaning of programs and abstract machines to provide an intermediate representation of the language’s implementation. Operational semantics can be presented as inference rules or, equivalently, as formulas in a weak meta-logic permitting quantification at first-order and second-order types. Such semantic specifications provide high-level and clear descriptions of programming languages, often handling numerous syntactic details in a declarative and simple fashion. Abstract machines can be presented as rewrite rules describing single-step operations on the state of a computation. Such specifications provide an intermediate level of representation for many practical implementations of programming languages. The construction of abstract machines has traditionally been performed by hand, with correctness proofs following later. We demonstrate how to take a specification for an evaluator in the highlevel, flexible style of operational semantics and derive, through formally justifiable steps, an abstract machine that implements that evaluator. While providing a direct proof of the correctness of derived abstract machines, these derivations also provide guidance for extending such machines and illustrate relationships among various abstract machines.

Because operational semantics specifications can have rich structure, completely automatic methods for constructing abstract machines from them seem feasible only for restricted classes of operational semantics. While identifying these classes and the corresponding procedures for constructing machines is of interest, we focus only on a general strategy for constructing machines and provide two examples of this task. Applying our approach to wider classes of languages and machines than considered here (for example, imperative languages and machines using a continuation-passing style) requires finding new transformations that will most certainly be dependent upon the particular structure of the semantic specification and machine for each case. The examples presented, however, demonstrate the kind of reasoning required for simple functional languages and environment-based abstract machines, and suggest the feasibility of similar transformations for other languages and architectures.

The basic goal of the derivations described in this paper differs slightly from the principal goal of most program translations. Typical translations involve rewriting programs in a source language into a different, target language. Compilation is such a process. Our specifications of both operational semantics and abstract machines sit inside a single meta-logic. Most of our effort in transforming specifications attempts to make various aspects of computation that are implicit in the way one specification relies on this metalogic explicit within another specification. In this way, transformed specifications rely less on the meta-logic. For example, one set of transformations changes a specification that uses second-order quantification to a specification that only uses first-order quantification. By continuing this kind of transformation, it is possible to reduce the specification’s reliance on the meta-logic to a point where theorem proving using that specification can be done by a simple rewriting of computation states that is modeled well using abstract machines.

This paper is organized as follows. In Section 2 we give a general description of the classes of operational semantics and abstract machines that we consider in later sections.

In Section 3 we present the meta-logic in which we specify operational semantics. This meta-logic provides various high-level features for simple manipulation of bound variables and contexts. In Section 4 we present two high-level and declarative specifications of evaluators which use second-order quantification, and then we transform them into specifications using only first-order quantification. Included in this section is a treatment of the translation from terms represented in a simply typed λ-calculus (with second-order constants) to terms in a language using only first-order constants. In Section 5 we take the first-order specifications developed in Section 4 and apply appropriate transformations to them until we produce systems describing abstract machines. The resulting proof systems are equivalent to the Krivine machine [Cur90] (for the call-by-name case) and a variant of the SECD machine [Lan64] (for the call-by-value case). In Section 6 we describe how the derivations of Sections 4 and 5 can be modified or extended to yield machines for richer languages that include recursion, a conditional and other new language features. Finally, in Section 7 we discuss relations to other work, and in Section 8 we summarize our results.

2. Operational Semantics and Abstract Machines

A recent trend in programming language design has been the use of operational semantics to define the semantics of a programming language. The particular style of operational semantics we consider here was inspired by Martin-Löf [Mar84] and uses sets of inference rules as specifications. Various instances of this approach have been called Proof-Theoretic Semantics, Natural Semantics and Relational Semantics [Han90, Kah87, MTH90]. This style of semantics has proved well suited to specifying evaluation strategies for realistic programming languages. Direct implementations of operational semantics require several general, symbolic techniques that are generally found in theorem provers or logic programming languages.

Abstract machines have been effectively used as intermediate and low-level architectures suitable for supporting serious implementations of a wide variety of programming languages, including imperative, functional, and logic programming languages. Abstract machines are distinguished from operational semantics by having simple and direct algorithmic implementations that can employ efficient data structures. On the other hand, abstract machines are distinguished from lower-level, machine-code implementations because typically the former uses pattern matching for destructing data while the latter explicitly addresses the notions of structure sharing, storage allocation, and register allocation.

One goal of this paper is to connect these two methods of specifying the evaluation of programming languages and, in doing so, to provide means of producing abstract machines from operational semantics. Below we provide an overview of each of these paradigms.

2.1. Operational Semantics

The phrase “structural operational semantics” is attributed to Plotkin, based on his seminal paper “A Structural Approach to Operational Semantics” [Plo81]. Although that term has come to describe a few different styles of specifications, in that paper it is used to describe evaluation in terms of a one-step reduction relation and his inference rules axiomatize this relation. Martin-Löf uses an operational semantics for describing type theory [Mar85]. While he does not present the definition as a set of inference rules, his notion of evaluation is both compositional and syntax directed. Milner is perhaps the first to use inference rules to axiomatize evaluation to canonical form in his descriptions of the dynamic semantics of Standard ML, including the latest specification of the full language [MTH90].

The work presented here was initially inspired by the work in Natural Semantics, as described in [Kah87]. That work uses a first-order meta-logic with inference rules presented using sequents. We extend this work by using a higher-order (and higher-level) meta-logic employing less explicit, natural deduction-style inference rules. As a reference point we present a simple example of natural semantics, namely type inference for a simple functional language containing function abstraction and application. We begin by defining a first-order abstract syntax for the language. We introduce three constants var: string → term, lam: (string × term) → term, and com: (term × term) → term for constructing variables, λ-abstractions, and applications (combinations), respectively. For example, we represent the familiar combinators I, K and S as follows:

Concrete Syntax  Abstract Syntax
λx.x  lam(“x”, var(“x”))
λxλy.x  lam(“x”, lam(“y”, var(“x”)))
λxλyλz.xz(yz) lam(“x”, lam(“y”, lam(“z”,

com( \begin{matrix}com(var(“x”),var(“z”)), \\ com(var(“y”),var(“z”)))))) \end{matrix}

To specify type inference we must also represent types as objects and we can do this by introducing a new type ty and the constants tvar: string → ty and arrow: (ty × ty) → ty. The relationship between a program and its type is denoted by the predicate of the metalogic hastype of meta-logic type (((string × ty) list) × term × ty) → o. (Following Church [Chu40], we use o to denote the type of meta-logic propositions). The first argument of hastype is a context binding variable names to types. For example, the proposition

hastype(nil, lam(“i”, var(“i”)), arrow(tvar(“a”), tvar(“a”)))

relates the combinator I to its type. (List constructors are nil and the infix symbol ::.) We axiomatize such propositions via the set of inference rules in Figure 1. The member predicate is assumed to be defined such that if member((X, T), Γ) is provable then (X, T) is the leftmost pair in Γ in which the left component is X. If the proposition

\frac{member((X, T), Γ)}{hastype(Γ, var(X), T)}  \frac{hastype((X, S) :: Γ, M, T)}{hastype(Γ, lam(X, M), arrow(S, T))}

\frac{hastype(Γ, M, arrow(S, T)) hastype(Γ, N, S)}{hastype(Γ, com(M, N), T)}

Fig. 1. Axiomization of type inference

hastype(γ, t, τ) is provable using this set of rules then the term (encoded by) t has type (encoded by) τ, given the assumptions in γ for the types of free object-variables of t.

In this setting and in others, the phrase “operational semantics” can be a misnomer, because such semantic specifications may lack a clear operational or algorithmic implementation. The term deductive semantics is more accurate, as the meanings of semantic judgments are given by deductions; the task of theorem proving or proof construction is left unspecified. One focus of our paper is the systematic restructuring of specifications so that rather simple algorithms can provide complete theorem provers. Because proofs in the meta-logic of semantic judgments describe the course of a computation, they will play a central role in justifying each restructuring of operational semantics.

2.2. Abstract Machines

Many abstract machines have much in common, and we define here the formal notion of Abstract Evaluation System (AES) that captures and abstracts some of this commonality. We assume some familiarity with term rewriting, its terminology and the notion of computation in a rewriting system [HO80]. Recall that a term rewriting system is a pair (Σ, R) such that Σ is a signature and R is a set of directed equations {l_{i} ⇒ r_{i}}_{i∈I} with l_{i}, r_{i} ∈ T_{Σ}(X) and V(r_{i}) ⊆ V(l_{i}). Here, T_{Σ}(X) denotes the set of first-order terms with constants from the signature Σ and free variables from X, and V(t) denotes the set of free variables occurring in t. We restrict our attention to first-order systems, i.e., Σ is a first-order signature, though this is not essential. Definition 1. An Abstract Evaluation System is a quadruple (Σ, R, ρ, S) such that the pair (Σ, R ∪ {ρ}) is a term rewriting system, ρ is not a member of R, and S ⊆ R. Evaluation in an AES is a sequence of rewriting steps with the following restricted structure. The first rewrite rule must be an instance of the ρ rule. This rule can be understood as “loading” the machine to an initial state given an input expression. The last rewrite step must be an instance of a rule in S: these rules denote the successful termination of the machine and can be understood as “unloading” the machine and producing the answer or final value. All other rules are from R. We also make the following significant restriction to the general notion of term rewriting: all rewriting rules must be applied to a term at its root. This restriction significantly simplifies the computational complexity of applying rewrite rules during evaluation in an AES. A term t ∈ T_{Σ}(∅) evaluates to the term s (with respect to the AES (Σ, R, ρ, S)) if there is a series of rewriting rules satisfying the restrictions above that rewrites t into s.

M  ⇒ ⟨ nil, M,  nil⟩
⟨  E,  λM, X :: S⟩ ⇒ ⟨X :: E, M,  S⟩
⟨  E, M ˆ N,  S⟩ ⇒ ⟨ E, M, {E, N}:: S⟩
⟨{E′, M}:: E,  0,  S⟩ ⇒ ⟨ E′, M,  S⟩
⟨  X :: E, n + 1,  S⟩ ⇒ ⟨ E, n,  S⟩
⟨  E,  λM,  nil⟩ ⇒  {E, λM}

\begin{matrix}M  ⇒ & ⟨nil, nil, M :: nil, nil⟩ \\ ⟨S, E, λM :: C, D⟩  ⇒ & ⟨\{E, λM\}:: S, E, C, D⟩ \\ ⟨S, E, (M ˆ N) :: C, D⟩  ⇒ & ⟨S, E, M :: N :: ap:: C, D⟩ \\ ⟨S, E, n:: C, D⟩  ⇒ & ⟨nth(n, E) :: S, E, C, D⟩ \\ ⟨X :: \{E′, λM\}:: S, E, ap:: C, D⟩ ⇒ & ⟨nil, X :: E′, M :: nil, (S, E, C) :: D⟩ \\ ⟨X :: S, E, nil, (S′, E′, C′) :: D⟩ ⇒ & ⟨X :: S′, E′, C′, D⟩ \\ ⟨X :: S, E, nil, nil⟩  ⇒ & X \end{matrix}

Fig. 2. The Krivine machine (top) and SECD machine (bottom)

In certain situations, it might be sensible to have a more restricted definition of AES. In particular, allowing only linear rewrite rules (rules whose left-hand sides have no repeated variables) simplifies an implementation of an AES by eliminating the need for a costly runtime equality check (to be certain that the duplicated variables are instantiated to the same term). Similarly, requiring an AES to be deterministic (that is, no two rewrite rules can be used on the same term) is also sensible, especially in the context of modeling evaluation of functional programs. We note that all the examples presented in this paper do, in fact, satisfy both of these additional restrictions.

The SECD machine [Lan64] and Krivine machine [Cur90] are both AESs and variants of these are given in Figure 2. The syntax for λ-terms uses de Bruijn notation with ˆ (infix) and λ as the constructors for application and abstraction, respectively, and {E, M} denotes the closure of term M with environment E. The first rule given for each machine is the “load” rule or ρ of their AES description. The last rule given for each is the “unload” rule. (In each of these cases, the set S is a singleton.) The remaining rules are state transformation rules, each one moving the machine through a computation step.

A state in the Krivine machine is a triple ⟨E, M, S⟩ in which E is an environment, M is a single term to be evaluated and S is a stack of arguments. A state in the SECD machine is a quadruple ⟨S, E, C, D⟩ in which S is a stack of computed values, E is an environment (here just a list of terms), C is a list of commands (terms to be evaluated) and D is a dump or saved state. The expression nth(n, E), used to access variables in an environment, is treated as a function that returns the n + 1^{st} element of the list E.

Although Landin’s original description of the SECD machine used variables names, our use of de Bruijn numerals does not change the essential mechanism of that machine.

3. The Meta-Language

All specifications of evaluation given in this paper, whether high-level or low-level, can be given as formulas or as inference rules within a simple meta-logic.

3.1. Types, Terms, and Formulas

Let S be a finite, non-empty set of non-logical primitive types (sorts) and let o be the one logical primitive type, the type of formulas. (o is not a member of S.) A type is either o, a member of S, or a functional type τ →σ in which both τ and σ are types. The function type constructor associates to the right: read τ_{1} → τ_{2} → τ_{3} as τ_{1} → (τ_{2} → τ_{3}). The order of a type is the measure of how deeply function types are nested to the left: primitive types are of order 0 and the type τ_{1} → ⋯ → τ_{n} → τ_{0}, in which τ_{0} is primitive and n > 0, is one greater than the maximum order of the types τ_{1}, …, τ_{n}.

The logical constants ∧ (conjunction) and ⊃ (implication) have type o → o → o and the logical constant ∀_{τ} (universal quantification of type τ) has type (τ → o) → o, for every type τ that does not contain o. A signature Σ is a finite set of typed, non-logical constants. We often enumerate signatures by listing their members as pairs, written a: τ, in which a is a constant of type τ. Although attaching a type in this way is redundant, it makes reading signatures easier. Occurrences of o are restricted in the types of nonlogical constants: if a constant c in Σ has type τ_{1} → ⋯ → τ_{n} → τ_{0}, in which n ≥ 0 and τ_{0} is a primitive type, then the types τ_{1}, …, τ_{n} may not contain o. If τ_{0} is o then c is called a predicate symbol. A signature is n^{th}-order if all its constants are of order n or less and at least one constant in it is of order n. Only first-order and second-order signatures are used in this paper.

A constant or variable of type τ is a term of type τ. If t is a term of type τ → σ and s is a term of type τ, then the application (t s) is a term of type σ. Application associates to the left: read the expression (t_{1} t_{2} t_{3}) as ((t_{1} t_{2}) t_{3}). Finally, if x is a variable of type τ and t is a term of type σ, then the abstraction λx t is a term of type τ → σ. The usual definition of free and bound variable occurrences are assumed as well as the notion of α-conversion. The logical constants ∧ and ⊃ are written in the familiar infix form. The expression ∀_{τ} (λz t) is written simply as ∀_{τ} z t. A term of type o is a formula. When t and s are λ-terms, the expression t = s denotes the mathematical proposition that t and s are α-convertible.

For variable x and term s of the same type, t[s/x] denotes the operation of substituting s for all free occurrences of x in t, systematically changing bound variable names in t to avoid free variable capture. Besides the relation of α-conversion, terms are also related to other terms by the following rules of β- and η-conversions.

• The term s β-converts to the term s′ if s contains a subformula occurrence of the form (λx t)t′ and s′ arises from replacing that subformula occurrence with t[t′/x].

• The term s η-converts to the term s′ if s contains a subformula occurrence of the form λx (t x), in which x is not free in t, and s′ arises from replacing that subformula occurrence with t.

The binary relation conv, denoting λ-conversion, is defined so that t conv s if there is a list of terms t_{1}, …, t_{n}, with n ≥ 1, t equal to t_{1}, s equal to t_{n}, and for i = 1, …, n − 1, either t_{i} converts to t_{i+1} or t_{i+1} converts to t_{i} by α, β, or η conversion. Expressions of the form λx (t x) are called η-redexes (provided x is not free in t) while expressions of the form (λx t)s are called β-redexes. A term is in λ-normal form if it contains no β or η-redexes. Every term can be converted to a λ-normal term, and that normal term is unique up to the name of bound variables. See [HS86] for a more complete discussion of these basic properties of the simply typed λ-calculus.

3.2. Specifications as Formulas

Our specification of evaluators uses a weak extension to Horn clause logic. In particular, let syntactic variables A range over atomic formulas and B range over possibly universally quantified atomic formulas. Formulas used for specifications are closed formulas of the form

∀z_{1} … ∀z_{m}[(B_{1} ∧ … ∧ B_{n}) ⊃ A] (m, n ≥ 0).

(If n = 0 the implication is not written.) These formulas differ from Horn clauses only in that the B_{i}’s are not necessarily atomic: they may be universally quantified atomic formulas. Occurrences of such universal quantifiers are called embedded universal quantifier occurrences. The quantifier occurrences ∀z_{i} are called outermost universal quantifier occurrences.

A specification is a pair ⟨Σ, P⟩ in which Σ is a signature and P is a finite, non-empty set of these extended Horn clauses with the following restrictions.

1 The signature Σ is exactly the set of non-logical constants with occurrences in for-

mulas in P. Thus, Σ does not need to be listed separately. 2 If a formula in P contains an embedded universal quantifier occurrence, then that

quantifier occurrence binds a variable of primitive type and Σ is a second-order signature.

3 If Σ is first-order then all of the outermost quantifier occurrences in formulas in P bind variables of (non-logical) primitive type. In this case, the set P must contain just first-order Horn clauses; that is, they contain no embedded quantifiers.

Such pairs ⟨Σ, P⟩ are used to specify the extension to predicates that are members of Σ. In particular, if p : τ_{1} → ⋯ → τ_{n} → o is a member of Σ, then the tuple ⟨t_{1}, …, t_{n}⟩ (for closed terms t_{i}) is in the extension of p if and only if the closed formula (p t_{1} ⋯ t_{n}) is provable from P and all the constants in the terms t_{1}, …, t_{n} are in Σ. Since the formulas permitted in specifications are so weak, classical logic provability here coincides with intuitionistic and minimal logic provability. In each of these cases, equality of terms and formulas is λ-convertibility.

For example, let S be the set {i} containing only one primitive type, let Σ_{0} be the second-order signature

{abs : (i → i) → i, app : i → i → i, eval : i → i → o},

and let P_{0} be the set containing the two formulas

∀_{i→i}m (eval (abs m) (abs m))
∀_{i}p∀_{i}q∀_{i}v∀_{i→i}m (eval p (abs m) ∧ eval (m q) v ⊃ eval (app p q) v).

Untyped λ-terms are represented using the constants abs (denoting abstraction) and app (denoting application). We discuss this syntax further in Section 4.1. This example has no embedded universal quantifier occurrences but it does have one outermost quantified variable whose type is of order 1. The specification ⟨Σ_{0}, P_{0}⟩ is used in Section 4 to give a high-level specification of call-by-name evaluation.

For another example, let S = {i, nat, list}, and consider the second-order signature

Σ_{1} = {abs : (i → i) → i, app : i → i → i, 0 : nat, 1 : nat, + : nat → nat → nat, nil : list, :: : i → list → list, count : list → i → nat → o}

and the set P_{1} containing the four formulas

∀_{list}l∀_{i}p∀_{i}q∀_{nat}c∀_{nat}d(count l p c ∧ count l q d ⊃ count l (app p q) (1 + (c + d)))

∀_{list}l∀_{i→i}m∀_{i}x∀_{nat}c(∀_{i}x(count (x:: l) (m x) c) ⊃ count l (abs m) c)
∀_{list}l∀_{i}x(count (x:: l) x 0)
∀_{list}l∀_{i}x∀_{i}y∀_{nat}c(count l x c ⊃ count (y :: l) x c).

(Here the list constructor :: is written in infix notation.) The pair ⟨Σ_{1}, P_{1}⟩ can be used to count the number of occurrences of the constant app in a term. In particular, if the atomic formula (count nil t n) is provable from P_{1} then n is an arithmetic expression equal to the number of occurrences of app in t. The functional interpretation of operations such as + are not part of the logic we have described here. For example, if there is a proof of the formula

count nil (absλx(absλy(app (app x y) (app y x)))) n

from Σ_{1} and P_{1} then that proof contains a subproof of the formula

count (d:: c:: nil) (app (app c d) (app d c)) n,

where c and d are eigenvariables of the proof. Thus, eigenvariables can be used to name bound variables when it is important to “descend” through an abstraction. This latter formula is provable if and only if n is the expression 1 + (1 + (0 + 0) + (1 + (0 + 0))). Beyond this example, the most sophisticated integer computations we need are those for incrementing positive integers, and for that, special treatment of integers is not necessary. At first glance, it may appear that the first argument of count that lists free variables is not needed for this specification. It is only used to determine whether or not the term in the second argument of count is a variable. Given the specification of terms that we have picked, it is clear that a term is a variable if and only if it is not an app or an abs. Specifying such a negative condition, however, is not possible in this meta-logic, and, hence, we are required to replace it with the positive condition of finding the second argument in the first argument.

3.3. Specifications as Proof Systems

Because of the simple structure of formulas in specifications we can describe specifications instead as proof systems by replacing formulas with inference rules. We view a clause of the form

∀z_{1} … ∀z_{m}[B_{1} ∧ … ∧ B_{n} ⊃ A]

as an inference rule of the form

\frac{B_{1} ⋯ B_{n}}{A}

in which the universal quantifiers ∀z_{1} … ∀z_{m} are implicitly assumed. We use the convention that all capitalized letters occurring in formulas of inference rules are variables implicitly quantified by outermost universal quantifiers. The clauses specifying count above can be specified as the following set of inference rules.

\begin{matrix}\frac{count L P C count L Q D}{count L (app P Q) (1 + (C + D))} & \frac{∀_{i}x(count (x:: L) (M x) C)}{count L (abs M) C} \\ \overline{count (X :: L) X 0} & \frac{count L X C}{count (Y :: L) X C} \end{matrix}

Inference rules of this kind only explicitly mention one logical connective, universal quantification, and occurrences of it are permitted only in the premises of rules. Thus, to complete a proof system we must specify the introduction rule for the universal quantifier. This and the rule for λ-conversion are

\frac{B[y/x]}{∀x B} ∀-I  and  \frac{B}{B′} λ.

These rules have the following provisos: for ∀-I, the eigenvariable y must not be in Σ or free in ∀x B; and for λ, we must have B conv B′. Usual notions of natural deduction [Gen69, Pra65] are assumed. Since there are no implications to introduce, proofs here do not involve the discharging of assumptions. (Adding such occurrences of implication is natural and useful for a wide range of specifications [Han90]; such implications, however, play only a small role in the specification of evaluators and so are not considered here.) A proof system is first-order or second-order if its equivalent presentation as a specification ⟨Σ, P⟩ is such that Σ is first-order or second-order, respectively.

In the rest of this paper, we present specifications as inference rules. It is important to note, however, that proofs in classical (or intuitionistic or minimal) logic using specifications-as-formulas are isomorphic to proofs using specifications-as-proof-systems. The choice of which presentation to use is only one of notational convenience.

3.4. Abstract Evaluation Systems as Proof Systems

While specifications form weak logical systems, they provide high-level mechanisms for the specification of evaluation in object-language functional programs. Many of these mechanisms, such as universal quantification, higher-order types, and λ-conversion, do not correspond to anything that appears in abstract evaluation systems. The following restricted proof systems, however, do correspond to AESs. Definition 2. A set of first-order inference rules is AES-defining if there are two binary predicate symbols p and q (not necessarily distinct) such that

•every axiom is of the form \overline{p s t} in which s and t are terms and V(t) ⊆ V(s);

•there is a distinguished inference rule of the form \frac{p t z}{q s z} in which s and t are terms,

V(t) ⊆ V(s), and z is a variable not free in either s or t; and •inference rules that are neither axioms nor the distinguished rule are of the form

\frac{p t z}{p s z} in which s and t are terms, V(t) ⊆ V(s), and z is a variable that is not free

in either s or t. For every AES-defining proof system I we can define an AES (Σ, R, ρ, S) (modulo the renaming of free variables) such that the following condition holds: for all terms s and t, I ⊢ q s t if and only if there exists some AES-rewriting sequence s ⟹^{ρ} s′ ⟹^{∗} s′′ ⟹^{r} t for some r ∈ S and some terms s′ and s′′ (⟹^{∗} denotes zero or more rewritings using R-rules). The correspondence between some given I and (Σ, R, ρ, S) can be described as follows:

• I contains the axiom \overline{p s t} if and only if S contains the rewrite rule s ⇒ t;

• I contains the distinguished rule \frac{p t z}{q s z} if and only if ρ is s ⇒ t; and

• I contains the rule \frac{p t z}{p s z} if and only if R contains s ⇒ t.

One important characteristic of AES-defining proof systems is the use of an “output” variable in the inference rules. Every inference rule (other than the axioms) is either of

the form \frac{p t z}{p s z} or \frac{p t z}{q s z} in which z is a variable (implicitly universally quantified).

Thus, for every proof in such a proof system there is a single term which is the second argument for every formula occurrence in the proof. Obviously, most specifications of evaluators are not AES-defining proof systems. First-order specifications can fail to satisfy the requirements of AES-defining proof systems in a number of ways. Particular violations that concern us later are proof systems that contain inference rules with 1 multiple formulas in their premises; 2 variables in their premises that do not also occur in their consequents; or

3 the form \frac{p t y}{p s z} in which y and z are not the same variable or they occur in s or t.

We can systematically convert a proof system containing inference rules with multiple premises to an equivalent (modulo a simple relation between provable formulas) system containing only rules with at most one premise. The latter two cases, however, are more problematic and no single method appears universally applicable.

3.5. Implementations of the Meta-Logic

Meta-logical specifications can be interpreted as logic programs and the literature on implementing logic programs can be directly applied to provide implementations of specifications. If a specification is first-order, then Prolog or the TYPOL language of the CENTAUR system [Kah87] can provide a depth-first interpreters of it. Since the higherorder logic programming language λProlog [NM88] supports higher-order quantification, λ-conversion, and embedded universal quantification, it can be used to give a depth-first implementation of the full meta-logic. Although depth-first interpretation is not generally complete, it is complete for those AES-defining proof systems that are deterministic (at most one rule can be applied at a given point in building a proof in a bottom-up fashion). Because almost all the AES-defining proof systems presented here are deterministic, λProlog can be used to provide correct implementations of them. Since such implementations are also tail-recursive, the result of compiling them should be efficient, iterative programs. By translating the specifications in this paper into λProlog code, we have been able to experiment with them. We found such prototyping and experimentation valuable in understanding the dynamics of various specifications.

4. From Explicit to Implicit Abstractions in Terms

This section begins with the specification of call-by-name and call-by-value as proof systems using the approach described in Section 3.3. Our first specifications represent object-level, untyped λ-terms using a meta-level syntax that employs simply typed λterms over a second-order signature. This approach makes it possible to map objectlevel abstractions directly to meta-level abstractions. Since the elegant and declarative meta-level operations for handling explicit abstractions are available, specifications can be clear, concise, and suitably abstracted from numerous implementation details. As we plan to construct abstract machines that use only first-order terms to encode object-level programs, we must translate terms using a second-order signature in which λ-abstractions are available explicitly to terms over a first-order signature in which abstractions are available only implicitly. The task of changing the specification of evaluation to accommodate this change in term-level syntax is not trivial. This section shows how this change can be effected for call-by-name and call-by-value evaluation.

4.1. Specifying Two Evaluators

In this section and the next, we only consider the untyped λ-calculus since it is rich enough to illustrate several problems in the evaluation of functional program. In Section 6 we consider several of those language extensions needed for more realistic functional programming languages, and demonstrate how our methods can be applied to those extensions.

The untyped λ-terms can be encoded into simply typed λ-terms of base type tm using two constants abs : (tm → tm) → tm and app : tm → tm → tm, for encoding object-level abstraction and application, respectively. (A formal definition of the encoding and its various properties can be found in [Han90].) Some example terms in this syntax are listed below.

Untyped λ-terms  Simply typed λ-terms
λx.x  (abs λu.u)
λy.y  (λz.z)(abs λu.u)
(λx.x)(λy.y)  (app (abs λu.u) (abs λv.v))

All three untyped λ-terms are β-convertible, but only the first two are α-convertible. Only the first two simply typed λ-terms are β-convertible. By convention, we typically select the unique (up to α-conversion) simply typed λ-term in βη-long normal form to represent the corresponding untyped λ-term term. That is, although (abs λu.u) and (λz.z)(abs λv.v) are equal meta-level terms and both encode λx.x, we only refer to the βη-long normal term (the first one here) as the encoding of the given untyped λ-term.

We observe that α-equivalent terms in the untyped λ-calculus map to λ-convertible terms in the simply typed λ-calculus of the meta-logic and a β-redex in the untyped λcalculus maps to a meta-level term of the form (app (abs s) t), which is not a meta-level β-redex.

To demonstrate some simple computations using this encoding, consider the following two examples. First, to determine if two terms p, q : tm are representations of α-convertible untyped (object-level) λ-terms, we only need to check if the equality p = q is provable in the meta-logic (such equality contains the meta-level conversion rules for α, β, and η).

For the second example, consider specifying object-level substitution. This can be done with using the 3-place predicate subst: tm → tm → tm → o, which is axiomatized using the simple axiom

∀_{tm→tm}A ∀_{tm}B (subst (abs A) B (A B)).

Thus if s, t, u : tm are encodings of untyped terms λx.p, q, r, respectively, and meta-level proposition (subst s t u) is an instance of the above axiom, then, at the object-level, r is α-convertible to the term p[q/x]. (See [Han90] for a proof of this correspondence).

The two inference rules in Figure 3 specify call-by-name evaluation and the two inference rules in Figure 4 specify call-by-value evaluation. In both of these cases, values are λ-terms in weak-head normal form. Rather than explicitly use the axiom for subst

\overline{eval (abs M) (abs M)}  \frac{eval P (abs M)  eval (M Q) V}{eval (app P Q) V}

Fig. 3. High-level specification of call-by-name evaluation

\overline{eval (abs M) (abs M)}  \frac{eval P (abs M)  eval Q R  eval (M R) V}{eval (app P Q) V}

Fig. 4. High-level specification of call-by-value evaluation

described above, these evaluators use the meta-level expressions (M Q) and (M R), respectively, to specify substitution via meta-level β-conversion. Alternatively, we could use the axiom for subst by expressing the rule for application (in the call-by-name case) as

\frac{eval P (abs M)  subst (abs M) Q R  eval R V}{eval (app P Q) V} .

Notice that these inference rules contain variables of the functional type tm → tm and no rule contains explicit mention of bound variables. If we name the rules in Figure 3 by E, then E ⊢ eval s t if and only if t encodes the weak-head normal form (whnf) obtained by a normal-order reduction of the untyped λ-term encoded by s. A similar statement can be made for the call-by-value inference rules.

These inference rules provide a high-level specification of evaluation in several senses. Below we focus on two of these senses, namely, the use of meta-level β-conversion to automatically perform object-level substitution of terms for bound variables and the use of λ-terms instead of simpler first-order terms in the meta-language.

4.2. Introducing Closures into the Call-by-Name Evaluator

To prepare for a change in the meta-level representation of untyped λ-terms, we introduce three predicates isabs, isapp and apply into the call-by-name evaluator in order to move the actual representation of terms away from the clauses that directly describe evaluation. The resulting inference system is given in Figure 5. Notice that the constants abs and app do not occur in those inference rules that mention the eval predicate. Using elementary facts about unfolding of inferences rules, it is immediate that the eval-facts provable from Figure 3 and from Figure 5 are identical. (A brief discussion of unfolding can be found in Appendix A.)

We now introduce the new constant clo : tm→(tm→tm)→tm to “name” object-level β-redexes. All meta-level terms containing clo are λ-convertible to terms of the form

(clo t_{1} λx_{1}(… (clo t_{n} λx_{n} s) …)) (n ≥ 0)  (∗)

in which s is either (app s_{1} s_{2}) for some s_{1} and s_{2}, (abs s′) for some s′, or one of the bound variables x_{1}, …, x_{n}. Depending on these three cases, we say that (∗) is the closure of an application, the closure of an abstraction, or the closure of a variable, respectively.

\frac{isapp A P Q  eval P R  apply Q R S  eval S V}{eval A V}

\frac{isabs P}{eval P P}

\overline{isabs (abs M)}  \overline{isapp (app P Q) P Q}  \overline{apply Q (abs M) (M Q)}

Fig. 5. Addition of some meta-level predicates.

Furthermore, all terms that appear in evaluators we consider have the additional property that the terms t_{1}, …, t_{n} are all closed terms and hence contain no occurrences of the bound variables x_{1}, …, x_{n}. If n = 0 then (∗) simply denotes s. Terms of the form (∗) are abbreviated using the syntax (clo t̄ λx̄ s).

Let t be a term built from abs, app, and clo as described above. The term t^{0} denotes the λ-normal form of the result of replacing every occurrence of clo in t with the term λuλv (v u). This mapping replaces all named β-redexes with meta-level β-redexes, which are then removed in the process of forming the λ-normal form.

Since the rules for isabs, isapp, and apply in Figure 5 are sensitive to the particular structure of terms, these rules must be modified to handle terms containing clo. For example, rules for isabs and isapp must now determine whether terms are closures of abstractions and applications. Since terms can also be closures of variables, we introduce the isvar predicate to test for such terms and to return the term in the closure that corresponds to that variable. The rules listed in Figure 6 address this additional structure.

As with the count example in Section 3.2, when reading the inference rules in Figure 6 from the bottom to top, the eigenvariables introduced by universally quantified premises can be seen as naming the bound variables of the λ-abstraction that they instantiate. Consider, for example, proving the formula

isvar nil (clo t_{1} λx_{1}(… (clo t_{n} λx_{n} s) …)) t.

If this atomic formula has a proof, that proof must also contain a subproof of the formula

isvar ((c_{n}, t_{n}) :: ⋯:: (c_{1}, t_{1}) :: nil) s′ t

where s′ is the result of replacing the bound variables x_{1}, …, x_{n} in s with the (distinct) eigenvariables c_{1}, …, c_{n}, respectively. The proof of this latter formula is essentially the computation that determines which of these eigenvariables is equal to s′ and that t is the term associated with that eigenvariable.

Let ⊢_{5} denote provability from the inference rules in Figure 5 and let ⊢_{6} denote provability from the inference rules in Figure 6. The proof of the following lemma follows from inspection of the inference rules for the meta-level predicates isabs, isapp, isvar and apply given in Figure 6. Lemma 3. Let r be a term of type tm over the constants abs, app and clo.

\frac{isapp A P Q  eval P R  apply Q R S  eval S V}{eval A V}

\frac{isabs P}{eval P P}  \frac{isvar nil P T  eval T V}{eval P V}

\overline{isabs (abs M)}  \frac{∀x (isabs (M x))}{isabs (clo T M)}

\overline{isapp (app P Q) P Q}  \frac{∀x (isapp (A x) (M x) (N x))}{isapp (clo T A) (clo T M) (clo T N)}

\frac{∀x (isvar ((x, T) :: E) (M x) V)}{isvar E (clo T M) V}  \overline{isvar ((X, T) :: E) X T}  \frac{isvar E X T}{isvar ((Y, S) :: E) X T}

\overline{apply Q (abs M) (clo Q M)}  \frac{∀x (apply Q (M x) (N x))}{apply Q (clo T M) (clo T N)}

Fig. 6. Evaluation with closures represented using clo : tm → (tm → tm) → tm.

1⊢_{6} isabs r if and only if r is the closure of an abstraction.

2⊢_{6} isapp r r_{1} r_{2} for r_{1} and r_{2} terms of type tm if and only if r is of the closure of an application, that is, it is of the form (clo t̄ λx̄ (app z_{1} z_{2})) for some terms z_{1} and z_{2} of type tm, in which case r_{1} is (clo t̄ λx̄ z_{1}) and r_{2} is (clo t̄ λx̄ z_{2}). When this relationship holds, (app r_{1}^{0} r_{2}^{0}) = r^{0}. 3⊢_{6} isvar nil r s if and only if r is the closure of a variable, that is, it has the form

(clo t_{1} λx_{1}(… (clo t_{n} λx_{n} x_{i}) …)) (n ≥ 1)

for some i such that 1 ≤ i ≤ n. In this case, s is the term t_{i}. When this relation holds, s^{0} = r^{0}. 4⊢_{6} apply t r s if and only if r is the closure of an abstraction, that is, it is of the form (clo ū λx̄ (abs z)) for some term z of type tm → tm and s is of the form (clo ū λx̄ (clo t z)). When this relationship holds, there is a term w of type tm → tm such that r^{0} = (abs w) and (w t^{0}) conv s^{0}. In particular, ⊢_{5} apply t^{0} r^{0} s^{0}. The following two propositions establish the correspondence between the proof systems

in Figures 5 and 6. Proposition 4. Let t and r be two terms of type tm such that r^{0} = t. If there is a term v such that ⊢_{5} eval t v, then there exists a term u such that u is the closure of an abstraction, ⊢_{6} eval r u, and u^{0} = v.

Proof. Let t and r be two terms of type tm such that r^{0} = t, and assume that there is a term v such that ⊢_{5} eval t v. First, consider the case where r is the closure of a variable. By Lemma 3, ⊢_{6} isvar nil r s where s is a proper subterm of r and s^{0} = r^{0}. Thus, if we can show that there exists a term u such that ⊢_{6} eval s u and u^{0} = v, then we have ⊢_{6} eval r u via the proof rule for eval which has (isvar nil r s) as a premise. If s is still the closure of a variable, repeat this step again. This repetition terminates in reducing ⊢_{6}-provability of (eval r v) to ⊢_{6}-provability of (eval r′ v) where r′ is a proper subterm of r, (r′)^{0} = r^{0}, and r′ is the closure of an application or abstraction.

Assuming that r is the closure of an application or abstraction, we can proceed by induction on the structure of proofs in Figure 5 of (eval t v).

For the base case, assume that (eval t v) follows from the fact that t = v and ⊢_{5} isabs t. Thus r is the closure of a abstraction and by Lemma 3, ⊢_{6} isabs r, so ⊢_{6} eval r r. Thus, r is the promised value for u.

For the inductive case, assume that (eval t v) follows from

⊢_{5} isapp t t_{1} t_{2}, ⊢_{5} eval t_{1} (abs w), ⊢_{5} apply t_{2} (abs w) s and ⊢_{5} eval s v.

Since t is the term (app t_{1} t_{2}), it must be the case that r is the closure of an application. By Lemma 3, ⊢_{6} isapp r r_{1} r_{2} for some r_{1} and r_{2} such that r_{1}^{0} = t_{1} and r_{2}^{0} = t_{2}. By the inductive hypothesis, there is a u_{1} such that u_{1}^{0} = (abs w), u_{1} is the closure of an abstraction, and ⊢_{6} eval r_{1} u_{1}. By Lemma 3 there is a term z such that ⊢_{6} apply r_{2} u_{1} z and z^{0} conv (w r_{2}^{0}). Since s conv (w t_{2}), we have s conv z^{0}. Using the inductive hypothesis again, we conclude that there is a u_{2} such that ⊢_{6} eval z u_{2}, u_{2} is the closure of an abstraction, and u_{2}^{0} = v. Thus, from

⊢_{6} isapp r r_{1} r_{2}, ⊢_{6} eval r_{1} u_{1}, ⊢_{6} apply r_{2} u_{1} z, and ⊢_{6} eval z u_{2},

we can conclude that ⊢_{6} eval r u_{2}, which completes this proof. □

The following proposition establishes a converse to the preceding proposition. Proposition 5. Let r and u be two closed, λ-terms such that ⊢_{6} eval r u. Then ⊢_{5} eval r^{0} u^{0}.

Proof. A proof of (eval r u) using Figure 6 can be converted directly to a proof of (eval r^{0} u^{0}) using Figure 5 by the following three steps. First, remove all proof rules above any formula occurrence whose head symbol is either the predicate isabs, isapp, or apply. Second, repeatedly remove instances of the inference rule for eval that has isvar in its premise by discarding the proof of its left premise and making the proof of the right premise the proof of the conclusion of that inference rule occurrence. Finally, replace every occurrence of a term t that is the argument of some predicate of some formula occurrence in the proof with the term t^{0}. It is now an easy exercise to verify that the resulting proof is indeed a ⊢_{5}-proof of (eval r^{0} u^{0}). □

The inference rules in Figure 6 successfully avoid performing substitution of terms for bound variables by making use of a closure-like structure. These rules still depend on using λ-abstraction and universal quantification at the meta-level. We are now in a position to remove this dependency.

A de Bruijn-style representation of terms containing clo can be built by introducing the first-order constant clo′. We treat indices in terms containing clo′ in such a way that the second argument of clo′ behaves as an abstraction. Consider the first-order signature

{ˆ : fotm → fotm → fotm, λ : fotm → fotm, clo′ : fotm → fotm → fotm, var : nat → fotm},

where ˆ denotes application, λ denotes abstraction (this is an overloading of the λ symbol), clo′ denotes the closure construction, and var maps natural numbers into terms encoding bound variables by their offsets. For the sake of brevity, we often abbreviate the term (var n) by n. Here, clo′ treats its second argument as an abstraction by modifying offsets of variables in that argument. Following [Bru72], closed terms of type tm can be placed in one-to-one correspondence with those terms of type fotm for which all indices denoting bound variables have an offset to an actual occurrence of a λ or a clo′. Using this first-order signature, the λ-term (clo t_{1} λx_{1}(… (clo t_{n} λx_{n} s) …)) translates to the first-order term (clo′ t′_{1} (… (clo′ t′_{n} s′) …)) of type fotm, where t′_{1}, …, t′_{n}, s′ are the translations of t_{1}, …, t_{n}, s, respectively. An index i at the position of s denotes a variable to be replaced by the term t_{n−i}.

Since clo′ is being used now to attach a list of terms t_{1}, …, t_{n} to the term s, clo′ can be replaced with explicit lists; that is, the above term can be represented simply as {t′_{n}::⋯::t′_{1} ::nil, s′}. Of course, now an index of i at the position of s must be interpreted as referring to the i + 1^{th} member of the associated list of terms and the construction { , } has type fotm list × fotm → fotm. For example, the term

(clo (abs λx.x) λu(clo (abs λx(absλy y)) λv(app v u)))

would be translated to the term of type fotm {λλ0 :: λ0 :: nil, 0 ˆ 1}.

This final representation of syntax has several advantages over the one using clo or clo′. First, it involves first-order constants only. Second, simple pattern matching can determine if a term embedded in a closure is an abstraction, application, or variable index; recursing down a series of clo’s is no longer needed. Third, the reversing of closures involved in proving isvar is not needed and the auxiliary list argument to isvar can be dropped. Finally, this syntax also makes it natural to identify a term s that is not a top-level { , } with {nil, s} and to identify the doubly nested closure expression {ℓ, {t:: nil, s}} with simply {t:: ℓ, s}. Given this change in the representation of terms, we can easily rewrite our inference rules to those presented in Figure 7. As in the transformation of the rules in Figure 5 and Figure 6, the only rules that change are those involved with the definition of the predicates isabs, isapp, isvar, and apply.

If t is a term of type tm built from the constants abs, app, and clo, let t^{∗} be the corresponding de Bruijn-style representation of t of type fotm over the constants ˆ , λ, { , }, and var. The proof of the following proposition follows immediately from the motivation of the inference rules in Figure 7 given above. Proposition 6. Let t and v be two terms of type tm built from the constants abs, app, and clo. Then ⊢_{6} eval t v if and only if ⊢_{7} eval t^{∗} v^{∗}.

Assuming that we are only interested in proving eval-atoms, the inference rules in Figure 7 can be simplified, using unfolding transformations, to the inference rules N_{0}, which are displayed in Figure 8. These are further transformed in Section 5.

4.3. Introducing Closures for Call-by-Value

We can follow the approach above to construct a first-order specification of the callby-value evaluator in Figure 4. Because the essential steps are the same as for the call-by-name case, with most of the rules in each system being the same, we present here only the different inference rules required for call-by-value evaluation.

\frac{isapp A P Q  eval P R  apply Q R S  eval S V}{eval A V}

\frac{isabs P}{eval P P}  \frac{isvar P T eval T V}{eval P V}

\overline{isabs \{E, λM\}}  \overline{isapp \{E, P ˆ Q\} \{E, P \} \{E, Q\}}

\overline{isvar \{T :: E, 0\} T}  \frac{isvar \{E, n\} T}{isvar \{X :: E, n + 1\} T}

\overline{apply Q \{E, λM\} \{Q:: E, M\}}

Fig. 7. Evaluation using list structures for closures.

\overline{eval \{E, λM\} \{E, λM\}}  (N_{0}.1)
\frac{eval \{E, M\} \{E′, λM′\} eval \{\{E, N\}:: E′, M′\} V}{eval \{E, M ˆ N\} V}  (N_{0}.2)
\frac{eval X V}{eval \{X :: E, 0\} V}  (N_{0}.3)
\frac{eval \{E, n\} V}{eval \{X :: E, n + 1\} V}  (N_{0}.4)

Fig. 8. The N_{0} proof system

The first step in the section above introduces the new predicates isabs, isapp, and apply. The exact same modifications of proof systems can be done for the call-by-value case with the only difference being the rule for application:

\frac{isapp A P Q  eval P R  eval Q S  apply S R T  eval T V}{eval A V} .

The next step, which introduces the constant clo, follows as before, although the inference rule for evaluating closures of variables is now just

\frac{isvar nil P V}{eval P V} ,

as no further evaluation is required. So the call-by-value version at this stage is just the set of rules in Figure 6, except for this rule and the rule for application, which is as above. The transition to a proof system that employs the first-order signature over type fotm follows as before, and all the rules are the same except the ones corresponding to the

\overline{eval \{E, λM\} \{E, λM\}}  (V_{0}.1)
\frac{eval \{E, M\} \{E′, λM′\}  eval \{E, N\} R  eval \{R:: E′, M′\} V}{eval \{E, (M ˆ N)\} V} (V_{0}.2)
\overline{eval \{X :: E, 0\} X}  (V_{0}.3)
\frac{eval \{E, n\} V}{eval \{X :: E, n + 1\} V}  (V_{0}.4)

Fig. 9. The V_{0} proof system

two rules noted above. Finally, when we unfold these rules to simplify their structure, we obtain the proof system V_{0}, displayed in Figure 9.

5. Constructing Two Abstract Machines

In this section we transform the two first-order evaluators listed at the end of Section 4 into abstract machines. The transformation steps used in this section vary in generality: some apply to a wide range of inference rules specifying evaluation strategies while some are particular to a given evaluator. In all cases, however, transformations are motivated by two goals. The first goal is to continue making a specification less dependent on the meta-logic in which it is situated. For example, in the previous section, we replaced explicit abstractions using simply typed λ-terms with implicit abstractions using de Bruijn indices and first-order terms. Here we go further by eliminating, for example, any need for general (first-order) unification during proof construction. Our second goal is to commit to certain decisions left implicit or undetermined in a specification so that the resulting specification immediately yields an explicit algorithm.

5.1. Constructing a Call-by-Name Machine

We wish to convert the inference rules of system N_{0} (presented at the end of Section 4.2) to an AES-defining set of inference rules to obtain an abstract machine that implements (weak head) normal-order reduction for untyped λ-terms. The proof rules in N_{0} fail to be AES-defining for two reasons. First, proofs in N_{0} branch when an application is evaluated. Second, the rule for application has two variables, E′ and M′, in the premise that are not in the conclusion. The first problem is solved by a general technique; the second problem, however, seems to have no general solution. The bulk of this section describes a series of transformations to address this second problem.

We first address the branching structure of proofs in N_{0}. Rule N_{0}.2 has two premises. During bottom-up proof construction, proofs for these two premises can be constructed in either order, or even in parallel. The choice is left to the particular implementation of the meta-logic. We can choose a sequential strategy and enforce its use by applying the following transformation. We introduce the new predicate symbol prove : (o list) → o

\overline{prove nil}  (N_{1}.1)
\frac{prove G}{prove (eval \{E, λM\} \{E, λM\}) :: G}  (N_{1}.2)
\frac{prove (eval \{E, M\} \{E′, λM′\}) :: (eval \{\{E, N\}:: E′, M′\} V) :: G}{prove (eval \{E, M ˆ N\} V) :: G} (N_{1}.3)
\frac{prove (eval X V) :: G}{prove (eval \{X :: E, 0\} V) :: G}  (N_{1}.4)
\frac{prove (eval \{E, n\} V) :: G}{prove (eval \{X :: E, n + 1\} V) :: G}  (N_{1}.5)

Fig. 10. The N_{1} proof system

and the atomic axiom (prove nil). Each inference rule

\frac{A_{1} ⋯ A_{n}}{A_{0}} of N_{0} is rewritten as \frac{prove A_{1} :: ⋯:: A_{n} :: G}{prove A_{0} :: G}

for variable G (of type (o list)) that is not free in any A_{i}. This kind of transformation is applicable to any proof system in which all inference rules contain only atomic formulas as premises. In the case of N_{0} this transformation produces the new system N_{1} given in Figure 10. The argument to prove represents the collection of formulas that remain to be proved. This list behaves like a stack during bottom-up proof construction, with the first formula in this list always chosen as the next one to prove. Constants such as prove of type (o list) → o are not formally allowed in our meta-logic (argument types are not permitted occurrences of the type o). To be formally correct here is simple: introduce a new primitive type, say b, let prove be of type (b list)→o instead and replace occurrences of eval in N_{1} with a new constant, say evl, of type tm → tm → b. For simplicity we continue to use just the type o.

Lemma 7. For all closed atomic formula (eval {ℓ, s} v),

N_{0} ⊢ (eval {ℓ, s} v) if and only if N_{1} ⊢ prove (eval {ℓ, s} v) :: nil.

The proof uses a straightforward induction on the structure of proofs in the two systems.

With N_{1} we have solved the problem of having inference rules with multiple premises. We are left to consider the problem of variables occurring in the premise but not in the conclusion of a rule. For the case of N_{1} this concerns rule N_{1}.3. We can characterize this problem more generally, however, in the context of operational semantics. These distinguished variables typically serve as placeholders or temporary names for intermediate results used in computing the final result of the computation specified by the inference rule. This idea is discussed in [How91] where a class of rules called evaluation rules is defined. Our concern here is in providing a technique for eliminating explicit reference to these variables.

For the case of N_{1} we exploit properties particular to proofs in this system (and subsequent ones as we introduce new proof systems). Unfortunately, these techniques do not extend to general, widely applicable strategies, but they do serve to illustrate the kind of reasoning possible for manipulating proof systems. In devising the steps involved in the following construction we were assisted by knowing the approximate structure of the resulting abstract machine.

A useful manipulation of proof systems involves introducing partial instantiations of an inference rule. Partial instances of a rule are constructed by substituting (possibly open) terms for some of the schema variables of the rule, with the free variables of these terms becoming schema variables of the new rule. (A schema variable is one that is implicitly universally quantified.) Clearly we can always add (to a proof system) instances of a rule already in the system. Furthermore, we can replace a rule by a set of its partial instances if every instance of the original rule is also an instance of one of the partial instances. We apply this idea to rule N_{1}.2. The variable G in this rule is of type (o list) and because there are only two list constructors (nil and ::), all possible instances of G are also instances of either nil or A:: G′ for some instances of A and G′. Thus, we can replace rule N_{1}.2 by the two inference rules:

\frac{prove nil}{prove (eval \{L, λM\} \{L, λM\}) :: nil}  (N_{1}.2a)

\frac{prove A:: G′}{prove (eval \{L, λM\} \{L, λM\}) :: A:: G′} . (N_{1}.2b)

Notice that the premise of N_{1}.2a is always trivially provable. In fact, we can unfold the rules N_{1}.1 and N_{1}.2a to produce the axiom

\overline{prove (eval \{L, λM\} \{L, λM\}) :: nil} . (N_{1}.2a′)

Further, notice that rules N_{1}.2b, 3, 4, 5 all have premises whose list arguments are non-nil and hence instances of N_{1}.1 cannot occur immediately above instances of these rules. If we use rule N_{1}.2a′ then we no longer need rule N_{1}.1 for non-trivial proofs. Taking rules N_{1}.2a′, 2b, 3, 4, 5 (relabeling them as shown) yields the N_{2} proof system displayed in Figure 11. Lemma 8. For all s, t, N_{1} ⊢ (prove (eval s t)::nil) if and only if N_{2} ⊢ (prove (eval s t):: nil). The proof of this Lemma is a straightforward induction on the size of N_{1} and N_{2} proofs and uses the reasoning outlined above.

Note that N_{1} and N_{2} are not precisely equivalent since N_{1} ⊢ (prove nil) but N_{2} ⊬ (prove nil). Since we are only interested in atomic prove statements that contain a non-empty list of formulas, this discrepancy is irrelevant.

The premise of rule N_{2}.3 contains two occurrences of each of the two variables L′ and M′ which do not occur in the conclusion. The following proposition describes a redundancy within these proof rules that allows us to remove one occurrence of each of L′ and M′.

\overline{prove (eval \{L, λM\} \{L, λM\}) :: nil}  (N_{2}.1)
\frac{prove A:: G}{prove (eval \{L, λM\} \{L, λM\}) :: A:: G}  (N_{2}.2)
\frac{prove (eval \{L, M\} \{L′, λM′\}) :: (eval \{\{L, N\}:: L′, M′\} V) :: G}{prove (eval \{L, M ˆ N\} V) :: G}  (N_{2}.3)
\frac{prove (eval X V) :: G}{prove (eval \{X :: L, 0\} V) :: G}  (N_{2}.4)
\frac{prove (eval \{L, n\} V) :: G}{prove (eval \{X :: L, n + 1\} V) :: G}  (N_{2}.5)

Fig. 11. The N_{2} proof system

Proposition 9. Let a be a formula, let Π be an N_{2} proof of (prove a :: nil) and let (prove a_{1} :: ⋯:: a_{n} :: nil), for n ≥ 2, be a formula occurring in Π. Then for all i = 1, …, n − 1, a_{i} has the form (eval s {ℓ, λt}) and a_{i+1} has the form (eval {s′:: ℓ, t} v) for some terms s, s′, ℓ, t and v.

Proof. Assume that the proposition does not hold for some formula a and proof Π. Let prove a_{1} :: ⋯:: a_{n} :: nil be the formula in Π closest to the root that does not have the desired form. Since n ≠ 1, this atom is the premise of some inference rule. That inference rule must be N_{2}.3 since the conclusion of any other inference rule applied to that formula would not have the desired form. If the inference rule was N_{2}.3, then the first two atoms, a_{1} and a_{2}, do have the required form. Hence, some pair in a_{2}::⋯::a_{n}::nil must not have the required form, and again the conclusion of this inference rule does not have the require form, contradicting the assumption. □

Thus, every instance of the inference rule N_{2}.2 in an N_{2} proof of (prove a :: nil) is also an instance of

\frac{prove (eval \{\{L′, M′\}:: L, M\} V) :: G}{prove (eval \{L, λM\} \{L, λM\}) :: (eval \{\{L′, M′\}:: L, M\} V) :: G} .

This inference rule could therefore replace N_{2}.2. The structural information of Proposition 9 can be used in a more interesting fashion: we can introduce a new predicate symbol eval′ : fotm → fotm → o and modify N_{2} to get the proof system N_{3} so that atomic formulas of the form

\begin{aligned}prove & (eval c_{1} \{ℓ_{1}, λt_{1}\}) :: (eval \{c_{2} :: ℓ_{1}, t_{1}\} \{ℓ_{2}, λt_{2}\}):: \\ & ⋯:: (eval \{c_{n} :: ℓ_{n−1}, t_{n−1}\} \{ℓ_{n}, λt_{n}\}) :: nil \end{aligned}

in N_{2} are replaced by formulas of the form

prove (eval c_{1} {ℓ_{1}, λt_{1}}) :: (eval′ c_{2} {ℓ_{2}, λt_{2}}) :: ⋯:: (eval′ c_{n} {ℓ_{n}, λt_{n}}) :: nil

in N_{3} proofs. Here, a new predicate eval′ is used to show that a variant of eval is intended: while the proposition (eval s t) states that s evaluates to t, the proposition

\overline{prove (eval \{L, λM\} \{L, λM\}) :: nil}  (N_{3}.1)
\frac{prove (eval \{\{L_{1}, M_{1}\}:: L, M\} V) :: G}{prove (eval \{L, λM\} \{L, λM\}) :: (eval′ \{L_{1}, M_{1}\} V) :: G}  (N_{3}.2)
\frac{prove (eval \{L, M\} \{L′, λM′\}) :: (eval′ \{L, N\} V) :: G}{prove (eval \{L, M ˆ N\} V) :: G}  (N_{3}.3)
\frac{prove (eval X V) :: G}{prove (eval \{X :: L, 0\} V) :: G}  (N_{3}.4)
\frac{prove (eval \{L, n\} V) :: G}{prove (eval \{X :: L, n + 1\} V) :: G}  (N_{3}.5)

Fig. 12. The N_{3} proof system

(eval′ s t) occurring in the context

(eval s′ {ℓ, λt′}) :: (eval′ s t) :: ⋯:: nil

states that {s:: ℓ, t′} evaluates to t. The proof system N_{3} is displayed in Figure 12. Lemma 10. For all s, t, N_{2} ⊢ (prove (eval s t)::nil) if and only if N_{3} ⊢ (prove (eval s t):: nil).

The proof follows from Proposition 9 and the discussion above. Note that the distinction between the predicate symbols eval and eval′ is semantic. Syntactically, however, we can use just one symbol instead of the two if we restrict our attention to formulas of the form

prove (eval c_{1} {ℓ_{1}, λt_{1}}) :: (eval′ c_{2} {ℓ_{2}, λt_{2}}) :: ⋯:: (eval′ c_{n} {ℓ_{n}, λt_{n}}) :: nil

(for n ≥ 1) because only the rules N_{3}.2 and N_{3}.3 manipulate eval′ predicates and always as the second element in a list of formulas.

The next transformation is a simple reorganization of data structures that exploits the isomorphism between a list-of-pairs and a pair-of-lists. The constants eval and eval′ can be viewed as pairing constructor (pairing a term with a value). The predicate prove takes a list of such pairs. An equivalent formulation uses the binary predicate prove_{1} : (fotm list) → (fotm list) → o that takes a pair of lists. The explicit pairing constructors can be eliminated in this way. This is done in the proof system N_{4} displayed in Figure 13.

Note that for any formula occurring in an N_{4} proof we can easily construct the corresponding formula occurrence in an N_{3} proof: use eval to pair together the first elements in the lists, and use eval′ to pair together all the remaining elements. Given the motivation for N_{4} above and the fact that the syntactic distinction between the constructors eval and eval′ is not relevant, the following is immediate. Lemma 11. For all s, t, N_{3} ⊢ (prove (eval s t) :: nil) if and only if N_{4} ⊢ (prove_{1} s:: nil t:: nil).

Recall that an AES-defining system must have an output variable as part of the atomic

\overline{prove_{1} \{L, λM\}:: nil \{L, λM\}:: nil}  (N_{4}.1)
\frac{prove_{1} \{\{L_{1}, M_{1}\}:: L, M\}:: S V :: T}{prove_{1} \{L, λM\}::\{L_{1}, M_{1}\}:: S \{L, λM\}:: V :: T}  (N_{4}.2)
\frac{prove_{1} \{L, M\}::\{L, N\}:: S \{L′, λM′\}:: V :: T}{prove_{1} \{L, M ˆ N\}:: S V :: T}  (N_{4}.3)
\frac{prove_{1} X :: S V :: T}{prove_{1} \{X :: L, 0\}:: S V :: T}  (N_{4}.4)
\frac{prove_{1} \{L, n\}:: S V :: T}{prove_{1} \{X :: L, n + 1\}:: S V :: T}  (N_{4}.5)

Fig. 13. The N_{4} proof system

\overline{prove_{2} \{L, λM\}:: nil \{L, λM\}:: nil \{L, λM\}}  (N_{5}.1)
\frac{prove_{2} \{\{L_{1}, M_{1}\}:: L, M\}:: S V :: T Z}{prove_{2} \{L, λM\}::\{L_{1}, M_{1}\}:: S \{L, λM\}:: V :: T Z}  (N_{5}.2)
\frac{prove_{2} \{L, M\}::\{L, N\}:: S \{L′, λM′\}:: V :: T Z}{prove_{2} \{L, M ˆ N\}:: S V :: T Z}  (N_{5}.3)
\frac{prove_{2} X :: S V :: T Z}{prove_{2} \{X :: L, 0\}:: S V :: T Z}  (N_{5}.4)
\frac{prove_{2} \{L, n\}:: S V :: T Z}{prove_{2} \{X :: L, n + 1\}:: S V :: T Z}  (N_{5}.5)

Fig. 14. The N_{5} proof system

formula being proved. This variable is set by the axioms and is preserved by all the other inference rules. Towards such a structure for our rules, we state the following trivial proposition. Proposition 12. For any terms s, t, the leaf of an N_{4} proof of (prove_{1} s:: nil t:: nil) must be an occurrence of the formula (prove_{1} t:: nil t:: nil).

We exploit this property of proofs by introducing a third argument to the prove_{1} predicate, modifying the one N_{4} axiom to identify this new argument with the final value t from the second argument t:: nil and modifying the remaining inference rules to preserve the value of this argument. The resulting proof system, called N_{5} and displayed in Figure 14, replaces prove_{1} with the new predicate prove_{2} : (fotm list)→(fotm list)→ fotm → o of three arguments. Lemma 13. For all s, t, N_{4} ⊢ (prove_{1} s :: nil t :: nil) if and only if N_{5} ⊢ (prove_{2} s :: nil t:: nil t). The proof follows from Proposition 12.

\overline{prove_{3} \{L, λM\}:: nil \{L, λM\}}  (N_{6}.1)
\frac{prove_{3} \{\{L′, N\}:: L, M\}:: S Z}{prove_{3} \{L, λM\}:: \{L′, N\}:: S Z}  (N_{6}.2)
\frac{prove_{3} \{L, M\}:: \{L, N\}:: S Z}{prove_{3} \{L, M ˆ N\}:: S Z}  (N_{6}.3)
\frac{prove_{3} X :: S Z}{prove_{3} \{X :: L, 0\}:: S Z}  (N_{6}.4)
\frac{prove_{3} \{L, n\}:: S Z}{prove_{3} \{X :: L, n + 1\}:: S Z}  (N_{6}.5)

Fig. 15. The N_{6} proof system

Now, N_{5} is not an AES-defining system only because in rule N_{5}.3 the variables L′ and M′ occur in the premise but not in the conclusion. Consider simplifying the inference rules of N_{5} by replacing each inference rule of the form

\frac{(prove_{2} t′_{1} t′_{2} t′_{3})}{(prove_{2} t_{1} t_{2} t_{3})} with \frac{(prove_{3} t′_{1} t′_{3})}{(prove_{3} t_{1} t_{3})}

where prove_{3} : (fotm list) → fotm → o is a new binary predicate. This kind of generalization is complementary to the instantiation transformations that we applied earlier. The resulting system, called N_{6}, is displayed in Figure 15.

Observe that all schema variables free in the premise of any N_{6} rule are also free in the conclusion of that rule. Furthermore, observe that for every N_{5} inference rule, the schema variables occurring free in the second argument of prove_{2} occur nowhere else in the premise. Thus this second argument is, in some sense, independent of the other arguments in premise formulas. Observe also that in any N_{5}-provable formula the first and second arguments are always lists of the same length and the second argument is always of the form {ℓ_{1}, λs_{1}}:: {ℓ_{2}, λs_{2}}:: ⋯:: nil. Thus for any N_{5}-provable formula, if the first and third arguments of this formula match the corresponding arguments in the premise of an inference rule, then the second argument must also match its corresponding argument in the premise of the rule. That is, the second argument supplies no constraint on the construction of N_{5} proofs and so can be safely discarded. This fact is formalized in the proof of the following proposition.

Lemma 14. For all s, t, N_{5} ⊢ (prove_{2} s::nil t::nil t) if and only if N_{6} ⊢ (prove_{3} s::nil t).

Proof. The proof in the forward direction is immediate: given a proof in N_{5} simply delete the second argument of all atomic formulas and change prove_{2} to prove_{3} throughout. We prove the reverse direction by proving the slightly more general statement: for all n ≥ 0, and terms s, s_{1}, …, s_{n}, t, if N_{6} ⊢ (prove_{3} s_{n} :: …:: s_{1} :: s:: nil t) then there exists terms t_{1}, …, t_{n} such that N_{5} ⊢ (prove_{2} s_{n}::…::s_{1} ::s::nil t_{n}::⋯::t_{1} ::t::nil t). The proof proceeds by induction on the height h of an N_{6} proof Π.

Base: For h = 1, Π must be of the form

\overline{(prove_{3} \{ℓ, λs\}:: nil \{ℓ, λs\})}

and so n = 0. The corresponding N_{5} proof is simply

\overline{(prove_{2} \{ℓ, λs\}:: nil \{ℓ, λs\}:: nil \{ℓ, λs\})} .

Step: Assume the statement holds for proofs of height h ≥ 1 and let Π be an N_{6} proof of (prove_{3} s_{n} :: …:: s_{1} :: s:: nil t) with height h + 1. We show that there exists an N_{5} proof Δ of (prove_{2} s_{n} :: …:: s_{1} :: s:: nil ℓ t) for some ℓ = t_{n} :: ⋯:: t_{1} :: t:: nil.

Let (prove_{3} s′_{m}:: …:: s′_{1} :: s′:: nil t) be the premise of the last inference of Π. By the inductive hypothesis, there exist terms t_{1}, …, t_{m} such that (prove_{2} s′_{m} :: …:: s′_{1} :: s′ :: nil t_{m} :: ⋯:: t_{1} :: t:: nil t) has an N_{5} proof Δ′. We proceed now by cases according to the last inference rule of Π.

1If the last rule is N_{6}.4 (N_{6}.5) then n = m, and let ℓ = t_{m} :: ⋯:: t_{1} :: t :: nil. The required proof Δ is then built from Δ′ and N_{5}.4 (N_{5}.5). 2If the last rule is N_{6}.2 then n = m + 1 and s′_{m} = {{ℓ_{1}, m_{1}}:: ℓ_{2}, m_{2}} for some ℓ_{1}, m_{1}, ℓ_{2}, m_{2}. Let ℓ = {ℓ_{2}, λm_{2}}:: t_{m} :: ⋯:: t_{1} :: t:: nil. Again the required proof Δ is constructed from Δ′ and N_{5}.2. 3If the last rule is N_{6}.3 then m = n + 1 and m > 0. Let ℓ = t_{m−1} :: ⋯:: t_{1} :: t:: nil. The proof Δ is constructed from Δ′ and N_{5}.3. It is trivial to verify that in each case the ℓ we construct is of the form t_{n}::⋯::t_{1}::t::nil

for some t_{1}, …, t_{n}. Letting n = 0 yields the required proof for the lemma. □

We now can state the main result of this section. Theorem 15. For all s, t, N_{0} ⊢ (eval s t) if and only if N_{6} ⊢ (prove_{3} s:: nil t). The proof follows from linking together all the lemmas in this section.

Notice that N_{6} is simply an AES-defining proof system for call-by-name evaluation if we add to it the load rule

\frac{prove_{3} \{nil, M\}:: nil Z}{cbn M Z} .

The abstract machine encoded by this proof system is given in Figure 16. Its state consists of a list (or stack) of closures {E, M}:: S. Compare this with the description in Figure 2 in which the state consists of the triple ⟨E, M, S⟩.

5.2. Constructing a Call-by-Value Machine

In this section we construct a machine for call-by-value evaluation using a strategy similar to the one applied in the previous section. Starting with the first-order specification V_{0} derived in Section 4.3, we construct the proof system V_{1} (displayed in Figure 17) in which inference rules involving atomic formulas are replaced by inference rules involving stacks of such formulas.

\begin{matrix}M ⇒ & \{nil, M\}:: nil \\ \{E, M ˆ N\}:: S ⇒ & \{E, M\}:: \{E, N\}:: S \\ \{E, λM\}:: \{E′, N\}:: S ⇒ & \{\{E′, N\}:: E, M\}:: S \\ \{X :: E, 0\}:: S ⇒ & X :: S \\ \{X :: E, n + 1\}:: S ⇒ & \{E, n\}:: S \\ \{E, λM\}:: nil ⇒ & \{E, λM\} \end{matrix}

Fig. 16. A call-by-name abstract machine

\overline{prove nil}  (V_{1}.1)
\frac{prove G}{prove (eval \{E, λM\} \{E, λM\}) :: G}  (V_{1}.2)

\frac{prove (eval \{E, M\} \{E′, λM′\}) \begin{matrix}::(eval \{E, N\} R) \\ ::(eval \{R:: E′, M′\} V) :: G \end{matrix}}{prove (eval \{E, M ˆ N\} V) :: G}  (V_{1}.3)

\frac{prove G}{prove (eval \{X :: E, 0\} X) :: G}  (V_{1}.4)
\frac{prove (eval \{E, n\} V) :: G}{prove (eval \{X :: E, n + 1\} V) :: G}  (V_{1}.5)

Fig. 17. The V_{1} proof system

Lemma 16. For all terms ℓ, s and v,

V_{0} ⊢ (eval {ℓ, s} v) if and only if V_{1} ⊢ (prove (eval {ℓ, s} v) :: nil).

The proof is similar to the proof of Lemma 7.

As with the call-by-name case we are again faced with the task of eliminating variables that occur only in the premise of a rule. The problematic variable occurrences in this case are E′ and M′ in rule V_{1}.3. There seems to be no simple generalization to Proposition 9 that reveals any redundancy in the inference rules of V_{1}. Thus, we appeal to a more general transformation (described in more detail in [Han90]) for introducing value stacks. We give here just an outline of this transformation and its applicability to operational semantics.

The formula (eval p v) represents a relation between an input program p and an output value v. We can formalize this notion of input and output by considering the following general form of an inference rule.

\frac{prove (eval p_{1} v_{1}) :: (eval p_{2} v_{2}) :: ⋯:: (eval p_{n} v_{n}) :: G}{prove (eval p v) :: G}  (∗)

The use of explicit lists of formulas enforces a left-to-right order in which these formulas are solved during bottom-up proof construction. Assume that during proof construction p is a closed term (known) and v is a variable (unknown) yet to be instantiated with a closed term. To ensure that a program p_{i} depends only on known information we restrict occurrences of free variables as follows: every free variable of p_{i} must either occur in p or in some v_{j} for some j < i. Thus an instance of program p_{i} can be determined from the program p (which we assume is given as input) and the results v_{j} of previous computations. We also assume that every variable occurring in v occurs in some v_{i} (1 ≤ i ≤ n). For a similar characterization of input and output within evaluation rules, see [How91].

If such variable restrictions hold for all inference rules in a proof system then we can reformulate the inference rules into a more functional, rather than relational, style. Instead of a binary predicate eval : fotm → fotm → o taking a program and a value as arguments we use a unary predicate eval_{1} : fotm → instr taking just a program as an argument and producing an instruction (using the new type instr). The unary predicate prove : (o list) → o is replaced by a ternary predicate prove_{1} : (instr list) → (fotm list) → fotm → o. The first argument is a list of instructions, replacing the list of predicates. The second argument is a value stack representing the values produced by instructions that have already been evaluated. The third argument represents the result of the original program (occurring at the root of the proof tree). Now the basic idea of the transformation we employ is that the value or result of a program is pushed onto the value stack during bottom-up proof construction. So if (prove (eval p v)::nil) is provable then a proof of (prove_{1} (eval_{1} p) :: ℓ s v_{0}) must have a subproof (prove_{1} ℓ v:: s v_{0}). This transformation directly addresses the elimination of meta-level variables occurring in the premise, but not conclusion, of inference rules. These variables provide access to intermediate results, and this is the same service the stack provides. The full details of this transformation are presented in [Han90].

Using this transformation we can construct the new proof system V_{2} (given in Figure 18) from V_{1}. This step introduces a new constant ϕ : instr. Lemma 17. For all terms p and v, V_{1} ⊢ (prove (eval p v) :: nil) if and only if V_{2} ⊢ (prove_{1} (eval_{1} p) :: nil nil v). The proof follows immediately from Theorem 7.11 of [Han90].

In any V_{2}-provable proposition (prove_{1} ℓ s z), the list ℓ consists only of eval_{1} or ϕ instructions. As eval_{1} and ϕ are the only constructors for instr, we can replace the terms of type instr with ones of type fotm. We first replace prove_{1} with a new predicate prove_{2} : (fotm list) → (fotm list) → fotm → o; then replace terms (eval_{1} p) with just p; and replace ϕ : instr with a new constant ψ : fotm. Performing this transformation yields V_{3}, displayed in Figure 19. Lemma 18. For all terms p and v, V_{2} ⊢ (prove_{1} (eval_{1} p) :: nil nil v) if and only if V_{3} ⊢ (prove_{2} p:: nil nil v). The proof is a trivial induction on the height of proof trees.

For any V_{3}-provable proposition (prove_{2} ℓ s v), ℓ is a list in which each element is either a closure {e, t} or the term ψ. We can view this as a list of only closures if

\overline{prove_{1} nil V :: nil V}  (V_{2}.1)
\frac{prove_{1} C \{E, λM\}:: S V}{prove_{1} (eval_{1} \{E, λM\}) :: C S V}  (V_{2}.2)
\frac{prove_{1} (eval_{1} \{E, M\}) :: (eval_{1} \{E, N\}) :: ϕ:: C S V}{prove_{1} (eval_{1} \{E, M ˆ N\}) :: C S V}  (V_{2}.3)
\frac{prove_{1} C X :: S V}{prove_{1} (eval_{1} \{X :: E, 0\}) :: C S V}  (V_{2}.4)
\frac{prove_{1} (eval_{1} \{E, n\}) :: C S V}{prove_{1} (eval_{1} \{X :: E, n + 1\}) :: C S V}  (V_{2}.5)
\frac{prove_{1} (eval_{1} \{R:: E, M\}) :: C S V}{prove_{1} ϕ:: C R:: \{E, λM\}:: S V}  (V_{2}.6)

Fig. 18. The V_{2} proof system

\overline{prove_{2} nil V :: nil V}  (V_{3}.1)
\frac{prove_{2} C \{E, λM\}:: S V}{prove_{2} \{E, λM\}:: C S V}  (V_{3}.2)
\frac{prove_{2} \{E, M\}:: \{E, N\}:: ψ :: C S V}{prove_{2} \{E, M ˆ N\}:: C S V}  (V_{3}.3)
\frac{prove_{2} C X :: S V}{prove_{2} \{X :: E, 0\}:: C S V}  (V_{3}.4)
\frac{prove_{2} \{E, n\}:: C S V}{prove_{2} \{X :: E, n + 1\}:: C S V}  (V_{3}.5)
\frac{prove_{2} \{R:: E, M\}:: C S V}{prove_{2} ψ :: C R:: \{E, λM\}:: S V}  (V_{3}.6)

Fig. 19. The V_{3} proof system

we introduce a new symbol ψ′ : fotm and replace ψ with a dummy closure {nil, ψ′}. We can again replace such a list with a pair of lists by introducing a new predicate prove_{3} : ((fotm list) list)→(fotm list)→(fotm list)→fotm→o. Now instead of having a list of pairs (the first argument of prove_{2}), we have a pair of lists (the first two arguments of prove_{3}). We are thus led to the proof system V_{4} displayed in Figure 20. Lemma 19. V_{3} ⊢ (prove_{2} {ℓ, m}:: nil nil v) if and only if V_{4} ⊢ (prove_{3} ℓ:: nil m:: nil nil v). The proof is a trivial induction on the height of proof trees.

The dummy environment associated with the constant ψ′ can be eliminated since it contains no information and it only appears on top of the environment stack E when ψ′

\overline{prove_{3} nil nil V :: nil V}  (V_{4}.1)
\frac{prove_{3} L C \{E, λM\}:: S V}{prove_{3} E :: L λM :: C S V}  (V_{4}.2)
\frac{prove_{3} E :: E :: nil:: L M :: N :: ψ′ :: C S V}{prove_{3} E :: L (M ˆ N) :: C S V}  (V_{4}.3)
\frac{prove_{3} L C X :: S V}{prove_{3} (X :: E) :: L 0 :: C S V}  (V_{4}.4)
\frac{prove_{3} E :: L n:: C S V}{prove_{3} (X :: E) :: L n + 1 :: C S V}  (V_{4}.5)
\frac{prove_{3} (R:: E) :: L M :: C S V}{prove_{3} nil:: L ψ′ :: C R:: \{E, λM\}:: S V}  (V_{4}.6)

Fig. 20. The V_{4} proof system

is on top of the term stack C. Rules V_{4}.3 and V_{4}.6 can be replaced by the following two rules.

\frac{prove_{3} E :: E :: L M :: N :: ψ′ :: C S V}{prove_{3} E :: L M ˆ N :: C S V}  (V_{4}.3′)

\frac{prove_{3} (R:: E) :: L M :: C S V}{prove_{3} L ψ′ :: C R:: \{E, λM\}:: S V}  (V_{4}.6′)

If we combine the first three arguments of prove_{3} into a tuple (making prove_{3} a binary predicate) then the resulting proof system is AES-defining. Figure 21 contains the corresponding abstract evaluation system: the CLS machine. (We have switched the order of the first two arguments.) It can be viewed as a dumpless SECD machine. As in the previous section we can introduce an appropriate rule to load the machine. This can be derived by considering how the original binary predicate (eval P V) has evolved into the four-place predicate (prove_{3} L C S V). The first argument of prove_{3}, a stack of environments, corresponds to the environment (E) and dump (D) of the SECD. The second argument of prove_{3} corresponds to the code stack (C) of the SECD. The third argument of prove_{3} acts as the argument stack (S) of the SECD. The constant ψ′ in our machine corresponds to the instruction ap (or @) found in the description of the SECD machine [Lan64]. This simplified machine avoids using an explicit dump in favor of maintaining a stack of environments such that the i^{th} term on the code stack is evaluated with respect to the i^{th} environment on the E stack (ignoring the occurrences of ψ′ which are not evaluated with respect to an environment). While the original SECD machine stores the entire state on the dump, the only required information is the old environment and the code associated with it. Comparing this machine with the SECD machine given in Figure 2, we note a one-to-one correspondence between the rules in the two machines, except for the two rules that manipulate the dump of the SECD.

\begin{matrix}M  ⇒ & ⟨M :: nil, nil:: nil, nil⟩ \\ ⟨λM :: C, E :: L, S⟩  ⇒ & ⟨C, L, \{E, λM\}:: S⟩ \\ ⟨(M ˆ N) :: C, E :: L, S⟩  ⇒ & ⟨M :: N :: ψ′ :: C, E :: E :: L, S⟩ \\ ⟨0 :: C, (X :: E) :: L, S⟩  ⇒ & ⟨C, L, X :: S⟩ \\ ⟨n + 1 :: C, (X :: E) :: L, S⟩ ⇒ & ⟨n:: C, E :: L, S⟩ \\ ⟨ψ′ :: C, L, R:: \{E, λM\}:: S⟩ ⇒ & ⟨M :: C, (R:: E) :: L, S⟩ \\ ⟨nil, nil, V :: S⟩  ⇒ & V \end{matrix}

Fig. 21. The CLS machine

There is a close relationship between our CLS machine and the Categorical Abstract Machine (CAM) [CCM87]. The latter can be viewed as a compiled version of the former. Both utilize a stack of environments and a stack of result values, though in the CAM these two stacks have been merged into one structure. The codes for the two machines are different. The CLS machine operates on a list of λ-terms (plus the constant ψ′) while the CAM operates on a list of instructions for manipulating its stack. These instructions do, however, correspond closely to operations performed on terms in the CLS, and recent work has shown this correspondence by defining the compilation of λ-terms into CAM instructions from the definition of the CLS machine [Han91].

6. Language and Machine Extensions

In this section we consider some extensions to our simple, object-level programming language, making it more realistic. We demonstrate how these new features can be specified via our high-level inference rules, and we outline how the transformations of the previous section apply to these new features.

6.1. The Second-Order Lambda Calculus

The object-language we have considered so far is just the untyped λ-calculus. Considering the simply typed calculus as the object-language adds nothing new to the theory of evaluation, since evaluation, in this case, can be viewed as an untyped operation. We can just erase the types of a simply typed term and apply untyped reduction to these terms.

A more interesting case involves the second-order lambda calculus, or System F [Gir86], in which types play a more important role during reduction. We begin by defining the syntax for this calculus.

The types of F are given by the following grammar, where α ranges over type variables.

T ::= α | T → T | ∀α.T.

The terms of F are defined inductively as follows:

1 for any type σ, we have a denumerable set of variables of type σ, and these are all

terms of type σ; 2 if t is a term of type τ and x^{σ} is a variable of type σ, then λx^{σ}.t is a term of type

σ → τ; 3 if t and u are terms of types σ → τ and σ, respectively, then (t u) is a term of type τ; 4 if t is a term of type σ and α is a type variable, such that for all free variables x^{τ} in

t, α does not occur free in τ, then Λα.t is a term of type ∀α.σ; and 5 if t is a term of type Λα.σ and τ is a type, then t{τ} is a term of type σ[τ/α].

Reduction in System F can be characterized by two rules:

(λx^{α}.t)u ⟹ t[u/x^{α}]  and  (Λα.t){τ} ⟹ t[τ/α],

with the first just being the typed version of β-reduction for term application. Our goal is to axiomatize normal-order reduction (to weak head normal form) as we did with the untyped calculus. We start by defining an abstract syntax for types and terms of System F. We assume two (meta-level) syntactic sorts, ty and tm, to denote object-level types and terms, respectively, of System F. The following signature will be used to present the abstract syntax of such terms and types.

⇒: ty → ty → ty app : tm → tm → tm
pi : (ty → ty) → ty abs : ty → (tm → tm) → tm
tapp : tm → ty → tm
tabs : (ty → tm) → tm.

Types are constructed using the two constants ⇒ (infix) and pi, for example, (pi λα(α ⇒ α)). Terms are constructed using the remaining constants. Term application is denoted as app; term abstraction is denoted as abs, where its first argument is the type of the abstracted variable. Type application is denoted by tapp and type abstraction is denoted by tabs. For example, we can represent the term Λβ((Λα(λx^{α}.x)){β → β}) by the term

(tabs λb(tapp (tabs λa(abs a λx.x)) (b ⇒ b))).

As we did in Section 4, we can axiomatize a reduction relation by introducing a predicate symbol eval : tm → tm → o. The four rules in Figure 22 axiomatize normal-order reduction to weak head normal form. Notice how meta-level β-reduction provides objectlevel substitution of both terms and types.

Applying techniques analogous to those of Section 4, we can introduce a first-order syntax for this calculus, using de Bruijn-style notation. This syntax is given by the following signature

⇒: foty → foty → foty ˆ : (fotm × fotm) → fotm (infix)
∀ : foty → foty  λ : (foty × fotm) → fotm
tvar : nat → foty ˆ ˆ : (fotm × foty) → fotm (infix)

Λ : fotm → fotm var : nat → fotm

(The overloading of the type for ⇒ should not cause any confusion). Type application is written t ˆ ˆ τ for term t and type τ. Type abstraction is written Λt for term t. The

\overline{eval (abs T M) (abs T M)}  \overline{eval (tabs H) (tabs H)}

\frac{eval P (abs T M) eval (M Q) V}{eval (app P Q) V}

\frac{eval P (tabs H) eval (H T) V}{eval (tapp P T) V}

Fig. 22. Call-by-name evaluation for System F

\overline{eval \{E, λ(T, M)\} \{E, λ(T, M)\}}  \overline{eval \{E, ΛH\} \{E, ΛH\}}

\frac{eval \{E, P \} \{E′, λ(T, M)\} eval \{\{E, Q\}:: E′, M\} V}{eval \{E, P ˆ Q\} V}

\frac{eval \{E, P \} \{E′, ΛH\} eval \{\{ ; |E, T | ; \}:: E′, H\} V}{eval \{E, P ˆ ˆ T \} V}

\frac{eval X V}{eval \{X :: E, 0\} V}  \frac{eval \{E, n\} V}{eval \{X :: E, n + 1\} V}

Fig. 23. A first-order specification of call-by-name evaluation for System F

non-negative integers are de Bruijn indices and are coerced into types foty and fotm by tvar and var, respectively. For brevity, we simply write n for both (tvar n) and (var n). Here, λ, Λ, and ∀ act as nameless binders and an occurrence of a (type or term) variable is given by an index that refers to the number of λ’s, Λ’s, and ∀’s to its (the variable’s) binding occurrence. For example, the term Λα.λx^{α}.x becomes Λλ(1, 0). The 1 refers to the type variable bound by Λ and the 0 refers to the term variable bound by λ. The abstract syntax of the term Λβ((Λα(λx^{α}.x)){β → β}) over this signature is Λ((Λ(λ (1, 0)) ˆ ˆ (0 ⇒ 0)).

Translating the evaluation specification above into one using this new syntax, following the approach of Section 4, yields the proof system in Figure 23. We have introduced a new form of closure, { ; |E, T | ; }, denoting the closure of type T with environment E, as types may now contain variables that are bound in the environment, just as with terms.

Finally, by following the steps of Section 5.1, we can produce an abstract machine corresponding to these rules and it is given in Figure 24.

Evaluation here is not sufficiently different than in the untyped case, since types are never evaluated and once they are moved into a closure, they are never retrieved. This example is included here largely to show that the transformation techniques of the previous two sections can be applied equally well in this typed situation.

\begin{matrix}M ⇒ & \{nil, M\}:: nil \\ \{E, M ˆ N\}:: S ⇒ & \{E, M\}:: \{E, N\}:: S \\ \{E, λM\}:: \{E′, N\}:: S ⇒ & \{\{E′, N\}:: E, M\}:: S \\ \{X :: E, 0\}:: S ⇒ & X :: S \\ \{X :: E, n + 1\}:: S ⇒ & \{E, n\}:: S \\ \{E, M ˆ ˆ T \}:: S ⇒ & \{E, M\}:: \{ ; |E, T | ; \}:: S \\ \{E, ΛM\}:: \{|E′, T |\}:: S ⇒ & \{\{|E′, T |\}:: E, M\}:: S \\ \{E, λM\}:: nil ⇒ & \{E, λM\} \\ \{E, ΛM\}:: nil ⇒ & \{E, ΛM\} \end{matrix}

Fig. 24. A machine for System F

6.2. Recursive Expressions

Recursion can be introduced into our object-language by introducing a constant that acts like the Y combinator. In particular, let the constant fix : (tm → tm) → tm be added to the second-order signature used in the beginning of Section 4. Evaluation of recursive expressions is given simply by the rule

\frac{eval (M (fix M)) V}{eval (fix M) V} .

Operationally, this rule performs an unwinding of the recursive definition by using metalevel β-reduction to do substitution. Those transformations used in Section 4 that replaced a second-order signature with a first-order signature can be applied also to this rule. The second-order constant fix must be replaced with a first-order constant μ : fotm → fotm that acts as a binder just like the constant λ. The corresponding transformation of the above evaluation rule, which can be added to both the call-by-name proof system N_{0} and the call-by-value proof system V_{0}, is the following rule.

\frac{eval \{\{E, μM\}:: E, M\} V}{eval \{E, μM\} V} .

Notice that this rule does not violate any of the conditions for AES-defining proof systems. The sequence of transformations applied to proof systems in Section 5 can be applied to both the proof systems N_{0} and V_{0} extended with this rule for recursion. In the call-by-name case, we would need to simply add the rewrite rule

⟨{E, μM}:: S⟩ ⇒ ⟨{{E, μM}:: E, M}:: S⟩

to the machine in Figure 16.

If we perform the series of transformations used for call-by-value evaluation, we need to add to proof system V_{4} the inference rule

\frac{prove_{3} (\{E, μM\}:: E) :: L M :: C S Z}{prove_{3} E :: L μM :: C S Z} ,

which translates to the rewrite rule

⟨μM :: C, E :: L, S⟩ ⇒ ⟨M :: C, ({E, μM}:: E) :: L, S⟩.

This rewrite rule can be added to the specification of the CLS machine in Figure 21.

6.3. Conditional Expressions

Introducing a conditional expression to our object-language provides a challenge requiring a new transformation. Using the constants if : tm → tm → tm → tm, true : tm, and false : tm we can construct terms representing conditional expressions. Evaluation of such expressions is specified via the two inference rules

\frac{eval P true  eval Q V}{eval (if P Q R) V} and \frac{eval P false  eval R V}{eval (if P Q R) V} .

The transformations to abstract syntax that uses a first-order signature are straightforward and yield the two rules

\frac{eval \{E, P \} true eval \{E, Q\} V}{eval \{E, (if P Q R)\} V}

\frac{eval \{E, P \} false eval \{E, R\} V}{eval \{E, (if P Q R)\} V} .

(Here, we assume that the types of if, true, and false now involve the primitive type fotm instead of tm.) Let V′_{0} be V_{0} extended with these two new rules (we only consider the more difficult call-by-value situation here). Transforming V_{0} into V_{1} required introducing the prove predicate and an explicit list of formulas. Following this transformation here yields V′_{1}, which is just V_{1} extended with the rules

\frac{prove (eval \{E, P \} true) :: (eval \{E, Q\} V) :: G}{prove (eval \{E, (if P Q R)\} V) :: G}

\frac{prove (eval \{E, P \} false) :: (eval \{E, R\} V) :: G}{prove (eval \{E, (if P Q R)\} V) :: G} .

Paralleling the transformation from V_{1} to V_{2} yields V′_{2}, which is V_{2} plus the following four rules:

\frac{prove_{1} (eval_{1} \{E, P \}) :: (ϕ_{1} E Q) :: C S Z}{prove_{1} (eval_{1} \{E, (if P Q R)\}) :: C S Z}

\frac{prove_{1} (eval_{1} \{E, P \}) :: (ϕ_{2} E R) :: C S Z}{prove_{1} (eval_{1} \{E, (if P Q R)\}) :: C S Z}

\frac{prove_{1} (eval_{1} \{E, Q\}) :: C S Z}{prove_{1} (ϕ_{1} E Q) :: C true:: S Z} \frac{prove_{1} (eval_{1} \{E, R\}) :: C S Z}{prove_{1} (ϕ_{2} E R) :: C false:: S Z} .

Notice that the evaluation of a conditional uses the same stack that is used for functional application. The final two transformations of V_{2} to V_{4} were simplifications of data structures, and these two transformations apply directly to the rules above, yielding the following four rules that must be added to V_{4} to derive V′_{4}:

\frac{prove_{3} E :: E :: L P :: (ψ_{1} Q) :: C S Z}{prove_{3} E :: L (if P Q R) :: C S Z}

\frac{prove_{3} E :: E :: L P :: (ψ_{2} R) :: C S Z}{prove_{3} E :: L (if P Q R) :: C S Z}

\frac{prove_{3} E :: L Q:: C S Z}{prove_{3} E :: L (ψ_{1} Q) :: C true:: S Z} \frac{prove_{3} E :: L R:: C S Z}{prove_{3} E :: L (ψ_{2} R) :: C false:: S Z} .

Notice that (ϕ_{1} E Q) and (ϕ_{2} E R) have been replaced by just (ψ_{1} Q) and (ψ_{2} R) in this transformation since the environment E appears at the front of the list in the first argument of prove_{2} in those inference rules that “introduce” ϕ_{1} and ϕ_{2}.

The proof system V′_{4} is an AES-defining proof system, and the abstract machine it encodes is formed by adding the following rewrite rules to those in Figure 21.

\begin{matrix}⟨ & E :: L, & (if P Q R) :: C, & S⟩ ⇒ & ⟨ & E :: E :: L, & P :: (ψ_{1} Q) :: C, & S⟩ \\ ⟨ & E :: L, & (if P Q R) :: C, & S⟩ ⇒ & ⟨ & E :: E :: L, & P :: (ψ_{2} R) :: C, & S⟩ \\ ⟨ & E :: L, & (ψ_{1} Q) :: C, & true:: S⟩ ⇒ & ⟨ & E :: L, & Q:: C, & S⟩ \\ ⟨ & E :: L, & (ψ_{2} R) :: C, & false:: S⟩ ⇒ & ⟨ & E :: L, & R:: C, & S⟩ \end{matrix}

This abstract machine is not as simple as we would like it to be because the first two rewrites share the same left-hand side. This means that rewriting would need to perform backtracking in order to do evaluation. Appendix B contains a transformation that can be used to “factor” the common parts of these two evaluation rules. Applying this factoring transformation to the four inference rules that are added to V_{4} yields the following three rules:

\frac{prove_{3} E :: E :: L P :: (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C S Z}{prove_{3} E :: L (if P Q R) :: C S Z}

\frac{prove_{3} L C_{1} @ C S Z}{prove_{3} L (choice C_{1} C_{2}) :: C S Z} \frac{prove_{3} L C_{2} @ C S Z}{prove_{3} L (choice C_{1} C_{2}) :: C S Z} .

Here, the infix symbol @ is used to denote list concatenation.

Because the only rule that mentions choice in the premise is the first rule above, the last two rules can be replaced by the following instantiations (making the obvious simplification of (α:: nil) @ C to α:: C):

\frac{prove_{3} L (ψ_{1} Q) :: C S Z}{prove_{3} L (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C S Z}

\frac{prove_{3} L (ψ_{2} R) :: C S Z}{prove_{3} L (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C S Z} .

We can now unfold these two rules with the two containing ψ_{1} and ψ_{2} in their conclusions.

This yields the following two rules:

\frac{prove_{3} E :: L Q:: C S Z}{prove_{3} E :: L (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C true:: S Z}

\frac{prove_{3} E :: L R:: C S Z}{prove_{3} E :: L (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C false:: S Z} .

These two rules plus the if introduction rule above provide a suitable definition for the conditional expression. The resulting proof system is AES-defining and rewriting will not require any backtracking. The corresponding abstract machine is given by adding the following rewrites:

⟨E :: L, (if P Q R) :: C, S⟩ ⇒ ⟨E :: E :: L, P :: (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C, S⟩

⟨E :: L, (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C, true:: S⟩ ⇒ ⟨E :: L, Q:: C, S⟩
⟨E :: L, (choice (ψ_{1} Q) :: nil (ψ_{2} R) :: nil) :: C, false:: S⟩ ⇒ ⟨E :: L, R:: C, S⟩

We can simplify these rules by combining some constants: since choice expressions are always of the form (choice (ψ_{1} Q)::nil (ψ_{2} R)::nil), we can introduce the “abbreviated” form (choice′ Q R), modifying the rules appropriately.

6.4. Pairs

We can introduce strict pairs to our object-language by introducing a new signature item pair : tm → tm → tm for constructing pairs of terms. In the highest level evaluator, the inference rule for evaluating a pair is

\frac{eval P_{1} V_{1} eval P_{2} V_{2}}{eval (pair P_{1} P_{2}) (pair V_{1} V_{2})} .

In the first-order setting using closures, the rule for evaluating a pair is

\frac{eval \{E, P_{1}\} V_{1} eval \{E, P_{2}\} V_{2}}{eval \{E, (pair P_{1} P_{2})\} (pair V_{1} V_{2})}

and this can be added to V_{0}. (Again, we assume that the type of pair is now fotm → fotm → fotm.)

Now, following the derivations in Section 5.2, we eliminate branching rules, producing the rule

\frac{prove (eval \{E, P_{1}\} V_{1}) :: (eval \{E, P_{2}\} V_{2}) :: G}{prove (eval \{E, (pair P_{1} P_{2})\} (pair V_{1} V_{2})) :: G} .

To accommodate the next step, that of introducing an value stack, we first split the above rule into the following two rules:

\frac{prove (eval \{E, P_{1}\} V_{1}) :: (eval \{E, P_{2}\} V_{2}) :: (mkpair V_{1} V_{2} V) :: G}{prove (eval \{E, (pair P_{1} P_{2})\} V) :: G}

\frac{prove G}{prove (mkpair V_{1} V_{2} (pair V_{1} V_{2})) :: G} .

These two rules essentially split the act of producing the values V_{1} and V_{2} from the act of constructing the pair of these two values. Using these two rules we can introduce a value stack, producing the following new rules:

\frac{prove_{1} (eval_{1} \{E, P_{1}\}) :: (eval_{1} \{E, P_{2}\}) :: ϕ_{3} :: C S Z}{prove_{1} (eval_{1} \{E, (pair P_{1} P_{2})\} ) :: C S Z}

\frac{prove_{1} (mkpair V_{1} V_{2}) :: C S Z}{prove_{1} ϕ_{3} :: C V_{2} :: V_{1} :: S Z}

\frac{prove_{1} C (pair V_{1} V_{1}) :: S Z}{prove_{1} (mkpair V_{1} V_{2} ) :: C S Z} .

Folding the latter two rules yields

\frac{prove_{1} C (pair V_{1} V_{1}) :: S Z}{prove_{1} ϕ_{3} :: C V_{2} :: V_{1} :: S Z} .

The remaining transformation steps are straightforward, producing the following rules for the CLS machine:

\begin{matrix}⟨(pair P_{1} P_{2}) :: C, E :: L, S⟩ ⇒ & ⟨P_{1} :: P_{2} :: ψ_{3} :: C, E :: E :: L, S⟩ \\ ⟨ψ_{3} :: C, L, V_{2} :: V_{1} :: S⟩ ⇒ & ⟨C, L, (pair V_{1} V_{2}) :: S⟩. \end{matrix}

(The switch from ϕ_{3} : o to ψ_{3} : fotm reflects the change in type of the instruction list C.)

6.5. Primitive Constants and Constructors

We can introduce constants and data constructors in a variety of ways. We present a method in which they are treated similarly. All constants are assumed to be in normal form, and so they evaluate to themselves. Data constructors are assumed strict and their arguments are encoded as pairs.

For constants, we introduce the new signature item const : string → fotm, and we represent each constant c of our object-language by the term (const c). Then we specify evaluation by the single rule

eval (const c) (const c)

and this translates to the machine rule

⟨(const c) :: C, E :: L, S⟩ ⇒ ⟨C, L, (const c) :: S⟩.

For data constructors, we introduce the new signature item constr, and we represent each constructor c(t1,…,tn) of our object-language by the term (constr c args) in which args is the encoding of the tuple (t_{1}, …, t_{n}). Then we specify evaluation by the single rule

\frac{eval A B}{eval (constr K A) (constr K B)}

and this translates (via a process similar to that for pairs) to the machine rules

\begin{matrix}⟨(constr K A) :: C, E :: L, S⟩ ⇒ & ⟨A:: (mkconstr K) :: C, L, S⟩ \\ ⟨(mkconstr K) :: C, E :: L, B :: S⟩ ⇒ & ⟨C, L, (constr K B) :: S⟩. \end{matrix}

6.6. Primitive Functions

Primitive functions can also be added in a straightforward way. We first assume that all primitive functions are strict and unary. In our first-order abstract syntax we encode primitive operators by introducing the constructor prim : string → fotm in which the operation is denoted by a string name. The evaluation of primitive functions can be specified via the rule

\frac{eval \{L, M\} (prim Op)  eval \{L, N\} R  oper(Op, Q) = V}{eval \{L, M ˆ N\} V} ,

where oper(Op, Q) = V denotes the property that applying the primitive function Op to the argument Q yields result V.

Now, following the derivation of Section 5.2, we can produce the following two rules:

\begin{matrix}⟨(M ˆ N) :: C, E :: L, S⟩ ⇒ & ⟨M :: N :: ψ_{4} :: C, E :: E :: L, S⟩ \\ ⟨ψ_{4} :: C, L, R:: (prim Op) :: S⟩ ⇒ & ⟨C, L, oper(Op, R) :: S⟩. \end{matrix}

Adding these two rules to our CLS machine produces a problem similar to the one encountered with the conditional statement. The machine has two possible reduction steps for applications: one for the case of primitive function application (introducing the constant ψ_{4}) and one for application of a lambda abstraction (introducing the constant ψ′). By factoring these two rules using the transformation described in Appendix B, performing some unfolding and renaming some collection of constants, we can simplify the description of application to the rules below (for a new constant ψ_{5} : fotm).

\begin{matrix}⟨(M ˆ N) :: C, E :: L, S⟩  ⇒ & ⟨M :: N :: ψ_{5} :: C, E :: E :: L, S⟩ \\ ⟨ψ_{5} :: C, L, R:: \{E′, M\}:: S⟩  ⇒ & ⟨M :: C, (R:: E′) :: L, S⟩ \\ ⟨ψ_{5} :: C, L, R:: (prim Op) :: S⟩ ⇒ & ⟨C, L, oper(Op, R) :: S⟩. \end{matrix}

7. Related Work

Previous work using abstract machines as an intermediate-level representation for a language has relied on informal methods for defining the machines or for relating them to source languages, or both. The principal advantage of this approach is the flexibility afforded in designing the structure of machines, as there are no a priori restrictions on the data structures or control structures that can be used. Considerations of efficiency, not evident in the semantic specifications, can be accommodated. The principal disadvantage, however, is the potential difficulty of proving that the abstract machines correctly implement a given language. Another disadvantage is the potential difficulty in extending the machines to accommodate new language features.

The prototypical abstract machine for a functional programming language is the SECD machine, and a proof of its correctness can be found in [Plo76]. While demonstrating the correctness of this machine with respect to an operational semantics, this proof does not provide much intuition regarding the overall structure of the machine or how it can be extended to handle a more substantial language. Our methods, however, provide a basis for proving such machines correct and, as demonstrated in Section 6, provide support for extending the machines to accommodate additional language features.

An example of an abstract machine used in an actual implementation of a language is the Functional Abstract Machine [Car84], a variant of the SECD machine, which has been optimized to allow fast function application. This machine, designed for implementing the ML language, addresses issues including efficient local variable storage, efficient closure construction and function manipulation, and exception handling. The design of this machine was influenced both by the structure of ML, for which it provides an intermediate level of representation, and also by concerns for efficient handling of data structures. This machine would not naturally be constructed by the naive strategy we have presented without a better understanding of architectural concerns. We believe, however, that the techniques we have developed could be adapted to prove the correctness of the FAM relative to an operational semantics for the core subset of ML that it implements.

Our use of operational semantics as the basis for language definitions supports a simple means for describing both semantics and machines in a single framework, namely proof systems. This uniformity contributes to the simple construction and verification of machines from semantics. In addition, operational semantics provides a natural setting for explicitly separating static and dynamic semantics. An alternative approach to language definition and implementation uses denotational semantics to define languages but also uses abstract machines as an implementation mechanism. One example of this approach uses a two-level meta-language to distinguish between compile-time and run-time operations of a denotational semantics and translates the run-time operations into an intermediate-level machine code [NN88]. The abstract machine and compiler defined in this way, though strongly influenced by denotational semantics, are given informally, and a correctness proof is still required to relate the denotational semantics, target language semantics, and compiler. Unfortunately, this proof requires some complex mathematical machinery (e.g., Kripke-like relations) to define a relation between the denotations of programs and the actions performed by abstract machines. This complexity seems inherent in this approach to compiler correctness due to fundamental differences between denotational definitions and abstract machine definitions.

The distinction between compile-time and run-time operations provided by this twolevel meta-language corresponds partly to the separation of operational semantics into distinct static and dynamic semantics specifications. In our work we have started with a dynamic semantics and not attempted to make any further distinction in the semantics regarding stages of operation. Thus our abstract machines operate on the same language, though perhaps in a different syntax, as the operational semantics. Additional separation of these abstract machines into compile-time and run-time operations, producing a level of machine code similar to that produced in the above approach, can be found in [Han91].

An alternative approach to constructing abstract machines from semantics is explored in [Wan82] where a continuation-style denotational semantics is used instead of operational semantics. The proposed technique involves choosing special-purpose combinators to eliminate λ-bound variables in the semantics and discovering standard forms for the resulting terms, to obtain target code that represents the meaning of the source code. The resulting abstract machine interprets these combinators. This approach relies on heuristics to choose appropriate combinators and discover properties of these combinators. Verification of the abstract machines constructed using this method is not addressed.

Finally, all the proof systems used in this paper can be naturally represented in the dependent type system LF [HHP87]. It is then possible to use the Elf implementation [Pfe91] of LF to implement the various transformations we have presented. Initial work in this direction is reported in [HP92].

8. Summary

We presented a general method for translating the operational semantics of evaluators into abstract machines. We believe that the choice of operational semantics as a starting point for semantics-directed implementations of programming languages is advantageous as it provides both a high-level and natural specification language and, as argued here, can be translated into intermediate architectures found in real, hand-crafted compilers. Though not automatic, our method provides a flexible approach for designing representations of languages that are suitable to machine implementation.

The translation from operational semantics to abstract machine proceeds via a series of transformations on the operational semantics. These specifications are given by proof systems axiomatizing evaluation relations, and the proofs constructible in these systems provide concrete objects representing the computation steps performed during evaluation. By examining the structure of these proofs, we can identify properties (of proofs and/or the proof system) that allow us to transform the proof system and also the proofs. Because proofs are syntactic objects that can be encoded as terms in a logic, we believe that most of the manipulations described here can be performed by an automated system, providing, at least, machine checked proofs of the construction of abstract machines.

Specifications within a second-order meta-logic can leave many aspects of computation implicit: implementations of the meta-logic must provide for such features as backtracking, unification, stacking of goals, etc. The central goal of the transformations presented here has been to make some of these implicit aspects more explicit within the specification. Thus, as the transformations continue, fewer features of the meta-logic are required. In our examples, transformations are continued until the the meta-logic can be modeled using a simple, iterative rewriting system characterized here as an abstract machine.

Appendix A. Unfolding Rules

One common kind of transformation on inference rules is a simple unfolding of two rules, producing a single new rule. Let R_{1} and R_{2} be two inference rules of the form

\frac{A_{1} A_{2} ⋯ A_{n}}{A}  \frac{B_{1} B_{2} ⋯ B_{m}}{B}

\frac{\begin{matrix}Ξ_{1} \\ θ(σ(B_{1})) \end{matrix} ⋯ \begin{matrix}Ξ_{2} \\ θ(σ(B_{i−1})) \end{matrix} \begin{matrix}Ξ_{3} \\ θ(σ(A_{1})) \end{matrix} ⋯ \begin{matrix}Ξ_{4} \\ θ(σ(A_{n})) \end{matrix} \begin{matrix}Ξ_{5} \\ θ(σ(B_{i+1})) \end{matrix} ⋯ \begin{matrix}Ξ_{6} \\ θ(σ(B_{m})) \end{matrix}}{θ(σ(B))}  (∗)

\frac{\begin{matrix}Ξ_{1} \\ θ(σ(B_{1})) \end{matrix} ⋯ \begin{matrix}Ξ_{2} \\ θ(σ(B_{i−1})) \end{matrix}  \frac{\begin{matrix}Ξ_{3} \\ θ(σ(A_{1})) \end{matrix} ⋯ \begin{matrix}Ξ_{4} \\ θ(σ(A_{n})) \end{matrix}}{θ(σ(B_{i}))}  \begin{matrix}Ξ_{5} \\ θ(σ(B_{i+1})) \end{matrix} ⋯ \begin{matrix}Ξ_{6} \\ θ(σ(B_{m})) \end{matrix}}{θ(σ(B))}  (†)

Fig. 25. Eliminating derived rules

for n, m ≥ 1, respectively, such that for some i, 1 ≤ i ≤ m, A and B_{i} unify with unifier σ. Then the following rule, denoted as σ(R_{1}/R_{2})_{i}, is a derived rule from R_{1} and R_{2}:

\frac{σ(B_{1}) ⋯ σ(B_{i−1}) σ(A_{1}) ⋯ σ(A_{n}) σ(B_{i+1}) ⋯ σ(B_{m})}{σ(B)} .

We call R_{1} and R_{2} the unfolded rules. We assume no clashes of the universally quantified variables occurring in these terms, as these variables can always be renamed. Note that for two given inference rules, a number of derived rules can exist based on possible choices of i and σ. Theorem 20. Let E be a proof system including two rules R_{1} and R_{2} with σ(R_{1}/R_{2})_{i} a derived rule for some σ and i. Then for all formulas A, E ⊢ A if and only if E ∪ {σ(R_{1}/R_{2})_{i}} ⊢ A.

Proof. The proof in the forward direction is trivial as any E proof is also a E ∪ {σ(R_{1}/R_{2})_{i}} proof. In the reverse direction we show that for any A and any E ∪ {σ(R_{1}/R_{2})_{i}} proof of A all occurrences of σ(R_{1}/R_{2})_{i} can be replaced by instances of R_{1} and R_{2}. Assume R_{1}, R_{2}, σ, i and σ(R_{1}/R_{2})_{i} are as described above. Now let Π be any E ∪ {σ(R_{1}/R_{2})_{i}} proof containing some instance of σ(R_{1}/R_{2})_{i} and let Ξ be a subproof of Π whose last inference rule is an instance of σ(R_{1}/R_{2})_{i}. This subproof must be of the form (∗) in Figure 25 for some substitution θ. Since σ(B_{i}) equals σ(A), we can construct another proof Ξ′ of θ(σ(B)) that contains one less instance of σ(R_{1}/R_{2})_{i} as given by (†) in Figure 25. Repeating this process until there are no more instances of σ(R_{1}/R_{2})_{i} yields an E proof. □

While it is not generally true that the inference rule σ(R_{1}/R_{2})_{i} can replace R_{1} and R_{2}, such replacement is possible at several points in this paper. When this is possible, we need to show that in any proof using R_{1} and R_{2}, these two rules occur together (as illustrated above) and hence can be replaced by instances of the unfolded rule (setting σ to the most general unifier, in this case).

Appendix B. Factoring Inference Rules

Call a proof system deterministic if for any provable proposition there exists a single (normal) proof of that proposition. Proof systems specifying the evaluation of functional programs usually are deterministic. Unfortunately, this property does not necessarily imply that the naive bottom-up construction of proofs is free from backtracking. For example, a bottom-up strategy may need to backtrack because for a given proposition, multiple inference rules may be applicable, even though only one can eventually lead to a proof.

We consider a class of proof systems for which bottom-up proof search requires backtracking, and we describe a transformation that effectively removes the need to backtrack. Our transformation is closely related to the factorization of context free production rules with common initial segments, and it has also been examined in [Sil90]. The following transformation can be used in conjunction with other transformations to remove the need for backtracking in some proof systems. For notational convenience we abbreviate α_{1} :: ⋯:: α_{n} :: C as α⃗ @ C. Factoring Transformation. Let E be a proof system in which every non-axiom inference rule is of the form

\frac{prove α⃗′ @ C δ′}{prove α:: C δ}

where C is either nil or a meta-variable. Furthermore, assume E has a pair of rules of the form

( \frac{prove α⃗′ @ β⃗ @ C δ′}{prove α:: C δ} , \frac{prove α⃗′ @ γ⃗ @ C δ′}{prove α:: C δ} )

for some terms α, α⃗′, β⃗, γ⃗, δ and δ′. Let E^{ch} be a proof system that contains the following three classes of inference rules: 1 For a new, fixed constant choice, the two inference rules

\frac{prove C_{1} @ C Z}{prove (choice C_{1} C_{2}) :: C Z} and \frac{prove C_{2} @ C Z}{prove (choice C_{1} C_{2}) :: C Z}

are members of E^{ch}. Here, Z, C, C_{1}, and C_{2} are schema variables for both of these rules.

2 For each pair of rules of the form displayed above, add to E^{ch} the inference rule

\frac{prove α⃗′ @ (choice β⃗ γ⃗) :: C δ′}{prove α:: C δ} .

3 Finally, every inference rule of E not in such a pair is added to E^{ch}.

This transformation provides a means for delaying a choice between two inference rules (during bottom-up proof construction) until after their common initial segment (α⃗) has been “processed.” Theorem 21. Let E^{ch} be obtained from some system E as given by the Factoring Transformation above and let (prove α⃗ δ) be a closed proposition containing no occurrences of choice. Then E ⊢ (prove α⃗ δ) if and only if E^{ch} ⊢ (prove α⃗ δ). The proof is by a straightforward induction on the height of proofs.

Acknowledgements. We are grateful to the reviewers of this paper and to Eva Ma From Operational Semantics to Abstract Machines 45

for their detailed comments and suggestions for improving this paper. Both authors have been supported in part by grants ONR N00014-88-K-0633, NSF CCR-87-05596, and DARPA N00014-85-K-0018 through the University of Pennsylvania. Hannan has also been supported by the Danish Natural Science Research Council under the DART project. Miller has also been supported by SERC Grant No. GR/E 78487 “The Logical Framework” and ESPRIT Basic Research Action No. 3245 “Logical Frameworks: Design Implementation and Experiment” while he was visiting the University of Edinburgh.

REFERENCES

[Bru72] N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5):381– 392, 1972.

[Car84] Luca Cardelli. Compiling a functional language. In 1984 Symposium on LISP and Functional Programming, pages 208–217, ACM, 1984.

[CCM87] Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The categorical abstract machine. The Science of Programming, 8(2):173–202, 1987.

[Chu40] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[Cur90] Pierre-Louis Curien. The λρ-calculus: An Abstract Framework for Environment Machines. Technical Report, LIENS–CNRS, 1990.

[Gen69] Gerhard Gentzen. Investigations into logical deduction. In M. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131, North-Holland Publishing Co., 1969.

[Gir86] Jean-Yves Girard. The system F of variable types: fifteen years later. Theoretical Computer Science, 45:159 – 192, 1986.

[Han90] John Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, 1990.

[Han91] John Hannan. Staging transformations for abstract machines. In P. Hudak and N. Jones, editors, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, pages 130–141, ACM Press, 1991.

[HHP87] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science, pages 194– 204, IEEE Computer Society Press, 1987.

[HO80] Gérard Huet and D. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349–405, Academic Press, 1980.

[How91] Doug Howe. On computational open-endedness in Martin-Löf’s type theory. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 162–172, IEEE Computer Society Press, 1991.

[HP92] John Hannan and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1992.

[HS86] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and λ-calculus. Cambridge University Press, 1986.

[Kah87] Gilles Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22–39, Springer-Verlag LNCS, Vol. 247, 1987.

J. Hannan and D. Miller 46

[Lan64] Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(5):308– 320, 1964.

[Mar84] Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory Lecture Notes, BIBLIOPOLIS, Napoli, 1984.

[Mar85] Per Martin-Löf. Constructive Mathematics and Computer Programming, pages 167–184. Prentice-Hall, 1985.

[MTH90] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.

[NM88] Gopalan Nadathur and Dale Miller. An overview of λProlog. In K. Bowen and R. Kowalski, editors, Fifth International Conference and Symposium on Logic Programming, MIT Press, 1988.

[NN88] Flemming Nielson and Hanne Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56:59–133, 1988.

[Pfe91] Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon D. Plotkin, editors, Logical Frameworks, Cambridge University Press, 1991.

[Plo76] Gordon Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(1):125–159, 1976.

[Plo81] Gordon Plotkin. A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark, September 1981.

[Pra65] Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Uppsala, 1965.

[Sil90] Fabio da Silva. Towards a Formal Framework for Evaluation of Operational Semantics Specifications. LFCS Report ECS–LFCS–90–126, Edinburgh University, 1990.

[Wan82] Mitchell Wand. Deriving target code as a representation of continuation semantics. ACM Trans. on Programming Languages and Systems, 4(3):496–517, 1982.