A Simply Typed Context Calculus with First-class Environments

Masahiko Sato^{∗}  Takafumi Sakurai^{†}

Yukiyoshi Kameyama^{‡}

March 10, 2002

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. The notion of contexts is important in theoretical investigations such as contextual equivalence and evaluation contexts, but it is getting important in modeling practical computations as well. For instance, to model distributed computing, we often need to represent open terms (terms with free variables) and dynamic binding of variables, and that kind of representation is also necessary to treat modules as first-class citizens. Such a representation can be given by formalizing contexts and the hole-filling operations, but we refer to [10] for related discussions. Here we point out that the key idea is to link distributed objects through the names of variables.

∗Graduate School of Informatics, Kyoto University, Yoshida-Honmachi, Sakyo-ku, Kyoto, 606-8501, Japan, masahiko@kuis.kyoto-u.ac.jp

†Department of Mathematics and Informatics, Chiba University, Yayoi 1-33, Inage, Chiba, 263-8522, Japan, sakurai@math.s.chiba-u.ac.jp

‡Institute of Information Sciences and Electronics, University of Tsukuba, Tennodai 1-1-1, Tsukuba, 305-8573, Japan, kam@is.tsukuba.ac.jp

Recently there have been several attempts to formalize the notion of context and thereby make computing with contexts possible. For example, Talcott [19], Lee-Friedman [11], Dami [5], Hashimoto-Ohori [10], Sands [16], Mason [12] and Bognar-de Vrijer [4] 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 the language is logically wellbehaved 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:

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

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 [10] 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 [19], and Mason [12] 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 λε [18] 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 first-class 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 metalevel 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 compare our calculus with some related works. In section 7, we give concluding remarks.

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 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 variables.

In the following, we will use declaration as a synonym for a finite set of variables. We use E, F and Γ, Δ etc. as meta variables for declarations. A 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⟩. As we explained in the introduction, we need to distinguish different variables which have the same name, and we use levels for this purpose. Levels can be considered as a generalization of de Bruijn indices, as is shown by the example in the next section. Let x and y be variables. We write x ≤ y if y ≡ ♯^{l}x for some l ≥ 0.

We write V for the set of all the variables. Let E be a finite set of variables. We define ⇑^{E} as the unique bijection from V to V − E which preserves the names of variables (that is, ♮(⇑^{E}(x)) = ♮(x) for any variable x) and 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}. 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 {♯^{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. We will use ⇑^{E} later to systematically rename variables to avoid collision with the variables in E.

Let Γ, E, and F be 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} , \\ ⇑^{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 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, ♯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.

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

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

As we will see in section 3, we will use ⇕_{F}^{E} to rename variables when the order of two binders are exchanged. The definition of ⇕_{F}^{E} may seem complicated, but if E and F are sets of pure variables (that is, bound variables are pure), the definition is simplified as follows.

Lemma 2.1 Let E and F be sets of pure variables. We have

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

Proof. Suppose x ∉ F and x ∉ E ⇑^{F}. By x ∉ F, there exists y such that x = ⇑^{F} (y). Then, we have ⇑^{F} (y) ∉ E ⇑^{F}, that is, y ∉ E. Therefore, there exists z such that y = ⇑^{E}(z). Then, we have x = ⇑^{F} (⇑^{E}(z)) and ⇕_{F}^{E}(x) = ⇑^{E}(⇑^{F} (⇓_{E}(⇓_{F} (x)))) = ⇑^{E}(⇑^{F} (z)). So, ⇑^{E}(⇑^{F} (z)) = ⇑^{F} (⇑^{E}(z)) implies ⇕_{F}^{E}(x) = x. We will be done when we show ⇑^{E}(⇑^{F} (z)) = ⇑^{F} (⇑^{E}(z)) in the following.

Let n be the level of z. Then, there exists a pure variable z_{0} such that z = ♯^{n}z_{0}. Since E and F are sets of pure variables, we have

⇑^{E}(⇑^{F} (z)) = \{ \begin{matrix}♯^{n+2}z_{0} & if z_{0} ∈ E ∩ F , \\ ♯^{n+1}z_{0} & if z_{0} ∈ (E − F) ∪ (F − E), \\ ♯^{n}z_{0} & otherwise. \end{matrix}

So, we have ⇑^{E}(⇑^{F} (z)) = ⇑^{F} (⇑^{E}(z)). □

If E and F do not have common variable names (that is, E and F are ‘irrelevant’), ⇕_{F}^{E} is an identity function.

Lemma 2.2 Let E and F be declarations such that {♮(x) | x ∈ E} ∩ {♮(x) | x ∈ F } = ∅. We have ⇕_{F}^{E}(x) = x.

Proof. In this proof, we write ♮(E) for {♮(x) | x ∈ E}. First, note that ♮(x) ∉ ♮(E) implies ⇑^{E}(x) = ⇓_{E}(x) = x. We prove the lemma by cases.

(i) If x ∈ F, then ♮(x) ∉ ♮(E) because ♮(E) ∩ ♮(F) = ∅. Therefore, ⇕_{F}^{E}(x) = ⇑^{E}(x) = x.

(ii) If x ∈ E ⇑^{F}, then ♮(x) ∈ ♮(E ⇑^{F}) = ♮(E). Therefore, ⇕_{F}^{E}(x) = ⇓_{F} (x) = x.

(iii) Otherwise, we have three cases. (1) If ♮(x) ∈ ♮(E), then ⇕_{F}^{E}(x) = ⇑^{E}(⇑^{F} (⇓_{E}(⇓_{F} (x)))) = ⇑^{E}(⇓_{E}(x)) = x. (2) If ♮(x) ∈ ♮(F), then ⇕_{F}^{E}(x) = x is proved similarly. (3) Otherwise, trivial. □

Lemma 2.3 We have the following identities.

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

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

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

Proof. 1, 2. Easy.

3. Since (Γ − E) ∩ E = ∅, there exists Γ′ such that Γ − E = Γ′ ⇑^{E}. Then, we have Γ = (Γ ∩ E) ∪ Γ′ ⇑^{E}. Similarly, there exists Γ′′ such that Γ′ = (Γ′ ∩ F) ∪ Γ′′ ⇑^{F}. Therefore, we have

((Γ − E)⇓_{E} − F)⇓_{F} = (Γ′ ⇑^{E} ⇓_{E} − F)⇓_{F}
= (Γ′ − F)⇓_{F} = Γ′′ ⇑^{F} ⇓_{F} = Γ′′.

On the other hand, we have

Γ⇕_{E}^{F} = ((Γ ∩ E) ∪ (Γ′ ∩ F)⇑^{E} ∪ Γ′′ ⇑^{F} ⇑^{E})⇕_{E}^{F}
= (Γ ∩ E)⇑^{F} ∪ (Γ′ ∩ F)⇑^{E} ⇓_{E} ∪ Γ′′ ⇑^{F} ⇑^{E} ⇓_{E} ⇓_{F} ⇑^{E} ⇑^{F}
= (Γ ∩ E)⇑^{F} ∪ (Γ′ ∩ F) ∪ Γ′′ ⇑^{E} ⇑^{F} .

So, we have

(Γ⇕_{E}^{F} − F)⇓_{F} = ((Γ ∩ E)⇑^{F} ∪ Γ′′ ⇑^{E} ⇑^{F})⇓_{F} = (Γ ∩ E) ∪ Γ′′ ⇑^{E}.

Therefore, we have

((Γ⇕_{E}^{F} − F)⇓_{F} − E)⇓_{E} = (Γ ∩ E) ∪ Γ′′ ⇑^{E} − E ⇓_{E} = Γ′′ ⇑^{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

{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 (envI), the variables x_{1}, …, x_{n} must be mutually distinct.

Figure 1: Typing rules of λκε

of free 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 the order of a_{i}/x_{i} (i = 1, …, n) in e does not matter and 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. A canonical environment term is a canonical term which is at the same time an environment term.

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 [18] 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.

\begin{matrix}\begin{matrix}\{y\} ⊢ y : A ⇒ A ⇒ B & \{♯♯x\} ⊢ ♯♯x : A \\ \{y, ♯♯x\} ⊢ y(♯♯x) : A ⇒ B \end{matrix} & \{x\} ⊢ x : A \\ \{y, ♯♯x, x\} ⊢ y(♯♯x)x : B \end{matrix} ; \{y, ♯x\} ⊢ λx. y(♯♯x)x : A ⇒ B ; \{\} ⊢ κ\{♯x, y\}. λx. y(♯♯x)x : (A ⇒ B)^{\{♯x,y\}}

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 κ. As suggested by the type of κ-abstracts, κ abstracts named variables, while we intend that λ abstracts nameless variables. It is possible to eliminate names in λ-abstracts by taking the distinguished name ι, replacing λx^{A} by κ{⟨0, ι, A⟩}, 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. However, unlike the traditional λ-calculus, we do not identify αequivalent terms when we define substitution, but introduce α-equivalence later as an auxiliary notion that is necessary to describe conservativity over λ-calculus. (See also the comments after the definition of α-equivalence in section 3.)

3 Substitution and α-equivalence

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 [6].

2Strictly 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.

Before going into technical details, we explain our method by comparing it with the traditional method of defining substitution for terms with named variables [2] and also with the method invented by de Bruijn [6]. 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 not occur, the result of substitution obtained by our method is the same as that obtained by the traditional method.

After defining the substitution, we define α-equivalence of terms. As we will see later, our definition of α-equivalence is also simpler than the existing definitions of α-equivalence, and the proof that the relation is indeed an equivalence relation is also simpler. Again, some examples will 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)
≡_{α} λ♯^{1}x. λ♯^{1}x. (λ♯^{1}x. ♯^{2}x(♯^{1}x♯^{3}x))(♯^{1}x♯^{2}x)

3The idea of renaming free variables is introduced in [17].

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

If we write 1, 2 and 3 for ♯^{1}x, ♯^{2}x and ♯^{3}x, respectively, in the second term above, we get λ1. λ1. (λ1. 2(13))(12). Therefore, this term is essentially the same as the representation of the first term in de Bruijn indices. Similarly, the third term becomes λ1. λ2. (λ3. 2(31))(21), and this term is essentially the same as the representation of the first term in de Bruijn levels, or, using the terminology of Gunter [9], corresponds to the CCC model representation. We can therefore see that our terms are natural extensions of both traditional concrete terms with variable names and name free terms a la de Bruijn that use indices and levels.

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 ϕ is total if and only if ϕ_{E} is 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, ♯x}.

(λ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(♯^{5}x).

Note that FV(λx. x(♯^{3}x)) = {♯^{2}x}, and {♯^{2}x}⇑^{E} = {♯^{4}x}, which is equal to FV(λx. x(♯^{5}x)). Similarly, we have (λx. x(♯^{3}x))↓_{E} ≡ λx. x(♯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.

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/x, (x ♯x)/♯x}. Then we have:

(λx. x ♯^{2}x)[s] ≡ λx. (x ♯^{2}x)↕_{{x}}^{{x,♯x}}[s↑^{{x}}]

≡ λx. (♯^{2}x ♯x)[{♯^{4}x/x, (♯x ♯^{2}x)/♯x}]
≡ λx. (⇓_{{x,♯x}}(♯^{2}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 ♯^{2}x is bound by λx and ♯^{2}x is bound by s. When s goes into the scope of λx, x and ♯^{2}x should be renamed to ♯^{2}x and ♯x, respectively so that they are bound by λx and s↑^{{x}}.

We are now ready to define the notion of α-equivalence. We prepare an infinite set of identifiers ι_{1}, ι_{2}, … that are not used in λκε. We write ι_{k}^{A} or just ι_{k} for a variable ⟨0, ι_{k}, A⟩. An extended term is a term constructed from variables of λκε and variables ι_{1}, ι_{2}, . . .. We also assume that we have a total order ≺ on variables. We define a transformation ^{∗λ} that transforms a term t to an extended term t^{∗λ} using the following rules.

1. x^{∗λ} := x.

2. (λx. a)^{∗λ} := λι_{1}. a^{∗λ}[{ι_{1}/x}].

3. (ba)^{∗λ} := b^{∗λ}a^{∗λ}.

4. (κE. a)^{∗λ} := κE. a^{∗λ}.

5. (a·f)^{∗λ} := a^{∗λ}·f^{∗λ}.

6. {a_{1}/x_{1}, …, a_{n}/x_{n}}^{∗λ} := {a_{1}^{∗λ}/x_{1}, …, a_{n}^{∗λ}/x_{n}}.

7. (e[[b]])^{∗λ} := e^{∗λ}[[b^{∗λ}]].

We define another transformation ^{∗ε} using the rules obtained by replacing ^{∗λ} of rules 1–6 by ^{∗ε} and the following rules.

7. (e[[b]])^{∗ε} := e^{∗ε}[[b^{∗ε}]], if e is not a canonical environment term.

8. ({a_{1}/x_{1}, …, a_{n}/x_{n}}[[b]])^{∗ε} :={a_{p(1)}^{∗ε}/ι_{1}, …, a_{p(n)}^{∗ε}/ι_{n}}[[b^{∗ε}[{ι_{1}/x_{p(1)}, …, ι_{n}/x_{p(n)}}]]] where p is a permutation on 1..n such that x_{p(1)} ≺ ⋯ ≺ x_{p(n)} and the type of ι_{k} is the type of x_{p(k)}.

Let a and b be terms. If a^{∗λ} ≡ b^{∗λ}, we write a ≡_{α}^{λ} b and say a is α^{λ}-equivalent to b. If a^{∗ε} ≡ b^{∗ε}, we write a ≡_{α}^{ε} b (or a ≡_{α} b) and say a is α^{ε}-equivalent to b (or a is α-equivalent to b). In the following, we apply ^{∗λ} and ^{∗ε} to extended terms (the definition should be clear), but we do not apply the notion of α^{λ}- or α^{ε}-equivalence to extended terms.

We have introduced α^{λ}-equivalence to expresses our intention that λ abstracts nameless variables. But it is not satisfactory because α^{λ}-equivalence is not preserved by reduction. Therefore, we have introduced α^{ε}-equivalence as an equivalence that is preserved by reduction. (See Theorem 5.17.)

The α-equivalence in λκε also satisfies the following properties:

Theorem 3.1 1. If Γ ⊢ a : A and a ≡_{α}^{λ} b, then Γ ⊢ b : A.

2. If Γ ⊢ a : A and a ≡_{α}^{ε} b, then Γ ⊢ b : A.

3. Let a and b be terms, s be a canonical environment term, and ρ be λ or ε. If a ≡_{α}^{ρ} b, then a[s] ≡_{α}^{ρ} b[s].

Proof. We can prove 1 and 2 by the induction on the derivation Γ ⊢ a : A. We will prove 3 in section 5, because we need some properties of substitution and α-equivalence to prove this theorem. □

Here, we refer to some preceding works that have relations with our exchange operator and our definition of substitution. The definition of substitution by Fiore, Plotkin, and Turi [7] is similar to ours, that is, the 2nd clause of our definition corresponds to the 2nd clause of the definition of the substitution operation σ : δΛ × Λ → Λ [7], and we think that it should be possible to establish a precise correspondence. We also make a remark about label-selective λ-calculus [8]. In label-selective λ-calculus, abstracts and arguments are labeled and the labels are used in argument-passing. The label consists of a symbol and a number and the number changes when the label is pushed into the scope of λ-abstracts. Since argument-passing corresponds to selecting the field of record by label, we can say label-selective λ-calculus incorporates an idea similar to ours.

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 5.9 that we can faithfully compute substitution internally by using these reduction rules, and at the same time the system enjoys the strong normalizability (Theorem 5.26). In fact, as can be seen in, e.g., Melliès [13] and Bloo and Rose [3], the strong normalizability of calculi of explicit substitutions and explicit environments is a subtle problem. The reader is referred to [18] 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 reflexive and 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. (s ≡ {♯^{3}x/x, (x ♯x)/♯x} 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 ♯^{2}x]] →_{ε} λx. (s↑^{{x}})[[(x ♯^{2}x)↕_{{x}}^{{x,♯x}}]]
≡ λx. {♯^{4}x/x, (♯x ♯^{2}x)/♯x}[[(♯^{2}x ♯x)]]
→^{∗}_{ε} λx. ((♯^{2}x)↓_{{x,♯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 [10]. 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 three 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}. x + z/X}[[(λu. X·{u/x} + y)3]])x
→^{∗}_{ε} (λz. (λu. (κ{x}. x + z)·{u/x} + y)3)x
→_{λ} {x/z}[[(λu. (κ{x}. x + z)·{u/x} + y)3]]
→^{∗}_{ε} (λu. (κ{x}. x + ♯x)·{u/x} + y)3
→_{λ} {3/u}[[(κ{x}. x + ♯x)·{u/x} + y]]
→^{∗}_{ε} (κ{x}. x + ♯x)·{3/x} + y
→_{κ} {3/x}[[x + ♯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. First, we give an alternative definition of substitution (Lemma 5.5) which is useful in proving the properties of λκε. Then, we show that the meta-level operation of substitution is internally realized by the operation of evaluation (Theorem 5.9). We also show that λκε enjoys subject reduction property (Theorem 5.13), confluence property (Theorem 5.14), conservativity over the simply typed λβ-calculus (Theorem 5.24), and strong normalizability (Theorem 5.26). Theorems 5.14, 5.24, 5.26 establish the purity of λκε, and as a corollary to the confluence of λκε, we see that the operations of hole filling and β-reduction always commute.

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 be {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 be {♯^{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 5.5 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{ϕ}, and ϕa for ϕ(a), if there is no fear of confusion.

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

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

2. ϕ_{E_{1}···E_{n}}(⇑^{E_{n}} ⋯ ⇑^{E_{1}}x) ≡ ϕ(x)↑^{E_{1}} ⋯↑^{E_{n}}.

3. ⇕_{F}^{E}⇑^{F} ⇑^{E}x ≡ ⇑^{E}⇑^{F} x.

Proof. 1, 2. Straightforward.

3. Note that ⇑^{F} ⇑^{E}x ∉ F and ⇑^{F} ⇑^{E}x ∉ E ⇑^{F}. □

Lemma 5.2 Let ϕ : V → T be a (possibly) partial function, a be a term, and E, E_{1}, …, E_{n} be declarations. Then, \overline{ϕ_{E}}(a↑^{E}) ≡ \overline{ϕ}(a)↑^{E} holds. As a corollary, \overline{ϕ_{E_{1}···E_{n}}}(a↑^{E_{1}} ⋯↑^{E_{n}}) ≡ \overline{ϕ}(a)↑^{E_{1}} ⋯↑^{E_{n}}.

Proof. First, we prove the lemma in the case ϕ is restricted to ψ : V → V. We prove, by induction on the construction of a, that the identity

ψ_{E\overline{F}} (⇑^{E}\overline{F} (a)) ≡ ⇑^{E}\overline{F} (ψ\overline{F} (a))  (⋆)

holds for any sequence of declarations \overline{F} ≡ F_{1} ⋯ F_{n}.

1. a is a variable:

(a) ⇓_{F_{i+1}} ⋯ ⇓_{F_{n}}a ∈ F_{i} for some i: In this case, both sides of (⋆) are a by Lemma 5.1 clause 1.

(b) Otherwise: In this case, there is a variable y such that a ≡ ⇑^{F_{n}} ⋯ ⇑^{F_{1}}y. By Lemma 5.1 clause 2, we have

LHS of (⋆) ≡ ψ_{E\overline{F}} (⇑^{F_{n}} ⋯ ⇑^{F_{1}}⇑^{E}y) ≡ ⇑^{F_{n}} ⋯ ⇑^{F_{1}}⇑^{E}(ψ(y)),
RHS of (⋆) ≡ ⇑^{E}\overline{F} ⇑^{F_{n}} ⋯ ⇑^{F_{1}}(ψ(y)) ≡ ⇑^{F_{n}} ⋯ ⇑^{F_{1}}⇑^{E}(ψ(y)).

(The last ≡ holds because ψ(y) is a variable.)

2. a ≡ e[[b]]: We have

LHS of (⋆) ≡ ψ_{E\overline{F}} (⇑^{E}\overline{F} (e))[[ψ_{E\overline{F} TY(e)}(⇑^{E}_{\overline{F} TY(e)}(b))]],
RHS of (⋆) ≡ ⇑^{E}\overline{F} (ψ\overline{F} (e))[[⇑^{E}_{\overline{F} TY(e)}(ψ_{\overline{F} TY(e)}(b))]].

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

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

Next, we prove the lemma in the general case. Similarly to the restricted case, we prove ϕ_{E\overline{F}} (⇑^{E}\overline{F} (a)) ≡ ⇑^{E}\overline{F} (ϕ\overline{F} (a)) by induction on a. The induction proceeds in exactly the same way except that, in case 1-(b), we need the lemma in the restricted case to show

⇑^{E}\overline{F} ⇑^{F_{n}} ⋯ ⇑^{F_{1}}(ϕ(y)) ≡ ⇑^{F_{n}} ⋯ ⇑^{F_{1}}⇑^{E}(ϕ(y)),

because ϕ(y) is a term. (⇑^{E}_{F_{1}···F_{i}} is used as ψ.) □

Lemma 5.3 Let a be a term, s be a canonical environment term, and E, F be declarations.

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

2. a↑^{E} ↓_{E} ≡ a, a↕_{F}^{E} ↕_{E}^{F} ≡ a.

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

Proof. We can prove these identities similarly to Lemma 5.2. We prove by induction on a, but we need to generalize each function ϕ to ϕ\overline{F} by parameterizing with a sequence of declarations \overline{F}, so that the function can handle bound variables correctly when it is pushed into the scope in the induction step. In the base case of the induction, we apply the case analysis of variables given in the proof of Lemma 5.2. As for 1, we can prove by induction on a that [s]\overline{F} (⇑^{TY(s)}\overline{F} (a)) ≡ a holds for any sequence of declarations \overline{F}. □

Lemma 5.4 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. Put X := TY(s). We prove, by induction on the construction of a, that 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}}] ≡ [s]_{E_{0}E_{1}···E_{n}}(a) (⋆)

holds for any declarations E_{0}, E_{1}, …, E_{n}.

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.)

(a) y_{i+1} ∈ E_{i} for some i: We have a_{j} ≡ a (j ≤ i) by Lemma 5.1 clause 1 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 Lemma 5.1 clause 2,3, we have

a_{i+2} ≡ ⇕_{E_{i+1}}^{X}_{E_{i+2}···E_{n}}(⇑^{E_{n}} ⋯ ⇑^{E_{i+1}}⇑^{X}y_{i+1})
≡ ⇑^{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,

LHS of (⋆) ≡ ⇓_{X}⇑^{X}y_{n+1} ≡ y_{n+1},
RHS of (⋆) ≡ a

by Lemma 5.1 clause 1. 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,

LHS of (⋆) ≡ y_{0}[s↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}}],
RHS 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 Lemma 5.1 clause 2,3, 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}.

Put y′ := ⇑^{E_{n}} ⋯ ⇑^{E_{2}}⇑^{E_{1}}⇑^{E_{0}}⇓_{X}y_{0}. Then,

LHS of (⋆) ≡ ⇓_{X}⇑^{X}y′ ≡ y′,
RHS of (⋆) ≡ (⇓_{X}y_{0})↑^{E_{0}} ↑^{E_{1}} ⋯↑^{E_{n}} ≡ y′.

Therefore, (⋆) holds.

2. a ≡ e[[b]]: Put 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,

LHS of (⋆) ≡ ϕ(e)[[ϕ′(b)]][t] ≡ ϕ(e)[t][[ϕ′(b)↕_{E}^{X}[t↑^{E}]]],
RHS of (⋆) ≡ [s]_{E_{0}E_{1}···E_{n}}(e)[[[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 5.5 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.4 in the case a is of the form λx. b, κE. b, or e[[b]]. □

Lemma 5.6 corresponds to the Substitution Lemma [2] 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 5.6 (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/x, (x ♯x)/♯x} in the lemma. Then, we have

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

(See also the example below the definition of the substitution in section 3.)

Proof of Lemma 5.6. Put X:=TY(s) and Y :=TY(t). We prove, by induction on the construction of a, that the identity

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

holds for any sequence of declarations \overline{E} ≡ E_{1} ⋯ E_{n}. The lemma follows from the case n = 0 of this identity and Lemma 5.5.

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

(a) y ∈ X: We have

LHS of (⋆) ≡ [t]\overline{E}([s](y)↑^{E_{1}} ⋯↑^{E_{n}}) ≡ [t]([s](y))↑^{E_{1}} ⋯↑^{E_{n}}

by Lemma 5.2. On the other hand, since ⇕_{X}^{Y}y ≡ ⇑^{Y} y in this case and [t↑^{X}](⇑^{Y} y) ≡ y by Lemma 5.3 clause 1, we have

[t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(a)) ≡ [t↑^{X}](⇑^{Y} y)↑^{E_{1}} ⋯↑^{E_{n}} ≡ y ↑^{E_{1}} ⋯↑^{E_{n}},

so, by Lemma 5.2,

RHS of (⋆) ≡ [[t](s)]\overline{E}(y ↑^{E_{1}} ⋯↑^{E_{n}}) ≡ [[t](s)](y)↑^{E_{1}} ⋯↑^{E_{n}}.

Let s ≡ {s_{1}/x_{1}, …, s_{m}/x_{m}}, then y ≡ x_{i} for some i. Therefore,

[t]([s](y)) ≡ [t](s_{i}),
[[t](s)](y) ≡ [{[t](s_{1})/x_{1}, …, [t](s_{m})/x_{m}}](y) ≡ [t](s_{i})

Therefore, (⋆) holds.

(b) y ∈ Y ⇑^{X}: We have

LHS of (⋆) ≡ [t]\overline{E}([s](y)↑^{E_{1}} ⋯↑^{E_{n}}) ≡ [t](⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}

by Lemma 5.2 and Lemma 5.3 clause 1. 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}},

so, by Lemma 5.2,

RHS of (⋆) ≡ [[t](s)]\overline{E}([t↑^{X}](⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}})
≡ [[t](s)]([t↑^{X}](⇓_{X}y))↑^{E_{1}} ⋯↑^{E_{n}}.

Let t ≡ {t_{1}/x_{1}, …, t_{m}/x_{m}}, then ⇓_{X}y ≡ x_{i} for some i. Therefore,

[t](⇓_{X}y) ≡ t_{i},
[[t](s)]([t↑^{X}](⇓_{X}y)) ≡ [[t](s)](t_{i} ↑^{X}) ≡ t_{i} ↑^{X} ↓_{X} ≡ t_{i}.

Therefore, (⋆) holds.

(c) Otherwise: We have

LHS 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,

RHS of (⋆) ≡ (⇓_{X}⇓_{Y} ⇑^{Y} ⇑^{X}⇓_{Y} ⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}
≡ (⇓_{Y} ⇓_{X}y)↑^{E_{1}} ⋯↑^{E_{n}}.

2. a ≡ e[[b]]: Put σ_{1} := [[t](s)]_{\overline{E} TY(e)}, σ_{2} := [t↑^{X}]_{\overline{E} TY(e)}, and ϕ:= ⇕_{X}^{Y}_{\overline{E} TY(e)}. Then, we have

LHS of (⋆) ≡ [t]\overline{E}([s]\overline{E}(e))[[[t]_{\overline{E} TY(e)}([s]_{\overline{E} TY(e)}(b))]],
RHS of (⋆) ≡ [[t](s)]\overline{E}([t↑^{X}]\overline{E}(⇕_{X}^{Y} \overline{E}(e)))[[σ_{1}(σ_{2}(ϕ(b)))]].

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

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

Lemma 5.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. We can prove, by induction on a, that the identity

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

holds for any sequence of declarations \overline{E}. In the case a is a variable, we apply the case analysis similar to the one in the proof of Lemma 5.6 and use Lemma 5.3 clause 3. □

The reduction is compatible with substitution.

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

Proof. By Lemma 5.5 and Lemma 5.7. □

As we have studied in [18], 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 5.9 Let s be a canonical environment term. Then, for any term a, a[s] =_{ε} s[[a]] holds.

Proof. We define the size |a| of a term a as follows.

1. |x|:= 1

2. |λx. b|:= |b| + 1

3. |ba|:= |b| + |a| 4. |κE. a|:= |a| + 1

5. |a·e|:= |a| + |e|

6. |{a_{1}/x_{1}, …, a_{n}/x_{n}}|:= |a_{1}| + ⋯ + |a_{n}| + 1

7. |e[[a]]|:= |e| + |a|

For terms e_{1}, …, e_{n}, a, we prove the identity

(e_{1}[[⋯ e_{n}[[a]] ⋯]])[s] =_{ε} s[[e_{1}[[⋯ e_{n}[[a]] ⋯]]]]  (⋆)

by induction on the lexicographic order (|e_{1}[[⋯ e_{n}[[a]] ⋯]]|, |a|).

1. a is a variable: We put X := TY(s), E_{i} := TY(e_{i}), y_{n+1} := a, and y_{i} := ⇓_{E_{i}}(y_{i+1}).

(a) y_{i+1} ∈ E_{i} for some i: We put f := e_{1}[[⋯ e_{i−1}[[e_{i}]] ⋯]]. Since

e_{1}[[⋯ e_{n}[[a]] ⋯]] →^{∗}_{ε} e_{1}[[⋯ e_{i}[[y_{i+1}]] ⋯]] →^{∗}_{ε} f[[y_{i+1}]]

holds, we have

LHS of (⋆) →^{∗}_{ε} (f[[y_{i+1}]])[s] ≡ f[s][[y_{i+1} ↕_{E_{i}}^{X}[s↑^{E_{i}}]]],
RHS of (⋆) →^{∗}_{ε} s[[f[[y_{i+1}]]]] →_{ε} s[[f]][[y_{i+1}]].

Since we have

y_{i+1} ↕_{E_{i}}^{X}[s↑^{E_{i}}] ≡ ⇑^{X}(y_{i+1})[s↑^{E_{i}}] ≡ ⇓_{X}(⇑^{X}(y_{i+1})) ≡ y_{i+1},

the identity (⋆) holds by the induction hypothesis for e_{1}, …, e_{i−1}, e_{i}.

(b) Otherwise: Since e_{1}[[⋯ e_{n}[[a]] ⋯]] →^{∗}_{ε} y_{1}, the identity (⋆) holds from s[[y_{1}]] →_{ε} y_{1}[s].

2. a ≡ λy. b: By successively using (fun), we have

e_{1}[[⋯ e_{n}[[λy. b]] ⋯]] →^{∗}_{ε} λy. e′_{1}[[⋯ e′_{n}[[b′]] ⋯]]

where e′_{1}, …, e′_{n}, b′ are obtained by applying push/exchange operations to e_{1}, …, e_{n}, b respectively. By Theorem 5.8 and the definition of substitution,

LHS of (⋆) →^{∗}_{ε} λy. (e′′_{1}[[⋯ e′′_{n}[[b′′]] ⋯]][s′])

where e′′_{1}, …, e′′_{n}, b′′, s′ are obtained by applying push/exchange operations to e′_{1}, …, e′_{n}, b′, s respectively. On the other hand, we have

RHS of (⋆) →^{∗}_{ε} s[[λy. e′_{1}[[⋯ e′_{n}[[b′]] ⋯]]]] →_{ε} λy. s′[[e′′_{1}[[⋯ e′′_{n}[[b′′]] ⋯]]]].

Since the size of a term does not change by push/exchange operations, we can apply the induction hypothesis.

3. a ≡ e[[b]]: (e_{1}[[⋯ e_{n}[[e[[b]]]] ⋯]])[s] =_{ε} s[[e_{1}[[⋯ e_{n}[[e[[b]]]] ⋯]]]] by the induction hypothesis for e_{1}, …, e_{n}, e, b.

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

We can generalize the internalized version of Substitution Lemma (Lemma 5.6).

Lemma 5.10 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. (Sketch) We can prove the following identities:

⇑^{X}_{E}(a) ≡ ⇕_{X}^{E}(⇑^{X}(a)), ⇕_{X}^{F}_{E}(⇕_{X}^{E}(⇕_{F}^{E}_{X}(a))) ≡ ⇕_{F}^{E}(⇕_{X}^{E}_{F} (⇕_{X}^{F}(a))),

where a is a term and E, F, X are declarations. Using these identities, we can prove this lemma by induction of the size of a. □

In the following, we prove several important theorems. Especially, Theorem 5.14, 5.24 and 5.26 will establish the purity of our calculus.

Theorem 5.11 (Closed Normal Term is Canonical) If ⊢ c : C and c is normal, then c is canonical.

Proof. We omit the proof, because this theorem can be proved in the same way as in [18]. □

Lemma 5.12 If Γ ⊢ a : A, then Γ⇑^{E} ⊢ a↑^{E} : A and Γ⇕_{F}^{E} ⊢ a↕_{F}^{E} : A for any declarations E, F.

Proof. (Sketch) In this proof, we use the notation ϕ(Γ) := {ϕ(x) | x ∈ Γ} for ϕ : V → V. We can prove that if Γ ⊢ a : A, then

⇑^{E}\overline{E}(Γ) ⊢ ⇑^{E}\overline{E}(a) : A, ⇕_{F}^{E}\overline{E}(Γ) ⊢ ⇕_{F}^{E}\overline{E}(a) : A

for any sequence of declarations \overline{E}, by the induction on the derivation Γ ⊢ a : A. □

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

Proof. 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 2.3. By Lemma 5.12, we are done. □

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

Proof. The proof is a straightforward extension of that for λε [18], 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 λβ and λε [18]. We first prove that α-equivalence is preserved by reduction.

Lemma 5.15 Let ^{∗} be ^{∗λ} or ^{∗ε}, a be a λκε-term, and E, F be declarations. We have the following identities.

FV(a^{∗}) = FV(a), TY(a^{∗}) = TY(a),
(a↑^{E})^{∗} ≡ a^{∗} ↑^{E}, (a↓_{E})^{∗} ≡ a^{∗} ↓_{E}, (a↕_{F}^{E})^{∗} ≡ a^{∗} ↕_{F}^{E}.

Proof. FV(a^{∗}) = FV(a) can be proved by induction on a. TY(a^{∗}) = TY(a) can be proved easily. For the rest of identities, we give a sketch of the proof of (a↑^{E})^{∗} ≡ a^{∗} ↑^{E}, because other ones can be proved similarly.

Put X := {x_{1}, …, x_{n}} and I := {ι_{1}, …, ι_{n}}. We can prove the identity:

(⇑^{E}_{X}(a))[{ι_{1}/x_{1}, …, ι_{n}/x_{n}}] ≡ ⇑^{E}_{I}(a[{ι_{1}/x_{1}, …, ι_{n}/x_{n}}]).

Using this identity, we can prove that (⇑^{E}\overline{F} (a))^{∗} ≡ ⇑^{E}\overline{F} (a^{∗}) holds for any sequence of declarations \overline{F} by induction on a. □

Lemma 5.16 Let E and F be declarations such that {♮(x) | x ∈ E}∩{♮(x) | x ∈ F } = ∅. Then, we have a↕_{F}^{E} ≡ a.

Proof. We can prove that ⇕_{F}^{E}\overline{F} (a) ≡ a holds for any sequence of declarations \overline{F} by induction on a and Lemma 2.2. □

Theorem 5.17 If a ≡_{α} a′, a →_{λκε} b, a′ →_{λκε} b′, and the position of the redex of a →_{λκε} b and that of the redex of a′ →_{λκε} b′ are the same, then b ≡_{α} b′.

Proof. This theorem is proved by induction on a →_{λκε} b. We prove only the base case e[[λx. b]] →_{λκε} λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]]. Other cases are similar or trivial. In this case, we have a term e′[[λx′. b′]] such that e[[λx. b]] ≡_{α} e′[[λx′. b′]] and e′[[λx′. b′]] →_{λκε} λx′. (e′ ↑^{{x′}})[[b′ ↕_{{x′}}^{TY(e′)}]]. So, we will prove

λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]] ≡_{α} λx′. (e′ ↑^{{x′}})[[b′ ↕_{{x′}}^{TY(e′)}]]  (⋆)

in the following. We have two cases according to the form of e. (In the following, ^{∗} stands for ^{∗ε} and ι for ι_{1}.)

1. e is not a canonical environment term: In this case, we have e^{∗} ≡ e^{′∗} and b^{∗}[{ι/x}] ≡ b^{′∗}[{ι/x′}], since e[[λx. b]] ≡_{α} e′[[λx′. b′]]. On the other hand, we have

(λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]])^{∗}
≡ λι. ((e↑^{{x}})[[b↕_{{x}}^{TY(e)}]])^{∗}[{ι/x}]
≡ λι. (e↑^{{x}})^{∗}[{ι/x}][[((b↕_{{x}}^{TY(e)})^{∗} ↕_{TY(e)}^{{x}})[{ι/x}]]]
≡ λι. e^{∗}[[b^{∗}[{ι/x}]]]

by Lemma 5.15 and Lemma 5.3 clause 1,2. We also have

(λx′. (e′ ↑^{{x′}})[[b′ ↕_{{x′}}^{TY(e′)}]])^{∗} ≡ λι. e^{′∗}[[b^{′∗}[{ι/x′}]]]

by the same calculation. Therefore, we have (⋆).

2. e ≡ \{a_{1}/y_{1}, …, a_{n}/y_{n}\}: By putting \{\overline{ι}/\overline{y}\} := \{ι_{1}/y_{p(1)}, …, ι_{n}/y_{p(n)}\} where y_{p(1)} ≺ ⋯ ≺ y_{p(n)}, we have

(e[[λx. b]])^{∗} ≡ \{a_{p(1)}^{∗}/ι_{1}, …, a_{p(n)}^{∗}/ι_{n}\}[[(λx. b)^{∗}[\{\overline{ι}/\overline{y}\}]]].

We also put Y := \{y_{1}, …, y_{n}\}, I := \{ι_{1}, …, ι_{n}\}, and \overline{ι}′:= ♯ι_{1}, ι_{2}, …, ι_{n}. Then, we have

(λx. b)^{∗}[\{\overline{ι}/\overline{y}\}] ≡ (λι. b^{∗}[\{ι/x\}])[\{\overline{ι}/\overline{y}\}]
≡ λι. (b^{∗}[\{ι/x\}])↕_{\{ι\}}^{Y}[\{\overline{ι}/\overline{y}\}↑^{\{ι\}}] ≡ λι. b^{∗}[\{ι/x\}][\{\overline{ι}′/\overline{y}\}]

by Lemma 5.16 for Y and {ι}. Since e[[λx. b]] ≡_{α} e′[[λx′. b′]], e′ should be an environment term such that e′ ≡ {a′_{1}/y′_{1}, …, a′_{n}/y′_{n}} and a_{p(i)}^{∗} ≡ a′_{q(i)}^{∗} where y′_{q(1)} ≺ ⋯ ≺ y′_{q(n)}. Putting \{\overline{ι}/\overline{y′}\}:=\{ι_{1}/y′_{q(1)}, …, ι_{n}/y′_{q(n)}\}, we have

b^{∗}[\{ι/x\}][\{\overline{ι}′/\overline{y}\}] ≡ b^{′∗}[\{ι/x′\}][\{\overline{ι}′/\overline{y′}\}].

On the other hand, we have

(λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]])^{∗}
≡ λι. ((e↑^{{x}})[[b↕_{{x}}^{Y}]])^{∗}[{ι/x}]
≡ λι. \{c_{p(1)}/ι_{1}, …, c_{p(n)}/ι_{n}\}[[(b↕_{\{x\}}^{Y})^{∗}[\{\overline{ι}/\overline{y}\}]]][\{ι/x\}]
≡ λι. \{d_{p(1)}/ι_{1}, …, d_{p(n)}/ι_{n}\}[[((b↕_{\{x\}}^{Y})^{∗}[\{\overline{ι}/\overline{y}\}])↕_{I}^{\{x\}}[\{ι/x\}]]]

where we put c_{i} := (a_{i} ↑^{{x}})^{∗} and d_{i} := (a_{i} ↑^{{x}})^{∗}[{ι/x}]. Then, we have

((b↕_{\{x\}}^{Y})^{∗}[\{\overline{ι}/\overline{y}\}])↕_{I}^{\{x\}}[\{ι/x\}] ≡ (b↕_{\{x\}}^{Y})^{∗}[\{\overline{ι}/\overline{y}\}][\{ι/x\}]
≡ (b↕_{\{x\}}^{Y})^{∗} ↕_{Y}^{\{x\}}[\{ι↑^{I}/x\}][\{\overline{ι}/\overline{y}\}] ≡ b^{∗}[\{♯ι/x\}][\{\overline{ι}/\overline{y}\}]

and d_{i} ≡ a_{i}^{∗} by Lemma 5.16 for {x} and I, Lemma 5.15 and Lemma 5.3 clause 1,2. By the same calculation, we have

(λx′. (e′ ↑^{{x′}})[[b′ ↕_{{x′}}^{TY(e′)}]])^{∗}
≡ λι. \{a′_{q(1)}^{∗}/ι_{1}, …, a′_{q(n)}^{∗}/ι_{n}\}[[b^{′∗}[\{♯ι/x′\}][\{\overline{ι}/\overline{y′}\}]]].

Therefore, we have (⋆). □

Note that α^{λ}-equivalence is not preserved by reduction. For example, (λx. x)z and (λy. y)z are α^{λ}-equivalent, but {z/x}[[x]] and {z/y}[[y]] are not.

Now we can describe the conservativity of λκε over λβ. Let λκε/α be the system obtained by identifying α-equivalent terms in λκε. By Theorem 5.17, the reduction relation in λκε becomes the reduction relation in λκε/α.

Theorem 5.18 (Conservativity) Let a and b be terms of λβ. Then, a →^{∗} b

in λκε/α iff a →^{∗} b in λβ.

Proof. This theorem can be proved in the same way as in [18], which uses the translation from terms of λε to terms of λβ. □

To describe the conservativity theorem (Theorem 5.18), we have identified α-equivalent terms in λκε, because α-equivalent terms are identified in λβ. But we can give an elaborated description by using the feature of λκε that α-conversion is not necessary to reduce terms. In the following, we will prove the conservativity of λκε over λε and λβ described in a different style (Theorem 5.22, 5.24). For this purpose, we embed the terms of λε in the λκεterms. A general λε-term is a λκε-term such that its typing derivation uses the (axiom), (⇒I), (⇒E), (envI), (envE) rules only, and in the derivation, x in (⇒I) is a pure variable, x_{1}, …, x_{n} in (envI) are pure variables, and E in (envE) is a set of pure variables. A term is pure if all the variables used in the (axiom) rule in its typing derivation are pure variables. A λε-term is a pure general λε-term. Next we represent the reduction rules of λε in λκε. The rules of λε are (var), (funapp), (env), (eval) of λκε and the following two rules.

(gc′) e[[a]] ↦_{ε} a, if TY(e) ∩ FV(a) = ∅.
(fun′) e[[λx. b]] ↦_{ε} λx. e[[b]], if x ∉ TY(e) ∪ FV(e).

But unlike λκε, α^{λ}-equivalent terms are identified in λε. Therefore, we represent the reduction rules as follows: Let a and b be λε-terms. We write a →^{λε} b if there exist λε-terms a′ and b′ such that a ≡_{α}^{λ} a′, b ≡_{α}^{λ} b′, and a′ is reduced to b′ by the above rules. We write ^{λε}→^{∗} for the reflexive and transitive closure of →^{λε}.

Lemma 5.19 Let a be a λε-term and E, F be sets of pure variables.

1. E ∩ FV(a) = ∅ iff a↑^{E} ≡ a iff a↑^{E} is a λε-term.

2. E ∩ FV(a) = ∅ iff a↓_{E} ≡ a iff a↓_{E} is a λε-term.

3. E ∩ F ∩ FV(a) = ∅ iff a↕_{F}^{E} ≡ a iff a↕_{F}^{E} is a λε-term.

Proof. Since a is a λε-term, all the variables in a are of level 0. Therefore, we need to prove only the case a is a variable. But it is easily checked. □

Lemma 5.20 1. Let e[[a]] be a λε-term. Then, a↓_{TY(e)} ≡ a iff TY(e) ∩ FV(a) = ∅.

2. Let e[[λx. b]] be a λε-term. Then, λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]] ≡ λx. e[[b]] iff x ∉ TY(e) ∪ (FV(e) ∩ FV(b)).

Proof. By Lemma 5.19. □

By this lemma, we know that (gc) restricted to λε-terms is (gc′), but (fun) restricted to λε-terms requires a weaker condition than (fun′). However, this difference is not essential as we see in Lemma 5.21.

Lemma 5.21 If a and b are general λε-terms, a′ is a λε-term, a ≡_{α} a′, and a →_{λε} b, then there is a λε-term a′′ and b′ such that a′ ≡_{α}^{λ} a′′, b′ ≡_{α} b, and a′′ →_{λε} b′. Here, if a →_{λε} b by (fun), then a′′ →_{λε} b′ by (fun′), otherwise, a′′ →_{λε} b′ by the same rule as a →_{λε} b.

Proof. This theorem is proved by induction on a →_{λε} b. We prove only the base case e[[λx. b]] →_{λε} λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]]. Other cases are similar or trivial. In this case, we have a λε-term e′[[λx′. b′]] such that e[[λx. b]] ≡_{α} e′[[λx′. b′]]. Then, we can find a λε-term λx′′. b′′ such that λx′′. b′′ ≡_{α}^{λ} λx′. b′ and x′′ ∉ TY(e′) ∪ FV(e′). So, we will prove

λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]] ≡_{α} λx′′. e′[[b′′]]  (⋆)

in the following. We have two cases according to the form of e. (In the following, ^{∗} stands for ^{∗ε} and ι for ι_{1}.)

1. e ≢ {a_{1}/y_{1}, …, a_{n}/y_{n}}: In this case, we have e^{∗} ≡ e^{′∗} and b^{∗}[{ι/x}] ≡ b^{′′∗}[{ι/x′′}], since e[[λx. b]] ≡_{α} e′[[λx′′. b′′]]. On the other hand, we have

(λx. (e↑^{{x}})[[b↕_{{x}}^{TY(e)}]])^{∗} ≡ λι. e^{∗}[[b^{∗}[{ι/x}]]]

as we have shown in the proof of Theorem 5.17. By a similar calculation, but using x′′ ∉ TY(e′) and x′′ ∉ FV(e′) in this case, we have

(λx′′. e′[[b′′]])^{∗} ≡ λι. e^{′∗}[[b^{′′∗}[{ι/x′′}]]].

Therefore, we have (⋆).

2. e ≡ {a_{1}/y_{1}, …, a_{n}/y_{n}}: As we have shown in the proof of Theorem 5.17, we have

a_{p(i)}^{∗} ≡ a′_{q(i)}^{∗}, b^{∗}[\{ι/x\}][\{\overline{ι}′/\overline{y}\}] ≡ b^{′′∗}[\{ι/x′′\}][\{\overline{ι}′/\overline{y′}\}]

where y_{p(1)} ≺ ⋯ ≺ y_{p(n)}, \{\overline{ι}/\overline{y}\}:= \{ι_{1}/y_{p(1)}, …, ι_{n}/y_{p(n)}\}, e′ ≡ \{a′_{1}/y′_{1}, …, a′_{n}/y′_{n}\}, y′_{q(1)} ≺ ⋯ ≺ y′_{q(n)}, and \{\overline{ι}/\overline{y′}\} := \{ι_{1}/y′_{q(1)}, …, ι_{n}/y′_{q(n)}\}. We have also shown

(λx. (e↑^{\{x\}})[[b↕_{\{x\}}^{TY(e)}]])^{∗} ≡ λι. \{a_{p(1)}^{∗}/ι_{1}, …, a_{p(n)}^{∗}/ι_{n}\}[[b^{∗}[\{♯ι/x\}][\{\overline{ι}/\overline{y}\}]]].

By a similar calculation, but using x′′ ∉ Y and x′′ ∉ FV(a′_{i}) in this case, we have

(λx′′. e′[[b′′]])^{∗} ≡ λι. \{a′_{q(1)}^{∗}/ι_{1}, …, a′_{q(n)}^{∗}/ι_{n}\}[[b^{′′∗}[\{♯ι/x′′\}][\{\overline{ι}/\overline{y′}\}]]].

Therefore, we have (⋆). □

Theorem 5.22 (Conservativity) Let a and b be λε-terms.

1. If a →^{∗}_{λκε} b, then there is a λε-term b′ such that a ^{λε}→^{∗} b′ and b ≡_{α} b′.

2. If a ^{λε}→^{∗} b, then there is a λε-term b′ such that a →^{∗}_{λκε} b′ and b ≡_{α} b′.

Proof. 1. The reduction sequence a →^{∗}_{λε} b is of the form a_{1} →_{λε} ⋯ →_{λε} a_{n} where a ≡ a_{1} and b ≡ a_{n}. (Note that a_{i} is a general λε-term.) We define λε-terms a′_{i} (i = 1, …, n) and a′′_{i} (i = 1, …, n − 1) as follows. First, we put a′_{1} := a_{1}. Next, assume we have a λε-term a′_{i} such that a_{i} ≡_{α} a′_{i}. By Lemma 5.21, there are λε-terms a′′_{i} and a′_{i+1} such that a′′_{i} →_{λε} a′_{i+1}, a′_{i} ≡_{α}^{λ} a′′_{i}, and

a_{i+1} ≡_{α} a′_{i+1}. Since a′_{i} →^{λε} a′_{i+1}, we have a_{1} ^{λε}→^{∗} a′_{n}.

2. The reduction sequence a ^{λε}→^{∗} b is of the form a_{1} →^{λε} ⋯ →^{λε} a_{n} where a ≡ a_{1} and b ≡ a_{n}. We define λε-terms a_{i}^{∘} (i = 1, …, n) as follows. First, we put a_{1}^{∘}:= a_{1}. Next, assume we have a_{i}^{∘} such that a_{1} →^{∗}_{λε} a_{i}^{∘} and a_{i}^{∘} ≡_{α} a_{i}.

Since a_{i} →^{λε} a_{i+1}, we have a′_{i} and a′_{i+1} such that a′_{i} ≡_{α}^{λ} a_{i}, a′_{i+1} ≡_{α}^{λ} a_{i+1},

and a′_{i} →_{λε} a′_{i+1}. So we have a′_{i} ≡_{α} a_{i}^{∘}. By Lemma 5.21, there is a λε-term

a_{i+1}^{∘} such that a_{i}^{∘} →_{λε} a_{i+1}^{∘} and a_{i+1}^{∘} ≡_{α} a′_{i+1}. So, we have a_{1} →^{∗}_{λε} a_{i+1}^{∘} and

a_{i+1}^{∘} ≡_{α} a_{i+1}. Therefore, we can take a_{n}^{∘} as b′. □

In [18], it is proved that λε is a conservative extension of the simply typed lambda calculus λβ. To express the conservativity within λκε, we embed the λβ-terms in the λκε-terms similarly to 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. We represent the reduction rule of λβ in λκε as follows: Let a and b be λβ-terms. We write a →^{β} b if there exist λβ-terms a′ and b′ such that a ≡_{α} a′, b ≡_{α} b′, and a′ →_{β} b′, where the conversion ↦_{β} is defined by the following rule.

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

Then, we have the following theorem.

Theorem 5.23 (Theorem 5.8 [18]) Let a and b be λβ-terms. Then, a ^{β}→^{∗}

b iff a ^{λε}→^{∗} b.

By combining Theorem 5.22 and 5.23, we have the conservativity of λκε over the simply typed λβ-calculus.

Theorem 5.24 (Conservativity) Let a and b be λβ-terms. Then, a ^{β}→^{∗} b iff there is a λβ-term b′ such that a →^{∗}_{λκε} b′ and b ≡_{α} b′.

Proof. The only-if-part is proved by Theorem 5.22 and 5.23. The if-part is proved as follows. By Theorem 5.22, there is a λε-term c such that a ^{λε}→^{∗} c and b′ ≡_{α} c. Let a_{n−1} →^{λε} c be the last step of the reduction sequence. Then there exist a′_{n−1} and c′ such that a′_{n−1} →_{λε} c′, a_{n−1} ≡_{α}^{λ} a′_{n−1}, and c ≡_{α}^{λ} c′. Since c is a λβ-term, b ≡_{α}^{λ} c. So, we have b ≡_{α}^{λ} c′. Therefore, we have a_{n−1} →^{λε} b, so that a ^{λε}→^{∗} b. By Theorem 5.23, we have a ^{β}→^{∗} b. □

Now, we prove Theorem 3.1 which relates α-equivalence and substitution.

Lemma 5.25 Let a be a λκε-term and s be a canonical environment term.

(a[s])^{∗λ} ≡ a^{∗λ}[s^{∗λ}], (a[s])^{∗ε} ≡ (a^{∗ε}[s^{∗ε}])^{∗ε}

Proof. The first identity can be proved similarly to Lemma 5.15. The second one can also be proved similarly, but we have to take care of the case that a has a subterm z[[b]] and s is of the form {…, e/z, …} where e is a canonical environment term. □ Proof of Theorem 3.1. By Lemma 5.25, we have (a[s])^{∗λ} ≡ a^{∗λ}[s^{∗λ}] ≡ b^{∗λ}[s^{∗λ}] ≡ (b[s])^{∗λ} and (a[s])^{∗ε} ≡ (a^{∗ε}[s^{∗ε}])^{∗ε} ≡ (b^{∗ε}[s^{∗ε}])^{∗ε} ≡ (b[s])^{∗ε}. □

Theorem 5.26 (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 λε [18], because we can treat the cases of (abs) and (absapp) similarly to the cases of (fun) and (funapp). □

6 Related Works

In this section, we compare our calculus with some related works.

In the formulation of contexts in λκε, first-class environments (or explicit substitutions) play an essential role. Abadi et al [1] first introduced explicit substitutions, and there are many interesting works on this subject since then. However, to our knowledge, the λε-calculus [18] is the only language which is pure in our sense. We therefore designed our calculus as an extension of λε.

The style of the presentation of our paper is very close to that of Hashimoto-Ohori [10]. Both our calculus and the calculus presented in [10] are simply typed calculi which include simply typed λβ-calculus as their subcalculus. The system in [10] 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.

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

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 [12] introduces a system with first-class contexts in which contexts are directly represented as terms in his calculus. However, he defines holefilling as a meta-level operation. It is therefore not possible to compute holefilling within his system. Unlike these systems, in λκε, contexts are directly representable as terms of λκε, and we can compute hole-filling within λκε.

Sands [16] uses Pitts’ [14] definition of contexts and shows that holefilling 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 [16] 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.

7 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 [18] and also we have realized our hope, which we stated in the conclusion of [18], 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.

References

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit Substitutions. Journal of Functional Programming, 1:375–416, 1991.

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

[3] R. Bloo and K.H. Rose. Preservation of Strong Normalization in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In van Vliet J. C., editor, Proc. CSN’95 (Computer Science in Netherlands), 1995. (ftp://ftp.diku.dk/

    diku/semantics/papers/D-246.ps).

[4] M. Bognar and R. de Vrijer. A calculus of lambda calculus contexts. J. Automated Reasoning, 27:29–59, 2001.

[5] L. Dami. A Lambda-Calculus for Dynamic Binding. Theoretical Computer Science, 192:201–231, 1998.

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

[7] M. Fiore, G. Plotkin, and D. Turi. Abstract Syntax and Variable Binding (Extended Abstract). In Proc. 14th Symposium on Logic in Computer Science, pages 193–202, 1999.

[8] J. Garrigue and H. Aït-Kaci. The Typed Polymorphic Label-Selective λ-Calculus. In Proc. 21st Annual ACM Symposium on Principles of Programming Languages, pages 35–48, 1994.

[9] C. Gunter. Semantics of Programming Languages. The MIT Press, 1992.

[10] M. Hashimoto and A. Ohori. A Typed Context Calculus. Preprint RIMS-1098. Research Institute for Mathematical Sciences, Kyoto University, 1996. (Journal version is to appear in Theoretical Computer Science.).

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

[12] I. Mason. Computing with Contexts. Higher-Order and Symbolic Computation, 12:171–201, 1999.

[13] P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In Proc. Second International Conference on Typed Lambda Calculi and Applications, LNCS 902, pages 328–349, 1995.

[14] A. M. Pitts. 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.

[15] H. Sakurada. An Interpretation of a Context Calculus in an Environment Calculus. Transactions of Information Processing Society of Japan: Programming, 41(SIG 9 (PRO 8)):1–7, 2000.

[16] D. Sands. Computing with Contexts - a simple approach. Electronic Notes in Theoretical Computer Science, 10, 1998.

[17] M. Sato. Theory of Symbolic Expressions, II. Publ. of Res. Inst. for Math. Sci., Kyoto Univ., 21:455–540, 1985.

[18] M. Sato, T. Sakurai, and R. Burstall. Explicit Environments. Fundamenta Informaticae, 45(1-2):79–115, 2001.

[19] C. Talcott. A Theory of binding structures and applications to rewriting. Theoretical Computer Science, 112(1):99–143, 1993.