A Short Proof of the Lexical Addressing Algorithm

Mitchell Wand^{∗}

College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA

June 29, 1994

Abstract

The question of how to express binding relations, and in particular, of proving the correctness of lexical addressing techniques, has been considered primarily in the context of compiler correctness proofs. Here we consider the problem in isolation. We formulate the connections between three different treatments of variables in programming language semantics: the environment coding, the natural coding, and the lexical-address coding (sometimes called the Frege coding, the Church coding, and the deBruijn coding, respectively). By considering the problem in isolation, we obtain shorter and clearer proofs. The natural coding seems to occupy a central place, and the other codings are proved equivalent by reference to it.

1. Denotational definitions of programming languages generally treat lexically-scoped variables in the source language in one of three ways:

1. The most common approach is an environment model, in which the output of the semantics is a term which is passed an environment, that is, a map from identifiers to values. (e.g. [6, 10])

∗Work supported by the National Science Foundation under grant number CCR-8801591. This report should be cited as: Information Processing Letters, to appear.

2. A second approach is a natural model, in which the scoping relationships of the variables in the source language are modelled using lambda-binding in the target language. (e.g. [2, 9, 7]^{1})

3. Yet a third approach is a lexical-address model, in which the output of the semantics is a term which is passed a sequence of values. The translation uses a symbol table to decide which element of the sequence to retrieve. [5] This corresponds to the use of a lexical address or access link to locate a non-local variable [1, pp. 416–419].

The second approach is sometimes called “Church-style;” One might call the other two “Frege-style” and “deBruijn-style” codings, since the primary characteristic of the first is that it produces a combinator, of the second that it makes binding primitive, and of the third that it eliminates identifiers in favor of something like deBruijn indices.

While these techniques are all well-known, the relationship between them is not. In this note, we present a short proof formulating the relationships between these models. The proof itself is very simple; what is new here is a precise statement of the theorem.

The question of how to express binding relations, and in particular, of proving the correctness of lexical addressing techniques, has been considered primarily in the context of compiler correctness proofs. For example, in [11], we proved the correctness of a lexical addressing mechanism using a rather complex set of combinators. Clinger [4] proves a similar result for a Scheme compiler by considering the usual semantic environment as a composition of a compile-time environment and a run-time environment. More recently, we used arguments about data-structure representations to obtain the same result [12]. Here we consider the problem in isolation. This leads to shorter and clearer proofs.

2. We regard denotational semantics as a syntax-directed translation from a source language to a target language. The target language is typically some version of the lambda-calculus. We use ≡ to define syntactic transformations, and = to indicate provability in some lambda-theory.

For simplicity, we choose our source language to be a language similar to the language of lambda-terms:

1This is not to be confused with Kahn’s “natural semantics” [3], which addresses quite different issues.

⟨exp⟩::=⟨identifier⟩

proc ⟨identifier⟩ ⟨exp⟩ (⟨exp⟩ ⟨exp⟩)

We let I range over source language identifiers and M range over source language expressions. The free variables of any source expression M are defined in the usual way.

Our target language will be a lambda-calculus with the following properties:

• For each source language identifier I, there is a lambda-variable v_{I} and a constant c_{I}, and the maps I ↦ v_{I} and I ↦ c_{I} are injective.

• It includes a conditional, with a true value T, a false value F, and a test eq? such that eq? c_{I}c_{I} = T and eq? c_{I}c_{J} = F for all distinct I and J.

• It includes standard primitives for manipulating lists and integers.

The constants c_{I} correspond to the usual construction of including identifiers in the semantic domains. It does not matter whether the target language is typed or not, since all our terms will be well-typed in any reasonable type system. The combinators listed above may be coded in the target language using standard codings or adjoined as new constants; this choice may depend on whether the target language is typed.

In this paper we work in an untyped system. To help the reader, we adopt some conventions about λ-calculus variable names. We use variables like v (with subscripts, superscripts, primes, etc.) to range over values, like u to range over environments (functions from identifiers c_{I} to values), and like w to range over lists or sequences (usually of values).

3. The natural semantics is given as follows:

N [[I]]≡v_{I}
N [[proc I M]]≡λv_{I}.N [[M]]

N [[(M N)]]≡(N [[M]] N [[N]])

This translation is very simple: it merely translates source language identifiers into target-language identifiers. Note that the free variables of N [[M]] are the lambda variables of the form v_{I}, where I is free in M.

4. The environment semantics is well-known:

E[[I]]≡λu.(uc_{I})
E[[proc I M]]≡λu.λv.E[[M]](ext c_{I}vu)
E[[(M N)]]≡λu.((E[[M]] u) (E[[N]] u))

where

ext cvu = λq.(if (eq? q c) then v else (uq))

is the usual functional extension combinator. Note that E[[M]] is always a closed lambda-term.

5. The lexical semantics is somewhat more complicated. It uses the auxiliary notion of a symbol table, which in this example is just a sequence ξ of source language identifiers.

We first give the algorithm R[[−]]− for computing lexical addresses. It takes a source language identifier I, a symbol table ξ, and produces a term which is either of the form v_{I} (corresponding to a global reference) or first(rest^{(n)} w), where n corresponds to the position of I in ξ.

R[[I]][]≡v_{I}
R[[I]][I, ξ]≡first w
R[[I]][J, ξ]≡(R[[I]]ξ)[w := rest w]

Here [I, ξ] is a compile-time list-construction operator, and [w := rest w] is the usual substitution operator.

The behavior of R[[−]]− can be understood in terms of a canonical sequence of values. If ξ is a symbol table, then let V_{ξ} denote the term defined as follows:

V_{[]}≡nil
V_{[I,ξ]}≡cons v_{I}V_{ξ}

where nil and cons are the standard run-time list-structure combinators.

Lemma 1 (λw.R[[I]]ξ)V_{ξ} = v_{I}

Proof: By induction on ξ: If ξ = [], then the left-hand side is just (λw.v_{I})V_{ξ}, which reduces to v_{I}. If ξ is of the form [I, ξ′], then we have

(λw.R[[I]][I, ξ′])V_{[I,ξ′]}=(λw. first w)(cons v_{I}V_{ξ′})
=v_{I}

Last, for J ≠ I we have

(λw.R[[I]][J, ξ′])V_{[J,ξ′]}=(λw.(R[[I]]ξ′)[w := rest w])V_{[J,ξ′]}
=(λw.(λw.(R[[I]]ξ′))(rest w))(cons v_{J}V_{ξ′})
=(λw.R[[I]]ξ′)V_{ξ′}
=v_{I}

QED

6. The lexical-address semantics takes two arguments: a source term and a symbol table.

L[[I]]ξ≡λw.R[[I]]ξ
L[[proc I M]]ξ≡λw.λv.(L[[M]][I, ξ] (cons vw))
L[[(M N)]]ξ≡λw.((L[[M]]ξ w) (L[[N]]ξ w))

L[[M]]ξ produces a lambda term in which the only free variables are those free in M but not present in ξ, and in which no c_{I} appear. Indeed, if M and N are source expressions which are α-congruent in the usual sense, then L[[M]] ≡ L[[N]]. Note that the corresponding statement is false for E[[−]], since α-conversion does not affect the constants c_{I}.

Since L[[I]]ξ is always either of the form λw.v_{I} (corresponding to a global reference) or λw. first(rest^{(n)} w), we may replace the latter form by a combinator fetch n, corresponding to the usual deBruijn index or lexical address. These remarks justify the use of the phrase “the lexical-addressing algorithm” in the title. However, we shall not pursue this variant in this note.

7. We can illustrate these translations with an example. Let M be the source expression proc X (X Y). Then the translations are:

N [[M]] ≡ λv_{X}.(v_{X}v_{Y})

\begin{matrix}E[[M]] ≡ λu.λv.( & (λu.((λu.(uc_{X}))u)((λu.(uc_{Y}))u)) \\ (ext c_{X}vu)) \end{matrix}

L[[M]][] ≡ λwλv.((λw.((λw.(first w))w)((λw.v_{Y})w))
(cons vw))

Note that the environment coding is closed, and that the lexical-address coding contains no identifiers c_{I}. Notice how the reference to X is replaced by first w; in a pure lexical-address system this might be expressed by the concrete syntax fetch-lexical 1.

8. To relate these semantics, we need to have a common way to refer to the “current value” associated with the source language identifier I. We use the lambda variable v_{I} for this purpose. We may now state the main theorems.

Theorem 1 L[[M]]ξV_{ξ} = N [[M]].

Proof: By induction on M:

L[[I]]ξV_{ξ} = (λw.R[[I]]ξ)V_{ξ} = v_{I} = N [[I]]

L[[(MN)]]ξV_{ξ} = (L[[M]]V_{ξ} L[[N]]V_{ξ}) = (N [[M]] N [[N]]) = N [[(MN)]]

L[[proc I M]]ξV_{ξ}= λv.L[[M]][I, ξ](cons vV_{ξ})
= λv_{I}.L[[M]][I, ξ](cons v_{I}V_{ξ}) (by α-conversion)
= λv_{I}.L[[M]][I, ξ]V_{[I,ξ]}  (def. of V_{[I,ξ]})
= λv_{I}.N [[M]]
= N [[proc I M]]

Note that in the α-conversion step, we know the v_{I} does not occur free in L[[M]][I, ξ] since I appears in the symbol table [I, ξ].

Theorem 2 Let Γ_{M} be the collection of equations uc_{I} = v_{I}, for each free variable I of M. Then

Γ_{M} ⊢ E[[M]]u = N [[M]]

Proof: By induction on M. If M is an identifer I, then E[[I]]u = uc_{I} = v_{I} = N [[I]]. For an application, we have:

E[[(MN)]]u = (E[[M]]u E[[N]]u) = (N [[M]] N [[N]]) = N [[(MN)]]

For the abstraction case, we observe that if uc_{J} = v_{J} for each identifier J free in proc I M, then ext c_{I}v_{I}uc_{J} = v_{J} for each identifier I free in M (since the free variables of M are the free variables of the abstraction plus possibly I). This observation allows us to use the induction hypothesis in the following calculation:

N [[proc I M]] ≡ λv_{I}.N [[M]]
E[[proc I M]]u= λv.E[[M]](ext c_{I}vu)
= λv_{I}.E[[M]](ext c_{I}v_{I}u) (by α-conversion)
= λv_{I}.N [[M]]  (by IH)

The use of such a “natural deduction” style of lambda-calculus is presented in a more formal way in [13].

9. Our “natural” translation was purposely chosen to be trivial, so as to concentrate on the handling of variables, but similar results may be obtained for more substantial translations, such as continuation semantics. For the continuation semantics, the natural semantics is given in [8]. The three translations are:

N [[I]]≡λκ.(κ v_{I})
N [[proc I M]]≡λκ.(κ (λv_{I}.N [[M]]))
N [[(M N)]]≡λκ.(N [[M]] (λm.(N [[N]] (λn.((m n) κ)))))
E[[I]]≡λuκ.(κ (u c_{I}))
E[[proc I M]]≡λuκ.(κ (λv.(E[[M]] (ext c_{I}vu))))
E[[(M N)]]≡λuκ.((E[[M]] u) (λm.((E[[N]] u) (λn.((m n) κ)))))
L[[I]]ξ≡λwκ.(k R[[I]]ξ)
L[[proc I M]]ξ≡λwκ.(κ λv.(L[[M]][I, ξ] (cons vw)))
L[[(M N)]]ξ≡λwκ.((L[[M]] w) (λm.((L[[N]] w) (λn.((m n) κ)))))

The proof of the corresponding theorems follow, mutatis mutandum.

10. We have formulated the close connections between three different treatments of variables in programming language semantics: the environment coding, the natural coding, and the lexical-address coding. The natural coding seems to occupy a central place, and the other codings are proved equivalent by reference to it.

References

[1] Aho, A.V., Sethi, R., and Ullman, J.D., Compilers: Principles, Techniques, and Tools, Addison-Wesley, 1985.

[2] Church, A. “A formulation of the simple theory of types,” J. of Symbolic Logic 5 (1940), 56–68.

[3] Clément, D., Despeyroux, J., Despeyroux, T., and Kahn, G. “A Simple Applicative Language: Mini-ML” Proc. 1986 ACM Symp. on Lisp and Functional Programming, 13–27.

[4] Clinger, W. “The Scheme 311 Compiler: An Exercise in Denotational Semantics,” Conf. Rec. 1984 ACM Symposium on Lisp and Functional Programming (August, 1984), 356–364.

[5] deBruijn, N., “Lambda-Calculus Notation with Nameless Dummies, a tool for Automatic Formula Manipulation,” Indag. Mat. 34 (1972), 381–392.

[6] Milne, R. and Strachey C. A Theory of Programming Language Semantics, Chapman & Hall, London, and Wiley, New York, 1976.

[7] Pfenning, F., and Elliott, C., “Higher-Order Abstract Syntax,” Proc. SIGPLAN ’88 Conf. on Prog. Lang. Design and Implementation, (June, 1988), 199–208.

[8] Plotkin, G.D. “Call-by-Name, Call-by-Value and the λ-Calculus,” Theoret. Comp. Sci. 1 (1975) 125–159.

[9] Reynolds, J.C. “The Essence of Algol,” in Algorithmic Languages, (J. W. deBakker and J.C. van Vliet, eds.) North-Holland, Amsterdam, 1981, pp. 345–372.

[10] Stoy, J.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA., 1977.

[11] Wand, M. “Deriving Target Code as a Representation of Continuation Semantics” ACM Trans. on Prog. Lang. and Systems 4, 3 (July, 1982) 496–517.

[12] Wand, M. “From Interpreter to Compiler via Higher-Order Abstract Assembly Language,” (1989), submitted for publication.

[13] Wand, M., and Wang, Z.-Y., “Conditional Lambda-Theories and the Verification of Static Properties of Programs,” (with Z-Y Wang), Proc. 5th IEEE Symposium on Logic in Computer Science (1990), to appear.