The Tail Recursive SECD Machine

John D. Ramsdell
The MITRE Corporation
October 1996 Revised September 1997

Abstract. One method for producing verified implementations of programming languages is to formally derive them from abstract machines. Tail recursive abstract machines provide efficient support for iterative processes via the ordinary function calling mechanism. This document argues that the use of tail recursive abstract machines incurs only a small increase in theorem proving burden when compared with what is required when using ordinary abstract machines. The position is supported by comparing correctness proofs performed using the Boyer-Moore theorem prover. The cost of efficient support for iteration is small.

Introduction

More than twenty years ago, Gordon Plotkin published a famous paper that examines the relation between the Lambda Calculus and ISWIM, a programming language based on the Lambda Calculus [Plotkin75]. ISWIM has an operational semantics given by the SECD machine. The paper includes a proof that the semantics defined by the SECD machine is equivalent to a recursively defined function which implements applicative order evaluation of lambda terms. In that order, the bodies of lambda terms are not evaluated and the arguments of combinations are evaluated before they are substituted.

For efficiently reasons, most programming languages in use today use applicative order evaluation. In addition, most functional programming languages require that their implementations be tail recursive. This means that programmers can use recursively defined functions to specify iterative processes.

The SECD machine is not tail recursive. Every application of a function to an argument causes the push of information onto the dump, the SECD machine's equivalent of a control stack. The SECD machine implements the caller saves convention, which means that the callee is free to do as it pleases with the SEC (stack, environment, and code) part of an SECD's machine state.

This document presents a tail recursive SECD machine (TR-SECD). There are several ways of defining a TR-SECD machine. The TR-SECD machine within implements a callee saves convention, which means that the callee must ensure that a return to the caller results in the restoration of the SEC part of the TR-SECD machine. This version of a TR-SECD machine is motivated by VLisp Scheme specification and implementation [GuttmanEtAl95].

Many efforts aimed at formally deriving efficient implementations of programming languages produce non-tail recursive implementations. Some start with the SECD machine, and some start with the Categorical Abstract Machine [Hannan91]. The thesis of this document is that using tail recursive abstract machines results in implementations that efficiently handle iterative processes with only a modest increase in theorem proving burden.

Support for the thesis is provided by presenting two fully automated correctness proofs. The first proof shows that a recursively defined evaluation function for the Lambda Value Calculus is equal to an evaluation function defined by the SECD machine [secd.events]. The second proof shows that the same recursively defined evaluation function is equal to an evaluation function defined by the TR-SECD machine [trsecd.events]. A study of the two proofs shows that the correctness proof the TR-SECD machine is only slightly more complex than the one for the SECD machine.

Each correctness proof was performed using the Boyer-Moore theorem prover [BoyerMoore88] [NQTHM-1992]. The logic of the Boyer-Moore theorem prover is first order, and the system provides extensive support for recursive functions and inductive proofs.

This document gives a high level description of the two SECD machines. It then describes the encoding of the descriptions in the logic of the Boyer-Moore theorem prover. Finally, it compares the relative difficultly of both proofs.

The SECD Machines

Given the emphasis on machine generated proofs, the issues associated with variable name conflicts have been avoided by the use of nameless lambda terms. In addition, given the lack of support for mathematics in HTML, math will be rendered using an SML-like syntax. Backslash will stand for the Greek letter lambda.

The objects manipulated by the TR-SECD machine are given by the following grammar:

  K --> ...                         Con   Constants
  N --> 1 | N + 1                   Num   Variables
  V --> K | \M                      Val   Values
  M --> V | N | (M M)               Exp   Expressions
  L --> (V, E)                      Clsr  Closures
  S --> nil | L :: S                Stk   Stack
  E --> nil | L :: E                Env   Environments
  C --> ret | call | M :: C         Code  Code Sequences
  D --> halt | (S, E, C, D)         Dmp   Dumps
Objects manipulated by the SECD machine differ only in the fact that code sequences differ.
  C --> ret | call :: C | M :: C    Code  Code Sequences
Following Plotkin, primitives are defined by giving a delta function which maps pairs of constants to closed values. Note that the delta function can be partial.

A nameless lambda term is closed iff the free variable limit of the term is zero. The free variable limit is computed as follows:

  fv : Exr --> Num
  fv K = 0
  fv N = N
  fv \M = N,          (N + 1 = fv M)
  fv \M = 0,              (0 = fv M)
  fv (M M') = max(fv M, fv M')
This evaluation function for the Lambda Value Calculus is recursive.
  eval : Exp --> Val
  eval K = K
  eval \M = \M
  eval (M M') = eval(subst(M", V, 1)),
                  (eval M = \M" and eval M' = V)
  eval (M M') = delta(K, K'),
                   (eval M = K and eval M' = K')
Nameless substitution is defined using two recursive functions, subst and bump. The value of subst(M, V, N) is the result of substituting value V for variable N in expression M.
  subst : Exp * Val * Num --> Exp
  subst(K, V, N) = K
  subst(N, V, N') = V,              (N = N')
  subst(N, V, N') = N,              (N < N')
  subst(N + 1, V, N') = N,          (N >= N')
  subst(\M, V, N)
    = \subst(M, bump(V, 0), N + 1)
  subst((M M'), V, N)
    = (subst(M, V, N) subst(M', V, N))
  bump : Exp * Nat --> Exp
  bump(K, N) = K
  bump(N, N') = N,                  (N <= N')
  bump(N, N') = N + 1,              (N > N')
  bump(\M, N) = \bump(M, N + 1)
  bump((M M'), N) = (bump(M, N) bump(M', N))

TR-SECD Machine

The function step is the transition function for the Tail Recursive SECD machine. The transition function step' for the original SECD machine will be given in a later section.
  step : Dmp --> Dmp
  step(L :: S, E, ret, (S', E', C', D')) = (L :: S', E', C', D')
  step(S, E, N :: C, D) = (lookup(N, E) :: S, E, C, D)
  step(S, E, K :: C, D) = ((K, nil) :: S, E, C, D)
  step(S, E, \M :: C, D) = ((\M, E) :: S, E, C, D)
  step((\M, E') :: L :: S, E, call, D) = (S, L :: E', M' :: ret, D)
  step((K, E') :: (K', E") :: S, E, call, D)
    = ((delta(K, K'), nil) :: S, E, ret, D)
  step(S, E, (M M') :: ret, D) = (S, E, M' :: M :: call, D)
  step(S, E, (M M') :: C, D) 
    = (nil, E, M' :: M :: call, (S, E, C, D)),           (C != ret)
The value associated with a variable in a given environment is computed by the function lookup.
  lookup : Num * Env --> Clsr
  lookup(1, L :: E) = L
  lookup(N + 1, L :: E) = lookup(N, E)
A run of the TR-SECD machine produces a value when an accepting state is detected. The function run is undefined if it reaches an error state, or fails to reach an accepting state for any other reason.
  run : Dmp --> Val
  run(L :: S, E, ret, halt) = real L
  run D = run(step D),   (otherwise)
The expression represented by a pair consisting of an expression and an environment is computed by the function real, which uses the auxiliary function butt. It can easily be shown that the function real produces a value when applied to a closure.
  real : Exp * Env --> Exp
  real(M, nil) = M
  real(M, L :: E) = real(subst(M, butt(real L, E), 1), E)
  butt : Exp * Env --> Exp
  butt(M, nil) = M
  butt(M, L :: E) = bump(butt(M, E), 0)

Correctness Proof

The correctness of the TR-SECD machine is expressed in the following theorem.

Correctness Theorem. If the expression M is closed,

  eval M = run(nil, nil, M :: ret, halt)
This remainder of this section contains the important lemmas used to prove Theorem 1.

Substitution Lemma. If real(\M', E) = \M and real(V', E') = V, then

  subst(M, V, 1) = real(M', (V', E') :: E)
A value environment is defined inductively.
  1. nil is a value environment
  2. (V, E) :: E' is a value environment if
An expression M is said to be closed in environment E iff E is a value environment and fv M <= length E. A closure (V, E) is said to be a value closure iff V is closed in E.

To control the complexity of the proofs, the correctness proof is factored into a stage which verifies the correctness of environments and substitution, and a later stage which verifies the correctness of the control information. The following lemma is aimed at the first stage.

Reduction Lemma. Assume expression M is closed in environment E. If eval(real(M, E)) is undefined, then reduce(M, E) is undefined, otherwise

  1. eval(real(M, E)) = real(reduce(M, E))
  2. reduce(M, E) is a value closure
where the definition of function reduce follows.
  reduce : Exp * Env --> Clsr
  reduce(K, E) = (K, nil)
  reduce(\M, E) = (\M, E)
  reduce(N, E) = lookup(N, E)
  reduce((M M'), E) = reduce(M", L :: E'),
                  (reduce(M, E) = (\M", E') and reduce(M', E) = L)
  reduce((M M'), E) = (delta(K, K'), nil),
             (reduce(M, E) = (K, E') and reduce(M', E) = (K', E"))
Adequacy Lemma. Assume expression M is closed in environment E, and reduce(M, E) is defined. Then
  run(S, E, M :: C, D) = run(reduce(M, E) :: S, runenv(M, E, C), C, D)
where the definition of function runenv follows.
  runenv : Exp * Env * Code --> Env
  runenv(K, E, C) = E
  runenv(\M, E, C) = E
  runenv(N, E, C) = E
  runenv((M M'), E, ret) = runenv(M", L :: E', ret),
                  (reduce(M, E) = (\M", E') and reduce(M', E) = L)
  runenv((M M'), E, ret) = E,
             (reduce(M, E) = (K, E') and reduce(M', E) = (K', E"))
  runenv((M M'), E, C) = E,                             (C != ret)
Note that the introduction of functions reduce and runenv allow a statement of adequacy using only universally quantified variables.

Faithfulness Lemma. Assume expression M is closed in environment E, and reduce(M, E) is not defined, then run(S, E, M :: C, D) is not defined.

The SECD Machine

Recall that the objects manipulated by the original SECD machine differ from those manipulated by the TR-SECD machine only in the fact that code may follow the call symbol.

The function step' is the transition function for the SECD machine. Notice the first four clauses are identical to the ones which define the TR-SECD transition function.

  step' : Dmp --> Dmp
  step'(L :: S, E, ret, (S', E', C', D')) = (L :: S', E', C', D')
  step'(S, E, N :: C, D) = (lookup(N, E) :: S, E, C, D)
  step'(S, E, K :: C, D) = ((K, nil) :: S, E, C, D)
  step'(S, E, \M :: C, D) = ((\M, E) :: S, E, C, D)
  step'((\M, E') :: L :: S, E, call :: C, D) 
    = (nil, L :: E', M' :: ret, (S, E, C D))
  step'((K, E') :: (K', E") :: S, E, call :: C, D)
    = ((delta(K, K'), nil) :: S, E, C, D)
  step'(S, E, (M M') :: C, D) = (S, E, M' :: M :: call :: C, D)
The statement of the correctness theorem, as well as the supporting lemmas remains unchanged with the exception of the Adequacy Lemma.

SECD Adequacy Lemma. Assume expression M is closed in environment E, and reduce(M, E) is defined. Then

  run'(S, E, M :: C, D) = run'(reduce(M, E) :: S, E, C, D)

The Boyer-Moore Theorem Prover

The logic of the Boyer-Moore Theorem Prover is a quantifier free, first order logic with recursive functions. The lack of quantifiers is handled by replacing each existentially quantified variable by a function that produces a witness.

All the functions used in the proofs are total, yet most of the functions presented in previous sections are partial. Many of the partial functions can be extended to become total functions by adding clauses which produce an error value distinct from the ordinary values.

Since zero is often a default value in NQTHM, it is usually selected as the error value in the encoding of the descriptions used in NQTHM. For example, the function lookup is made total by using zero as an error value. Variables are encoded as the positive integers, not natural numbers as one might expect.

There is no extension of the function eval that is total. Instead, the function evaluate is used.

  evaluate : Exp * Nat --> Val + {0}
  evaluate M 0 = 0
  evaluate(K, N + 1) = K
  evaluate(\M, N + 1) = \M
  evaluate((M M'), N + 1) = evaluate(subst(M", V, 1), N),
                  (evaluate(M, N) = \M" and evaluate(M', N) = V)
  evaluate((M M'), N + 1) = delta(K, K'),
                   (evaluate(M, N) = K and evaluate(M', N) = K')
  evaluate(M, N + 1) = 0,                            (otherwise)
The function eval is defined at M if evaluate(M, N) is a value for some natural number N. Furthermore, eval M = evaluate(M, N) whenever evaluate(M, N) is a value.

The statement of the correctness theorems include a implicit quantification over all delta functions that have certain properties. NQTHM-1992 has a CONSTRAIN event suited to this task.

Given the lack of support for partial functions in NQTHM-1992, one might think another theorem prover would be better for this job. The Boyer-Moore theorem prover's ability to find inductive proofs was exploited and some of the proofs about the nameless lambda calculus were taken verbatim from a proof of the Church-Rosser Theorem [Shankar94], which comes with the theorem prover. The author never gave other provers fair consideration, but would welcome comparisons based on this problem.

The Boyer-Moore Proofs

Each of the two proofs is divided into the same six topics. The first section defines nameless lambda terms, substitution, and evaluation. The second section defines reduction and concludes with a proof of the Substitution Lemma and the Reduction Lemma. The first two sections of each proof are identical.

The third section defines the SECD machine. The TR-SECD machine is defined by the transition function step, and the original SECD machine is defined by the transition function step'. The encoding of the function run maps a dump and a natural number to a dump. The natural number is called the step count.

  run' : Dmp * Nat --> Dmp
  run'(D, 0) = D
  run'(D, N + 1) = run'(step D, N) 
The fourth section defines a timed version of the function reduce. This function yields both a closure and the step count required to compute the closure. The TR-SECD machine version of timed reduction is slightly more complex than the original SECD machine version because the step count differs depending on whether a call is tail recursive.

The fifth section contains a proof of the TR-SECD or the SECD Adequacy Lemma. The sixth and final section contains a proof of the Faithfulness Lemma.

Proofs and Tail Recursion

The proofs reveal the intuition behind calling the TR-SECD machine tail recursive. Consider the adequacy proof for both the SECD and TR-SECD machines. For both machines, the ret rule is the only way to reduce the depth of the dump. While specifying the details of the inductive proof for the SECD machine, one finds that each use of a call rule is matched by a use of a ret rule.

In the TR-SECD machine, applications are treated differently depending on whether they are tail combinations. The following grammar partitions combinations into two categories. Tail combinations are marked with angle brackets while non-tail combinations retain the original syntax for combinations. The start symbol is T.

  T --> U | <W W>           TE    Tail expressions
  W --> U | (W W)           NTE   Non-tail expressions
  U --> K | \T | N          NA    Non-applications
For the TR-SECD machine, each use of a ret rule is matched by a call rule for a non-tail combination. A use of a call rule for a tail combination has no matching use of the ret rule. The implication is that calls of tail combinations do not cause a net growth of the depth of the dump and constitute the most compelling reason for believing the TR-SECD machine is tail recursive.

An equivalent method for identifying tail combinations is based on contexts. A combination context is an expression when its hole is replaced by a combination. The set of combination contexts is defined by:

  X --> [] | \X | (X M) | (M X)
The term that results from substituting combination (M M') into the hole in context X is X[(M M')].

A proper subset of combination contexts is the set of tail contexts. This set is defined by Y as follows:

  Y --> [] | Z
  Z --> \Y | (Z M) | (M Z)

Given a term M=X[(M' M")], (M' M") is defined to be a tail combination if X is a tail context, otherwise it is a non-tail combination.

A Comparison of the Proofs

The differences between the correctness proofs of the two machines can be put into three categories.
  1. Some of the function definitions must differ to account for the tail recursiveness of the TR-SECD machine. The function defining the transition function and the function defining timed reduction are examples.
  2. The hints used to tell the theorem prover how to perform complex inductions must differ because the ones for the TR-SECD machine require additional cases for tail recursive calls. An understanding of the TR-SECD machines makes the definition of the hints straightforward.
  3. Occasionally, functions with no counterpart are required for the TR-SECD correctness proof. The function runenv is an example. The required definition of each of these functions was obvious.
While the differences between the proofs is not large, the difference in the CPU time used while performing the proofs is large. The correctness proof for the TR-SECD machine requires roughly 50% more CPU time than that used by the proof for the SECD machine. The theorem prover easily handles the extra cases, but the cases take a substantial amount of additional time.

Readers with experience with the Boyer-Moore theorem prover are invited to read the file of events for the TR-SECD and SECD correctness proofs. The section on the Adequacy Lemma succinctly provides support to the thesis of this document.

References

[BoyerMoore88] Boyer, Robert S. and J Strother Moore, A Computational Logic Handbook, Academic Press, Inc, 1988.

[GuttmanEtAl95] Guttman, Joshua D., Vipin Swarup, and John D. Ramsdell, "The VLISP Verified Scheme System", in VLISP: A Verified Implementation of Scheme, J. D. Guttman and M. Wand Eds., pp. 33-110, Kluwer Academic Publishers, 1995.

[Hannan91] Hannan, John, "Making Abstract Machines Less Abstract", in Lecture Notes in Computer Science, J. Hughes Ed., Vol. 524, pp. 618-635, Springer-Verlag, 1991

[Plotkin75] Plotkin, Gordon D., "Call-By-Name, Call-By-Value, and the Lambda Calculus", Theoretical Computer Science, Vol 1, pp. 125-159, North-Holland, 1975.

[Shankar94] Shankar, Natarajan, Metamathematics, Machines, and Goedel's Proof, Cambridge University Press, 1994.

Disclaimer

This paper reflects the views of the author and makes no statement about the views of The MITRE Corporation.

Copyright

Copyright 1996 John D. Ramsdell. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, this copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of John D. Ramsdell.

Top