A simply typed context calculus with first-class environments

Masahiko Sato^{1}, Takafumi Sakurai^{2}, and Yukiyoshi Kameyama^{1}

1 Graduate School of Informatics, Kyoto University

                  {masahiko,kameyama}@kuis.kyoto-u.ac.jp

2 Department of Mathematics and Informatics, Chiba University

                       sakurai@math.s.chiba-u.ac.jp

Abstract. We introduce a simply typed λ-calculus λκε which has both contexts and environments as first-class values. In λκε, holes in contexts are represented by ordinary variables of appropriate types and hole filling is represented by the functional application together with a new abstraction mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context. λκε is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing. The traditional method of defining substitution does not work for our calculus. So, we also introduce a new method of defining substitution. Although we introduce the new definition of substitution out of necessity, the new definition turns out to be conceptually simpler than the traditional definition of substitution.

1 Introduction

Informally speaking, a context (in λ-calculus) is a λ-term with some holes in it. For example, writing [ ] for a hole, λy. [ ] is a context, and by filling the hole in it with x + y, we get λy. x + y. By this operation, the variable y in x + y gets captured and becomes bound in λy. x + y, and the variable x remains to be free. So, unlike substitution, hole filling may introduce new and intended bound variables.

Recently there have been several attempts to formalize the notion of context and thereby make computing with contexts possible. For example, Talcott [16], Lee-Friedman [8], Dami [5], Hashimoto-Ohori [7], Sands [13], Mason [9] and Bognar-de Vrijer [3] made notable contributions. However, as far as we know, there is as yet no proposal of a language which has contexts as first-class values and which is at the same time pure in the following sense. We understand that a functional language is pure^{1} if (i) it is a conservative extension of the untyped or simply typed λβ-calculus, (ii) confluent and (iii) strongly normalizing (SN) if the language is typed and has preservation of strong normalization (PSN) property if the language is untyped. The conservative extension property guarantees that

1 We have introduced this notion of purity in [15].

the language is logically well-behaved and the confluence property and SN or PSN would guarantee that the language is computationally well-behaved.

In this paper, we introduce the calculus λκε (κ is for context and ε is for environment) which is pure in the above sense and which has contexts and environments as its first class values, so that we can bind contexts and environments to variables and return them as the values of computations. λκε is a simply typed calculus, and in λκε, holes are represented by ordinary variables of appropriate types (which we will call hole types) and hole filling is represented by the functional application together with a new abstraction mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context.

We now illustrate some of the difficulties we face in formalizing the notion of context, and explain our solution informally by relating it to previous works. First, let us consider the context:

a[ ] ≡ λx. (λy. x + [ ])3.

If we fill the hole in a[ ] with the term x + y, we get

a[x + y] ≡ λx. (λy. x + (x + y))3.

By β-reducing it, we can convert a[x + y] to λx. x + (x + 3). Since we wish to compute with contexts, we would also like to reduce the β-redex (λy. x + [ ])3 in a[ ]. If we reduce it naïvely, we get x + [ ], so that a[ ] reduces to λx. x + [ ]. Now, if we fill the hole in λx. x + [ ] with x + y, we get λx. x + (x + y). This shows that hole filling and β-reduction do not commute if we define hole filling and β-reduction as above. In this example, we can note that the hole in the original context a[ ] is within the scope of λx and λy, while the hole in the β-reduced context is only within the scope of λx. This means that a part of the information as to which variables should be captured at the hole is lost if one reduces a β-redex which has a hole in it. Hashimoto-Ohori [7] did not solve this problem. Instead they put restriction on the β-reduction rule in their system and prohibited such β-reductions like the above example.

To solve this problem, we introduce the type A^{E} which represents the set of objects obtained by abstracting objects of type A with respect to a set E = {x_{1}, …, x_{n}} of variables. Canonical objects of type A^{E} are abstracts of the form κE. a where a is of type A and the κE binder declares that the variables in E should be understood as local in a. Moreover, E is also a type and its canonical elements are environments of the form {a_{1}/x_{1}, …, a_{n}/x_{n}}. Then, an object a of type A^{E} can be instantiated to an object b of type A by applying the abstract a to an environment e = {a_{1}/x_{1}, …, a_{n}/x_{n}}. We write a·e for the application of the abstract a to the environment e. For example, (κ{x, y}. x + y)·{1/x, 2/y} can be reduced to 3.

In this setting, we can represent the above context a[ ] as

C ≡ λx. (λy. x + X·{x/x, y/y})3

where X represents the hole and its type is of the form A^{{x,y}}. Now, suppose that we wish to fill the hole X with the term x + y. Then, we can achieve this hole filling by substituting κ{x, y}. x + y for X in C. By this substitution, we have:

D ≡ λx. (λy. x + (κ{x, y}. x + y)·{x/x, y/y})3.

D can be reduced to λx. (λy. x + (x + y))3, which can be further reduced to λx. x + (x + 3) as expected. Let us now see what happens if we reduce the β-redex in C first and then fill the hole with x + y. By β-reducing C, we get λx. x + X·{x/x, 3/y}. Substituting κ{x, y}. x + y for X in this term, we have

λx. x + (κ{x, y}. x + y)·{x/x, 3/y},

which we can further reduce to λx. x + (x + 3). We can thus see that hole filling and β-reduction commute in this case.

The idea of decorating a hole with an environment is due to Talcott [16], and Mason [9] also used this idea in his calculus of contexts that has contexts as first-class values. However, in Mason’s system, environments appear in a term containing holes only as annotations. This means that such environments are objects outside the system. We present our calculus λκε as an extension of λε [15] which is a simply typed λ-calculus that has environments as first class values. So, environments are first-class objects in λκε. Moreover, Mason defines hole filling only as a meta-level operation. Therefore, although contexts are firstclass values in his system, one cannot compute hole filling within his system. In contrast to this, we can compute hole filling within our system. For example, we can express the above example of filling a[ ] with x + y as follows:

(λX. λx. (λy. x + X·{x/x, y/y})3)(κ{x, y}. x + y).

We can compute the above term in λκε, and we get λx. x + (x + 3).

We now turn to another problem in the formalization of contexts. Consider the informal context λx. [ ]. If we fill the hole in this context with x, we get the term λx. x. This term is α-equivalent to λy. y. What is the context which is α-equivalent to λx. [ ] and which, when filled with x, becomes λy. y? It is certainly preferable that such a context exists, since, otherwise, hole filling and α-conversion will not always commute. A naïve attempt is to α-convert λx. [ ] to λy. [ ]. But this does not work, since filling λy. [ ] with x results in λy. x which is not α-equivalent to λy. y. We can solve this problem easily in our setting as follows. In λκε, the context λx. [ ] is written as λx. X·{x/x} and this context is α-equivalent to λy. X·{y/x}. Filling these holes in these two contexts with x is achieved by substituting κ{x}. x for X in these contexts, and the results are λx. (κ{x}. x)·{x/x} and λy. (κ{x}. x)·{y/x} respectively. Then they are reduced to λx. x and λy. y as expected.

In this paper we also introduce a new method of defining substitution. As we explain below, the traditional method of defining substitution does not work for our calculus. We are therefore forced to use the new method, but, we believe our new definition of substitution is mathematically cleaner than the traditional method of defining substitution. We now give an example where the traditional method of defining substitution fails to work. By way of comparison, we first consider the λ term a ≡ λx. x + y. What is the result of substituting x for y in a? We must be careful enough to avoid the variable clash and rename the bound variable x in a to a fresh variable, say, z, and we get λz. z + x as the result of the substitution. Now consider the abstract b ≡ κ{x}. x + y. What will be the result c of substituting x for y in b? If we perform substitution by the same method as above, we get κ{z}. z + x which is wrong for the following reason. Note that b·{2/x} reduces to 2 + y. So, c·{2/x} must reduce to 2 + x. However, we cannot reduce (κ{z}. z + x)·{2/x} since the argument {2/x} does not match the binder κ{z}. By the same token, the term (κ{z}. z + x)·{2/x} is not even typable. We can thus see that, unlike variables bound by the λ binder, we cannot rename variables bound by the κ binder. To cope with this situation, we introduce a new method of defining substitution where we rename free variables (if necessary) to achieve the capture avoiding substitution. So, our substitution will yield κ{x}. x + ♯x as the result of substituting x for y in b, where ♯x in the scope of the κ{x} binder is a renamed form of the free variable x and it stands for the free variable x.

The paper is organized as follows. In section 2, we introduce the type system of λκε, and introduce derivation rules that are used to define (typed) terms together with their types and free variables. There, we define variables so that they naturally contain both ordinary variables with names and variables as de Bruijn indices. In section 3, we define substitution as a meta-level operation. In section 4, we give reduction rules of λκε and give some examples of computations in λκε. In section 5, we show that λκε enjoys a number of desirable properties such as confluence and strong normalizability. In section 6, we give concluding remarks. Due to lack of space, we have omitted almost all proofs. A full version of

this paper with proofs is accessible at http://www.sato.kuis.kyoto-u.ac.jp/
~masahiko/index-e.html.

2 The Type System

In this section, we define the type system of λκε by defining the notion of a derivation of a typing judgment. A typing judgement is an expression of the form Γ ⊢ a : A, and if it is derivable then it means that the expression a is a term whose type is A and whose set of free variables is Γ.

In the following we assume that we have given a finite set of atomic types which we do not specify further in this paper. We also assume that we have infinitely many identifiers (i). Then, we define variables and types simultaneously as follows.

A variable (we will use x, y, z, u, v as meta-variables for variables) is a triple ⟨k, i, A⟩ where k is a natural number, i is an identifier and A is a type. A variable ⟨k, i, A⟩ is called a pure variable if k = 0. Types (A, B) are defined by the following grammar:

A, B ::= K | E | A ⇒ B | A^{E}

where K ranges over atomic types and E over finite sets of pure variables.

In the following, we will use declaration as a synonym for a finite set of variables and pure declaration as a synonym for a finite set of pure variables. We use Γ, Δ etc. as meta variables for declarations and E, F as meta variables for pure declarations. A pure declaration {x_{1}, …, x_{n}} will also be called an environment type since it is the type of environments whose canonical forms are elements of the form {a_{1}/x_{1}, …, a_{n}/x_{n}}.

If x ≡ ⟨k, i, A⟩, then we call k the level of x, i the name of x and A the type of x. In this case, we sometimes write x^{A} for x and also write ♯^{l}x for ⟨k + l, i, A⟩, ♯x for ♯^{1}x, and x̄ for ⟨0, i, A⟩.

We write V for the set of all the variables. Let E be a pure declaration. We define a function ⇑^{E} : V → V−E by ⇑^{E}(x):=♯x if x̄ ∈ E and ⇑^{E}(x):=x if x̄ ∉ E. We also define ⇓_{E} as the inverse function of ⇑^{E}. Note that ⇓_{E}(x) is defined only when x ∉ E. For example, if E is empty, then ⇑^{E}(x) = x for any variable x. If E is {x, y}, then ⇑^{E}(x) = ♯^{1}x, ⇑^{E}(♯^{1}x) = ♯^{2}x, ⇑^{E}(z) = z, ⇓_{E}(♯^{2}x) = ♯^{1}x, and ⇓_{E}(x) is undefined. We will use ⇑^{E} later to systematically rename variables to avoid collision with the variables in E.

Let Γ be a declaration and E, F be pure declarations. We define the declarations Γ ⇑^{E} and Γ ⇓_{E} as follows:

Γ ⇑^{E} := {⇑^{E}(x) | x ∈ Γ }, Γ ⇓_{E} := {⇓_{E}(x) | x ∈ Γ },

where Γ ⇓_{E} is defined only when Γ ∩ E is empty. Furthermore, given two declarations E and F, we define a function ⇕_{F}^{E} : V → V as follows.

⇕_{F}^{E}(x) := \{ \begin{matrix}⇑^{E}(x) & if x ∈ F , \\ ⇓_{F} (x) & if x ∈ E ⇑^{F} , \\ x & otherwise. \end{matrix}

We give a few examples here. If E is {x}, then ⇕_{E}^{E}(x) = ♯x, ⇕_{E}^{E}(♯x) = x, and ⇕_{E}^{E}(♯^{2}x) = ♯^{2}x. If E is {x, y} and F is {x}, then ⇕_{F}^{E}(x) = ♯x, ⇕_{F}^{E}(♯x) = x, ⇕_{F}^{E}(y) = y, and ⇕_{F}^{E}(z) = z. As we will see in the next section, we will use ⇕_{F}^{E} to rename variables when the order of two binders are exchanged.

Using the function ⇕_{F}^{E}, we define the declaration Γ ⇕_{F}^{E} as follows.

Γ ⇕_{F}^{E} := {⇕_{F}^{E}(x) | x ∈ Γ }.

Lemma 1. We have the following equations.

1. Γ ⇑^{E} ∩ E = ∅.

2. Γ ⇑^{E} ⇓_{E} = Γ. If Γ ∩ E = ∅, then Γ ⇓_{E} ⇑^{E} = Γ.

3. ((Γ − E)⇓_{E} − F)⇓_{F} = ((Γ ⇕_{E}^{F} − F)⇓_{F} − E)⇓_{E}.

A typing judgment is an expression of the form Γ ⊢ a : A where Γ is a declaration and A is a type. We have the typing rules in Figure 1 that are used to derive typing judgments, where those rules whose names end with ‘I’ (‘E’) introduce (eliminate, respectively) the types mentioned in the rule names.

An expression a is said to be a term if a typing judgment of the form Γ ⊢ a : A is derivable for some Γ and A. In this case, we say that Γ is the set of free

{x} ⊢ x^{A} : A (axiom)

{Γ ⊢ b : B \atop (Γ − \{x\})⇓_{\{x\}} ⊢ λx^{A}. b : A ⇒ B} (⇒I)  \begin{matrix}Γ ⊢ b : A ⇒ B & Δ ⊢ a : A \\ Γ ∪ Δ ⊢ ba : B \end{matrix} (⇒E)

{Γ ⊢ a : A \atop (Γ − E)⇓_{E} ⊢ κE. a : A^{E}} (absI)  \begin{matrix}Γ ⊢ a : A^{E} & Δ ⊢ e : E \\ Γ ∪ Δ ⊢ a·e : A \end{matrix} (absE)

\begin{matrix}Γ_{1} ⊢ a_{1} : A_{1} & ⋯ & Γ_{n} ⊢ a_{n} : A_{n} \\ Γ_{1} ∪ … ∪ Γ_{n} ⊢ \{a_{1}/x_{1}^{A_{1}}, …, a_{n}/x_{n}^{A_{n}}\} : \{x_{1}, …, x_{n}\} \end{matrix} (envI)
\begin{matrix}Γ ⊢ e : E & Δ ⊢ a : A \\ Γ ∪ (Δ − E)⇓_{E} ⊢ e[[a]] : A \end{matrix} (envE)

In (⇒I), the variable x must be pure. In (envI), the variables x_{1}, …, x_{n} must be pure and mutually distinct.

Fig. 1. Typing rules of λκε

variables in a and write FV(a) for it and also say that A is the type of a and write TY(a) for it. Note that if e ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}, then TY(e) is {x_{1}, …, x_{n}}. We will say that these variables are bound by e. We also write T for the set of all the terms. A term is canonical if it is of the form λx.b, {a_{1}/x_{1}, …, a_{n}/x_{n}} or κE. a, that is, if it is obtained by one of the introduction rules. A term is said to be an environment term if its type is an environment type.

In (⇒I), since free variables in b are within the scope of λx^{A}, ⇓_{{x}} should be applied to Γ − {x} to refer to the variables in b from the outside of the binder. By the same reason, ⇓_{E} is used in (absI) and (envE). We have explained the intuitive meaning of the typing rules (absI) and (absE) for introducing and eliminating abstractions in section 1. The remaining typing rules come from λε, and the reader is referred to [15] for the detailed explanation of these rules. Here, we only remark that the term e[[a]] in the (envE) rule means to evaluate a in the environment e. So, for example, if e ≡ {λx. λy. x + y/z, 1/x, 2/u}, then e[[zxy]] is evaluated to 1 + y. Note that z and x in zxy are bound by e and y is free in e[[zxy]].

We give below a simple example of a derivation. In the example below, we assume that x and y are distinct pure variables.

{y} ⊢ y : A ⇒ A ⇒ B (axiom) {♯x} ⊢ ♯x : A (axiom) {y, ♯x} ⊢ y(♯x) : A ⇒ B (⇒E) {x} ⊢ x : A (axiom) {y, ♯x, x} ⊢ y(♯x)x : B (⇒E) {y, x} ⊢ λx. y(♯x)x : A ⇒ B (⇒I) {} ⊢ κ{x, y}. λx. y(♯x)x : (A ⇒ B)^{{x,y}} (absI).

It is easy to see that if Γ ⊢ a : A is derivable, then we can completely recover the entire derivation tree uniquely by inspecting the typed term a^{2}.

We have two kinds of abstractions λ and κ — λ abstracts nameless variables and κ abstracts named variables. We can eliminate λ by taking the distinguished named variable ι, replacing λ by κ{ι}, and using the de Bruijn index method that we explain in the next section. But we did not do so, because we want to design λκε so that it extends the traditional λ-calculus directly. (See also the comments at the end of section 3.)

3 Substitution

In this section we define substitution as a meta-level syntactic operation. Our definition is conceptually simpler than the ordinary definition of substitution where α-conversion is sometimes necessary to avoid the unwanted capture of variables. Our method of defining substitution is a simple extension of the method due to de Bruijn [4].

Before going into technical details, we explain our method by comparing it with the traditional method of defining substitution for terms with named variables [1] and also with the method invented by de Bruijn [4]. In the traditional method, for example, substitution of x for y in λx. y is done by first α-converting λx. y to, say, λz. y and then replacing y by x. Thus, the result of substitution is λz. x. The α-conversion was necessary to avoid unwanted capturing of x by the λx binder in the original term. So, in this approach, one has to define terms as equivalence classes of concrete terms modulo α-equivalence, and therefore, we have to check the well-definedness of the substitution, since we first define the substitution operation on concrete terms. Also, in this approach, one has to define α-equivalence before substitution, but the definition of α-conversion requires the notion of renaming variables which is similar to substitution.

We think that such complication in the traditional definition of substitution comes from the fact that avoidance of capturing free variables was achieved by the renaming of the name of the λ-binder. Our approach here is to avoid the capture of free variables by systematically renaming the free variables which would otherwise be captured^{3}. For instance, in case of the above example of substituting x for y in λx. y, we rename x to ♯x and substitute ♯x for y, so that the result of the substitution becomes λx. ♯x. We note that in the resulting term λx. ♯x, the variable ♯x is different from x within the scope of λx, and that ♯x refers to x outside the scope of λx. From this explanation, it should be easy to understand that the result of substituting x ∗ z for y in λx. λx. x + y is λx. λx. x + (♯^{2}x ∗ z). As can be seen from this example, we rename only those variables that would otherwise be captured. Therefore, in case capturing does

2 Strictly speaking, in order to have this property, we have to identify those derivations which are the same up to the difference of ordering of the premises of the (envI) rule.

3 We have introduced this idea of renaming free variables in [14].

not occur, the result of substitution obtained by our method is the same as that obtained by the traditional method.

We give another example to clarify the intuitive idea. Suppose that x, y, z are distinct pure variables. Then the following terms are all α-equivalent with each other.

λx. λy. (λz. y(zx))(yx)
≡_{α} λ♯^{0}x. λ♯^{0}x. (λ♯^{0}x. ♯^{1}x(♯^{0}x ♯^{2}x))(♯^{0}x ♯^{1}x)
≡_{α} λx. λy. (λx. y(x ♯x))(yx).

If we write 0, 1 and 2 for ♯^{0}x, ♯^{1}x and ♯^{2}x, respectively, in the second term above, we get λ0. λ0. (λ0. 1(02))(01). Therefore, this term is essentially the same as the representation of the first term in de Bruijn indices. We can therefore see that our terms are natural extensions of both traditional concrete terms with variable names and name free terms á la de Bruijn that use indices.

Let ϕ : V → V be a (possibly) partial function such that ϕ(x) may be undefined for some x ∈ V. We extend this function to the function \overline{ϕ} : T → T as follows. \overline{ϕ} will be total if and only if ϕ is total.

1. \overline{ϕ}(x) := ϕ(x).

2. \overline{ϕ}(λx. a) := λx. \overline{ϕ_{\{x\}}}(a).

3. \overline{ϕ}(ba) := \overline{ϕ}(b)\overline{ϕ}(a).

4. \overline{ϕ}(κF. a) := κF. \overline{ϕ_{F}} (a).

5. \overline{ϕ}(a·f) := \overline{ϕ}(a)·\overline{ϕ}(f).

6. \overline{ϕ}(\{a_{1}/x_{1}, …, a_{n}/x_{n}\}) := \{\overline{ϕ}(a_{1})/x_{1}, …, \overline{ϕ}(a_{n})/x_{n}\}.

7. \overline{ϕ}(e[[a]]) := \overline{ϕ}(e)[[\overline{ϕ_{TY(e)}}(a)]].

where, for each declaration E, ϕ_{E} : V → V is defined by

ϕ_{E}(x) := \{ \begin{matrix}x & if x ∈ E, \\ ⇑^{E}(ϕ(⇓_{E}(x))) & otherwise. \end{matrix}

(We note that if ϕ is not total, ϕ_{E} is also not total.)

We define the push operation ↑^{E} by putting a↑^{E}:=\overline{⇑^{E}}(a), the pull operation ↓_{E} by putting a↓_{E} := \overline{⇓_{E}}(a), and the exchange operation ↕_{F}^{E} by putting a↕_{F}^{E} := \overline{⇕_{F}^{E}}(a).

Let us give a few examples here. Let E be {x, y}.

(λx. x(♯^{3}x))↑^{E} ≡ \overline{⇑^{E}}(λx. x(♯^{3}x))
≡ λx. \overline{⇑^{E}_{\{x\}}}(x(♯^{3}x))
≡ λx. (\overline{⇑^{E}_{\{x\}}}(x))(\overline{⇑^{E}_{\{x\}}}(♯^{3}x))
≡ λx. x(⇑^{{x}}⇑^{E}⇓_{{x}}(♯^{3}x))
≡ λx. x(♯^{4}x).

Note that FV(λx. x(♯^{3}x)) = {♯^{2}x}, and {♯^{2}x}⇑^{E} = {♯^{3}x}, which is equal to FV(λx. x(♯^{4}x)). Similarly, we have (λx. x(♯^{3}x))↓_{E} ≡ λx. x(♯^{2}x).

For the exchange operation, we have:

(λx. (♯x)(♯^{2}x))↕_{{x}}^{{x}} ≡ λx. (♯^{2}x)(♯x),
(λx. (♯x)(♯^{2}x))↕_{{x}}^{{y}} ≡ λx. (♯x)(♯^{2}x),

where x and y are distinct pure variables.

We now define the substitution operation as follows. Let s ≡ {c_{1}/x_{1}, …, c_{n}/x_{n}} be a canonical environment term. Note that TY(s) = {x_{1}, …, x_{n}} in this case. For each term a we define a term a[s] inductively as follows. (We think that the 2nd clause below corresponds to the 2nd clause of the definition of the substitution operation σ : δΛ × Λ → Λ in Fiore-Plotkin-Turi [6], and we think that it should be possible to establish a precise correspondence.)

1. x[s] := \{ \begin{matrix}c_{i} & if x ≡ x_{i} for some i, \\ ⇓_{TY(s)}(x) & otherwise. \end{matrix}

2. (λx. b)[s] := λx. b↕_{{x}}^{TY(s)}[s↑^{{x}}].

3. (ba)[s] := b[s]a[s].

4. (κE. a)[s] := κE. a↕_{E}^{TY(s)}[s↑^{E}].

5. (a·e)[s] := a[s]·e[s].

6. ({a_{1}/x_{1}, …, a_{n}/x_{n}})[s] := {a_{1}[s]/x_{1}, …, a_{n}[s]/x_{n}}.

7. (e[[a]])[s] := e[s][[(a↕_{TY(e)}^{TY(s)})[s↑^{TY(e)}]]].

We call a[s] the result of substituting c_{1}, …, c_{n} for x_{1}, …, x_{n} in a.

Again we give a few examples. Let s be {♯^{3}x/y, (x ♯x)/x}. Then we have:

(λx. x ♯x)[s] ≡ λx. (x ♯x)↕_{{x}}^{{y,x}}[s↑^{{x}}]
≡ λx. (♯x x)[{♯^{4}x/y, (♯x ♯^{2}x)/x}]
≡ λx. (⇓_{{y,x}}♯x)(♯x ♯^{2}x)
≡ λx. x(♯x ♯^{2}x),
(λx. xy)[{z/y}] ≡ λx. xz,

where x, y, z are distinct pure variables.

In the first example, x in λx. x ♯x is bound by λx and ♯x is bound by s. When s goes into the scope of λx, x and ♯x should be renamed to ♯x and x, respectively so that they are bound by λx and s↑^{{x}}.

We can now define the α-equivalence using substitution as follows.

1. x ≡_{α} x

2. If a[{z/x}] ≡_{α} a′[{z/x′}], then λx. a ≡_{α} λx′. a′ where z is a variable such that z ∉ FV(a) ∪ FV(a′) ∪ {x, x′}.

3. If b ≡_{α} b′ and a ≡_{α} a′, then ba ≡_{α} b′a′.

4. If a ≡_{α} a′, then κE. a ≡_{α} κE. a′.

5. If a ≡_{α} a′ and e ≡_{α} e′, then a·e ≡_{α} a′·e′.

6. If a_{1} ≡_{α} a′_{1}, ⋯, a_{n} ≡_{α} a′_{n}, then {a_{1}/x_{1}, …, a_{n}/x_{n}} ≡_{α} {a_{1}/x_{1}, …, a_{n}/x_{n}}.

7. If a ≡_{α} a′ and e ≡_{α} e′, then e[[a]] ≡_{α} e′[[a′]].

Note that variables bound by κ are not renamed in the 4th clause because κ abstracts named variables. On the other hand, variables bound by λ may be renamed in the 2nd clause bacause λ plays the same role as λ in the traditional λ-calculus.

4 Reduction Rules

In this section we give reduction rules of the λκε calculus. We first define ↦_{λκε} as the union of the following three relations ↦_{λ}, ↦_{κ} and ↦_{ε}.

The relation ↦_{λ} is defined by the following single rule:

(λ) (λx. b)a ↦_{λ} {a/x}[[b]],

and the relation ↦_{κ} is defined by the following single rule:

(κ) (κE. a)·e ↦_{κ} e[[a]].

The relation ↦_{ε} is defined by the following 8 conversion rules.

(gc) e[[a]] ↦_{ε} a↓_{TY(e)}, if TY(e) ∩ FV(a) = ∅.

(var) {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{i}]] ↦_{ε} a_{i} (1 ≤ i ≤ n). (fun) e[[λx. b]] ↦_{ε} λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]]

(funapp) e[[ba]] ↦_{ε} e[[b]]e[[a]].

(abs) e[[κE. a]] ↦_{ε} κE. (e↑^{E})[[a↕_{E}^{TY(e)}]]. (absapp) e[[a·f]] ↦_{ε} e[[a]]·e[[f]].

(env) e[[{a_{1}/x_{1}, …, a_{n}/x_{n}}]] ↦_{ε} {e[[a_{1}]]/x_{1}, …, e[[a_{n}]]/x_{n}}.

(eval) e[[f[[x]]]] ↦_{ε} e[[f]][[x]], if x ∈ TY(f).

The rules other than (eval) are internalized forms of the clauses 1–6 of the definition of substitution in section 3. In these rules we have the environment term e in place of the canonical environment term s, and the rule (gc) is a generalization of the second case of clause 1. We can also internalize clause 7 directly and get a correct rule. But, we do not do so since it will result in a system where the strong normalization property does not hold. Instead we have the (eval) rule which corresponds to a special case of clause 7. Although the (eval) rule is a weak version of clause 7, we will see in Theorem 1 that we can faithfully compute substitution internally by using these reduction rules, and at the same time the system enjoys the strong normalizability (Theorem 6). In fact, as can be seen in, e.g., Melliès [10] and Bloo [2], the strong normalizability of calculi of explicit substitutions and explicit environments is a subtle problem. The reader is referred to [15] for a detailed discussion on our choice of the (eval) rule.

We write a →_{λ} b if b is obtained from a by replacing a subterm c in a by d such that c ↦_{λ} d. Similarly →_{κ}, →_{ε} and →_{λκε} are defined. The transitive closures of these reductions are denoted with asterisk (*), such as →^{∗}_{ε}. The equivalence relation generated by →_{λκε} is denoted by =_{λκε}, namely, the reflexive, symmetric, and transitive closure of →_{λκε}. Similarly =_{ε} is defined.

We give a few examples of reduction sequences. Let s ≡ {(x ♯x)/x, ♯^{3}x/y} in the second example.

(λx. λy. x)y →_{λ} {y/x}[[λy. x]]
→_{ε} λy. ({y/x}↑^{{y}})[[x↕_{{y}}^{{x}}]]
≡ λy. {♯y/x}[[x]] →_{ε} λy. ♯y.
s[[λx. x ♯x]] →_{ε} λx. (s↑^{{x}})[[(x ♯x)↕_{{x}}^{{x,y}}]]
≡ λx. {(♯x ♯^{2}x)/x, ♯^{4}x/y}[[(♯x x)]]
→^{∗}_{ε} λx. (⇓_{{x,y}}♯x)(♯x ♯^{2}x)
≡ λx. x(♯x ♯^{2}x).
(λX. λy. X·{y/y})(κ{y}. y) →_{λ} {κ{y}. y/X}[[λy. X·{y/y}]]
→^{∗}_{ε} λy. (κ{y}. y)·{y/y}
→_{κ} λy. {y/y}[[y]] →^{∗}_{ε} λy. y.

In the first example, y is renamed to ♯y so that it is not captured by the λy binder. The second example corresponds to the example given after the definition of substitution. The third example shows the hole-filling operation where y is captured by the λy binder.

We take an example from Hashimoto-Ohori’s paper [7]. Consider the term (λz. C[x + z])x where C is an (informal) context (λx. [ ] + y)3 and C[x + z] represents the hole-filling operation in the λ-calculus. In Hashimoto-Ohori’s calculus, this term can be written as

a ≡ (λz. (δX.(λu. X^{{u/x}} + y)3) ⊙_{{x/v}} (v + z))x

where X represents a hole, δX abstracts the hole X, and ⊙ is a hole-filling operator. {u/x} and {x/v} (called renamers) annotate X and ⊙ respectively. They are introduced to solve the problem of variable capturing. In our system, the above term can be written as

a ≡ (λz. (λX. (λu. X·{u/x} + y)3)(κ{x}. (x + z)))x.

We can compute this term in many ways, but, here we give two reduction sequences.

a →_{λ} {x/z}[[(λX. (λu. X·{u/x} + y)3)(κ{x}. x + z)]]
→^{∗}_{ε} (λX. (λu. X·{u/x} + y)3)(κ{x}. x + ♯x)
→_{λ} {κ{x}. x + ♯x/X}[[(λu. X·{u/x} + y)3]]
→^{∗}_{ε} (λu. (κ{x}. x + ♯x)·{u/x} + y)3

→_{κ} (λu. {u/x}[[x + ♯x]] + y)3
→^{∗}_{ε} (λu. u + x + y)3
→_{λ} {3/u}[[u + x + y]] →^{∗}_{ε} 3 + x + y.
a →_{λ} (λz. (λX. {3/u}[[X·{u/x} + y]])(κ{x}. x + z))x
→^{∗}_{ε} (λz. (λX. X·{3/x} + y)(κ{x}. x + z))x
→_{λ} (λz. {κ{x}. x + z/X}[[X·{3/x} + y]])x
→^{∗}_{ε} (λz. (κ{x}. x + z)·{3/x} + y)x
→_{κ} (λz. {3/x}[[x + z]] + y)x
→^{∗}_{ε} (λz. 3 + z + y)x
→_{λ} {x/z}[[3 + z + y]] →^{∗}_{ε} 3 + x + y.

We remark that, in the second reduction sequence above, we have first reduced the innermost β-redex (λu. X·{u/x} + y)3. Such a reduction is not possible in Hashimoto-Ohori’s calculus since in their system the β-conversion is prohibited when the redex contains a free hole. Though the roles of X^{{u/x}} and X·{u/x} are similar, u in X^{{u/x}} should always be a variable, while u in X·{u/x} can be substituted by an arbitrary term. This is the reason why our calculus need not put any restriction to the (λ)-reduction rule (the β-conversion).

We also remark on the hole-filling operations without going into the technical details. In Hashimoto-Ohori’s calculus, the renamer ν in ⊙_{ν} works as a variable binder to the second operand of ⊙ (i.e. to the term to be filled into the hole). Because their typing rule of M ⊙_{ν} N causes a side effect to the type of the free hole in N, they had to put the restriction that each free hole may occur at most once. Our κE binder, which plays the similar role to the renamer ν in ⊙_{ν}, does not have such a problem, because it is merely an abstraction.

Therefore, our calculus λκε can be regarded as a natural and flexible extension to Hashimoto-Ohori’s calculus.

5 Properties of λκε

In this section, we show that λκε enjoys a number of desirable properties. We first show that the meta-level operation of substitution is internally realized by the operation of evaluation (Theorem 1), and show some properties of substitution. We also show that λκε enjoys subject reduction property (Theorem 3), confluence property (Theorem 4), conservativity over the simply typed λβ-calculus (Theorem 5), and strong normalizability (Theorem 6). Theorems 4–6 establish the purity of λκε, and as a corollary to the confluence of λκε, we see that the operations of hole filling and β-reduction always commute.

As we have studied in [15], we can internalize the meta-level operation of substitution by means of evaluation terms which are of the form e[[a]]. We can show that the meta-level substitution and the internalized substitution coincide, that is, a[s] =_{κε} s[[a]] holds.

Theorem 1. Let s be a canonical environment term. Then, for any term a, a[s] =_{κε} s[[a]] holds.

Lemma 2 corresponds to the Substitution Lemma [1] in the λ-calculus, that is, M[x := K][y := L] ≡ M[y := L][x := K[y := L]] if x ≢ y and x ∉ FV(L).

Lemma 2 (Substitution Lemma). Let s and t be canonical environment terms. Then, for any term a, a[s][t] ≡ a↕_{TY(s)}^{TY(t)}[t↑^{TY(s)}][s[t]] holds.

Note that the effect of exchanging the order of two substitutions s and t is adjusted by applying the exchange operation ↕_{TY(s)}^{TY(t)} to a and the push operation ↑^{TY(s)} to t. For example, let a be x ♯x, s be {z/x}, and t be {♯^{3}x/y, (x ♯x)/x} in the Lemma. Then, we have

(x ♯x)[s][t] ≡ (z x)[t]
≡ z (x ♯x),
(x ♯x)↕_{{x}}^{{y,x}}[t↑^{{x}}][s[t]] ≡ (♯x x)[{♯^{4}x/y, (♯x ♯^{2}x)/x}][s[t]]
≡ (x (♯x ♯^{2}x))[{z/x}]
≡ z ((♯x ♯^{2}x)↓_{{x}})
≡ z (x ♯x).

(See also the example below the definition of the substitution in seciton 3.) The reduction is compatible with substitution.

Theorem 2. If a →^{∗}_{λκε} b, then a[s] →^{∗}_{λκε} b[s].

The following theorems will establish the purity of our calculus.

Theorem 3 (Subject Reduction). If Γ ⊢ a : A and a →_{λκε} b, then Δ ⊢ b : A for some Δ ⊆ Γ.

Theorem 4 (Confluence). →_{λκε} on λκε-terms is confluent.

Proof. The proof is a straightforward extension of that for λε, and we omit the details here. □

We remark that from the confluence of λκε, we see that the operations of hole filling and β-reduction always commute, since in λκε, hole filling is computed by reducing a term of the form (λX. a)(κE. b).

We next prove that λκε is a conservative extension of the simply typed lambda calculus λβ. For this purpose, we embed the λβ-terms in the λκε-terms. A λβ-term is a λκε-term such that its typing derivation uses the (axiom), (⇒I), (⇒E) rules only, and all the variables used in the (axiom) rule are pure variables. The α- and β-conversions over λβ terms are defined as usual.

Theorem 5 (Conservativity). Let a and b be λβ-terms. We have a →^{∗}_{αβ} b in λβ if and only if a →^{∗}_{λκε} b′ and b ≡_{α} b′ for some term b′ in λκε.

Proof. (Only-if part) easily follows from the fact that the β-conversion can be simulated by the λε-reduction rules up to the α-equivalence.

(If-part) can be proved in the same way as in [15], which uses the translation from λε-terms to λβ-terms. □

Theorem 6 (Strong Normalizability). If Γ ⊢ a : A, then a is strongly normalizable.

Proof. We can prove this theorem in the same way as the strongly normalizability theorem of λε [15], because we can treat the cases of (abs) and (absapp) similarly to the cases of (fun) and (funapp). □

6 Conclusion

We have introduced a simply typed λ-calculus which has both contexts and environments as first-class values. We have shown that our calculus, λκε, is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing. Thus we have shown that our language is pure in the sense of [15] and also we have realized our hope, which we stated in the conclusion of [15], to design a pure language that has both contexts and environments as first-class values. To the best of our knowledge, λκε is the first such language.

We have also introduced a new method of defining substitution which is conceptually simpler than traditional methods. We think that our method is also suitable for representing terms and computing substitutions on the computer.

We conclude the paper by comparing our calculus with some related works. The style of the presentation of our paper is very close to that of Hashimoto-Ohori [7]. Both our calculus and the calculus presented in [7] are simply typed calculi which include simply typed λβ-calculus as their subcalculus. The system in [7] enjoys subject reduction property and is confluent. However, neither conservativity over simply typed λβ-calculus nor strong normalizability are shown in the paper. Therefore, it is not known whether their system is pure in our sense^{4}. Also, their calculus has severe restrictions in that (i) each context may have at most one hole in it, and (ii) as we have explained in section 1, the application of the β-reduction is allowed only when the β-redex has no hole in it. Our calculus does not have such restrictions and β-reduction and hole-filling always commute.

Dami’s calculus λN [5] is a very simple and powerful calculus with named variables. It is possible to represent both contexts and hole-filling in λN. However, this is done by a translation of λβ calculus into λN. Therefore, it is hard to read the translated terms as contexts. On the other hand, Mason [9] introduces a system with first-class contexts in which contexts are directly represented as terms in his calculus. However, he defines hole-filling as a meta-level operation.

4 Sakurada [12] proved the strong normalizability of Hashimoto-Ohori’s calculus by interpreting it in λε.

It is therefore not possible to compute hole-filling within his system. Unlike these systems, in λκε, contexts are directly representable as terms of λκε, and we can compute hole-filling within λκε.

Sands [13] uses Pitts’ [11] definition of contexts and shows that hole-filling commutes with many relations on terms including α-equivalence. Pitts defines contexts by representing holes by (higher-order) function variables where each function variable has a fixed arity, and by representing hole-filling by substitution of a meta-abstraction for a function variable. For example, the term

λx. (λy. x + X·{x/x, y/y})3

in λκε can be expressed by

λx. (λy. x + ξ(x, y))3

where ξ is a binary function variable, and the substitution

{κ{x, y}. x + y/X}

in λκε can be expressed by

[(x, y)(x + y)/ξ].

As can be seen by this example, Pitts’ representation of contexts is structurally similar to ours, but the statuses of contexts are quite different. That is, Pitts’ contexts are meta-level objects outside the object language (λ calculus in case of the above example) and our contexts are internal objects of our language λκε. Because of this meta-level status of Pitts’ contexts, Sands [13] could successfully attach contexts to many languages and could prove that hole-filling commutes with many rules in a uniform way. In contrast to this, we have been interested in internalizing such meta-level objects as contexts and environments so that we can enrich λ-calculus to a more powerful programming language.

References

1. Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, North-Holland, 1981.

2. Bloo, R. and Rose, K.H., Preservation of Strong Normalization in Named Lambda Calculi with Explicit Substitution and Garbage Collection, Proceedings of CSN’95 (Computer Science in Netherlands), van Vliet J.C. (ed.), 1995.

    (ftp://ftp.diku.dk/diku/semantics/papers/D-246.ps)

3. Bognar, M. and de Vrijer, R., A calculus of lambda calculus contexts, available at:

    http://www.cs.vu.nl/~mirna/new.ps.gz.

4. de Bruijn, D. G., Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem, Indag. Math. 34, pp. 381-392, 1972.

5. Dami, L., A Lambda-Calculus for Dynamic Binding, pp. 201-231, Theoretical Computer Science 192, 1998.

6. Fiore, M., Plotkin, G., and Turi, D., Abstract Syntax and Variable Binding (Extended Abstract), Proc. 14th Symposium on Logic in Computer Science, pp. 193-202, 1999.

7. Hashimoto, M. and Ohori, A., A typed context calculus, Preprint RIMS-1098, Res. Inst. for Math. Sci., Kyoto Univ., 1996, Journal version is to appear in Theoretical Computer Science.

8. Lee, S.-R., and D. P. Friedman, Enriching the Lambda Calculus with Contexts: Toward a Theory of Incremental Program Construction, ACM SIGPLAN Notices, Proc. International Conference on Functional Programming, pp. 239-250, 1996.

9. Mason, I., Computing with Contexts, Higher-Order and Symbolic Computation 12, pp. 171-201, 1999.

10. Melliès, P.-A., Typed λ-calculi with explicit substitutions may not terminate, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902, pp. 328-349, 1995.

11. Pitts, A.M., Some notes on inductive and co-inductive techniques in the semantics of functional programs, Notes Series BRICS-NS-94-5, Department of Computer Science, University of Aarhus, 1994.

12. Sakurada, H., An interpretation of a context calculus in an environment calculus, Master Thesis, Dept. of Information Science, Kyoto Univ., 1999 (in Japanese).

13. Sands, D., Computing with Contexts - a simple approach, Proc. Higher-Order Operational Techniques in Semantics, HOOTS II, 16 pages, Electronic Notes in Theoretical Computer Science 10, 1998.

14. Sato, M., Theory of Symbolic Expressions, II, Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21, pp. 455-540, 1985.

15. Sato, M., Sakurai T., and Burstall, R., Explicit Environments, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 1581, pp. 340-354, 1999.

16. Talcott, C., A Theory of binding structures and applications to rewriting, Theoretical Computer Science 112:1, pp. 99-143, 1993.

A Appendix: Proofs

In the appendix, we allow any variables for bound variables, that is, variables in λ binders, variables in κ binders, and variables in environment types need not be pure variables. In the following, we will generalize ⇑^{E}, ⇓_{E}, and ⇕_{F}^{E} so that E and F can be declarations, but all the Lemmas and Theorems remain valid. (We use E, F as meta variables for declarations.)

We write V for the set of all the variables. We define an order ≤ on V by x ≤ y iff y ≡ ♯^{l}x for some l ≥ 0. Let E be a declaration. We define ⇑^{E} as the unique bijection from V to V − E which is monotone in the sense that for any variables x, y such that x ≤ y we have ⇑^{E}(x) ≤ ⇑^{E}(y). We also define ⇓_{E} as the inverse function of ⇑^{E}. For example, if E is {♯^{1}x, ♯^{3}x}, then ⇑^{E}(♯^{0}x) = ♯^{0}x, ⇑^{E}(♯^{2}x) = ♯^{4}x, ⇑^{E}(♯^{3}x) = ♯^{5}x, ⇓_{E}(♯^{2}x) = ♯^{1}x, and ⇓_{E}(♯^{3}x) is undefined.

Given two declarations E and F, we define a function ⇕_{F}^{E} : V → V as follows.

⇕_{F}^{E}(x) := \{ \begin{matrix}⇑^{E}(x) & if x ∈ F , \\ ⇓_{F} (x) & if x ∈ E ⇑^{F} , \\ ⇑^{E}(⇑^{F} (⇓_{E}(⇓_{F} (x)))) & otherwise. \end{matrix}

Since the above definition involves partial functions ⇓_{E} and ⇓_{F}, the function ⇕_{F}^{E} may also be partial. But, the fact is that ⇕_{F}^{E} is a bijection from V to V, and we can see this as follows. We will be done if we can check the claim that ⇕_{E}^{F}(⇕_{F}^{E}(x)) = x holds for any x ∈ V, since by the same argument we can see that ⇕_{F}^{E}(⇕_{E}^{F}(x)) = x holds for any x ∈ V. We prove the claim by cases.

(i) If x ∈ F, then ⇕_{E}^{F}(⇕_{F}^{E}(x)) = ⇕_{E}^{F}(⇑^{E}(x)) = x, since ⇑^{E}(x) ∈ F ⇑^{E}. (ii) If x ∈ E ⇑^{F}, then there exists a y ∈ E such that x = ⇑^{F} (y). Since ⇓_{F} (x)

is defined and equal to y, we have ⇕_{E}^{F}(⇕_{F}^{E}(x)) = ⇕_{E}^{F}(⇓_{F} (x)) = ⇕_{E}^{F}(y) = ⇑^{F} (y) = x.

(iii) Otherwise, ⇓_{F} (x) is defined since x ∉ F, and ⇓_{E}(⇓_{F} (x)) is defined since ⇓_{F} (x) ∉ E. Hence ⇕_{F}^{E}(x) is defined. It is easy to see ⇓_{F} (⇓_{E}(⇕_{F}^{E}(x))) is defined and equal to ⇓_{E}(⇓_{F} (x)). Hence ⇕_{E}^{F}(⇕_{F}^{E}(x)) = ⇑^{F} (⇑^{E}(⇓_{E}(⇓_{F} (x)))) = x.

We give an example here. If E is {x, ♯x} and F is {x}, then ⇕_{F}^{E}(x) = ♯^{2}x, ⇕_{F}^{E}(♯x) = x, ⇕_{F}^{E}(♯^{2}x) = ♯^{1}x, and ⇕_{F}^{E}(♯^{3}x) = ♯^{3}x.

A.1 Proof of Theorem 1

To prove Theorem 1, we need the internalized version of Lemma 2.

Lemma 3. Let e and f be environment terms. Then, for any term a, e[[f[[a]]]] =_{κε} e[[f]][[(e↑^{TY(f)})[[a↕_{TY(f)}^{TY(e)}]]]] holds.

Proof. Let F ≡ TY(f). We have e[[(κF. a)·f]] →_{κ} e[[f[[a]]]] and e[[(κF. a)·f]] →_{ε} e[[κF. a]]·e[[f]] →_{ε} (κF. (e↑^{F})[[a↕_{F}^{TY(e)}]])·e[[f]] →_{κ} e[[f]][[(e↑^{F})[[a↕_{F}^{TY(e)}]]]]. □

Proof of Theorem 1. By induction on the size of a. We prove only the case a is of the form e[[b]]. (Other cases are similar or trivial.) We have

(e[[b]])[s] ≡ e[s][[b↕_{TY(e)}^{TY(s)}[s↑^{TY(e)}]]]

by the definition of substitution. On the other hand, we have

s[[e[[b]]]] =_{κε} s[[e]][[s↑^{TY(e)}[[b↕_{TY(e)}^{TY(s)}]]]] =_{κε} e[s][[b↕_{TY(e)}^{TY(s)}[s↑^{TY(e)}]]]

by Lemma 3 and the induction hypothesis. □

A.2 Proofs of Lemma 2 and Theorem 2

It is sometimes useful to define the substitution operation in a similar way as push/pull/exchange operations. Let ϕ : V → T be a (possibly) partial function. We extend ϕ to the function \overline{ϕ} : T → T in the same way as \overline{ϕ} defined in section 3, except that ϕ_{E} is now defined as follows.

ϕ_{E}(x) := \{ \begin{matrix}x & if x ∈ E, \\ ϕ(x↓_{E})↑^{E} & otherwise. \end{matrix}

It is easy to see that if ϕ is total, then \overline{ϕ} is also a total function. That is, if a ∈ T, we have \overline{ϕ}(a) ∈ T.

Let s ≡ {b_{1}/x_{1}, …, b_{n}/x_{n}}. We define a total function [s] : V → T as follows:

[s](x) := \{ \begin{matrix}b_{i} & if x ≡ x_{i} for some i, \\ ⇓_{\{x_{1},...,x_{n}\}}(x) & otherwise. \end{matrix}

We give an example of this alternative definition of substitution. Let s ≡ {♯^{3}x/x, (x ♯x)/♯x}.

\overline{[s]}(λx. x ♯^{2}x) ≡ λx. \overline{[s]_{\{x\}}}(x ♯^{2}x)
≡ λx. ([s]_{{x}}(x))([s]_{{x}}(♯^{2}x))
≡ λx. x([s](♯^{2}x↓_{{x}})↑^{{x}})
≡ λx. x([s](♯x)↑^{{x}})
≡ λx. x((x ♯x)↑^{{x}})
≡ λx. x(♯x ♯^{2}x).

We show in Lemma 6 that \overline{[s]}(a) coincides with the substitution a[s] defined in section 3. In the following, we will write ϕ_{E_{1}···E_{n}} for (⋯ (ϕ_{E_{1}}) ⋯)_{E_{n}} and sometimes just write ϕ for \overline{ϕ} if there is no fear of confusion.

Lemma 4. Let ϕ : V → T be a (possibly) partial function, a be a term, s be a canonical environment term, and E, E_{1}, …, E_{n}, F be declarations.

1. If ⇓_{E_{i+1}}(⋯ ⇓_{E_{n}}(x) ⋯) ∈ E_{i} for some i, ϕ_{E_{1}···E_{n}}(x) ≡ x.

2. \overline{ϕ_{E}}(a↑^{E}) ≡ \overline{ϕ}(a)↑^{E}.

3. \overline{[s]}(a↑^{TY(s)}) ≡ a.

4. a↑^{E} ↑^{F} ↕_{F}^{E} ≡ a↑^{F} ↑^{E}

Proof. 1–3. Straightforward. 4. Note that ⇑^{E}⇑^{F} x ∉ E and ⇑^{E}⇑^{F} x ∉ F ⇑^{E} for any variable x. □

Lemma 5. Let s be a canonical environment term. Then, for any term a and declaration E, a↕_{E}^{TY(s)}[s↑^{E}] ≡ \overline{[s]_{E}}(a) holds.

Proof. Let E_{0}, E_{1}, …, E_{n} be declarations and let X ≡ TY(s). We prove the identity (⋆)

((⇕_{E_{n}}^{X} ∘ ⇕_{E_{n−1}}^{X}_{E_{n}} ∘ ⋯ ∘ ⇕_{E_{0}}^{X}_{E_{1}···E_{n}})(a))[s↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}}] ≡ \overline{[s]_{E_{0}E_{1}···E_{n}}}(a)

by induction on the construction of a.

1. a is a variable: We put a_{0} := a, a_{i+1} := ⇕_{E_{i}}^{X}_{E_{i+1}···E_{n}}(a_{i}), y_{n+1} := a, and y_{i} := ⇓_{E_{i}}(y_{i+1}). (If y_{i+1} ∈ E_{i} for some i, y_{j} (j ≤ i) is undefined.) Note that ⇕_{E}^{F}⇑^{E}⇑^{F} y ≡ ⇑^{F} ⇑^{E}y for any variable y and declarations F and E by Lemma 4.

(a) y_{i+1} ∈ E_{i} for some i: We have a_{j} ≡ a (j ≤ i) by Lemma 4 and ⇕_{E_{i}}^{X}y_{i+1} ≡ ⇑^{X}y_{i+1} by assumption. Therefore, we have a_{i+1} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{i+1}}⇑^{X}y_{i+1}. By the remark above, we have

a_{i+2} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{i+2}}⇕_{E_{i+1}}^{X}⇑^{E_{i+1}}⇑^{X}y_{i+1}
≡ ⇑^{E_{n}} ⋯ ⇑^{E_{i+2}}⇑^{X}⇑^{E_{i+1}}y_{i+1}
≡ ⇑^{E_{n}} ⋯ ⇑^{E_{i+2}}⇑^{X}y_{i+2}

We can proceed similarly and finally we have a_{n+1} ≡ ⇑^{X}y_{n+1}. Then, the left-hand side of (⋆) ≡ ⇓_{X}⇑^{X}y_{n+1} ≡ y_{n+1} and the right-hand side of (⋆) ≡ a by Lemma 4. Therefore, (⋆) holds.

(b) y_{1} ∉ E_{0} and y_{1} ∈ X ⇑^{E_{0}}: We have ⇕_{E_{0}}^{X}y_{1} ≡ ⇓_{E_{0}}y_{1} ≡ y_{0} ∈ X by assumption. Therefore, we have a_{1} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{1}}y_{0}. Since ⇑^{E_{1}}y_{0} ∉ E_{1} and ⇑^{E_{1}}y_{0} ∈ X ⇑^{E_{1}}, we have

a_{2} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇕_{E_{1}}^{X}⇑^{E_{1}}y_{0}
≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇓_{E_{1}}⇑^{E_{1}}y_{0}
≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}y_{0}

We can proceed similarly and finally we have a_{n+1} ≡ y_{0}. Then, the lefthand side of (⋆) ≡ y_{0}[s↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}}] and the right-hand side of (⋆) ≡ [s](y_{0})↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}}. Therefore, (⋆) holds.

(c) y_{1} ∉ E_{0} and y_{1} ∉ X ⇑^{E_{0}}: We have ⇕_{E_{0}}^{X}y_{1} ≡ ⇑^{X}⇑^{E_{0}}⇓_{X}⇓_{E_{0}}y_{1} by assumption. Therefore, we have a_{1} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{1}}⇑^{X}⇑^{E_{0}}⇓_{X}y_{0}. By the remark above, we have

a_{2} ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇕_{E_{1}}^{X}⇑^{E_{1}}⇑^{X}⇑^{E_{0}}⇓_{X}y_{0}
≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇑^{X}⇑^{E_{1}}⇑^{E_{0}}⇓_{X}y_{0}

We can proceed similarly and finally we have a_{n+1} ≡ ⇑^{X}⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇑^{E_{1}}⇑^{E_{0}}⇓_{X}y_{0}. Let y′ ≡ ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇑^{E_{1}}⇑^{E_{0}}⇓_{X}y_{0}. Then, the left-hand side of (⋆) ≡ ⇓_{X}⇑^{X}y′ ≡ y′ and the right-hand side of (⋆) ≡ (⇓_{X}y_{0})↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}} ≡ y′. Therefore, (⋆) holds.

2. a is of the form e[[b]]: Let E ≡ TY(e), ϕ ≡ ⇕_{E_{n}}^{X} ∘ ⇕_{E_{n−1}}^{X}_{E_{n}} ∘ ⋯ ∘ ⇕_{E_{0}}^{X}_{E_{1}···E_{n}}, ϕ′ ≡ ⇕_{E_{n}}^{X}_{E} ∘ ⇕_{E_{n−1}}^{X}_{E_{n}E} ∘ ⋯ ∘ ⇕_{E_{0}}^{X}_{E_{1}···E_{n}E}, and t ≡ s↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}}. Then, the left-hand side of (⋆) ≡

ϕ(e)[[ϕ′(b)]][t] ≡ ϕ(e)[t][[ϕ′(b)↕_{E}^{X}[t↑^{E}]]]

and the right-hand side of (⋆) ≡

\overline{[s]_{E_{0}E_{1}···E_{n}}}(e)[[\overline{[s]_{E_{0}E_{1}···E_{n}E}}(b)]].

Therefore, by the induction hypothesis, we have the identity.

3. Otherwise: Similar to the case 2 or trivial. □

Lemma 6. Let s be a canonical environment term. Then, for any term a, a[s] ≡ \overline{[s]}(a) holds.

Proof. By induction on the construction of a, using Lemma 5 in the case a is of the form λx. b, κE. b, or e[[b]]. □

Now, we can prove Lemma 2 and Theorem 2 using Lemma 6.

Proof of Lemma 2. In this proof, \overline{E} denotes the sequence E_{1} ⋯ E_{n}. Let X ≡ TY(s) and Y ≡ TY(t). We prove the identity (⋆)

[t]\overline{E}([s]\overline{E}(a)) ≡ [[t](s)]\overline{E}([t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(a)))

by induction on the construction of a. The lemma follows from the case n = 0 of this identity and Lemma 6.

1. a is a variable: If ⇓_{E_{i+1}}(⋯ ⇓_{E_{n}}(a) ⋯) ∈ E_{i} for some i, both sides of (⋆) are a by Lemma 4. Otherwise, we put y := ⇓_{E_{1}}(⋯ ⇓_{E_{n}}(a) ⋯). In this case, we can prove (⋆) by case analysis of y.

(a) If y ∈ X, the left-hand side of (⋆) ≡ [t]\overline{E}([s](y)↑^{E_{1}} ⋯↑^{E_{n}}) ≡ [t]([s](y))↑^{E_{1}} ⋯↑^{E_{n}} by Lemma 4. On the other hand, since ⇕_{X}^{Y}y ≡ ⇑^{Y} y, we have [t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(a)) ≡ [t↑^{X}](⇑^{Y} y)↑^{E_{1}} ⋯↑^{E_{n}} ≡ y ↑^{E_{1}} ⋯↑^{E_{n}}. Therefore, (⋆) holds.

(b) If y ∈ Y ⇑^{X}, the left-hand side of (⋆) ≡ [t]\overline{E}([s](y)↑^{E_{1}} ⋯↑^{E_{n}}) ≡ [t](⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}. On the other hand, since ⇕_{X}^{Y}y ≡ ⇓_{X}y, we have [t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(a)) ≡ [t↑^{X}](⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}. Therefore, (⋆) holds by Lemma 4.

(c) Otherwise, the left-hand side of (⋆) ≡ [t]\overline{E}([s](y)↑^{E_{1}} ⋯↑^{E_{n}}) ≡ (⇓_{Y} ⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}. On the other hand, since ⇕_{X}^{Y}y ≡ ⇑^{Y} ⇑^{X}⇓_{Y} ⇓_{X}y, the right-hand side of (⋆) is (⇓_{X}⇓_{Y} ⇑^{Y} ⇑^{X}⇓_{Y} ⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}} ≡ (⇓_{Y} ⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}.

2. a is of the form e[[b]]: The left-hand side of (⋆) ≡

[t]\overline{E}([s]\overline{E}(e))[[[t]_{\overline{E} TY(e)}([s]_{\overline{E} TY(e)}(b))]]

and the right-hand side of (⋆) ≡

[[t](s)]\overline{E}([t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(e)))[[σ_{1}(σ_{2}(ϕ(b)))]]

where σ_{1} ≡ [[t](s)]_{\overline{E} TY(e)}, σ_{2} ≡ [t↑^{X}]_{\overline{E} TY(e)}, and ϕ ≡ ⇕_{X}^{Y}_{\overline{E} TY(e)}. Therefore, by the induction hypothesis, we have the identity.

3. Otherwise: Similar to the case 2 or trivial. □

Lemma 7. Let ϕ : V → T be a (possibly) partial function, a be a term, and E, F be declarations. Then, \overline{ϕ_{F E}}(a↕_{F}^{E}) ≡ \overline{ϕ_{EF}} (a)↕_{F}^{E} holds.

Proof. Let \overline{E} ≡ E_{1} ⋯ E_{n}. We can prove the identity

ϕ_{F E\overline{E}}(⇕_{F}^{E}\overline{E}(a)) ≡ ⇕_{F}^{E}\overline{E}(ϕ_{EF \overline{E}}(a))

similarly to the proof of Lemma 2. □

Proof of Theorem 2. By Lemma 6 and Lemma 7. □

A.3 Proof of Theorem 3 Proof of Theorem 3. The theorem is proved by the induction on the derivation Γ ⊢ a : A and the reduction a →_{λκε} b. Here we verify only a few key cases.

\begin{matrix}⋮ . ; Γ ⊢ a : A ; (Γ − E)⇓_{E} ⊢ κE. a : A^{E} & ⋮ . ; Δ ⊢ e : E \\ (Γ − E)⇓_{E} ∪ Δ ⊢ (κE. a)·e : A \end{matrix} ↦_{κ}

\begin{matrix}⋮ . ; Δ ⊢ e : E & ⋮ . ; Γ ⊢ a : A \\ Δ ∪ (Γ − E)⇓_{E} ⊢ e[[a]] : A \end{matrix}.

\begin{matrix}⋮ . ; Γ ⊢ e : F & ⋮ . ; Δ ⊢ a : A ; (Δ − E)⇓_{E} ⊢ κE. a : A^{E} \\ Γ ∪ ((Δ − E)⇓_{E} − F)⇓_{F} ⊢ e[[κE. a]] : A^{E} \end{matrix} ↦_{ε}

\begin{matrix}⋮ . ; Γ ⇑^{E} ⊢ e↑^{E} : F & ⋮ . ; Δ⇕_{E}^{F} ⊢ a↕_{E}^{F} : A \\ Γ ⇑^{E} ∪ (Δ⇕_{E}^{F} − F)⇓_{F} ⊢ (e↑^{E})[[a↕_{E}^{F}]] : A \end{matrix} ; ((Γ ⇑^{E} ∪ (Δ⇕_{E}^{F} − F)⇓_{F}) − E)⇓_{E} ⊢ κE. (e↑^{E})[[a↕_{E}^{F}]] : A^{E}.

We have Γ ∪ ((Δ − E)⇓_{E} − F)⇓_{F} ≡ ((Γ ⇑^{E} ∪ (Δ⇕_{E}^{F} − F)⇓_{F}) − E)⇓_{E} from Lemma 1. We also have that, if Γ ⊢ a : A is derived, then Γ ⇑^{E} ⊢ a↑^{E} : A and Γ ⇕_{F}^{E} ⊢ a↕_{F}^{E} : A are derived for any E and F, hence we are done. □