Yale University

Department of Computer Science

A Syntactic Theory of Local Names

Martin Odersky

Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT 06520

Research Report YALEU/DCS/RR-965 May, 1993

A Syntactic Theory of Local Names

Martin Odersky

Yale University, Department of Computer Science, Box 2158 Yale Station, New Haven, CT 06520

Abstract

λν is an extension of the λ-calculus with a binding construct for local names. The extension is symmetric in identifiers and names, it has properties analogous to classical λ-calculus, and it preserves all observational equivalences of λ. The calculus is useful as a basis for modeling wide-spectrum languages that build on a functional core.

1 Introduction

Names are ubiquitous in programming. We find them as the substrate for mutable variables in imperative programming languages, for logic variables in Prolog, or for communication links in process algebras. Milner’s Turing Award Lecture [11] emphasizes naming as the key idea of the π-calculus [12, 13]. Even if names are in general introduced as the basis of more complex entieties, they can also be useful on their own. For instance, we often find statements like “let x be some fresh identifier” in definitions of denotational semantics or type checking algorithms.

Names are different from the identifiers serving as placeholders in functional languages: in contrast to a placeholder, nothing is ever substituted for a name. Conversely, equality tests are meaningful for names but not for placeholders. Names are also different from constant strings, at least if the programming language in question admits recursion. In this case, the same text string can denote different names in different recursive instances of a program construct.

This paper presents a syntactic theory that extends the λ-calculus with names. The basic idea is to generalize the notion of constant symbol already present in applied λ-calculus, by introducing an abstraction νn.M that binds a name n. Constant symbols in classical applied λ-calculus then become a special case of names that are not bound anywhere. The new calculus, λν, is pleasingly symmetric: Both placeholder-identifiers and names can be bound, and both are subject to α-renaming. The difference between the two lies in the operations that can be applied to them. One can substitute a term for an identifier, and one can compare two names for equality, but not vice versa.

By studying a theory that combines names with λabstractions we hope to gain some understanding of the issues involved in the design of wide-spectrum languages that build on a functional core. The main results of this work are:

• Names can be added to the λ calculus in a referentially transparent way. That is, full β remains a valid reduction rule.

• The resulting calculus, λν, is confluent and admits a standard evaluation function.

• The addition of names is fully compatible with functional programming. That is, every observational equivalence in λ carries over to λν. This has important practical consequences. We are guaranteed that every equational technique for verifying, transforming, or compiling functional programs is also applicable to programs with local names.

Many of the themes of this paper have also been addressed in the context of λ_{var} [18]. The main contribution of the present work over [18] is a considerably simpler theory that isolates the treatment of names from all other issues of imperative programming. This separation of concerns helped simplify the (rather hard) proofs on the observational equivalence theories of imperative languages. For this reason, we have based an extended version of the λ_{var}-report on λν [17].

Recent work on monads [14, 23, 24, 19, 8] shares with λν the motivation to extend functional programming languages to new application domains. Monads solve the problem of making sequencing explicit, which is needed if state is to be updated destructively. λν solves the orthogonal problem of expressing and encapsulating refer-

x ^{∈} Idents  λ-bound identifiers
n ^{∈} Names = Names^{c} ∪ Names^{ν}  names
n^{c}  ^{∈} Names^{c}  constants
n^{ν}  ^{∈} Names^{ν}  ν-bound local names
p ^{∈} P rimops  primitive operators
M ^{∈} Λν  terms
M ::= x | λx.M | M_{1} M_{2}
| n | νn.M | M_{1} == M_{2}
| (M_{1}, M_{2}) | p M

Figure 1: Syntax of λν

β  (λx.M) N  → [N/x] M
δ  p V  → δ(p, V)
eq  n == n  → true
n == m  → false  (n ≠ m)
ν_{λ}  νn.λx.M  → λx.νn.M
ν_{p}  νn.(M_{1}, M_{2}) → (νn.M_{1}, νn.M_{2})
ν_{n}  νn.m  → m  (n ≠ m)

Figure 2: Reduction rules for λν

ences. The two techniques complement each other well, as is shown in 2.

Several other calculi use a notion similar to names for expressing mutable variables in imperative languages. The motivation for these calculi comes partly from the desire to explain the semantics of existing languages (e.g. [5, 9] for Scheme or ML, [20, 10, 25] for Algol), and partly from the desire to extend functional programming with full imperative state [22, 18]. The calculi differ in the assumed order of evaluation, in the kinds of side effects that are admitted, in whether state is implicit or explicit, and in many other properties. But they all have in common an alphabet of α-renamable names that identify mutable variables. By factoring out this common concept, and studying it independently and irrespective of the particular additional semantics attached to names, we hope to find a common basis for the various approaches that describe state.

A theory with a motivation close to λν has also been developed independently by Pitts and Stark [15]. Even though the term languages of both theories are strikingly similar, their laws are fundamentally different. The nu-calculus of Pitts and Stark is intended to model names as they are used for ML-style references. It is not intended to be a referentially transparent extension of a functional core. Hence, our result of conservative extension does not apply to the nu-calculus.

The rest of this paper is structured as follows. Section 2 describes term syntax and reduction rules of λν, a calculus of functions and names. Section 3 presents two applications of local names, a type reconstruction algorithm and an implementation of state. Section 4 shows properties of λν, in particular its confluence and its standard evaluation function. Sections 5 and 6 discuss the observational equivalence theory of λν and prove that it is a conservative extension of the corresponding theory of λ. Section 7 concludes.

2 The λν calculus

Terms. The term-forming productions of λν are given in Figure 1. The three productions on the first line are those of classical, pure λ-calculus. The three productions on the next line are particular to λν. Besides λ-bound identifiers there is a new, countably infinite alphabet of names. Names fall into two classes, global and local. A global name n^{c} is an atomic constant. We assume that there are two such constants denoting the Boolean values true and false. A local name n^{ν} is a name that is bound in a name abstraction νn^{ν}.M. In contrast to the case of λ-bound identifiers, nothing is ever substituted for a name. Rather, names can be tested for equality, as in n_{1} == n_{2}. Both constants and local names can be operands of (==).

We study here an applied variant of λν. Accordingly, we have on the last line productions for pairs (M_{1}, M_{2}) and applied primitive operators p M. Primitive operators are always unary, but operators of greater arity can be obtained by currying. We assume that at least the following operators are defined:

\begin{aligned}pair? (M_{1}, M_{2}) & = & true \\ pair? & = & false \\ name? n & = & true \\ name? & = & false \\ fst (M_{1}, M_{2}) & = & M_{1} \\ snd (M_{1}, M_{2}) & = & M_{2} \end{aligned}

Notational conventions. We use BV (M) and F V (M) to denote the bound and free identifiers in a term M, respectively. Analogously, BN(M) and F N(M) denote bound and free local names in a term M. A term is closed if F V (M) = F N(M) = ∅. Closed terms are also called programs. Note that programs do not contain free local names n^{ν}, but they may contain constants.

We use M ≡ N for syntactic equality of terms (modulo α-renaming) and reserve M = N for convertibility. If R is a notion of reduction, we use ⟶_{R} to express that M reduces in one R reduction step to N, and M ⟶_{R} → N to express that M reduces in zero or more R-steps to N. We also use M ⟶^{Δ} N to express that M reduces to N by contracting redex Δ in M.

The syntactic category of values V comprises constants, names, pairs, and λ abstractions. An observable value (or answer) A is an element of some nonempty subset of the alphabet of constants.

\begin{aligned}V & ::= & c | n | (M_{1}, M_{2}) | λx.M \\ A & ∈ & Answers ⊆ Names^{c} \end{aligned}

A context C[ ] is a term with a single hole [ ] in it. C[M] denotes the term that results from replacing the hole in C[ ] with M.

Following Barendregt [1], we take terms that differ only in the representatives of bound identifiers and names to be equal. That is, all terms we write are representatives of equivalence classes of α-convertible terms. To avoid name capture problems in substitutions we restrict ourselves to representatives in which bound and free identifiers are always distinct, and we employ the same conventions for names.

We let letters L, M, N range over terms, and V and W range over values. We let letters m, n range over names. We use a ν-superscript with these to indicate a local name, and a c superscript to indicate a constant. Alternatively, we also use the letter c for a constant.

Reduction Rules. Figure 2 gives the reduction rules of λν. They define a reduction relation between terms in the usual way: we take (→) to be the smallest relation on Λν ×Λν that contains the rules in Figure 2 and that, for any context C, is closed under the implication

M → N ⇒ C[M] → C[N].

Equality (=) is the smallest equivalence relation that contains reduction (→).

Rule β is the usual reduction rule of pure λ-calculus. Rule δ expresses rewriting of applied primitive operators. To abstract from particular primitive operators and their rewrite rules, we only require the existence of a partial function δ from primitive operators p and values V to terms. δ can be arbitrary, as long as its result does not depend on the body of a an argument function, or the value of a local argument name. That is, we postulate that for every primitive operator p there exist closed terms N_{c}^{p} (c ^{∈} Names^{c}). N_{ν}^{p}, N_{λ}^{p} and N_{(·,·)}^{p} such that for all values V for which δ(p, V) is defined:

δ(p, V) = \{ \begin{matrix}N_{c}^{p} & if V ≡ c \\ N_{ν}^{p} & if V is a local name \\ N_{λ}^{p} & if V is a λ-abstraction \\ N_{(·,·)}^{p} M_{1} M_{2} & if V ≡ (M_{1}, M_{2}) \end{matrix}

Note that all primitive operators are strict, since δ requires its arguments to be values.

The remaining rules of Figure 2 are particular to λν. Rule eq defines (==) to be syntactic identity. Rule ν_{λ} says that ν- and λ-prefixes commute. Rule ν_{p} says that ν-prefixes distribute through pairs. Finally, rule ν_{n} says that a ν-prefixes is absorbed by any name that differs from the name bound in the prefix. Taken together, these rules have the effect of pushing names into a term, thus exposing the term’s outer structure and allowing it to interact with its environment.

An important consequence of these rules is that the term νn.n cannot be reduced further, but is not a value either, and hence cannot be decomposed or compared. In other words, the identity of a name is known only within its (dynamic) scope. This does not restrict expressiveness since it is always possible to extend the scope of a variable by passing the “rest” of the computation as a continuation (see the examples in the next section),

A Note on Church-Encoding Pairs. We have chosen to make the pairing function (·, ·) a primitive term constructor with associated primitive projections fst and snd. What would have happened if we had encoded pairs as functions instead? The Church-encoding of pairs defines a pairing function

λx.λy.λf.f x y

and associated projections

\begin{aligned}π_{1} & = & λp.p (λx.λy.x) \\ π_{2} & = & λp.p (λx.λy.y). \end{aligned}

The crucial question is what happens to ν_{p}, or, rather its Church-encoded form

νn.P M N = P (νn.M) (νn.N).  (1)

It is easily verified that this not an equality derivable from the other reductions. On the other hand, if we apply a projection π_{i} to each side of (1) then we do get an equality that is derivable from β and ν_{λ}. This is shown by some straightforward computation:

π_{1} (νn.P M N)

= (by definition of π_{1}, P)

(λp.p (λx.λy.x)) (νn.λf.f M N)

= (by β)

(νn.λf.f M N) (λx.λy.x)

= (by ν_{λ})

(λf.νn.f M N) (λx.λy.x)

= (by β)

νn.M

= (by definition of π_{1}, P and β)

π_{1} (P (νn.M) (νn.N))

The case where the projection is π_{2} is completely analogous. In summary, the ν_{p} rule for Church-encoded pairs is subsumed by ν_{λ} and β, as long as pairs are used as intended (i.e. only projections are applied to them).

3 Applications

To demonstrate how the new constructs in λν could be used in a functional programming language, we present two example applications: a type reconstruction algorithm, and an implementation of state-transformers. We use a program much like Haskell, writing \x -> M for λx.M and (.) for function composition. We extend Haskell by a new term construct new n ->M, the ASCII form of νn.M. Types are presented only informally; they are in general modeled after the type systems of ML and Haskell, with some polymorphic extensions in the second example. A name has type Name a, for some type a. The typing rule rule for ν is:

\frac{Γ.n : Name τ′ ⊢ M : τ}{Γ ⊢ νn.M : τ}

Example 3.1 (Type Reconstruction) Type reconstruction algorithms for polymorphically typed languages need to define fresh identifiers for type variables “on the fly”. To this purpose, a name supply is usually passed along as an additional argument to the type reconstruction function. Typically, names are represented as integers, and the name supply indicates the next unused integer. As an alternative, we present here a type reconstruction algorithm for the simply typed λ-calculus that replaces the name supply by bound λν names.

The code for the type checker is given in Figure 3. Types are either variables TV n or function types t1 :-> t2. The identifying part n of a type variable TV n is a name (of type TID, which is a synonym for Name ()). The main function tp constructs a proof for a goal e ⊢ a : t, where e is a typing environment, a is a term, and t is a type. e, a and t are the first three arguments of tp. The function returns a substitution transformer (of type SubstTran), which is a mapping that takes a continuation and a substitution and yields either failure or succeeds with some result type that is determined by the continuation. Success and failure are represented as the two alternatives of type E a. Fresh names are created in the clauses of tp that have to do with function abstraction and application. The unification function unify takes as arguments two types, a continuation, and a substitution. If the argument types are unifiable, it augments the argument substitution with their most general unifier, passing the result to its continuation.

  data Id          =  String                             unify            :: Type -> Type -> SubstTran a
  data Term        =  ID Id | AP Term Term |
                      LAM Id Term                        unify t1 t2 k s  =  case mgu (s t1) (s t2) of
  data TID         =  Name ()                                                  Suc s' -> k (s . s')
  data Type        =  TV TID | Type :-> Type                                   Err    -> Err
  data E a         =  Suc a | Err
                                                         tp               :: TypeEnv -> Term -> Type
  type TypeEnv     =  Id -> Type                                             -> SubstTran a
  type Subst       =  Type -> Type
  type SubstTran a =  (Subst -> E a) -> Subst -> E a     tp e (ID n) t    =  unify (e n) t
                                                         tp e (AP a b) t  =  new n ->
  upd              :: (a -> b) -> a -> b -> (a -> b)                           tp e a (TV n :-> t) .
  upd f x a y      =  if y == x then a else f y                                tp e b (TV n)
                                                         tp e (LAM x a) t =  new n -> new m ->
  mgu              :: Type -> Type -> E Subst                                  unify (TV n :-> TV m) t .
  -- most general unifier; definition is left out                              tp (upd e x (TV n)) a (TV m)

Figure 3: Type reconstruction algorithm for the simply typed λ-calculus.

If the arguments are not unifiable, type reconstruction fails.

Example 3.2 (State Transformers) State-transformers are a way to write imperative programs in a functional programming language, by treating an imperative statement as a function from states to states. They have received much attention recently. State-transformers can be classified according to whether they are global or local, and according to whether state is fixed or dynamic.

[23] and [24] describe local state-transformers that can be embedded in other terms and that operate on a fixed state data structure. By contrast, [19] describes global state-transformers that act as the main program and thus cannot be embedded in another term. State in [19] is dynamic, i.e. it consists of a heap with dynamically created references.

Figure 4 shows an implementation of local statetransformers with dynamic state. This is to my knowledge the first fully formal treatment of this class of statetransformers, even if [6] and [8] contain similar informal proposals.

State is represented as a polymorphic function from names of type Name a to terms of type a. Its type is:

     all a.Name a -> a

A state-transformer of type ST a is a function that takes a continuation and a state as arguments, and returns the result of the continuation. Its type is:

                                                             all b.(a -> State -> b) -> State -> b

Note that the polymorphic function types of state and state transformers exceed the capabilities of first-order type systems such as Haskell’s or ML’s. However, an efficient implementation of state transformers would treat type ST a as an abstract data type and would hide type State altogether, to guarantee that state is singlethreaded. Such an implementation could do with just let-polymorphism in the style of ML.

State transformers form a Kleisli monad, with return as the monad unit, and with infix (>>=) as the “bind” operator. If we leave out the redundant state parameter s this is just the standard continuation monad. The result type of a continution is an observer^{1} of type State -> a.

Function begin, of type ST a -> a, allows one to get out of the ST monad. begin runs its state transformer argument in an empty initial state and with the identity function as continuation.

The remaining operations access state. newref returns a freshly allocated reference as result. Its implementation is based on ν-abstraction. (n := a) updates the state, returning the unit value as result, while deref n returns the current value of the state at reference n.

This concludes our implementation of state in λν. It is

1in the sense of [22].

  type State  =  all a. Name a -> a
  type ST a   =  all b. (a -> State -> b) -> State -> b
-- Monadic Operators:                                     -- State-Based Operators:
  return          :: a -> ST a                              newref          :: ST (Name a)
  (>>=)           :: ST a -> (a -> ST b) -> ST b            (:=)            :: Name a -> a -> ST ()
  begin           :: ST a -> a                              deref           :: Name a -> ST a
  return a   k s  =  k a s                                  newref     k s  =  new n -> k n s
  (p >>= q)  k s  =  p (\x -> q x k) s                      (n := a)   k s  =  k () (upd s n a)
                                                            deref n    k s  =  k (s n) s
  begin p         =  p (\x -> x) bottom
  bottom          =  bottom                                 upd s n x m     =  if n == m then x else s m

Figure 4: State Transformers

perhaps surprising how simple such an implementation can be, once the problem of expressing local names is taken care of. However, one could argue that we have oversimplified, in that the implementation of Figure 4 does not really describe state! Indeed, there are two trouble-spots.

The first problem is caused by the fact that the state argument s is not linear in the definition of deref. Therefore, access to state is only single-threaded if the application s n in the body of deref gets resolved before control is passed to the continuation. But nothing in the implementation forces this evaluation order! One could solve the problem by making continuations strict in their first argument. However, this forces s n to be reduced to a value, which is needlessly drastic. To ensure single-threadedness, it is enough to just perform the function application without further evaluation.

Another problem concerns the meaning of readers and assignments that involve names from some outer block. In the implementation of Figure 4, such accesses are not errors. Instead, the read or write is performed on a locally allocated cell that is named by the non-local name. Therefore, the same name might identify several locations in different states. This approach, which is similar to the semantics of state in [21], is perfectly acceptable from a theoretical standpoint. But it raises some implementation problems, since it prevents the identification of names with machine addresses.

Both problems are solved by a slightly more refined implementation, which marks stored terms with a data constructor. We modify the type of state as follows:

                                                            type State  =  all a. Name a -> D a
                                                            data D a    =  D a

The implementation of the state-based operators then becomes:

                                                            newref   k s  =  new n ->
                                                                               k n (upd s n (D bottom))
                                                            (n := a) k s  =  case s n of
                                                                               D b -> k () (upd s n (D a))
                                                            deref n  k s  =  case s n of
                                                                               D a -> k a s

In the new implementation, the case construct in the body of deref forces s n to be evaluated before control is passed to the case-branch (we take D-patterns to be refutable). This takes care of the first problem. Moreover, both readers and writers require that an entry for the accessed reference exists in the local state, and newref allocates such an entry for a freshly created reference. This takes care of the second problem.

The contribution of λν to this implementation is rather subtle. It consists of the ν-abstraction in the code of newref and the equality test in function upd. Nevertheless, the presence of local names is important for modeling dynamic local state in a simple way. To see this, let’s try to model local state without local names, by representing heaps as arrays with references as indices, say. Now, any implementation of local state has to distinguish between variables that are defined in different begin-blocks. This is necessary to guard against access to non-local variables and against export of local variables out of their block, both referentially opaque operations. A straightforward scheme to distinguish between variables defined in different blocks would pass a name supply to each block, such that the block, and all the variables defined in it, can be tagged with a unique identifier. The problem with this scheme is that it has a “poisoning” effect on the environment that surrounds a block. Each function now has to pass along namesupply arguments even if the function itself does not contain begin-blocks as subterms. It is not clear what is be gained by this method over a program that contains a single, global state, and hence is imperative all the way to the top. Of course, we could have also used λν-names for the task of marking blocks uniquely. Such a scheme was described by Launchbury [8]. It might lead to more efficient implementations than the simpler method of equating references with names that we have used here.

Interestingly, it is possible in principle to model local state without local names. As part of the proof of observational extension it will be shown in Section 6 that there is another technique, somewhat similar to a de Bruijn numbering [3], that allows names to be distinguished without needing name supplies to be passed. However, due to its complexity the numbering method is hardly practical as a programming technique.

4 Fundamental Theorems

This section details the fundamental laws of λν: reduction is confluent and there is a standard evaluation function. The treatment largely follows [1], and we assume that the reader is familiar with the some of the more fundamental definitions and theorems given there.

4.1 Confluence

We show in this section analogues for λν of the Finite Developments and Church-Rosser theorems for the λcalculus.

Definition 4.1 Let λ_{0}ν be the extension of λν with labeled redexes (λ_{0}x.M) N and p_{0} V and with labeled reduction rules

\begin{aligned}β_{0} : & (λ_{0}x.M) N & → & [N/x] M \\ δ_{0} : & p_{0} V & → & δ(p, V). \end{aligned}

Let ⟶_{0} be the reduction relation generated by β_{0}, δ_{0}, eq, ν_{λ}, ν_{p}, ν_{n}.

Theorem 4.2 (Finite Developments) ⟶_{0} is strongly normalizing.

Proof: The proof is similar to the proof of finite developments in the pure λ calculus ([1],CH.11,§2). Let λ′ν be the extension of λ_{0} with weighted identifiers x^{k} and weighted primitive function application p_{0}^{k} M (k > 0). We define a norm ∥ · ∥ on λ′ν terms by

\begin{aligned}∥x∥ & = & 1 \\ ∥x^{k}∥ & = & k \\ ∥λx.M∥ & = & 1 + ∥M∥ \\ ∥λ_{0}x.M∥ & = & 1 + ∥M∥ \\ ∥M_{1} M_{2}∥ & = & ∥M_{1}∥ + ∥M_{2}∥ \\ ∥n∥ & = & 1 \\ ∥νn.M∥ & = & 2 × ∥M∥ \\ ∥M_{1} == M_{2}∥ & = & ∥M_{1}∥ + ∥M_{2}∥ \\ ∥(M_{1}, M_{2})∥ & = & 1 + ∥M_{1}∥ + ∥M_{2}∥ \\ ∥p M∥ & = & 1 + ∥M∥ \\ ∥p_{0}^{k} M∥ & = & k + ∥M∥ \end{aligned}

A term M ^{∈} Λ′ν has a decreasing weighting if for every occurrence of a labeled term (λ_{0}x.M_{1}) M_{2} in M, every occurrence of x in M_{1} has a weight k ≥ ∥M_{2}∥, and, for every occurrence of a labeled term p_{0}^{k} V in M, n+∥V ∥ > ∥δ(p, V)∥.

By a proof similar to the one in [1], Lemma 11.2.18(ii) one shows that, if M has a decreasing weighting, and M ⟶_{0} N, then N has a decreasing weighting. Furthermore, an easy case analysis on the notion of reduction ⟶_{0} in λ′ν shows that for all terms M, N ^{∈} Λ′ν,

M ⟶_{0} N ⇒ ∥M∥ > ∥N∥.

Since weightings are well-founded, ⟶_{0} is strongly normalizing on all terms in Λ′ν that have a decreasing weighting.

Now every term M in Λ_{0} can be transformed to a term with a decreasing weighting in Λ′ν, by giving appropriate weights to all labeled occurrences of identifiers and primitive functions. As a consequence, ⟶_{0} is strongly normalizing on λ_{0}ν.

Theorem 4.3 The notion of reduction in λν is Church-Rosser: if M → → M_{1} and M → → M_{2} then there is a term M_{3} s.t. M_{1} → → M_{3} and M_{2} → → M_{3}.

Proof: Using a case analysis on reduction rules, coupled with a case analysis on the relative position of redexes, one shows that the notion of reduction δν is weakly Church-Rosser and commutes with β. Then by Theorem 4.2 and Newman’s lemma ([1],CH.3,§1) δν is Church-Rosser, and together with the lemma of Hindley/Rosen ([1],CH.3,§3) this implies the proposition.

4.2 Evaluation

As programmers, we are interested not only in proving equality of terms, but also in evaluating them, i.e. reducing them to an answer. We now define a computable evaluation function that maps a term to an answer A iff λν ⊢ M = A. Following Felleisen [2], the evaluation function is defined by means of a context machine. At every step, the machine separates its argument term deterministically into an evaluation context and a redex and then performs a reduction on the redex. Evaluation stops once the argument is an answer. Evaluation contexts for λν are defined as follows:

E ::= [ ] | E M | p E | νn.E  (2)

The first three clauses generate evaluation contexts for the applied call-by-name λ-calculus, whereas the last clause is particular to λν.

Definition. The deterministic reduction relation ⟶_{d} on terms in Λν is the smallest relation that satisfies

M ⟶^{M} N ⇒ E[M] ⟶_{d} E[N].

A simple inspection of the productions for E establishes that ⟶_{d} is indeed deterministic:

Proposition 4.4 For any redexes Δ_{1}, Δ_{2} and evaluation contexts E_{1}, E_{2},

E_{1}[Δ_{1}] ≡ E_{2}[Δ_{2}] ⇒ E_{1} ≡ E_{2} ∧ Δ_{1} ≡ Δ_{2}.

A redex Δ is a head redex of a term M if M ≡ E[Δ], for some evaluation context E. A redex that is not head redex is called an internal redex. Reduction of internal redexes keeps head and internal redexes separate, in the sense of

Lemma 4.5 Let M be a program s.t. M ⟶^{Δ} N where Δ is an internal redex of M. Then,

(i) If N has a head redex then so has M, (ii) the residual of M’s head redex is head redex in N, (iii) the residuals of every internal redex in M are internal redexes in N.

Proof: Let Δ be an internal redex in M. By the definition of evaluation contexts (2), there is an evaluation context E, context C, term M′ such that

M ≡ E[M′ (C[Δ])].

(i) Let R be the reduct of Δ. Then

N ≡ E[M′ (C[R])].

Assume that N has a head-redex Δ_{h}. Then because of the form of evaluation contexts (2), either Δ_{h} is contained in M′, or Δ_{h} ≡ M′ (C[R]). In both cases, Δ_{h} is the residual of a head redex in M.

The proofs of parts (ii) and (iii) are similar.

Theorem 4.6 (Correspondence) For every program M ^{∈} Λν and every answer A,

M → → A ⇔ M ⟶_{d} → A.

Proof: Direction “⇐” follows immediately. To prove “⇒”, assume that M ⟶_{d} → A. One shows first as an intermediate result that, whenever M → → A, there is a term N s.t. M ⟶_{d} → N ⟶_{i} → A, where the reduction sequence N ⟶_{i} → A from N to A consists of only internal reductions. This result corresponds to the main lemma for the Curry/Feys standardization theorem ([1],CH.11,§4) and has exactly the same proof. That proof uses only the theorem of finite developments (Theorem 4.2 for λν) and a lemma equivalent to Lemma 4.5. The proposition then follows from the observation that no internal λν reduction ends in an answer, hence we must have N ≡ A.

5 Observational Equivalence

In this section we study observational equivalence, the most comprehensive notion of equivalence between program fragments. Intuitively, two terms are observationally equivalent if they cannot be distinguished by some experiment. Experiments wrap a term in some arbitrary context that binds all free identifiers and local names in a term. The only observation allowed in an experiment is whether the resulting program reduces to an answer, and, if so, to which one. We define observational equivalence for arbitrary extensions of applied λ calculus. In the following, let T be an equational theory that extends λ and has term language T erms(T ) and a set of answers Ans(T ) ⊂ Names^{c}(T ). We assume that Names^{c}(T )\Ans(T ) is infinite.

Definition 5.1 Two terms M, N ^{∈} T erms(T ) are observationally equivalent in T , written T ⊧ M ≅ N, iff for all contexts C in T erms(T ) such that C[M] and C[N] are closed, and for all answers A ^{∈} Ans(T ),

T ⊢ C[M] = A ⇔ T ⊢ C[N] = A.

Lemma 5.2 For any terms M, N ^{∈} T erms(T ),

T ⊧ M ≅ N ⇔ ∀C.T ⊧ C[M] ≅ C[N].

Proof: “⇒”: Assume M ≅ N, let A be an answer, and let C be a context. Let C′ be a context such that C′[C[M]] and C′[C[N]] are closed. Then M ≅ N implies

C′[C[M]] = A ⇔ C′[C[N]] = A.

Since C’ was arbitrary, C[M] ≅ C[N]. “⇐”: Pick C = [ ].

Lemma 5.3 For any two terms M, N ^{∈} T erms(T ),

T ⊧ λx.M ≅ λx.N ⇔ T ⊧ M ≅ N

Proof: “⇒”: Assume λx.M ≅ λx.N, let A be an answer, and let C be a context such that C[M] and C[N] are closed. Then

C[M] = A

⇔ (by β-conversion)

C[(λy.[y/x] M) x] = A

⇔ (premise)

C[(λy.[y/x] N) x] = A

⇔ (by β-conversion)

C[N] = A

Hence, M ≅ N.

“⇐” is a consequence of Lemma 5.2.

Proving Observational Equivalences

The definition of (≅) gives us only a very cumbersome way to reason about observational equivalence, since it relies on a universal quantification over all contexts. We now summarize two theorems that are useful for proving observational equivalences. The proof method is similar to the critical pair technique used in Knuth-Bendix completion [7]. For a more complete treatment, see [16].

The theorems require a more formal treatment of the rules for reduction and observational equivalence than the exposition in previous sections. The following is an excerpt of the relevant definitions of [16].

Both reduction rules and rules for observational equivalences are defined as relations between meta-terms. A meta-term is formed from the inductive definition of terms, meta-variables a, b, and a substitution construct [M/x]N, where M and N are meta-terms. Hence, metaterms include terms as a subset. A valuation is a mapping from meta-variables to meta-terms that is extended homomorphically to a mapping from meta-terms to meta-terms. A notion of reduction is expressed by a set of reduction rules

R = {L_{i} → R_{i}}_{i^{∈}I}

where I is an arbitrary (possibly infinite) index set, and all L_{i} and R_{i} are meta-terms. The reduction relation generated by R is the smallest relation between metaterms that contains all valuation instances of rules in R and that is closed under context formation. Likewise, we can define a notion of similarity ∼ by a symmetric set of rules

S = {S_{j} → T_{j}}_{j^{∈}J}

where again J is arbitrary and S_{j}, T_{j} are meta-terms. ∼ is then the smallest relation between meta-terms that contains all valuation instances of rules in S and that is closed under context formation.

Two meta-terms L_{1}, L_{2} overlap at a valuation ρ if there is a non-variable sub(meta-)term M of L_{i} such that ρM ≡ ρL_{j} (i, j ^{∈} {0, 1} i ≠ j).

Two sub(meta-)terms M_{1}, M_{2} of a common meta-term interfere wrt a set of meta-terms L if there is a valuation ρ and there are meta-terms L_{1}, L_{2} ^{∈} L such that M_{1} ≡ ρL_{1}, M_{2} ≡ ρL_{2} and L_{1} and L_{2} overlap at ρ. We sometimes do not mention the set L explicitly. In particular, when we say that a redex Δ and a pattern instance of a similarity P interfere, we mean that they interfere wrt the set of left-hand sides of reduction rules and similarities

{L_{i} | i ^{∈} I} ∪ {S_{j} | j ^{∈} J}.

Given similarity ∼, we define parallel similarity as follows: M∼_{1}N if M and N differ in sub(meta-)terms M_{1}, N_{1}, ...., M_{n}, N_{n}, M_{i} ∼ N_{i} for each i ^{∈} {1, ...n}, and the M_{i}, as well as the N_{i}, are pairwise non-interfering. The set {M_{1}, ..., M_{n}} sometimes is written as a superscript, as in

M ∼_{1}^{{M_{1},...,M_{n}}} N.

Two meta-terms M, N form a critical pair if there exists a root meta-term R, a redex Δ, and pattern instances of similarities P_{1}, ..., P_{n} (n ≥ 1), such that

R ⟶^{Δ} N  and  R ∼_{1}^{{P_{1},...,P_{n}}} M

and Δ interferes with each P_{i} (i = 1, .., n). The pair is deterministically critical if Δ is head redex in R. We use the notation

M∼_{1}R → N

for a critical pair M, N with root R.

A given set of equations can be shown to be an observational equivalence by formulating it as a similarity relation and showing that it satisfies the following two properties.

∼ preserves answers if M ∼ A implies M = A.

∼ is locally stable if, for all critical pairs N∼_{1}M → M′ there is a meta-term N′ such that the following diagram commutes.

M  M′ N  N′ . . . . . . . . . . . . . ≅ ∼_{1}  ^{.............}∼_{1}

Theorem 5.4 Let ≈ be the equivalence closure of ∼. If ∼ is locally stable and preserves answers then ≈ ⊆ ≅.

We also need a second, stronger version of Theorem 5.4 that applies if the calculus has a notion of evaluation contexts that satisfies the following two criteria.

Evaluation contexts are downward closed if, whenever C_{1}[C_{2}] is an evaluation context, then so is C_{2}. ∼ interferes with evaluation contexts, if some left-hand-side S_{j} of S overlaps with some sub(meta-)term of an inductive production for evaluation contexts.

If these criteria are fulfilled, a weaker notion of deterministic local stability is sufficient to guarantee that a similarity is an observational equivalence:

∼ is deterministically locally stable if for all deterministically critical pairs N∼_{1}M → M′ there are meta-terms M′′, N′ such that the following diagram commutes.

[figure: M; M′; M′′; N; N′; d; ^{. . . . . . . .}; d; . . . . . . . . . . . . . . . . . . . . .; ≅; ∼_{1}; ^{.............}; ∼_{1}]

Theorem 5.5 Let ≈ be the equivalence closure of ∼. If

• T has downward closed evaluation contexts,

• ∼ preserves evaluation contexts,

• ∼ is deterministically locally stable, and

• ∼ is answer-preserving

then ≈ ⊆ ≅.

A straightforward analysis shows that λν’s evaluation contexts are downward closed, Furthermore, since the productions for evaluation contexts contain only metavariables as sub(meta-)terms^{2}, no similarity relation can interfere with evaluation contexts. Hence, to prove that a similarity is an observational equivalence in λν it suffices to show that it satisfies the last two conditions of Theorem 5.5.

Theorem 5.5 will be used extensively in the next section. We use it here in the proof of

Proposition 5.6 The following are observational equivalences in λν:

νn.νm.M ≅ νm.νn.M  (n ≠ m)  (3)
νn.M ≅ M  (n ^{∉} F N(M)) (4)

Proof: We prove (3) here; the proof of (4) is given in [16].

Let a be a meta-variable and let

S = {νn.νm.a ≅ νn.νm.a | n, m ^{∈} Names^{ν}, n ≠ m}.

Let ∼ be the compatible valuation closure of S. Since no side of S matches an answer, ∼ vacuously preserves answers. We now show that ∼ is also deterministically locally stable.

Matching (3) against λν’s reduction rules establishes that a redex interferes with a pattern instance of S only if the redex is of the form νm.M, for some meta-term M, and the pattern instance is νn.νm.M, for n ≠ m. If νm.M is a redex, then M must be a λ-abstraction, a pair, or a name.

If M is a λ-abstraction, say λx.N, then the following diagram commutes:

[figure: νn.νm.λx.M; νn.λx.νm.M; λx.νn.νm.M; νm.νn.λx.M; λx.νm.νn.M; d; d; ∼; ∼]

If M is a name, say n′, then m ≠ n′ (otherwise there would be no redex), and the following diagram commutes.

2Note that a meta-term may not contain a variable ranging over contexts.

νn.νm.n′  νn.n′ νm.νn.n′  νn.n′ ≅  ≡ ∼

The bottom edge of this diagram is justified by (4), since m ≠ n′. The remaining case where M is a pair is omitted (it is found in [16]).

This shows that ∼ is deterministically locally stable. With Theorem 5.5, (3) follows.

6 Observational Extension

Definition 6.1 T is an observational extension of T_{0} if T erms(T ) ⊇ T erms(T_{0}) and, for all M ^{∈} T erms(T_{0}),

T_{0} ⊧ M ≅ N ⇒ T ⊧ M ≅ N.

The extension is conservative if the implication can be strengthened to an equivalence.

The main result of this section states that λν is an observational extension of λ. The proof relies on the construction of a syntactic embedding from λν to λ. Syntactic embeddings are certain functions (defined below) that map terms of one language to terms of a sublanguage.

6.1 Syntactic Embeddings

Definition 6.2 Given an inductively defined term language T erms, an extended term is formed from the inductive definitions of T erms and [ ]. (Hence, both terms and contexts are extended terms).

Definition 6.3 A term M is λ-closed iff F V (M) = ∅. M may contain free occurrences of local names.

Definition 6.4 (Syntactic Embedding) Let T and T_{0} be extensions of λ such that T erms(T ) ⊇ T erms(T_{0}) and Ans(T ) = Ans(T_{0}). Let E be a syntactic mapping from extended T -terms to extended T_{0}-terms. Then E is a syntactic embedding of T in T_{0} if it satisfies the following two requirements.

1. E preserves λ-closed T_{0}-subterms. For all T - contexts C, λ-closed T_{0}-terms M,

T_{0} ⊢ E[[C[M]]] = E[[C]] [M].

2. E preserves semantics. For all closed T -terms M, answers A,

T ⊢ M = A ⇔ T_{0} ⊢ E[[M]] = A.

Syntactic embeddings generalize the syntactic (macro) expansions of [4]. They are useful for two reasons. First, a syntactic embedding E of T in T_{0} allows us to extend models of T_{0} to all of T , simply by composing the denotation function of T_{0} with E. As a concrete example, the syntactic embedding from λν to λ given in Figure 5 gives us immediately a denotational semantics of λν. Since a syntactic embedding is the identity on programs in its codomain, the resulting semantics maps λ-terms to the functions they denote in the chosen model of classical λ-calculus. Second, and somewhat related to the first point, the existence of a syntactic embedding between two theories guarantees that all observational equivalences of the base theory are preserved in the extension^{3}. Indeed, we have:

Theorem 6.5 Let T and T_{0} be extensions of λ such that T erms(T ) ⊇ T erms(T_{0}) and Ans(T ) = Ans(T_{0}). If there is a syntactic embedding of T in T_{0} then T is an observational extension of T_{0}.

Proof: Assume that T_{0} ⊧ M ≅ N Then, forall answers A and T_{0}-contexts C_{0} such that C_{0}[M] and C_{0}[N] are closed,

T_{0} ⊢ C_{0}[M] = A ⇔ T_{0} ⊢ C_{0}[N] = A.

Assume first that both M and N are λ-closed. Let E be a syntactic embedding of T in T_{0}. Let C be a T -context such that C[M] and C[N] are closed, and let A be an answer such that C[M] = A. Then,

T ⊢ C[M] = A
⇔ (E preserves semantics)
T_{0} ⊢ E[[C[M]]] = A
⇔ (E preserves λ-closed T_{0} terms)
T_{0} ⊢ E[[C]] [M] = A
⇔ (premise: T_{0} ⊧ M ≅ N)
T_{0} ⊢ E[[C]][N] = A
⇔ (reverse the argument)
T ⊢ C[N] = A.

3Another approach to proving observational extension is based on constructing a retraction between models rather than a syntactic embedding between term languages [21]. At present, this seems to require a fully abstract denotational semantics of the base language, however.

Since A and C were arbitrary, T ⊧ M ≅ N. Now let M and N be arbitrary T_{0} terms, with F V (M) ∪ F V (N) = {x_{1}, ..., x_{n}}. Then,

T_{0} ⊢ M ≅ N
⇒ (Lemma 5.2)
T_{0} ⊢ λx_{1}…. λx_{n}.M ≅ λx_{1}…. λx_{n}.N
⇒ (first part of proof)
T ⊢ λx_{1}…. λx_{n}.M ≅ λx_{1}…. λx_{n}.N
⇒ (Lemma 5.3)
T ⊢ M ≅ N.

6.2 A Syntactic Embedding of λν in λ

The main difficulty in constructing a syntactic embedding of λν in λ has to do with the representation of names. Since names are subject to α-renaming, which is necessary to avoid name capture problems, we cannot simply assign a fixed constant symbol to a name. Instead, the embedding maps a name occurrence to a level number that indicates the number of ν’s between the occurrence of the name and its definition. This is somewhat similar to the de Bruijn numbering of λ-bound identifiers [3] (but see below for an important difference).

For instance, in νn.(νm.n, n), the first occurrence of n in the pair would have level number 1, while the second one would have level number 0. Level numbers have to be adjusted during reduction when ν abstractions are created or destroyed. For instance, νn.(νm.n, n) reduces (by rule ν_{n}) to νn.(n, n), a term in which both occurrences of n have number 0. The adjustments are performed by functions inc, dec and new. Intuitively, inc and dec add or subtract one to all level numbers in their argument terms. new is like dec, except that it is defined only on positive level numbers. For instance, the translation under N of νn.(νm.n, n) is new (new 1), 0)).

Adjustments are also necessary when a term is substituted in another. For instance, λx.(νn.x, x) is translated to λx.(new (inc x), x). This takes account of the increase in the number of surrounding ν’s when an argument term is substituted for x.

Note that there is an important difference between de Bruijn numbers and level numbers. Adjustment of de Bruijn numbers is a meta-operation whereas it is crucial that inc and dec are definable in the λ-calculus itself. Even if we had used a de Bruijn numbering scheme for all identifiers, level numbers and their their shift functions would still be needed.

We have to represent level numbers in such a way that they can be distinguished from other symbols in the translated terms. There are a number of ways of doing so. For instance, level numbers can be represented as pairs of a marker name, that is chosen to be distinct from the names of a mapped term M, and a Church-Numeral. (Note that this means that identity of the marker names depends on the mapped term). The precise representation of level numbers is irrelevant here; we abstract from it by denoting level numbers with numerals, and assume that we have a test function lnum?, successor and predecessor functions (+1) and (−1), and equality eq lnum on level numbers. In the following, we let the letters k and l range over level numbers.

Figure 5 gives an embedding E of λν in λ. The embedding is defined in terms of another syntactic mapping N, that takes as additional arguments a level number l that indicates the current ν-nesting level, and an environment ρ that maps identifiers and names to the nesting level of their definition.

Definition 6.6 (Admissible Environments) Given a term M and a level number l, the set Env(M, l) of environments that are admissible for M at level l is the set of all finite mappings ρ from identifiers and names to level numbers in 0..l that satisfy the following two requirements:

1. ρ is defined for each identifier and name free in M.

2. ρ maps different names to different level numbers.

Furthermore, we assume that each ρ ^{∈} Env(M, l) is undefined on all bound identifiers and names in M. This can always be achieved by choosing an appropriate αrepresentative for M.

Notation. ρ[x ↦ a] (or ρ[n ↦ a]) denotes the extension of environment ρ by the binding that maps x (or n) to a. To save parentheses, we assume that extension binds more strongly than function application, i.e f ρ[x ↦ a] parses f (ρ[x ↦ a]).

The embedding is defined in terms of a number of auxiliary functions, which for the moment are assumed to be primitive. They are:

• A function eq, such that

\begin{aligned}δ(eq, c) & = & λx.if (lnum? x) false (x == c) \\ δ(eq, l) & = & λx.if (name? x) false (eq lnum x l) \end{aligned}

and such that δ(eq, V) is undefined for values that are not constants or level numbers.

\begin{aligned}E[[M]] & = & N [[M]] 0 ⊥ \\ N [[x]] l ρ & = & inc^{(l–ρx)} x \\ N [[λx.M]] l ρ & = & λx.N [[M]] l ρ[x ↦ l] \\ N [[M_{1} M_{2}]] l ρ & = & (N [[M_{1}]] l ρ) (N [[M_{2}]] l ρ) \\ N [[n^{c}]] l ρ & = & n^{c} \\ N [[n^{ν}]] l ρ & = & l–ρn^{ν} \\ N [[νn.M]] l ρ & = & new (N [[M]] (l+1) ρ[n ↦ l+1]) \\ N [[M_{1} == M_{2}]] l ρ & = & eq (N [[M_{1}]] l ρ) (N [[M_{2}]] l ρ) \\ N [[(M_{1}, M_{2})]] l ρ & = & (N [[M_{1}]] l ρ, N [[M_{2}]] l ρ) \\ N [[p M]] l ρ & = & p′ (N [[M]] l ρ) \\ N [[[ ]]] l ρ & = & [ ] \end{aligned}

Figure 5: Syntactic embedding of λν in λ.

• For each primitive function in λν, a primitive function p′ such that δ(p′, N [[V]] l ρ) is defined for all l ≥ 0, ρ ^{∈} Env(V, l) iff δ(p, V) is defined, and

δ(p′, V) =

N [[N_{c}^{p}]] 0 ⊥  if V ≡ c
N [[N_{ν}^{p}]] 0 ⊥  if V is a level number
N [[N_{λ}^{p}]] 0 ⊥  if V is a λ-abstraction
(N [[N_{(·,·)}^{p}]] 0 ⊥) M_{1} M_{2} if V ≡ (M_{1}, M_{2})

• Primitive functions inc, dec, new, such that

\begin{aligned}δ(inc, l) & = & l+1 \\ δ(inc, c) & = & c \\ δ(inc, λx.M) & = & λx.[dec x/x] (inc M) \\ δ(inc, (M, N)) & = & (inc M, inc N) \\ δ(dec, l) & = & l–1 \\ δ(dec, c) & = & c \\ δ(dec, λx.M) & = & λx.[inc x/x] (dec M) \\ δ(dec, (M, N)) & = & (dec M, dec N) \\ δ(new, l) & = & l–1 if l ≠ 0 \\ δ(new, c) & = & c \\ δ(new, λx.M) & = & λx.[inc x/x] (new M) \\ δ(new, (M, N)) & = & (new M, new N) \end{aligned}

Ultimately, all these functions will be defined as λterms, but for now we assume that they are primitive functions. To keep the different calculi apart, we call the variant of λ with the new primitive functions λ′.

One checks easily that N preserves closed Λ-terms. Hence, the hardest part of showing that N is a syntactic embedding of λν in λ concerns the proof that N is semantics preserving. This proof is rather convoluted; it occupies all of the remainder of this section.

Outline of the proof of semantics preservation. The proof is in four parts. In the first part, we show that equal terms in λν are mapped (via N) to equal terms in λ′ (Lemma 6.32). In the second part, we show that N has a left inverse, N^{−1} (Lemma 6.34). We use the left inverse in the third part to show that different λν terms are mapped to different λ′ terms (Lemma 6.38). In the fourth part, we use the previous results to show that N preserves semantics (Lemma 6.39). This is also the part where we drop the assumption that eq, inc, dec, new and the p′ are primitive (Corollary 6.40).

The first part is the hardest. Its cornerstone is a syntactic characterization of the result of applying inc to an N -mapped term (Lemma 6.29). It relates function inc with ⇑_{k}, a syntactic shift operator on level numbers (Lemma 6.29). Informally, ⇑_{k} increments all nonnegative level numbers greater than or equal to k in a term. The detour via ⇑_{k} and ⇓_{k} is necessary since new and dec do not distribute through function application, but ⇓_{k} does, and we need this property to carry out the structural induction in later proofs.

An important property of ⇑_{k} and its inverse ⇓_{k} is that both mappings are preserved under reduction. (Lemma 6.26, Lemma 6.27). The following lemmas prepare the way for these results.

(5) [figure: inc (dec (λx.M)); inc (λx.[inc x/x] (dec M)); λx.[inc (dec x) / x] (inc (dec M)); λx.M; d; d; ∼_{1}; ∼]

First, some facts about inc, dec and new:

Lemma 6.7 For all M ^{∈} Λ′,

\begin{aligned}(i) & inc (dec M) & ≅ & M \\ (ii) & dec (inc M) & ≅ & M \end{aligned}

Proof: (i) We use the critical pairs technique described in Section 5. Let

S = {inc (dec a) ∼ a}

for some meta-variable a and let ∼ be the symmetric compatible valuation closure of S. We use Theorem 5.5 to show that ∼ ⊆ ≅.

It was shown already in [16] that λν has downwards closed evaluation contexts that are preserved by every similarity relation. Hence, it remains to be shown that ∼ preserves answers and that it is deterministically locally stable.

If M ∼ A, then, by the definition of S, M must be of the form inc (dec A). This term reduces to A, hence M = A. This shows that ∼ is answer preserving. We now show that ∼ is deterministically locally stable.

Since the RHS of S consists a single meta-variable, it cannot interfere with a redex. The left hand side can interfere in exactly one way, namely Δ ≡ dec M, for some term M. Furthermore, since Δ is a redex, M must be a λ-abstraction, a pair, a name, or a level number. We distinguish the four cases. In the case of a λ−abstraction, diagram (5) commutes.

In the case of a level number, the following diagram commutes.

(6)

[figure: inc (dec l)); inc (l − 1); l; l; d; d; ≡; ∼]

The other two cases are similar. This shows that ∼ is deterministically locally stable. Thus, by Theorem 5.5, ∼ ⊆≅.

The proof of (ii) is analogous.

Lemma 6.8 For all M, N in Λ′,

inc (M N) ≅ (inc M) (inc N)

Proof: Let

S = {inc(a b) ∼ (inc a) (inc b)}

and let ∼ be the symmetric compatible valuation closure of S. We use Theorem 5.5 to show that ∼ ⊆ ≅. Clearly, no side of S matches an answer, hence ∼ vacuously preserves answers. We now show that ∼ is deterministically locally stable. Assume first that a Δ interferes with the LHS of S. Then Δ must be of the form (λx.M) N, for some terms M, N. In this case the following diagram commutes.

(7)

[figure: inc ((λx.M) N); inc ([N/x]M); (inc (λx.M)) (inc N); d; ≅; ∼]

The ≅ diagonal follows from the following argument.

(inc (λx.M)) (inc N)
= (by definition of inc)
(λx.[dec x/x] (inc M)) (inc N)
= (by β-reduction)
[inc N/x] ([dec x/x] (inc M))
≡ (by combining the substitutions)
[dec (inc N) / x] (inc M)
≅ (by Lemma 6.7)
[N/x] (inc M)

(8) [figure: (inc (λx.M)) (inc N); (λx.[dec x/x] (inc M)) (inc N); [inc N/x] ([dec x/x] (inc M)); inc ((λx.M) N); d; d; ≅; ∼]

Assume now that a redex Δ interferes deterministically with the right hand side of S. Then Δ must be of the form inc L, for some term L that is a λ-abstraction, a pair, a name, or a level number. Furthermore, since Δ is by assumption head-redex, it must match the function part (inc a) of the RHS of S. We distinguish according to the form of L.

If L is a λ−abstraction λx.M, diagram (8) commutes.

The ≅ diagonal in (8) holds, since

inc ((λx.M) N)
= (by β-reduction)
inc ([N/x] M)
≅ (by Lemma 6.7)
[inc N/x] ([dec x/x] (inc M))

If L is a pair (M_{1}, M_{2}), the following diagram commutes.

(9)

[figure: (inc (M_{1}, M_{2})) (inc N); (inc M_{1}, inc M_{2}) (inc N); inc ((M_{1}, M_{2}) N); d; ≅; ∼]

The ≅ diagonal holds by a further application of Theorem 5.4 since both sides of ≅ are “stuck”, i.e. they do not interfere with any redex.

The cases where L is a name or a level number are analogous to the last case. The preceding discussion showed that ∼ is weakly locally stable. By Theorem 5.5, ∼ ⊆≅.

The proofs of the following three lemmas are omitted. They are like the last two proofs routine applications of Theorem 5.5.

Lemma 6.9 For all primitive operators p′, terms M ^{∈} Λ′,

inc (p′ M) ≅ p′ (inc M)

Lemma 6.10 For all M, N ^{∈} Λ′,

inc (eq M N) ≅ eq (inc M) (inc N)

Lemma 6.11 For all terms M ^{∈} Λ′,

new M = dec (neq 0 M),

where

neq l k  = k  if l ≠ k
neq l c  = c
neq l (λx.M) = λx.neq l M
neq l (M, N) = (neq l M, neq l N)

Next, some facts about N that are easily shown by an induction on the structure of the the term argument of N.

Lemma 6.12 For all terms M ^{∈} Λν, level numbers 0 ≤ k ≤ l, environments ρ ^{∈} Env(M, l),

(i) If x is not free in M,

N [[M]] l ρ[x ↦ k] ≡ N [[M]] l ρ.

(ii) If n is not free in M,

N [[M]] l ρ[n ↦ k] ≡ N [[M]] l ρ.

Lemma 6.13 For all closed terms M ^{∈} Λν, level numbers l, environments ρ ^{∈} Env(M, l),

N [[M]] l ρ ≡ N [[M]] 0 ⊥.

Lemma 6.14 For all M ^{∈} Λν, level numbers 0 ≤ k < l, environments ρ ^{∈} Env(M, l),

[inc x/x] (N [[M]] l ρ[x ↦ k+1]) ≡ N [[M]] l ρ[x ↦ k]

Proof: By an induction on the structure of M. The interesting base case for (i) is:

[inc x/x] (N [[x]] l ρ[x ↦ k+1])

≡ (by definition of N, substitution)

inc^{l−(k+1)} (inc x)

≡ (by definition of N)

N [[x]] l ρ[x ↦ k]

The corresponding case for (ii) is analogous. The other base cases and induction steps are all routine.

We now work towards giving a syntactic characterization of inc (N [[M]] l ρ) that relates inc with the syntactic operator ⇑_{k}. ⇑_{k} and its inverse ⇓_{k} are defined in Figures 6 and 7 (Note that ⇓_{k} is a partial function). Before we come to the correspondence result of (Lemma 6.29), we need to prove some facts about these shift operators.

Lemma 6.15 ⇓_{k} and ⇑_{k} are inverses. For all M ^{∈} Λ′, level numbers k,

⇓_{k} (⇑_{k} M) ≡ M,

and for all M ^{∈} Λ′, level numbers k, such that ⇓_{k} M is defined,

⇑_{k} (⇓_{k} M) ≡ M

Proof: An easy induction on the structure of M.

Lemma 6.16 ⇑ and ⇓ are compositional: For all contexts C, level numbers k, there exists an level number k′ such that, for arbitrary x ^{∉} F V (C[M]),

\begin{aligned}⇑_{k} (C[M]) & ≡ & [⇑_{k′} M/x] (⇑_{k} (C[x])) \\ ⇓_{k} (C[M]) & ≡ & [⇓_{k′} M/x] (⇓_{k} (C[x])) \end{aligned}

Proof: An easy structural induction on C.

Lemma 6.17 For all level numbers k,l_{1},l_{2},

l_{1} < l_{2} ⇒ ⇑_{k} l_{1} < ⇑_{k} l_{2}.

If l_{1} ≠ k and l_{2} ≠ k then also

l_{1} < l_{2} ⇒ ⇓_{k} l_{1} < ⇓_{k} l_{2}.

Proof: Easy.

Lemma 6.18 For all M ^{∈} Λ′, level numbers k, identifiers x,

\begin{aligned}⇑_{k} ([inc x/x] M) & ≡ & [inc x/x] (⇑_{k} M) \\ ⇑_{k} ([dec x/x] M) & ≡ & [dec x/x] (⇑_{k} M). \end{aligned}

Furthermore, provided either side is defined,

\begin{aligned}⇓_{k} ([inc x/x] M) & ≡ & [inc x/x] (⇓_{k} M) \\ ⇓_{k} ([dec x/x] M) & ≡ & [dec x/x] (⇓_{k} M), \end{aligned}

Proof: An easy induction on the structure of M.

Definition 6.19 The dec-excess of a subterm N of a Λ′-term M is the number of dec and new terms occurring on the path between N and the root of M minus the number of inc terms occurring on that path.

Definition 6.20 A term M is balanced if every occurrence of a bound identifier in M has the same dec-excess as its binding λ-term.

Lemma 6.21 For all terms M ^{∈} Λν, level numbers l, environments ρ ^{∈} Env(M, l): N [[M]] l ρ is balanced.

Proof: Follows directly from the definition of N.

Lemma 6.22 For all terms M, N ^{∈} Λ′, if M is balanced and M → N then N is balanced.

Proof: A straightforward analysis of the different reductions in λ′.

Lemma 6.23 For all terms M ^{∈} Λν, level numbers k: If M is closed then

⇑_{k} (N [[M]] 0 ⊥) ≡ N [[M]] 0 ⊥ ≡ ⇓_{k} (N [[M]] 0 ⊥)

Proof: An easy induction on the structure of M.

Lemma 6.24 (⇑_{k}-Substitution) For all terms M, N ^{∈} Λ′, level numbers k, if λx.M is balanced then

[⇑_{k} N/x] (⇑_{k} M) ≡ ⇑_{k} ([N/x]M).

Proof: Let l be a level number and let C be an n-hole context such that

M ≡ C[x, ..., x],  (10)

and x is not free in C. Since λx.M is balanced, the decexcess of every occurrence of x in M is 0. This means that there is an equal number of inc and dec/new nodes on every path from the root of C to a hole. Therefore, by the definition of ⇑_{k}, there is a n-hole context C′ such that for all terms N_{1}, ..., N_{n}

⇑_{k} (C[N_{1}, ..., N_{n}]) ≡ C′[⇑_{k} N_{1}, ..., ⇑_{k} N_{n}]. (11)

⇑_{k} l  ≡ l+1  if k ≤ l
≡ l  if k > l
⇑_{k} x  ≡ x
⇑_{k} c  ≡ c
⇑_{k} (λx.M) ≡ λx. ⇑_{k} M
⇑_{k} (MN)  ≡ (⇑_{k} M) (⇑_{k} N)
⇑_{k} (p′ M)  ≡ p′ (⇑_{k} M)
⇑_{k} (eq M N) ≡ eq (⇑_{k} M) (⇑_{k} N)
⇑_{k} (dec M) ≡ dec (⇑_{k+1} M)
⇑_{k} (inc M) ≡ inc (⇑_{k−1} M)
⇑_{k} (new M) ≡ ⇑_{k} (dec (neq 0 M))

Figure 6: Up-shift operator ⇑_{k}.

Hence,

[⇑_{k} N/x] (⇑_{k} M)

≡ (by (10))

[⇑_{k} N/x] (⇑_{k} C[x, ..., x])

≡ (by (11))

[⇑_{k} N/x] (C′[⇑_{k} x, ..., ⇑_{k} x])

≡ (by the definition of ⇑_{k})

[⇑_{k} N/x] (C′[x, ..., x])

≡ (by substitution)

C′[⇑_{k} N, ..., ⇑_{k} N]

≡ (by (11))

⇑_{k} (C[N, ..., N])

≡ (by (10))

⇑_{k} ([N/x]M).

Lemma 6.25 (⇓_{k}-Substitution) For all terms M, N ^{∈} Λ′, level numbers k, if λx.M is balanced and ⇓_{k} N and ⇓_{k} M are both defined then

[⇓_{k} N/x] (⇓_{k} M) ≡ ⇓_{k} ([N/x]M).

Proof: Analogous to the proof of Lemma 6.24

Lemma 6.26 For all terms M, N ^{∈} Λ′, level numbers k,

M → N ⇒ ⇑_{k} M → ⇑_{k} N

Proof: We distinguish according to the form of the redex Δ in M → N. Assume first that Δ coincides with M.

Case (λx.M) N In this case:

⇑_{k} ((λx.M) N)

≡ (⇑_{k} λx.M) (⇑_{k} N)
≡ (λx. ⇑_{k} M) (⇑_{k} N)

[⇑_{k} N/x] (⇑_{k} M)

≡ (by Lemma 6.24)

⇑_{k} ([N/x]M)

Case inc l If l < k–1, we have:

⇑_{k} (inc l)

≡ inc (⇑_{k−1} l)
≡ inc l
→ l+1
≡ ⇑_{k} (l+1)

On the other hand, if l ≥ k–1, we have:

⇑_{k} (inc l)
≡ inc (⇑_{k−1} l)
≡ inc (l+1)
→ l+2
≡ ⇑_{k} (l+1)

⇓_{k} l  ≡ l–1  if k < l
≡ l  if k > l
⇓_{k} x  ≡ x
⇓_{k} c  ≡ c
⇓_{k} (λx.M) ≡ λx. ⇓_{k} M
⇓_{k} (MN)  ≡ (⇓_{k} M) (⇓_{k} N)
⇓_{k} (p′ M)  ≡ p′ (⇓_{k} M)
⇓_{k} (eq M N) ≡ eq (⇓_{k} M) (⇓_{k} N)
⇓_{k} (dec M) ≡ dec (⇓_{k+1} M)
⇓_{k} (inc M) ≡ inc (⇓_{k−1} M)
⇓_{k} (new M) ≡ ⇓_{k} (dec (neq 0 M))

Figure 7: Down-shift operator ⇓_{k}.

Case inc (λx.M) In this case we have:

⇑_{k} (inc (λx.M))

≡ inc (λx. ⇑_{k−1} M)
→ (by definition of inc)

λx.inc ([dec x/x] (⇑_{k−1} M))

≡ (by Lemma 6.18)

λx.inc (⇑_{k−1} ([dec x/x] M))

≡ ⇑_{k} (λx.inc ([dec x/x] M))

Case inc c Case inc (M, N) are both easy.

Case dec l  Case dec (λx.M)  Case dec c

Case dec (M, N) are analogous to the last four cases.

Case eq l_{1} l_{2} If l_{1} = l_{2} then

⇑_{k} (eq l_{1} l_{2})

≡ eq (⇑_{k} l_{1}) (⇑_{k} l_{2})
→ (by definition of eq)

true

≡ ⇑_{k} true

If l_{1} ≠ l_{2} then, with Lemma 6.17, ⇑_{k} l_{1} ≠ ⇑_{k} l_{2}, and we have:

⇑_{k} (eq l_{1} l_{2})
≡ eq (⇑_{k} l_{1}) (⇑_{k} l_{2})
→ (by definition of eq)
false
≡ ⇑_{k} false

Case p′ M In this case we further distinguish according to the form of M. If M is a level number l, then ⇑_{k} l is some level number l′ and we have:

⇑_{k} (p′ l)
≡ p′(⇑_{k} l)
≡ p′ l′
→ (by definition of p′)
N [[N_{ν}^{p}]] 0 ⊥
≡ (by Lemma 6.23)
⇑_{k} (N [[N_{ν}^{p}]] 0 ⊥)

if M is a pair (M_{1}, M_{2}), we have

⇑_{k} (p′ (M_{1}, M_{2}))
≡ p′(⇑_{k} M_{1}, ⇑_{k} M_{2})
→ (by definition of p′)
(N [[N_{(·,·)}^{p}]] 0 ⊥) (⇑_{k} M_{)} (⇑_{k} M_{2})
≡ (by Lemma 6.23)
⇑_{k} (N [[N_{(·,·)}^{p}]] 0 ⊥) (⇑_{k} M_{1}) (⇑_{k} M_{2})
≡ ⇑_{k} ((N [[N_{(·,·)}^{p}]] 0 ⊥) M_{1} M_{2})

The remaining two cases, where M is a λ-abstraction or a constant, are similar.

This concludes the analysis for the case where Δ ≡ M. We now show the lemma for the general case that Δ is contained in M. Let C and R be such that

M ≡ C[Δ] ⟶^{Δ} C[R] ≡ N

By Lemma 6.16, there is an level number k′ such that for all terms L, ⇑_{k} (C[L]) ≡ [⇑_{k′} L/x] (C[x]) By the first part of the proof, ⇑_{k′} Δ → ⇑_{k′} R. Hence,

\begin{aligned}& ⇑_{k} M ≡ ⇑_{k} (C[Δ]) ≡ [⇑_{k′} Δ/x] (C[x]) \\ → & [⇑_{k′} R/x] (C[x]) ≡ ⇑_{k} (C[R]) ≡ ⇑_{k} N. \end{aligned}

The reverse of Lemma 6.26 also holds:

Lemma 6.27 For all terms M, N ^{∈} Λ′, level numbers k, if M → N and ⇓_{k} M is defined, then so is ⇓_{k} N and

⇓_{k} M → ⇓_{k} N.

Proof: Largely analogous to the proof of Lemma 6.26. We distinguish according to the form of the redex in M → N. The only three cases that are not completely symmetric to cases in the proof of Lemma 6.26 are.

Case inc l We distinguish two subcases: l < k–1 and l > k–1. (l = k–1 is impossible, since in this case neither ⇓_{k} (inc l) nor ⇓_{k} (l+1) are defined). If l < k–1, we have:

⇓_{k} (inc l)
≡ inc (⇓_{k−1} l)
≡ inc l
→ l+1
≡ ⇓_{k} (l+1).

On the other hand, if l > k–1, we have:

⇓_{k} (inc l)
≡ inc (⇓_{k−1} l)
≡ inc (l–1)
→ l
≡ ⇓_{k} (l+1).

Case dec l We distinguish again two subcases: l < k+1, and l > k+1. (Case l = k+1 is impossible). If l < k+1, we have:

⇓_{k} (dec l)
≡ dec (⇓_{k+1} l)
≡ dec l
→ l–1
≡ ⇓_{k} (l–1).

On the other hand, if l > k+1, we have:

⇓_{k} (dec l)
≡ dec (⇓_{k+1} l)
≡ dec (l–1)
→ l–2
≡ ⇓_{k} (l–1).

Case eq l_{1} l_{2} Since ⇓_{k} (eq l_{1} l_{2}) is defined, and

⇓_{k} (eq l_{1} l_{2}) ≡ eq (⇓_{k} l_{1}) (⇓_{k} l_{2}),

⇓_{k} l_{1} and ⇓_{k} l_{2} are both defined, which implies l_{1} ≠ k, l_{2} ≠ k. With Lemma 6.17, it follows that

l_{1} = l_{2} ⇔ ⇓_{k} l_{1} = ⇓_{k} l_{2}.

The case then follows as in Lemma 6.26.

We now use the fact that ⇑_{k} and ⇓_{k} are stable under reduction for a stepping stone towards Lemma 6.29.

Lemma 6.28 For all terms M,

neq 0 (⇑_{1} M) ≅ neq 1 (⇑_{0} M).  (12)

Proof: We use Theorem 5.5. (12) corresponds to the symmetric system of similarities

S =^{def} { neq i (⇑_{j} M) ∼ neq j (⇑_{i} M)
| M ^{∈} Λ′, i, j ^{∈} {0, 1}, i ≠ j
}

Let ∼ be the compatible valuation closure of S. We show that ∼ is deterministically locally stable. Let (P, Q) be a deterministically critical pair. Then (P, Q) falls into one of the categories (1.)–(5.) below. We show in each case that the critical pair can be completed.

1. The redex is contained in ⇑_{i} M, i.e.

\begin{aligned}P & ≡ & neq i (⇑_{j} M) ∼ neq j (⇑_{i} M) ⟶_{d} neq j N \\ & ≡ & Q \end{aligned}

where M, N ^{∈} Λ′, ⇑_{i} M ⟶_{d} N, i, j ^{∈} {0, 1}, i ≠ j.

In this case,

P

≡ neq i (⇑_{j} M)
≡ (by Lemma 6.15)

neq i (⇑_{j} (⇓_{i} (⇑_{i} M)))

→ (by Lemma 6.27, Lemma 6.26)

neq i (⇑_{j} (⇓_{i} N))

∼ (by definition of ∼)

neq j (⇑_{i} (⇓_{i} N))

≡ (by Lemma 6.15)

neq j N

≡ Q

Therefore, the following diagram commutes.

[figure: neq j (⇑_{i} M); neq j N ≡ Q; P ≡ neq i (⇑_{j} M); neq i (⇑_{j} (⇓_{i} N)); d; ∼; ∼]

2. The redex involves neq and a λ-abstraction, i.e.

P ≡ neq i (⇑_{j} λx.M) ∼ neq j (⇑_{i} λx.M)

⟶_{d} λx.neq j (⇑_{i} M)

≡ Q

where M ^{∈} Λ′, i, j ^{∈} {0, 1}, i ≠ j. In this case,

P

≡ neq i (⇑_{j} λx.M)
≡ neq i (λx. ⇑_{j} M)
→ λx.neq i (⇑_{j} M)
∼ λx.neq j (⇑_{i} M)
≡ Q

Therefore, the following diagram commutes.

[figure: neq j (⇑_{i} λx.M); λx.neq j (⇑_{i} M) ≡ Q; P ≡ neq i (⇑_{j} λx.M); λx.neq i (⇑_{j} M); d; ∼; ∼]

3. The redex involves neq and a pair, i.e.

P ≡ neq i (⇑_{j} (M, N)) ∼ neq j (⇑_{i} (M, N))

⟶_{d} (neq j (⇑_{i} M), neq j (⇑_{i} N))

≡ Q

where M, N ^{∈} Λ′, i, j ^{∈} {0, 1}, i ≠ j. This is essentially analogous to the last case.

4. The redex involves neq and a constant, i.e.

P ≡ neq i (⇑_{j} c) ∼ neq j (⇑_{i} c) ⟶_{d} c ≡ Q

where c is a constant, i, j ^{∈} {0, 1}, i ≠ j. Then P ≡ neq i (⇑_{j} c) → c which completes the critical pair.

5. The redex involves neq and a level number, i.e.

P ≡ neq i (⇑_{j} l) ∼ neq j (⇑_{i} l) ⟶_{d} ⇑_{i} l ≡ Q

where l is a level number, i, j ^{∈} {0, 1}, i ≠ j. We distinguish the two subcases i = 0, j = 1 and i = 1, j = 0. If i = 0, j = 1 then the root of the critical pair is neq 1 (⇑_{0} l). Since this is also a redex we must have ⇑_{0} l ≠ 1, and therefore l ≠ 0. But this implies ⇑_{1} l ≡ ⇑_{0} l ≠ 0. Therefore, neq 0 (⇑_{1} l) → ⇑_{1} l. In summary, the following diagram commutes:

[figure: neq 1 (⇑_{0} l); ⇑_{0} l ≡ Q; P ≡ neq 0 (⇑_{1} l); ⇑_{1} l; d; ∼; ≡]

The subcase where i = 1 and j = 0 is completely symmetric.

(1.)−(5.) together show that S is locally stable. Furthermore, since neither side of this system matches an answer, ∼ vacuously preserves answers. By Theorem 5.5, ∼ ⊆ ≅.

Lemma 6.29 Let σ be the syntactic mapping that substitutes inc x for x in M, for every free identifier x in M. That is, for all terms M,

σ M = [inc x/x]_{x^{∈}F V (M)} M.

Then for all M ^{∈} Λν, level numbers l, ρ ^{∈} Env(M, l),

inc (N [[M]] l ρ) ≅ σ (⇑_{0} (N [[M]] l ρ))

Proof: By induction on the structure of M. Case c In this case:

inc (N [[c]] l ρ)

≡ inc c
= c
≡ σ (⇑_{0} (N [[c]] l ρ)

Case n^{ν} In this case:

inc (N [[n^{ν}]] l ρ)

≡ inc (l–ρn^{ν})
= (by definition of inc)

l–ρn^{ν}+1

≡ σ (⇑_{0} (N [[n^{ν}]] l ρ)

Case x In this case:

inc (N [[x]] l ρ)

≡ inc (inc^{l–ρx}x)
≡ inc^{l–ρx}(inc x)
≡ σ (⇑_{0} (N [[x]] l ρ))

Case λx.M In this case:

inc (N [[λx.M]] l ρ)

≡ inc (λx.N [[M]] l ρ[x ↦ l])
= (by definition of inc)

λx.[dec x/x] (inc (N [[M]] l ρ[x ↦ l]))

= (by the induction hypothesis)

λx.[dec x/x] (σ (⇑_{0} (N [[M]] l ρ[x ↦ l])))

≡ σ (λx.[dec x/x] ([inc x/x]

(⇑_{0} (N [[M]] l ρ[x ↦ l]))))

≅ (by Lemma 6.7)

σ (λx. ⇑_{0} (N [[M]] l ρ[x ↦ l]))

≡ σ (⇑_{0} (N [[λx.M]] l ρ))

Case νn.M In this case:

inc (N [[νn.M]] l ρ)

≡ inc (new (N [[M]] (l+1) ρ[n ↦ l+1]))
= (by Lemma 6.11)

inc (dec (neq 0 (N [[M]] (l+1) ρ[n ↦ l+1])))

≅ (by Lemma 6.7)

dec (inc (neq 0 (N [[M]] (l+1) ρ[n ↦ l+1])))

≅ (by Lemma 6.8)

dec (neq 1 (inc (N [[M]] (l+1) ρ[n ↦ l+1])))

≅ (by the induction hypothesis)

dec (neq 1 (σ (⇑_{0} (N [[M]] (l+1) ρ[n ↦ l+1]))))

≡ (by rearrangement)

σ (dec (neq 1 (⇑_{0} (N [[M]] (l+1) ρ[n ↦ l+1]))))

≅ (by Lemma 6.28)

σ (dec (neq 0 (⇑_{1} (N [[M]] (l+1) ρ[n ↦ l+1]))))

≡ (by definition of ⇑_{k})

σ (⇑_{0} (dec (neq 0 (N [[M]] (l+1) ρ[n ↦ l+1]))))

≅ (by Lemma 6.11, Lemma 6.26)

σ (⇑_{0} (new (N [[M]] (l+1) ρ[n ↦ l+1])))

≡ σ (⇑_{0} (N [[νn.M]] l ρ))

Case MN In this case:

inc (N [[MN]] l ρ)

≅ (by Lemma 6.8)

(inc (N [[M]] l ρ)) (inc (N [[N]] l ρ))

≅ (by the induction hypothesis)

(σ (⇑_{0} (N [[M]] l ρ))) (σ (⇑_{0} (N [[N]] l ρ)))

≡ σ (⇑_{0} (N [[MN]] l ρ))

Case M == N In this case:

inc (N [[M == N]] l ρ)

≡ inc (eq (N [[M]] l ρ) (N [[N]] l ρ))
≅ (by Lemma 6.10)
eq (inc (N [[M]] l ρ)) (inc (N [[N]] l ρ))
≅ (by the induction hypothesis)
eq (σ (⇑_{0} (N [[M]] l ρ))) (σ (⇑_{0} (N [[N]] l ρ)))
≡ σ (⇑_{0} (eq (N [[M]] l ρ) (N [[N]] l ρ)))
≡ σ (⇑_{0} (N [[M == N]] l ρ))

Case p M In this case:

inc (N [[p M]] l ρ)
≡ inc (p′ (N [[M]] l ρ))
≅ (by Lemma 6.9)
p′ (inc (N [[M]] l ρ))
≅ (by the induction hypothesis)
p′ (σ (⇑_{0} (N [[M]] l ρ)))
≡ σ (⇑_{0} (N [[p′ M]] l ρ))

Case (M, N) In this case:

inc (N [[(M, N)]] l ρ)
= (by definition of inc)
(inc (N [[M]] l ρ), inc (N [[N]] l ρ))
≅ (by the induction hypothesis)
(σ (⇑_{0} (N [[M]] l ρ)), σ (⇑_{0} (N [[N]] l ρ)))
≡ σ (⇑_{0} (N [[(M, N)]] l ρ))

Using this characterization of inc in terms of ⇑_{k} gives us

Lemma 6.30 For all M ^{∈} Λν, level numbers l, ρ ^{∈} Env(M, l),

inc (N [[M]] l ρ) ≅ N [[M]] (l+1) ρ.

Proof: By Lemma 6.29,

inc (N [[M]] l ρ) ≅ σ (⇑_{0} (N [[M]] l ρ).  (13)

An easy induction on the structure of M shows that

σ (⇑_{0} (N [[M]] l ρ) ≅ N [[M]] (l+1) ρ  (14)

(13) and (14) together imply the lemma.

The next result states that N commutes (wrt ≅) with substitution.

Lemma 6.31 (Substitution) For all M, N ^{∈} Λν, level numbers l, ρ ^{∈} Env((λx.M) N, l),

[N [[N]] l ρ / x] (N [[M]] l ρ[x ↦ l]) ≅ N [[[N/x] M]] l ρ.

Proof: We use a structural induction on M. A direct proof of the equivalence fails for the case M ≡ νn.M′. We prove instead a stronger proposition:

For all M, N ^{∈} Λν, level numbers l, k, environments ρ′ ^{∈} Env(N, l) and ρ ^{∈} Env(λx.M, l+k), such that ρ extends ρ′,

[N [[N]] l ρ′ / x] (N [[M]] (l+k) ρ[x ↦ l]) (15)
≅ N [[[N/x] M]] (l+k) ρ.

Case x In this case:

[N [[N]] l ρ′ / x] (N [[x]] (l+k) ρ[x ↦ l])
≡ [N [[N]] l ρ′ / x] (inc^{k} x)
≡ inc^{k} (N [[N]] l ρ′)
≅ (by Lemma 6.30)
N [[N]] (l+k) ρ′
≡ (by Lemma 6.12)
N [[[N/x] x]] (l+k) ρ

Case y where y ≠ x In this case:

[N [[N]] l ρ′ / x] (N [[y]] (l+k) ρ[x ↦ l])
≡ [N [[N]] l ρ′ / x] (inc^{l+k–ρy} y)
≡ inc^{l+k–ρy} y
≡ N [[[N/x]y]] (l+k) ρ

Case c and Case n^{ν} are similar to the last case.

Case λy.M In this case:

[N [[N]] l ρ′ / x] (N [[λy.M]] (l+k) ρ[x ↦ l])
≡ λy.[N [[N]] l ρ′ / x]
(N [[M]] (l+k) ρ[x ↦ l][y ↦ l+k])
≅ (by the induction hypothesis)
λy.N [[[N/x]M]] (l+k) ρ[y ↦ l+k]
≡ N [[[N/x] λy.M]] (l+k) ρ

Case νn.M In this case:

[N [[N]] l ρ′ / x] (N [[νn.M]] (l+k) ρ[x ↦ l])
≡ new ([N [[N]] l ρ′ / x]
(N [[M]] (l+k+1) ρ[x ↦ l][n ↦ l+k+1]))
≡ (by the induction hypothesis)
new (N [[[N/x]M]] (l+k+1)
ρ[x ↦ l][n ↦ l+k+1])
≡ N [[[N/x] νn.M]] (l+k) ρ

Case M_{1} M_{2}  Case M == N  Case (M_{1}, M_{2})

Case p M are all easy induction steps.

We now show that the translation N is stable under reduction in λν:

Lemma 6.32 (Simulation) For all terms M, N ^{∈} Λ, level numbers l, environments ρ ^{∈} Env(M, l): If M → N then ρ ^{∈} Env(N, l) and

N [[M]] l ρ ≅ N [[N]] l ρ.  (16)

Proof: Assume M → N and let ρ ^{∈} Env(M, l). Then all free identifiers and names in N are also free in M, therefore ρ ^{∈} Env(N, l). To show (16), we distinguish according to the notion of reduction in M → N. By an argument analogous to the one at the end of the proof of Lemma 6.26, we can assume w.l.o.g. that the redex in the reduction from M to N coincides with M.

Case β In this case the redex is of the form (λx.M) N, and we have:

N [[(λx.M) N)]] l ρ
≡ (λx.N [[M]] l ρ[x ↦ l]) (N [[N]] l ρ)
= (by reduction in λ′)
[N [[N]] l ρ / x] (N [[M]] l ρ[x ↦ l])
= (by Lemma 6.31)
N [[[N/x] M]] l ρ

Case δ In this case the redex is of the form p V, where p is a primitive operator and V is a value. We further distinguish according to the form of V. If V is a local name n^{ν}, then N [[n^{ν}]] l ρ is a level number and we have:

N [[p n^{ν}]] l ρ
≡ p′ (ρn^{ν})
= (by reduction in λ′)
N [[N_{ν}^{p}]] 0 ⊥
≡ (by Lemma 6.13)
N [[N_{ν}^{p}]] l ρ
≡ N [[δ(p, n^{ν})]] l ρ

If V is a pair (M_{1}, M_{2}), then

N [[p (M_{1}, M_{2})]] l ρ
≡ p′ (N [[M_{1}]] l ρ, N [[M_{2}]] l ρ)
= (by reduction in λ′)
(N [[N_{(·,·)}^{p}]] 0 ⊥) (N [[M_{1}]] l ρ) (N [[M_{2}]] l ρ)
≡ (by Lemma 6.13)
(N [[N_{(·,·)}^{p}]] l ρ) (N [[M_{1}]] l ρ) (N [[M_{2}]] l ρ)
≡ N [[δ(p, (M_{1}, M_{2}))]] l ρ

The remaining cases, where V is a constant or a λabstraction, are similar.

Case eq In this case the redex is of the form n == m where n and m are names. If n and m are the same local name or constant then:

N [[n == n]] l ρ
≡ eq (N [[n]] l ρ) (N [[n]] l ρ)
= (by reduction in λ′)
true
≡ N [[true]] l ρ

If n and m are different local names then ρn and ρm are different level numbers, because ρ is injective. Therefore we have:

N [[n == m]] l ρ
≡ eq (ρn) (ρm)
= (by reduction in λ′)
false
≡ N [[false]] l ρ

A similar argument can be made in the case of different constants n, m.

If n is a local name and m is a constant, then N [[n]] l ρ is a level number and N [[m]] l ρ is a constant and we have:

N [[n == m]] l ρ
≡ eq (ρn) m
= (by reduction in λ′)
false
≡ N [[false]] l ρ

The remaining case, where n is a constant and m is a local name, is symmetric.

Case ν_{λ} In this case the redex is of the form νn.λx.M, and we have:

N [[νn.λx.M]] l ρ
≡ new (λx.N [[M]] (l+1) ρ[n ↦ l+1][x ↦ l+1])
≡ λx.new ([inc x/x]
(N [[M]] (l+1) ρ[n ↦ l+1][x ↦ l+1]))
= (by Lemma 6.14)
λx.new (N [[M]] (l+1) ρ[x ↦ l][n ↦ l+1])
≡ N [[λx.νn.M]] l ρ

Case ν_{p} In this case the redex is of the form νn.(M, N), and we have:

N [[νn.(M, N)]] l ρ
≡ new (N [[M]] (l+1) ρ[n ↦ l+1],
N [[N]] (l+1) ρ[n ↦ l+1])
= (by definition of new)
(new (N [[M]] (l+1) ρ[n ↦ l+1]),
new (N [[N]] (l+1) ρ[n ↦ l+1]))
≡ (N [[νn.M]] l ρ, N [[νn.N]] l ρ)

Case ν_{n} In this case the redex is of the form νn.m, where m is a name different from n. If m is a constant, we have:

N [[νn.m]] l ρ
≡ new m
= (by reduction in λ′)
m
≡ N [[νn.m]] l ρ

On the other hand, if m is a local name, we have:

N [[νn.m]] l ρ
≡ new (l+1–ρm)
= (by reduction in λ′, since ρ m ≤ l)
l–ρm
≡ N [[νn.m]] l ρ

The preceding lemma showed that N maps equal terms in Λν to equal terms in Λ′. We also need to show the converse: different terms in Λν are mapped to different terms in Λ′. To show this, we define in Figure 8 a mapping N^{−1} which is a left inverse of N. N^{−1} is a partial mapping from terms in Λ′, level numbers l and environments ρ ^{∈} ⋃{Env(M, l) | M ^{∈} Λν} to terms in Λν.

Definition 6.33 For a term M ^{∈} Λ′, let

Env^{−1}(M, l) = {ρ | ∃M′ ^{∈} Λν. ρ ^{∈} Env(M′, l)

∧ N^{−1}[[M]] l ρ is defined}.

We observe that N^{−1} is well-defined as a function. Since ρ maps different names to different level numbers, there is for any given pair (k, l) at most one name n such that ρn = l–k. Therefore, N^{−1} is a function.

Lemma 6.34 For all M ^{∈} Λν, level numbers l, ρ ^{∈} Env(M, l),

N^{−1}[[N [[M]] l ρ]] l ρ ≡ M

Proof: An easy induction on the structure of M. We present only two sample cases.

Case x In this case:

N^{−1}[[N [[x]] l ρ]] l ρ
≡ (by definition of N)
N^{−1}[[inc^{l–ρx} x]] l ρ
≡ (by definition of N^{−1})
N^{−1}[[x]] (ρx) ρ
≡ (by definition of N^{−1})
x

Case νn.M In this case:

N^{−1}[[N [[νn.M]] l ρ]] l ρ
≡ (by definition of N)
N^{−1}[[new (N [[M]] (l+1) ρ[n ↦ l+1])]] l ρ
≡ (by definition of N^{−1})
νn.N^{−1}[[N [[M]] (l+1) ρ[n ↦ l+1]]]
(l+1) ρ[n ↦ l+1]
≡ (by the induction hypothesis)
νn.M

Lemma 6.35 For all terms M ^{∈} Λ′, level numbers 0 ≤ k ≤ l, environments ρ ^{∈} Env^{−1}(M, l),

(i) If x is not free in M,

N^{−1}[[M]] l ρ[x ↦ k] ≡ N^{−1}[[M]] l ρ.

(ii) If n is not free in M,

N^{−1}[[M]] l ρ[n ↦ k] ≡ N^{−1}[[M]] l ρ.

Proof: Easy.

Lemma 6.36 For all M ^{∈} Λ′, level numbers 0 ≤ k ≤ l, environments ρ ^{∈} Env^{−1}(M, l),

(i)  N^{−1}[[M]] l ρ[x ↦ k]
≡ N^{−1}[[[dec x/x] M]] l ρ[x ↦ k+1]
(ii) N^{−1}[[M]] l ρ[x ↦ k+1]
≡ N^{−1}[[[inc x/x] M]] l ρ[x ↦ k]

Proof: (i) By an induction on the structure of M. The only interesting case is Case x . In this case,

N^{−1}[[k]] l ρ  ≡ n  if ρn = l–k
N^{−1}[[x]] l ρ  ≡ x  if ρx = l
N^{−1}[[c]] l ρ  ≡ c
N^{−1}[[λx.M]] l ρ  ≡ λx.N^{−1}[[M]] l ρ[x ↦ l]
N^{−1}[[M_{1} M_{2}]] l ρ  ≡ (N^{−1}[[M_{1}]] l ρ) (N^{−1}[[M_{2}]] l ρ)
N^{−1}[[(M_{1}, M_{2})]] l ρ ≡ (N^{−1}[[M_{1}]] l ρ, N^{−1}[[M_{2}]] l ρ)
N^{−1}[[p′ M]] l ρ  ≡ p (N^{−1}[[M]] l ρ)
N^{−1}[[eq M_{1} M_{2}]] l ρ ≡ N^{−1}[[M_{1}]] l ρ == N^{−1}[[M_{2}]] l ρ
N^{−1}[[inc M]] (l+1) ρ ≡ N^{−1}[[M]] l ρ
N^{−1}[[dec M]] l ρ  ≡ N^{−1}[[M]] (l+1) ρ
N^{−1}[[new M]] l ρ  ≡ νn.N^{−1}[[M]] (l+1) ρ[n ↦ l+1]  where n ∉ DOM(ρ) ∪ F N(M)

Figure 8: Syntactic embedding N^{−1}.

N^{−1}[[x]] l ρ[x ↦ k]
≡ (by definition of N^{−1})
inc^{l−k} x
≡ (by definition of N^{−1})
N^{−1}[[x]] (l+1) ρ[x ↦ k+1]
≡ (by definition of N^{−1})
N^{−1}[[[dec x/x] x]] l ρ[x ↦ k+1]

The proof of (ii) is analogous.

We now show the dual of the substitution lemma (Lemma 6.31).

Lemma 6.37 (Substitution-Dual) For all M, N ^{∈} Λν, level numbers l, ρ ^{∈} Env^{−1}((λx.M) N, l),

\begin{matrix}[N^{−1}[[N]] l ρ / x] (N^{−1}[[M]] l ρ[x ↦ l]) \\ ≡ N^{−1}[[[N/x] M]] l ρ. \end{matrix}

Note that this is stronger than the corresponding statement of Lemma 6.31, in that we have ≡ instead of ≅.

Proof: We use a structural induction on M. A direct proof of the proposition fails for the case M ≡ νn.M′. We prove instead a stronger proposition:

For all M, N ^{∈} Λν, level numbers l, k, environments ρ′ ^{∈} Env^{−1}(N, l) and ρ ^{∈} Env^{−1}(λx.M, l+k), such that ρ extends ρ′,

\begin{matrix}[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[M]] (l+k) ρ[x ↦ l]) \\ ≡ N^{−1}[[[N/x] M]] (l+k) ρ. \end{matrix}

Case x In this case k = 0 and

[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[x]] l ρ[x ↦ l])

≡ (by definition of N^{−1})
[N^{−1}[[N]] l ρ′ / x] x
≡ (by substitution)
N^{−1}[[[N/x] x]] l ρ′
≡ (by Lemma 6.35)
N^{−1}[[[N/x] x]] l ρ

Case y where y ≠ x In this case ρy = l+k, and

[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[y]] (l+k) ρ[x ↦ l])

≡ [N^{−1}[[N]] l ρ′ / x] y
≡ N^{−1}[[[N/x] y]] (l+k) ρ

Case c and Case l are similar to the last case.

Case λy.M In this case:

[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[λy.M]] (l+k) ρ[x ↦ l])
≡ [N^{−1}[[N]] l ρ′ / x]
(λy.N^{−1}[[M]] (l+k) ρ[x ↦ l][y ↦ l+k])
≡ (by the induction hypothesis)
λy.N^{−1}[[[N/x]M]] (l+k) ρ[x ↦ l][y ↦ l+k]
≡ N^{−1}[[[N/x] λy.M]] (l+k) ρ[x ↦ l]

Case inc M In this case l+k > 0, and

[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[inc M]] (l+k) ρ[x ↦ l])

≡ [N^{−1}[[N]] l ρ′ / x] (N^{−1}[[M]] (l+k–1) ρ[x ↦ l])
≡ (by the induction hypothesis)
N^{−1}[[[N/x] M]] (l+k–1) ρ
≡ N^{−1}[[[[N/x] (inc M)]] (l+k) ρ

Case dec M is similar to the last case.

Case new M In this case:

[N^{−1}[[N]] l ρ′ / x] (N^{−1}[[new M]] (l+k) ρ[x ↦ l])

≡ (by definition of N^{−1},
for some n ∉ DOM(ρ) ∪ F N(M))
[N^{−1}[[N]] l ρ′ / x]

(νn.N^{−1}[[M]] (l+k+1) ρ[x ↦ l][n ↦ l+k+1])

≡ (by the induction hypothesis)
νn.N^{−1}[[[N/x] M]] (l+k+1) ρ[n ↦ (l+k+1]
≡ N^{−1}[[[N/x] (new M)]] (l+k) ρ

Case M_{1} M_{2}  Case p M  Case eq M N  and

Case (M_{1}, M_{2}) are all simple induction steps.

We now show in the dual of Lemma 6.32 that the reverse translation N^{−1} is stable under reduction in λ′:

Lemma 6.38 (Simulation-Dual) For all M ^{∈} Λ′, level numbers l, ρ ^{∈} Env^{−1}(M, l), if M → N then

N^{−1}[[M]] l ρ = N^{−1}[[N]] l ρ

Note that this is stronger than the corresponding statement of Lemma 6.32, in that we have = instead of ≅.

Proof: We distinguish according to the form of the redex in M → N. Since N^{−1} is compositional, we may assume w.l.o.g. that M itself is the redex in the reduction step (this is justified as in the proof of Lemma 6.26).

Case (λx.M) N In this case:

N^{−1}[[(λx.M) N]] l ρ
≡ (by definition of N^{−1})
(λx.N^{−1}[[M]] l ρ[x ↦ l]) (N^{−1}[[N]] l ρ)
= (by reduction in λ′)
[N^{−1}[[N]] l ρ / x] (N^{−1}[[M]] l ρ[x ↦ l])
≡ (Lemma 6.37)
N^{−1}[[[N/x] M]] l ρ

Case p′ V If V is a level number k then N^{−1}[[k]] l ρ is a local name n^{ν}, and we have:

N^{−1}[[p′ k]] l ρ
≡ p n^{ν}
= (by reduction in λν)
N_{ν}^{p}
≡ (by Lemma 6.34)
N^{−1}[[N [[N_{ν}^{p}]] l ρ]] l ρ
≡ (by Lemma 6.13)
N^{−1}[[N [[N_{ν}^{p}]] 0 ⊥]] l ρ
≡ N^{−1}[[δ(p′, k)]] l ρ

If V is a λ-abstraction λx.M, we have:

N^{−1}[[p′ (λx.M)]] l ρ
≡ p (λx.N^{−1}[[M]] l ρ[x ↦ l])
= (by reduction in λν)
N_{λ}^{p}
≡ (by Lemma 6.34)
N^{−1}[[N [[N_{λ}^{p}]] l ρ]] l ρ
≡ (by Lemma 6.13)
N^{−1}[[N [[N_{λ}^{p}]] 0 ⊥]] l ρ
≡ N^{−1}[[δ(p′, λx.M)]] l ρ

The remaining cases, where V is a constant or a pair, are similar.

Case eq V W In this case V and W are level-numbers or constants, otherwise we would not have a redex. In each case N^{−1}[[V]] l ρ and N^{−1}[[W]] l ρ are names. Moreover, N^{−1}[[V]] l ρ == N^{−1}[[W]] l ρ iff V and W are the same level number or constant. Hence, if eq V W = true in λ′, then:

N^{−1}[[eq V W]] l ρ
≡ V == W
= true
≡ N^{−1}[[true]] l ρ

On the other hand, eq V W = false in λ′, then:

N^{−1}[[eq V W]] l ρ
≡ V == W
= false
≡ N^{−1}[[false]] l ρ

Case inc (λx.M) In this case l > 0, since otherwise ρ ^{∉} Env^{−1}(inc (λx.M), l), and we have

N^{−1}[[inc (λx.M)]] l ρ

≡ (by definition of N^{−1})

λx.N^{−1}[[M]] (l–1) ρ[x ↦ l–1]

≡ (by definition of N^{−1})

λx.N^{−1}[[inc M]] l ρ[x ↦ l–1]

≡ (by Lemma 6.36)

λx.N^{−1}[[[dec x/x] (inc M)]] l ρ[x ↦ l]

≡ (by definition of N^{−1})

N^{−1}[[λx.[dec x/x] (inc M)]] l ρ

Case inc k In this case l > 0, and we have:

N^{−1}[[inc k]] l ρ

≡ (by the definition of N^{−1})

N^{−1}[[k]] (l–1) ρ

≡ (by the definition of N^{−1},

for some n s.t. ρn = l–1–k) n

≡ (by the definition of N^{−1})

N^{−1}[[k+1]] l ρ

Case inc c In this case l > 0, and we have:

N^{−1}[[inc c]] l ρ

≡ (by the definition of N^{−1})

N^{−1}[[c]] (l–1) ρ

≡ (by the definition of N^{−1})

c

≡ (by the definition of N^{−1})

N^{−1}[[c]] l ρ

Case inc (M_{1}, M_{2}) is an easy induction step.

Case dec λx.M  Case dec k  Case dec c and

Case dec (M_{1}, M_{2}) are symmetric to the last four cas-

es.

Case new (λx.M) In this case:

N^{−1}[[new (λx.M)]] l ρ
≡ (by definition of N^{−1},
for some name n ^{∉} DOM(ρ) ∪ F N(T))
νn.λx.N^{−1}[[M]] (l+1) ρ[n ↦ l+1][x ↦ l+1]
= (by reduction in λ′)
λx.νn.N^{−1}[[M]] (l+1) ρ[n ↦ l+1][x ↦ l+1]
≡ (by Lemma 6.36)

λx.νn.N^{−1}[[[inc x/x]M]] (l+1) ρ[x ↦ l][n ↦ l+1]

≡ (by definition of N^{−1})
N^{−1}[[λx.[inc x/x] (new M)]] l ρ

Case new k In this case k > 0, since otherwise there would be no redex, and we have:

N^{−1}[[new k]] l ρ

≡ (by definition of N^{−1},

for some name n ^{∉} DOM(ρ) ∪ F N(T)) νn.N^{−1}[[k]] (l+1) ρ[n ↦ l+1]

≡ (by the definition of N^{−1},

for some name m s.t. ρm = l+1–k) νn.m

= (by reduction in λ′, since m ≠ n)

m

≡ (by the definition of N^{−1})

N^{−1}[[k–1]] l ρ

Case new c and Case new (M_{1}, M_{2}) are both easy.

Now everything is in place for the main lemma of this section:

Lemma 6.39 For all closed M ^{∈} Λν, answers A,

λν ⊢ M = A ⇔ λ′ ⊢ N [[M]] 0 ⊥ = A.

Proof: “⇒”: Assume M = A. Then M → → A since λν is Church-Rosser. By an induction on the length of reduction from M to A, using Lemma 6.32 at each step,

N [[M]] 0 ⊥ ≅ N [[A]] 0 ⊥.

But N [[A]] 0 ⊥ ≡ A, hence N [[M]] 0 ⊥ ≅ A. By the definition of ≅, this implies N [[M]] 0 ⊥ = A.

“⇐”: Assume N [[M]] 0 ⊥ = A. Then N [[M]] 0 ⊥ → → A since λ′ is Church-Rosser. By an induction on the length of reduction from M to A, using Lemma 6.38 at each step,

N^{−1}[[N [[M]] 0 ⊥]] 0 ⊥ = N^{−1}[[A]] 0 ⊥

The left-hand side of this equality is M by Lemma 6.34, whereas the right-hand side is A by the definition of N^{−1}. Hence, M = A.

We now drop the assumption that N maps to Λ′, where all p′, eq, inc, dec and new are primitive functions, and state the equivalent of Lemma 6.39 for λ. This rests on the fact that all p′, eq, inc, dec, and new are definable in λ. The definitions for p′, eq, inc are:

p′ = λx.if (lnum? x) (N [[N_{ν}^{p}]] 0 ⊥) (p x)
eq′ = λx.λy.if(lnum? x)

if(lnum? y) (eq lnum x y) (x == y)

(x == y)

inc = λx.if (lnum? x)

(x + 1) (if (name? x)

x (if (pair? x)

(inc (fst x), inc (snd x)) (λy.inc (x (dec y)))))

The definitions of dec and new are analogous to the one for inc.

Let Ñ be the syntactic mapping defined as in Figure 5 except that instead of the primitive functions p′, eq, inc, dec, new their defining λ-terms are used. Then clearly,

λ′ ⊢ N [[M]] l ρ ⇔ λ ⊢ Ñ [[M]] l ρ.

With Lemma 6.39, this implies:

Corollary 6.40 For all closed M ^{∈} Λν, answers A,

λν ⊢ M = A ⇔ λ ⊢ N [[M]] 0 ⊥ = A.

Corollary 6.41 E is a syntactic embedding of λν in λ

Proof: It is straightforward to verify that Ẽ preserves closed Λ subterms. With Corollary 6.40, E preserves semantics.

6.3 Putting It All Together

Theorem 6.42 λν is a conservative observational extension of λ.

Proof: By Corollary 6.41, E is a syntactic embedding of λν in λ. By Theorem 6.5 this implies that λν is an observational extension of λ. To show that the extension is conservative, assume λν ⊧ M ≅ N, for terms M, N ^{∈} Λ. Then we have

λν ⊢ C[M] = A ⇔ λν ⊢ C[N] = A

for all Λν-contexts C such that C[M] and C[N] are closed and therefore also for all such Λ-contexts. Since terms M ^{∈} Λ have only β and δ redexes, and since λ is closed under βδ reduction, this implies λ ⊧ M ≅ N.

7 Conclusions

λν is a syntactic theory for functions that create local names. The calculus is fully compatible with functional programming, in the sense that all observational equivalences of functional programming are preserved. There is good evidence that it is a useful foundation for modelling many constructs that so far were outside the domain of functional programming. For instance, 2 showed how imperative programming with mutable variables can be expressed in λν. It would be interesting to see other applications of the calculus, such as in logic or concurrent programming.

Some other areas are left to future research. In particular, one would like to study models for local names. Another question concerns implementation: How expensive are local names in practice? There exists a prototype implementation of λν in Yale Haskell, but it is not sufficiently integrated with the compiler to answer questions of efficiency.

Acknowledgements This work was supported in part by grant N00014-91-J-4043 from DARPA. I thank Kung Chen, Vincent Dornic and Dan Rabin for their comments on earlier versions of the paper. I had many important discussions with them and also with Paul Hudak. John Launchbury, Jayadev Misra, David Turner and Phil Wadler also commented on this work in useful discussions.

References

[1] H. P. Barendregt. The Lambda Calculus: its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984.

[2] E. Crank and M. Felleisen. Parameter-passing and the lambda-calculus. In Proc. 18th ACM Symposium on Principles of Programming Languages, Orlando, Florida, pages 233–244, January 1991.

[3] N. de Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae, 34:381–392, 1972.

[4] M. Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17:35– 75, 1991.

[5] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

[6] P. Hudak and D. Rabin. Mutable abstract datatypes – or – how to have your state and munge it too. Research Report YALEU/DCS/RR-914, Yale University, Department of Computer Science, July 1992.

[7] D. E. Knuth and P. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Compuatational Problems in Abstract Algebra, pages 263–297. Pergamon, Oxford, 1970.

[8] J. Launchbury. Lazy imperative programming. In SIPL ’93 ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, pages 46–56, June 1993. Yale University Research Report YALEU/DCS/RR-968.

[9] I. Mason and C. Talcott. Axiomatising operational equivalence in the presence of side effects. In IEEE Symposium on Logic in Computer Science, pages 284– 303, Asilomar, California, June 1989.

[10] I. A. Mason and C. L. Talcott. References, local variables, and operational reasoning. In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 186–197, Los Alamitos, California, June 1992. IEEE Computer Society Press.

[11] R. Milner. Elements of interaction. Communications of the ACM, 36(1):78–89, January 1993. Turing Award lecture.

[12] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I. Information and Computation, 100:1– 40, 1992.

[13] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, II. Information and Computation, 100:41–77, 1992.

[14] E. Moggi. Computational lambda-calculus and monads. In Proceedings 1989 IEEE Symposium on Logic in Computer Science, pages 14–23. IEEE, June 1989.

[15] M. Odersky. A syntactic method for proving observational equivalences. Research Report YALEU/DCS/RR-964, Department of Compter Science, Yale University, May 1993.

[16] M. Odersky. A syntactic method for proving observational equivalences. Research Report YALEU/DCS/RR-964, Department of Compter Science, Yale University, May 1993.

[17] M. Odersky and D. Rabin. The unexpurgated callby-name, assignment, and the lambda-calculus. Research Report YALEU/DCS/RR-930, Department of Computer Science, Yale University, May 1993.

[18] M. Odersky, D. Rabin, and P. Hudak. Call-by-name, assignment, and the lambda calculus. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 43–56, January 1993.

[19] S. L. Peyton Jones and P. Wadler. Imperative functional programming. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 71–84. ACM Press, January 1993.

[20] J. C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.

[21] J. G. Riecke. Delimiting the scope of effects. In Proc. Conf. on Functional Programming and Computer Architecture, pages 146–155, June 1993.

[22] V. Swarup, U. S. Reddy, and E. Ireland. Assignments for applicative languages. In J. Hughes, editor, Functional Programming Languages and Computer Architecture, pages 192–214. Springer-Verlag, August 1991. Lecture Notes in Computer Science 523.

[23] P. Wadler. Comprehending monads. In Proc. ACM Conf. on Lisp and Functional Programming, pages 61– 78, June 1990.

[24] P. Wadler. The essence of functional programming. In Proc.19th ACM Symposium on Principles of Programming Languages, pages 1–14, January 1992.

[25] S. Weeks and M. Felleisen. On the orthogonality of assignments and procedures in Algol. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 57–70. ACM Press, January 1993.