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.
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 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 DumpsObjects manipulated by the SECD machine differ only in the fact that code sequences differ.
C --> ret | call :: C | M :: C Code Code SequencesFollowing 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))
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 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.
nil is a value environment
(V, E) :: E' is a value environment if
fv V <= length E
E and E' are value environments
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
eval(real(M, E)) = real(reduce(M, E))
reduce(M, E) is a value closure
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.
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)
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 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.
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-applicationsFor 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.
runenv is an example. The
required definition of each of these functions was obvious.
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.
[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.