IOS Press

Explicit Environments

Masahiko Sato^{∗}

Graduate School of Informatics Kyoto University Kyoto, Japan masahiko@kuis.kyoto-u.ac.jp

Takafumi Sakurai^{†}

Department of Mathematics and Informatics Chiba University Chiba, Japan sakurai@math.s.chiba-u.ac.jp

Rod Burstall^{‡}

Department of Computer Science University of Edinburgh Edinburgh, UK rb@dcs.ed.ac.uk

Abstract. We introduce λε, a simply typed calculus with environments as first class values. As well as the usual constructs of λ and application, we have e[[a]] which evaluates term a in an environment e. Our environments are sets of variable-value pairs, but environments can also be computed by function application and evaluation in some other environments. The notion of environments here is a generalization of explicit substitutions and records. We show that the calculus has desirable properties such as subject reduction, confluence, conservativity over the simply typed λβ-calculus and strong normalizability.

∗Address for corespondance: Graduate School of Informatics, Kyoto University, Kyoto, Japan †Address for corespondance: Department of Mathematics and Informatics, Chiba University, Chiba, Japan ‡Address for corespondance: Department of Computer Science, University of Edinburgh, Edinburgh, UK

Keywords: explicit environments, simply typed calculus, confluence, conservativity, strong normalizability

1. Introduction

In this paper, we solve the problem of designing a pure functional language that has explicit environments. We understand that a functional language is pure 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 well-behaved and the confluence property and SN or PSN would guarantee that the language is computationally well-behaved.

What do we mean by explicit environments? An explicit environment is a set of variable-value pairs representing a finite function from variables to values

(i) which is equipped with an operation ·[[·]] such that, e[[a]] is the evaluation of a term a in the environment e, and

(ii) which can be the argument or result of a function. (It is a “first class value”.)

Explicit environments can be regarded as a generalization of explicit substitutions and records:

• An explicit substitution has property (i) above but not (ii).

• A record has property (ii) above but not (i).

Without the purity conditions, there are already several languages with explicit environments. For example, several versions of the programming language Scheme [2] have explicit environments. The Pebble language of Lampson and Burstall [15] also treated explicit environments (bindings). It used dependent types and no confluence result was obtained. Nishizaki [19, 18] also attempted to treat explicit environments, but his system does not satisfy the conservative extension condition because he avoided the problem of defining the set of free variables for a term of his language. As we will soon see, giving a correct definition of free variables in a term becomes a difficult problem if the term in question contains variables whose values are environments. These languages are, however, exceptional, and in most programming languages, environments are implicit in the sense that they are used at meta-level as a device for giving formal semantics of these languages or they are used when implementing these languages, but they do not appear as syntactic entities of these languages.

On the other hand, there are quite a few typed or untyped calculi of explicit substitutions including [1, 4, 6, 13], and some of these are pure in our sense. However, to the best of our knowledge, there are no calculi of explicit substitutions in which substitutions are first class objects. So, we believe that our language is the first pure language that has substitutions as its first class objects, since as we explain below we may regard environments as substitutions. Among the calculi of explicit substitutions, λx [6] is the simplest one and both typed and untyped λx are pure. They are simple because they do not have composition rules of substitutions. If we do not treat environments of λε as first class objects, λε becomes a similar calculus to typed λx, but we cannot do without composition rule of environments in the case of λε, because we have to handle nested environments as we see in section 2. Therefore, we had to develop new method to prove SN of λε.

Our use of ‘environment’ derives from LISP which has explicit environments in our sense. In what follows we will generally just say ‘environment’ for ‘explicit environment’ where the context makes this clear. A concept closely related to explicit environment is let declaration (SML) or local definition. In SML, declarations are not first class values, but they do permit some combination operations, such as ;.

Let us compare these language features, showing notations and their expressivity. When we give the formation rules for our calculus with environments we can be more precise.

• Explicit environment {a/x, b/y}[[c]]: Evaluate term c in an environment which binds x to a and y to b.

• Explicit substitution [x := a, y := b]c: Substitute a for x and b for y in term c.

• Record [x = a, y = b].x: Extract the x field of the record [x = a, y = b]; x is a field name.

• Let let x = a and y = b in c: Declare local variables x with value a, y with value b. Use these to evaluate c.

The syntax for these features show that our environments are the most general allowing terms for both e and a in e[[a]].

Explicit environment term[[term]]
Explicit substitution  [var := term, …, var := term]term
Record  term.fieldName
Let  let declaration in term

In the above table, declaration (d) is defined by the grammar:

d ::= var = term | d; d | d and d | local d in d.

In section 2, we make an attempt to design an untyped language with the conservative extension and confluence properties; this shows up a number of difficulties. In particular, we find that it is hard to define an untyped system. In section 3, we introduce a typed language λε by introducing typing rules for terms that will determine the (typable) terms of the language. In section 4, we give reduction rules of the λεcalculus and prove the subject reduction theorem for the calculus. In section 5, we prove the confluence of λε and prove that the λε-calculus is a conservative extension of the simply typed λβ-calculus. In section 6, we prove the strong normalizability of λε. By the results obtained in sections 3-6, we can see that λε provides a language we wanted to design. In section 7, we give concluding remarks and compare λε with other calculi.

2. An Attempt

We begin with a naïve approach, and try to develop an untyped calculus that would solve our problem. So, we wish to design a calculus with the mechanisms of:

• functional abstraction of an expression b with respect to a variable x, which we write as λx.b,

• application of a function b to an argument a, which we write as ba, and

• evaluation of an expression a in an environment e, which we write as e[[a]].

Such a calculus will provide us a way to pass an environment as an argument to a function and also a way to return an environment as the result of a functional application.

Let us use the untyped λβ-calculus as a base calculus for our calculus, since our calculus must be conservative over it. The syntax of the untyped λβ-calculus is as follows.

a, b ::= x ; variable | λx.b ; abstraction | ba ; application.

The λβ-calculus has the single conversion rule:

(β) (λx.b)(a) ↦_{β} b[x := a],

where b[x := a] stands for the result of applying the substitution operator [x := a] (which substitutes a for x) to the term b. This substitution operation is performed at meta-level, and we can get the result of this operation (which is a λ-term) by using the following definitional equalities as meta-level reduction rules (see, e.g., page 27 of [3]).

(S1) x[x := a] ≡ a (S2) y[x := a] ≡ y, if x ≢ y (S3) (λy.b)[x := a] ≡ λy.(b[x := a]) (S4) (bc)[x := a] ≡ (b[x := a])(c[x := a]).

In (S3), we assume the usual convention on variables, that is, we assume that the bound variable y is chosen so that y ≢ x and y is not free in a. This also means that we are identifying α-congruent expressions.

Now we try to add environments as first-class values to the λβ-calculus. Recall that an environment (say, e) is a finite set of bindings, where a binding is just a pair of a variable x and a term a which is usually written as a/x. So, any environment e can be written in the form:

e ≡ {a_{1}/x_{1}, a_{2}/x_{2}, …, a_{n}/x_{n}} (x_{i} distinct).

Such an e defines the following substitution function, which we again denote by e, and whose domain is the set of variables:

e(x) := \{ \begin{matrix}a_{i} & if x ≡ x_{i} for some i \\ x & otherwise. \end{matrix}

In this way, we may represent substitution by an environment.

Moreover, we wish to internalize the substitution operation which we normally perform at metalevel in order to carry out the β-reduction. We follow LISP’s approach [16] which uses an environment in applying a function to its arguments. So, we will try to simulate the application of the substitution [x_{1} := a_{1}, …, x_{n} := a_{n}] to a term a by the evaluation of the form:

{a_{1}/x_{1}, …, a_{n}/x_{n}}[[a]].

Putting these together, we define the terms of our calculus by the following grammar: a, b, e ::= x ; variable

| λx.b ; abstraction | ba ; application | {a_{1}/x_{1}, …, a_{n}/x_{n}}; environment | e[[a]] ; evaluation.

It should be clear that the above syntax can represent environments as first-class values. The problem, then, is to define conversion rules appropriately so that we can really do computations on environments.

To achieve this, we begin with the simulation of substitution by evaluation. As we saw above, substitution is carried out by β-reduction in the λ-calculus, and we wish to simulate it by the following rule.

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

In the λ-calculus, as we remarked above, b[x := a] is just a meta-level abbreviation for a term in the λ-calculus, but the corresponding term {a/x}[[b]] must be computed internally. By the same token, the definitional equalities for substitution (S1)-(S4) must become equalities in our calculus. So, it is natural to introduce the corresponding conversion rules, but here we encounter three problems.

Multiple substitution. The first problem is this. In the λ-calculus, a function always takes only one argument, so in order to carry out conversions, there is no need to define simultaneous substitutions such as [x := a, y := b]. This is also the case for some calculi [4, 6, 13] of explicit substitutions. But, since our calculus has first-class environments, our rules must be able to compute expressions of the form:

{a_{1}/x_{1}, a_{2}/x_{2}, …, a_{n}/x_{n}}[[b]].

where n ≥ 0. To solve this problem, let us introduce the following rules instead of the rules (S1)-(S4) and see if they work as expected.

(E1) {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{i}]] ↦ a_{i}. (E2) {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x]] ↦ x, if x ≢ x_{i} for all i. (E3) e[[λy.b]] ↦ λy.e[[b]]. (E4) e[[bc]] ↦ e[[b]]e[[c]]. (E5) e[[{a_{1}/x_{1}, …, a_{n}/x_{n}}]] ↦ {e[[a_{1}]]/x_{1}, …, e[[a_{n}]]/x_{n}}.

The rules (E1)-(E4) are generalized versions of (S1)-(S4). The rule (E5) is used to evaluate environments.

Determining free variables. We could thus solve the first problem, but we immediately face a second problem. Since the rule (E3) corresponds to (S3), we must formulate a precise condition under which (E3) may be applied. But, consider

{z[[y]]/x}[[λy.x]],

where x, y, z are distinct variables. In order to know if (E3) is applicable to this term, as in the case of standard λ-calculus, we have to know the set of free variables in z[[y]]. (Otherwise, we cannot even tell whether α-renaming is necessary or not.) What is the set of free variables in z[[y]]? It may look as if y and z are both free in z[[y]], but, we cannot tell if y is free or not, unless we know what variables are bound by z which is the environment we use to compute y. To overcome this difficulty, we will introduce a type system so that the type of z will give that information.

Nested evaluation. The third problem is that these rules are not sufficient. Consider the evaluation of

{{a/x}/y}[[y[[x]]]]

as an example, where a is an arbitrary term and x and y are distinct variables. This term asks us to evaluate x under the environment y where we have yet another external environment {{a/x}/y} which is used to evaluate y[[x]]. But, none of (E1)-(E5) are applicable to this term, since y is a variable. So, we need some rules that can handle nested evaluations. Note that we must accept this term as a syntactically meaningful expression, since environments are to be first-class values of the calculus. This expression is not meaningful in the calculi of explicit substitutions, since substitutions are not first-class values, so this problem does not occur in the calculi of explicit substitutions, but we have to solve it if we wish to include environments as first-class values of the calculus.

We have thus seen that the rules (E1)-(E5) are not sufficient and that the condition under which the rule (E3) may be applied is not so obvious. To solve these problems, we introduce a typed version of environment calculus in the following sections.

3. The Type System

In this section we introduce the λε-calculus^{1} as an extension of the simply typed λβ-calculus. We assume that we have an infinite set of variables which is a disjoint union of an infinite set of bindable variables and an infinite set of unbindable variables. We will design our syntax in such a way that an unbindable variable never gets bound. The distinction of these two kinds of variables will become important only in the proof of strong normalizability of our calculus. So, until then, the reader may read the paper assuming that all the variables are bindable.

The untyped λε-terms are defined by the following grammar, where z ranges over variables (bindable or unbindable), x over bindable variables and x_{1}, …, x_{n} (n ≥ 0) are distinct bindable variables.

a, b, e ::= z | λx.b | ba | {a_{1}/x_{1}, …, a_{n}/x_{n}} | e[[a]].

For each term a we associate a finite set Π(a) of strings over 1, 2, …, which we call positions, as follows. We call this set the position set of a. We use Λ to denote the empty string and π, σ, τ etc. to denote positions.

1. Π(x) := {Λ}.

2. Π(λx.a) := {Λ} ∪ 1Π(a).

3. Π(ba) := {Λ} ∪ 1Π(b) ∪ 2Π(a).

4. Π({a_{1}/x_{1}, …, a_{n}/x_{n}}) := {Λ} ∪ 1Π(a_{1}) ∪ ⋯ ∪ nΠ(a_{n}).

5. Π(e[[a]]) := {Λ} ∪ 1Π(e) ∪ 2Π(a).

For each π ∈ Π(a), we associate a term a/π as follows.

1ε is for environment.

1. a/Λ := a.

2. λx.a/1π := a/π.

3. ba/1π := b/π, ba/2π := a/π.

4. {a_{1}/x_{1}, …, a_{n}/x_{n}}/iπ := a_{i}/π (1 ≤ i ≤ n).

5. e[[a]]/1π := e/π, e[[a]]/2π := a/π.

If b ≡ a/π, then we say that b occurs in a at position π. Let π and σ be positions. We write π ⊑ σ if π is an initial substring of σ, that is, σ ≡ ππ′ for some π′. We write π ⊏ σ if π′ ≢ Λ.

We define types (A, B) and environment types (E) simultaneously as follows, where K ranges over atomic types and in the definition of E, n ≥ 0, x_{i} must be bindable variables and x_{i}^{A_{i}} must be distinct.

A, B ::= K | E | A ⇒ B
E ::= {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}}

If E ≡ {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} we say that x_{i}^{A_{i}} (1 ≤ i ≤ n) are in the environment type E. If a term e has type E by the typing rules we introduce below, then e is an environment and it is a first-class value of the calculus.

A declaration is an expression of the form x^{A} where x is a variable and A is a type. A context is a finite set {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} of declarations. We use Γ, Δ etc. as meta variables for contexts. We will write Γ, Δ for the union of the contexts Γ and Δ. Also, Γ − E will denote the context obtained from Γ by removing all the elements in E from Γ. We will sometimes omit the brackets { } of contexts.

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

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

\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}^{A_{1}}, …, x_{n}^{A_{n}}\} \end{matrix} (envI)

\begin{matrix}Γ ⊢ e : E & Δ ⊢ a : A \\ Γ, (Δ − E) ⊢ e[[a]] : A \end{matrix} (envE).

In (⇒I), x must be a bindable variable. We see by the (envI) rule that the environment type {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} for n = 0 becomes the unit type {} whose unique element is the empty environment {}.

An expression a is said to be a (typed) term if a typing judgment of the form Γ ⊢ a : A is derivable for some Γ and A. A λε-term is canonical if it is of the form λx^{A}.b or {a_{1}/x_{1}^{A_{1}}, …, a_{n}/x_{n}^{A_{n}}}, that is, if it is obtained by one of the introduction rules. A λε-term is neutral if it is not canonical. If Γ ⊢ a : A is derivable and Γ does not contain bindable variables (that is, all variables in Γ are unbindable variables), then a is said to be bindable variable free. A λε-term is said to be an environment term if its type is an environment type.

An untyped λε-term a′ is said to be typable if we can derive Γ ⊢ a : A for some Γ, a and A by using the above typing rules and a′ is obtained from a by erasing all the types in a (that is, by replacing each declaration x^{A} in a by x). In this case a′ is called the type-free form of a. Henceforth, we will often use the type-free form of λε-terms for the sake of notational simplicity.

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}. In this case, we write TY(a) (type of a) for A. 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 can now use TY(e) to tell if a given occurrence of a variable in a term is free. Consider the expression (λx.fxy)y. There are two free occurrences of y. We will describe an occurrence by a term with a hole (□) in it, and we say y is free at (λx.fx□)y and y is free at (λx.fxy)□. The syntax of occurrences is:

α, β, ε ::= □ | λx.β | βa | bα
| {…, a_{i−1}/x_{i−1}, α/x_{i}, a_{i+1}/x_{i+1}, …}
| ε[[a]] | e[[α]].

The inductive definition of ‘variable is free at occurrence’ follows the syntax of terms.

x is free at □ x is free at β x is free at λy.β (if x ≢ y)

x is free at β ; x is free at βa x is free at α ; x is free at bα

x is free at α x is free at {…, a_{i−1}/x_{i−1}, α/x_{i}, a_{i+1}/x_{i+1}, …}

x is free at ε x is free at ε[[a]] x is free at α x is free at e[[α]] (if x ∉ TY(e)).

We define FV(a) as the set of variables occurring free in a. It can be easily verified that if Γ ⊢ a : A is derivable, then Γ, considered as a set, is equal to FV(a). In particular, a is closed, i.e., FV(a) = ∅, iff ⊢ a : A is derivable.

We can easily define replacement of a variable in an occurrence to get a term, just textual replacement of the □.

• replace x in □:= x.

• replace x in βa:= (replace x in β)a, and so on.

α-congruence. Let a and b be terms and x, y be bindable variables of the same type such that y is fresh in a (that is, y is neither free nor bound in a). Then we will identify λx.a with λy.c where c is obtained from a by replacing each free occurrence of x by y. Here, the α-congruence means changing the names of λ bound variables but not those appearing in environment expressions as x in {a/x}.

2It is, in general, not possible to recover the typed form when its type-free form is given. Therefore, even if we write terms in type-free forms, it is only for the sake of simplicity, and we are in fact dealing with fully decorated typed terms.

We will write a : A if A ≡ TY(a). The following example gives a typing derivation for the term {y/x}[[x]] ≡ {y^{A}/x^{A}}[[x^{A}]]:

\begin{matrix}{y^{A} ⊢ y : A \atop y^{A} ⊢ \{y/x\} : \{x^{A}\}} & x^{A} ⊢ x : A \\ y^{A} ⊢ \{y/x\}[[x]] : A \end{matrix}.

The following example reveals the subtle point which is related to the fact that in the λε-calculus we can pass an environment as an argument to a function.

\begin{matrix}z^{\{x^{A⇒B},y^{A}\}} ⊢ z : \{x^{A⇒B}, y^{A}\} & \begin{matrix}x^{A⇒B} ⊢ x : A ⇒ B & y^{A} ⊢ y : A \\ x^{A⇒B}, y^{A} ⊢ xy : B \end{matrix} \\ z^{\{x^{A⇒B},y^{A}\}} ⊢ z[[xy]] : B \end{matrix} ; ⊢ λz.(z[[xy]]) : \{x^{A⇒B}, y^{A}\} ⇒ B

4. Reduction Rules

In this section we define a reduction relation →_{λε} on λε-terms. Then, in this and the following sections, we show that →_{λε} enjoys the subject reduction property, →_{λε} is confluent and strongly normalizing, and the λε-calculus is a conservative extension of the simply typed λβ-calculus. In this way, we can show that the λε-calculus solves the problem we posed in section 1.

We first define ↦_{λε} as the union of the two relations ↦_{λ} and ↦_{ε}, where the relation ↦_{λ} is defined by the following single rule:

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

and the relation ↦_{ε} is defined by the following 6 conversion rules. These 6 rules will be called ε-rules^{3}. They evaluate expressions of the form e[[a]].

(gc) e[[a]] ↦_{ε} a, if TY(e) ∩ FV(a) = ∅.
(var) {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{i}]] ↦_{ε} a_{i} (1 ≤ i ≤ n).
(abs) e[[λx.b]] ↦_{ε} λx.e[[b]], if x ∉ TY(e) ∪ FV(e).
(app) e[[ba]] ↦_{ε} e[[b]]e[[a]].
(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 first five rules correspond to the rules (E1)-(E5) we gave in section 2. The rules (var), (app) and (env) are exactly the same as (E1), (E4) and (E5), respectively. The garbage collection rule (gc), which collects e as a garbage, is a generalized version of (E2) (see [6]). We can see the correctness of this rule intuitively, because TY(e) ∩ FV(a) = ∅ means that variables in FV(a) are not bound by e. The (abs) rule pushes the environment e through the λx binder. Thanks to the typing information about e, we could precisely state the condition under which we may push the environment e through the λx binder. We note that the condition x ∉ TY(e) ∪ FV(e) can always be met by taking a suitable α-congruent term.

3ε is for environment.

As pointed out in section 2, these rules are not sufficient, so we introduced the last rule (eval) to take care of the nested evaluation sufficiently. It may seem that one needs a rule which reduces a term of the form e[[f[[a]]]] for any term a which may or may not be a variable. But, such a rule is not necessary, since if a is not a variable, then a is either of the form g[[b]], or otherwise we can reduce f[[a]] by one of the rules (abs), (app) or (env). If a is of the form g[[b]], then we can repeatedly apply this argument to f[[g[[b]]]]. So, we only need a rule that reduces e[[f[[x]]]]. Now, if x ∉ TY(f), then we can convert f[[x]] to x by the (gc) rule. In this way, we arrived at the rule (eval). Theorem 4.1 below shows that these reduction rules comprise a sufficiently rich set of reduction rules. We will discuss further about our choice of the reduction rules at the end of subsection 6.2.

If π ∈ Π(a) and b is a term which is of the same type as a/π, then a_{π}[b] stands for the term which is obtained from a by textually replacing its subterm a/π at π with b. Then the reduction relation → is defined by stipulating that a → a_{π}[b] if and only if a/π ↦_{λε} b. We write →^{∗} for the reflexive and transitive closure of the relation →, and →^{+} for the transitive closure of →.

A λε term a is said to be strongly normalizing (SN, for short) if there are no infinite reduction sequences starting from a. If a is SN, then we write ν(a) for the length of the longest reduction sequence starting from a. We understand that ν(a) = 0 if a is normal.

If \overline{e} ≡ e_{1}, …, e_{n}, then we will write \overline{e}[[a]] for e_{1}[[⋯ e_{n}[[a]] ⋯]].

The following theorem shows that we have a sufficiently rich set of reduction rules.

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

Proof: By induction on the derivation of c : C. We classify cases according to the last rule used to derive c : C.

1. (assume): Since c is closed, we do not have this case.

2. (⇒I): c is canonical in this case.

3. (⇒E): In this case c is of the form ba. Since b is closed and normal, by IH, we see that b is of the form λx.b′. Hence ba is not normal. This is a contradiction.

4. (envI): c is canonical in this case.

5. (envE): In this case c is of the form e[[a]] where e is closed and normal. Hence, by IH, we see that e ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}. Since c is normal, we see that a must be a variable or of the form f[[a′]].

5.1. a ≡ x: Since e[[x]] is closed, we see that x ∈ TY(e). So, we have x ≡ x_{i} for some i. Hence we have e[[x]] → a_{i} by the (var) rule. This is a contradiction. 5.2. a ≡ f[[a′]]: Since f[[a′]] is normal, we see that a′ is either a variable or of the form g[[a′′]]. By repeating this argument, we see that c is of the form e[[f[[\overline{g}[[x]]]]]], where \overline{g} ≡ g_{1}, …, g_{m} (m ≥ 0). In other words, c is of the form \overline{g′}[[e′[[f′[[x]]]]]]. Here we have two cases. 5.2.1.x ∈ TY(f′): In this case we get a contradiction, since we can convert c to \overline{g′}[[e′[[f′]][[x]]]] by the (eval) rule.

5.2.2.x ∉ TY(f′): In this case we get a contradiction, since we can convert c to \overline{g′}[[e′[[x]]]] by the (gc) rule. ⊓ ⊔

Let Γ and Γ′ be contexts. Then we say that Γ′ is a subcontext of Γ if each x^{A} in Γ′ is also in Γ. In other words, Γ′ is a subcontext of Γ if the set consisting of the members of Γ′ is a subset of the set consisting of the members of Γ. We will write Γ′ ⊆ Γ if Γ′ is a subcontext of Γ.

Our reduction relation →_{λε} enjoys the subject reduction property.

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

Proof: We first check that the theorem holds for each conversion rule. Here, we omit easy cases of (var), (abs) and (app).

1. (λ): In this case, the given typing derivation is as follows.

\begin{matrix}⋮ ; Γ ⊢ b : B ; Γ − \{x^{A}\} ⊢ λx.b : A ⇒ B & ⋮ ; Δ ⊢ a : A \\ (Γ − \{x^{A}\}), Δ ⊢ (λx.b)(a) : B \end{matrix}.

From this derivation, we have the following typing derivation for the term after the conversion.

\begin{matrix}⋮ ; Δ ⊢ a : A ; Δ ⊢ \{a/x\} : \{x^{A}\} & ⋮ ; Γ ⊢ b : B \\ Δ, (Γ − \{x^{A}\}) ⊢ \{a/x\}[[b]] : B \end{matrix}.

2. (gc): The derivation is as follows.

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

Note that Δ − E ≡ Δ since TY(e) ∩ FV(a) = ∅. We can convert this to the following derivation:

⋮ ; Δ ⊢ a : A.

3. (env): We have the following derivation where we put Δ ≡ Γ_{1}, …, Γ_{n} and F ≡ {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}}

\begin{matrix}⋮ ; Γ ⊢ e : E & \begin{matrix}⋮ ; Γ_{1} ⊢ a_{1} : A_{1} & ⋯ & ⋮ ; Γ_{n} ⊢ a_{n} : A_{n} \\ Δ ⊢ \{a_{1}/x_{1}, …, a_{n}/x_{n}\} : F \end{matrix} \\ Γ, (Δ − E) ⊢ e[[\{a_{1}/x_{1}, …, a_{n}/x_{n}\}]] : F \end{matrix}.

We can convert this as follows, where we put Π ≡ (Γ, (Γ_{1} − E)), …, (Γ, (Γ_{n} − E)).

\begin{matrix}⋮ ; Γ ⊢ e : E & ⋮ ; Γ_{1} ⊢ a_{1} : A_{1} \\ Γ, (Γ_{1} − E) ⊢ e[[a_{1}]] : A_{1} \end{matrix} ⋯ \begin{matrix}⋮ ; Γ ⊢ e : E & ⋮ ; Γ_{n} ⊢ a_{n} : A_{n} \\ Γ, (Γ_{n} − E) ⊢ e[[a_{n}]] : A_{n} \end{matrix} Π ⊢ \{e[[a_{1}]]/x_{1}, …, e[[a_{n}]]/x_{n}\} : F.

4. (eval): The derivation is:

\begin{matrix}⋮ ; Γ ⊢ e : E & \begin{matrix}⋮ ; Δ ⊢ f : F & x^{A} ⊢ x : A \\ Δ, (x^{A} − F) ⊢ f[[x]] : A \end{matrix} \\ Γ, (Δ − E) ⊢ e[[f[[x]]]] : A \end{matrix}.

Note that x^{A} ∈ F so that x^{A} − F is empty. We can convert this to the following derivation:

\begin{matrix}\begin{matrix}⋮ ; Γ ⊢ e : E & ⋮ ; Δ ⊢ f : F \\ Γ, (Δ − E) ⊢ e[[f]] : F \end{matrix} & x^{A} ⊢ x : A \\ Γ, (Δ − E) ⊢ e[[f]][[x]] : A \end{matrix}.

The rest of the proof is carried out by induction on the construction of an occurrence α such that α[a] → α[b]. This is easily verified by inspecting our typing rules. ⊓ ⊔

This theorem says not only that the type is preserved by reduction, but also that the reduction never introduces new free variables. Thus, if we start from a closed term, then we always get closed terms by reductions of the given term.

We conclude this section by giving simple examples of λε programs (i.e., closed λε-terms) which show the expressivity of the language. We assume that we have integer type and the successor function s.

{λf.λx.f(f(x))/double}[[

        {double s/add2}[[

             {doubleadd2/add4}[[add2(add4(0))]]

]]

]] →^{∗}_{λε} 6.

{λf.λe.{f(e[[x]])/x, f(e[[y]])/y}/pointwise}[[

pointwise s {1/x, 2/y}

]] →^{∗}_{λε} {2/x, 3/y}.

5. Confluence and Conservativity

In this section, we prove the confluence property of the λε-calculus by combining Hardin’s interpretation method [11] (which is a standard method used to prove the confluence of calculi of explicit substitutions [1, 4, 6, 13]) with Takahashi’s parallel reduction method [20].

First, we show the following lemma.

Lemma 5.1. →_{ε} on λε-terms is noetherian and confluent.

Proof: In order to show that →_{ε} is noetherian, we introduce the measure |a| which is a positive integer for each λε-term as follows.

1. |x|:= 1.

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

3. |ba|:= |b| + |a| + 1.

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

5. |e[[a]]|:= (|e| + 1)|a|. We can then verify that a →_{ε} b implies |a| > |b|. Now, we can easily verify that →_{ε} on λε-terms is weakly Church-Rosser by checking the overlapping cases. Hence, we have the confluence by Newman’s Lemma. ⊓ ⊔

A λε-term a is said to be ε-normal if a →_{ε} b holds for no b. By the above lemma, we see that for any λε-term a there uniquely exist an ε-normal term b such that a →^{∗}_{ε} b. We will write ε(a) for this b. ε-normal terms are characterized by the following grammar, where u ranges over ε-normal terms and v over ε-normal terms such that x ∈ TY(v) and which are not canonical, that is, not of the form {a_{1}/x_{1}, …, a_{n}/x_{n}}.

u ::= x | λx.u | uu | {u/x, …, u/x} | v[[x]]

We now define the parallel reduction relation ⇒ on ε-normal λε-terms as follows.

1. x ⇒ x.

2. If a ⇒ b, then λx.a ⇒ λx.b.

3. If a ⇒ c and b ⇒ d, then (λx.a)b ⇒ ε({d/x}[[c]]).

4. If a ⇒ c and b ⇒ d, then ab ⇒ cd.

5. If a_{i} ⇒ b_{i} for i = 1, …, n, then {a_{1}/x_{1}, …, a_{n}/x_{n}} ⇒ {b_{1}/x_{1}, …, b_{n}/x_{n}}.

6. If e ⇒ f, then e[[x]] ⇒ ε(f[[x]]). Next, with each ε-normal term a, we associate an ε-normal term a^{∗} as follows.

1. x^{∗} := x.

2. (λx.a)^{∗} := λx.a^{∗}.

3. ((λx.a)b)^{∗} := ε({b^{∗}/x}[[a^{∗}]]).

4. (ab)^{∗} := a^{∗}b^{∗}, if a is not an abstraction.

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

6. (e[[x]])^{∗} := ε(e^{∗}[[x]]). It is easy to see that a ⇒ a^{∗} for any ε-normal term a. In this section, we work only in the λε-calculus. So, we will write a → b (a →^{∗} b) for a →_{λε} b (a →^{∗}_{λε} b), respectively. We have the following key Lemmas 5.2-5.6.

Lemma 5.2. If a ⇒ b, then a →^{∗} b. Proof: Easy. ⊓ ⊔

The following lemma will be used in the proof of Lemma 5.4. Lemma 5.3. If c is ε-normal and y ∉ TY(e) ∪ FV(e), then ε(e[[{d/y}[[c]]]]) ≡ ε({e[[d]]/y}[[e[[c]]]]). Proof: By induction on the construction of c. Since c is ε-normal, we have the following cases.

1. c is a variable: We have three subcases here. 1.1. c ≡ y:

LHS ≡ ε(e[[{d/y}[[y]]]]) ≡ ε(e[[d]]) (by (var)).
RHS ≡ ε({e[[d]]/y}[[e[[y]]]])
≡ ε({e[[d]]/y}[[y]])  (by (gc))
≡ ε(e[[d]])  (by (var)).

1.2. c ≡ x ≢ y and x ∈ TY(e):

LHS ≡ ε(e[[{d/y}[[x]]]])
≡ ε(e[[x]])  (by (gc)).
RHS ≡ ε({e[[d]]/y}[[e[[x]]]])
≡ ε({e[[d]]/y}[[e]][[x]]) (by (eval))
≡ ε(e[[x]])  (by (gc)).

1.3. c ≡ x ≢ y and x ∉ TY(e):

LHS ≡ ε(e[[{d/y}[[x]]]])
≡ ε(e[[x]])  (by (gc))
≡ ε(x)  (by (gc)).
RHS ≡ ε({e[[d]]/y}[[e[[x]]]])
≡ ε({e[[d]]/y}[[x]])  (by (gc))
≡ ε(x)  (by (gc)).

2. c ≡ λx.b:

LHS ≡ ε(e[[{d/y}[[λx.b]]]])
≡ ε(e[[λx.{d/y}[[b]]]])  (by (abs))
≡ ε(λx.e[[{d/y}[[b]]]])  (by (abs))
≡ ε(λx.{e[[d]]/y}[[e[[b]]]]) (by ind. hyp.).
RHS ≡ ε({e[[d]]/y}[[e[[λx.b]]]])
≡ ε({e[[d]]/y}[[λx.e[[b]]]]) (by (abs))
≡ ε(λx.{e[[d]]/y}[[e[[b]]]]) (by (abs)).

3. c ≡ ba: Straightforward computation using the (app) rule.

4. c ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}: Straightforward computation using the (env) rule.

5. c ≡ f[[x]], x ∈ TY(f) and f is not canonical: Since x ∈ TY(f), we can compute as follows.

LHS ≡ ε(e[[{d/y}[[f[[x]]]]]])
≡ ε(e[[{d/y}[[f]][[x]]]])  (by (eval))
≡ ε(e[[{d/y}[[f]]]][[x]])  (by (eval))
≡ ε(ε(e[[{d/y}[[f]]]])[[x]]).
RHS ≡ ε({e[[d]]/y}[[e[[f[[x]]]]]])
≡ ε({e[[d]]/y}[[e[[f]][[x]]]])  (by (eval))
≡ ε({e[[d]]/y}[[e[[f]]]][[x]])  (by (eval))
≡ ε(ε({e[[d]]/y}[[e[[f]]]])[[x]]).

We have ε(e[[{d/y}[[f]]]]) ≡ ε({e[[d]]/y}[[e[[f]]]]) by induction hypothesis. So, we have LHS ≡ RHS.

⊓ ⊔

The following lemma will be used in the proof of Lemma 5.5.

Lemma 5.4. If ε(a) ⇒ ε(a′) and ε(e) ⇒ ε(e′), then ε(e[[a]]) ⇒ ε(e′[[a′]]).

Proof: By induction on the construction of ε(a). Since ε(a) is ε-normal, we have the following cases.

1. ε(a) ≡ x: We consider the following two subcases.

1.1. x ∈ TY(e): This case is further divided into the following two subcases.

1.1.1.ε(e) is canonical: In this case, ε(e) is of the form {…, b/x, …}. Since {…, b/x, …}[[x]] ↦ b, we have ε(e[[x]]) ≡ ε(ε(e)[[x]]) ≡ ε(b) ≡ b. On the other hand, since ε(e) ⇒ ε(e′), we have ε(e′) ≡ {…, b′/x, …}, where b ⇒ b′. Hence, we have ε(e[[x]]) ≡ b ⇒ b′ ≡ ε(ε(e′)[[x]]) ≡ ε(e′[[x]]). 1.1.2.ε(e) is not canonical: In this case, ε(e)[[x]] is in ε-normal form. So, we have ε(e[[x]]) ≡ ε(ε(e)[[x]]) ≡ ε(e)[[x]]. Since ε(e) ⇒ ε(e′), we have ε(e)[[x]] ⇒ ε(ε(e′)[[x]]) ≡ ε(e′[[x]]).

1.2. x ∉ TY(e): In this case, by Lemma 5.2 and the subject reduction property of λε, we have TY(e′) ≡ TY(e). Hence, we have ε(e[[x]]) ≡ x ⇒ x ≡ ε(e′[[x]]).

2. ε(a) ≡ λx.c, c ⇒ c′ and ε(a′) ≡ λx.c′: By induction hypothesis, we have ε(e[[c]]) ⇒ ε(e′[[c′]]). Hence, we have ε(e[[a]]) ≡ ε(λx.e[[c]]) ≡ λx.ε(e[[c]]) ⇒ λx.ε(e′[[c′]]) ≡ ε(e′[[a′]]).

3. ε(a) ≡ cd, c ⇒ c′, d ⇒ d′ and ε(a′) ≡ c′d′: In this case, by induction hypothesis, we have ε(e[[c]]) ⇒ ε(e′[[c′]]) and ε(e[[d]]) ⇒ ε(e′[[d′]]). Hence, ε(e[[a]]) ≡ ε(e[[c]])ε(e[[d]]) ⇒ ε(e′[[c′]])ε(e′[[d′]]) ≡ ε(e′[[a′]]).

4. ε(a) ≡ (λy.c)d, c ⇒ c′, d ⇒ d′ and ε(a′) ≡ ε({d′/y}[[c′]]): By induction hypothesis, we have ε(e[[c]]) ⇒ ε(e′[[c′]]) and ε(e[[d]]) ⇒ ε(e′[[d′]]). So,

ε(e[[a]]) ≡ ε(e[[(λy.c)d]])
≡ ε(e[[λy.c]])ε(e[[d]])
≡ (λy.ε(e[[c]]))ε(e[[d]])
⇒ ε({ε(e′[[d′]])/y}[[ε(e′[[c′]])]])
≡ ε({e′[[d′]]/y}[[e′[[c′]]]])
≡ ε(e′[[{d′/y}[[c′]]]]) (by Lemma 5.3)
≡ ε(e′[[a′]]).

5. ε(a) ≡ {…, c_{i}/x_{i}, …}, c_{i} ⇒ c_{i}′ and ε(a′) ≡ {…, c_{i}′/x_{i}, …}: In this case, by induction hypothesis, we have ε(e[[c_{i}]]) ⇒ ε(e′[[c_{i}′]]). Hence,

ε(e[[a]]) ≡ {…, ε(e[[c_{i}]])/x_{i}, …}
⇒ {…, ε(e′[[c_{i}′]])/x_{i}, …} ≡ ε(e′[[a′]]).

6. ε(a) ≡ f[[x]], x ∈ TY(f), f is not canonical, f ⇒ f′ and ε(a′) ≡ ε(f′[[x]]): By induction hypothesis, we have ε(e[[f]]) ⇒ ε(e′[[f′]]) and ε(e[[f]][[x]]) ⇒ ε(e′[[f′]][[x]]). Hence, we have ε(e[[a]]) ≡ ε(e[[f[[x]]]]) ≡ ε(e[[f]][[x]]) ⇒ ε(e′[[f′]][[x]]) ≡ ε(e′[[f′[[x]]]]) ≡ ε(e′[[a′]]). ⊓ ⊔

Lemma 5.5. If a →_{λ} a′, then ε(a) ⇒ ε(a′).

Proof: By induction on the construction of a.

1. a ≡ (λx.b)c and a′ ≡ {c/x}[[b]]: We have

ε(a) ≡ ε(λx.b)ε(c) ≡ (λx.ε(b))ε(c)
⇒ ε({ε(c)/x}[[ε(b)]]) ≡ ε({c/x}[[b]]) ≡ ε(a′).

2. a ≡ λx.b, b →_{λ} b′ and a′ ≡ λx.b′: By induction hypothesis, we have ε(b) ⇒ ε(b′). Hence, ε(a) ≡ λx.ε(b) ⇒ λx.ε(b′) ≡ ε(a′).

3. a ≡ bc, b →_{λ} b′ and a′ ≡ b′c: By induction hypothesis, we have ε(b) ⇒ ε(b′). So, we have ε(a) ≡ ε(bc) ≡ ε(b)ε(c) ⇒ ε(b′)ε(c) ≡ ε(b′c) ≡ ε(a′).

4. a ≡ bc, c →_{λ} c′ and a′ ≡ bc′: Similar to the above case.

5. a ≡ {…, b/x, …}, b →_{λ} b′ and a′ ≡ {…, b′/x, …}:

ε(a) ≡ ε({…, b/x, …})
≡ {…, ε(b)/x, …}
⇒ {…, ε(b′)/x, …} (by ind. hyp.)
≡ ε({…, b′/x, …}) ≡ ε(a′).

6. a ≡ c[[b]], c →_{λ} c′ and a′ ≡ c′[[b]]: By induction hypothesis, we have ε(c) ⇒ ε(c′). Hence, by Lemma 5.4, we have ε(a) ⇒ ε(a′).

7. a ≡ c[[b]], b →_{λ} b′ and a′ ≡ c[[b′]]: Similar to the above case. ⊓ ⊔

We also prepare the following lemma.

Lemma 5.6. ⇒ on ε-normal λε-terms is confluent.

Proof: We can easily verify that if a ⇒ b, then b ⇒ a^{∗}, and the confluence of ⇒ immediately follows from this fact. ⊓ ⊔

Using these lemmas, we can prove the confluence of →_{λε} as follows.

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

Proof: Suppose that a →^{∗} b and a →^{∗} c. Then by Lemma 5.5, we have ε(a) ⇒^{∗} ε(b) and ε(a) ⇒^{∗} ε(c). Hence, by Lemma 5.6, there exists a d such that ε(b) ⇒^{∗} d and ε(c) ⇒^{∗} d. So, by Lemma 5.2, we have ε(b) →^{∗} d and ε(c) →^{∗} d. Since, b →^{∗} ε(b) and c →^{∗} ε(c), we have b →^{∗} d and c →^{∗} d. ⊓ ⊔

Next, we show the conservativity of λε over the simply typed λβ-calculus, where by the simply typed λβ-calculus, we mean a typed calculus whose typing rules are (assume), (⇒I) and (⇒E) and whose only reduction rule is (β). We can state the conservativity theorem as follows.

Theorem 5.8. (Conservativity) Let a and b be typed λβ-terms. Then a →^{∗}_{β} b if and only if a →^{∗}_{λε} b.

In order to prove this theorem, we define simple λε-terms as follows. A λε-term is simple, if its type A is of the following form:

A, B ::= K | A ⇒ B

and its untyped form a can be constructed by the following grammar:

a, b ::= x | λx.b | ba | e[[a]]
e, f ::= {a/x} | e[[f]]

We note that any λβ-term is a simple λε-term. If e[[a]] is a simple λε-term, then we say that e is a simple environment term.

Before we state Lemma 5.9 we define a syntactic translation Φ which translates each simple λε-term to a λβ-term as follows. We also define auxiliary translation functions Ψ_{1} and Ψ_{2} at the same time.

1. Φ(x) ≡ x.
2. Φ(λx.b) ≡ λx.Φ(b).
3. Φ(ba) ≡ Φ(b)Φ(a).
4. Φ(e[[a]]) ≡ Φ(a)[Ψ_{1}(e) := Ψ_{2}(e)].

5. Ψ_{1}({a/x}) ≡ x.
6. Ψ_{1}(e[[f]]) ≡ Ψ_{1}(f).
7. Ψ_{2}({a/x}) ≡ Φ(a).
8. Ψ_{2}(e[[f]]) ≡ Ψ_{2}(f)[Ψ_{1}(e) := Ψ_{2}(e)].

We can easily verify the following lemma.

Lemma 5.9. Let a be a simple λε-term. If a →_{λε} b, then b is also simple and Φ(a) →^{∗}_{β} Φ(b).

Proof: We first note that the redex of the conversion a →_{λε} b is either a simple term or a simple environment term. In order to cover the case of a simple environment term, we also prove the following statement:

If e is a simple environment term and e →_{λε} f, then f is also a simple environment term,

Ψ_{1}(e) ≡ Ψ_{1}(f) and Ψ_{2}(e) →^{∗}_{β} Ψ_{2}(f).

By inspecting the grammar of simple terms and simple environment terms, we can easily see that these two classes of terms are respectively closed under λε-conversions.

Now, we prove the main assertions by classifying cases according to the rule used in the conversion a →_{λε} b. Of these cases, we only check the case where a itself is the redex and the (eval) rule is applied to a. In this case, a is of the form e[[f[[x]]]] and x ∈ TY(f). Then we have b ≡ e[[f]][[x]] and we can compute as follows.

Φ(e[[f[[x]]]]) ≡ Φ(f[[x]])[Ψ_{1}(e) := Ψ_{2}(e)]
≡ Φ(x)[Ψ_{1}(f) := Ψ_{2}(f)][Ψ_{1}(e) := Ψ_{2}(e)]
≡ x[x := Ψ_{2}(f)][Ψ_{1}(e) := Ψ_{2}(e)]
≡ Ψ_{2}(f)[Ψ_{1}(e) := Ψ_{2}(e)].

Φ(e[[f]][[x]]) ≡ Φ(x)[Ψ_{1}(e[[f]]) := Ψ_{2}(e[[f]])]
≡ Φ(x)[Ψ_{1}(f) := Ψ_{2}(f)[Ψ_{1}(e) := Ψ_{2}(e)]]
≡ x[x := Ψ_{2}(f)[Ψ_{1}(e) := Ψ_{2}(e)]]
≡ Ψ_{2}(f)[Ψ_{1}(e) := Ψ_{2}(e)].

Hence, we have Φ(e[[f[[x]]]]) ≡ Φ(e[[f]][[x]]), so that Φ(a) →^{∗}_{β} Φ(b). ⊓ ⊔

Proof of Theorem 5.8: The ‘only if’ part is trivial and the ‘if’ part follows from Lemma 5.9 by noting that Φ is identity on λβ-terms. ⊓ ⊔

6. Strong Normalizability

In this section, we prove the strong normalizability of the λε-calculus using the reducibility argument (see, e.g., [10]). So, for each type A, we define a set [A] of reducible terms of type A as follows. (a : A means that Γ ⊢ a : A is derivable for some Γ.)

1. If a : A and A is atomic or the empty environment type {}, then a ∈ [A] iff a is SN.

2. If b : A ⇒ B, then b ∈ [A ⇒ B] iff ba ∈ [B] for all a ∈ [A].

3. If e : E and E is a non-empty environment type, then e ∈ [E] iff e[[x^{A}]] ∈ [A] for all x^{A} ∈ E.

We can prove the following fundamental proposition as in [10].

Proposition 6.1.

(CR1) If c ∈ [C], then c is SN.

(CR2) If c ∈ [C] and c → c′, then c′ ∈ [C].

(CR3) If c : C is neutral and c′ ∈ [C] for all c′ such that c → c′, then c ∈ [C].

Proof: By induction on C.

1. C is atomic or C ≡ {}: (CR1) is tautology in this case, and (CR2) and (CR3) are simple properties of SN terms.

2. C ≡ A ⇒ B:

(CR1) Suppose that b ∈ [A ⇒ B]. Then, for any a ∈ [A], we have ba ∈ [B]. But, by (CR3) for [A], we know that any x : A is in [A]. Hence we have bx ∈ [B]. Then, by (CR1) for [B], we know that bx is SN. Hence b must also be SN.

(CR2) Suppose that b ∈ [A ⇒ B] and b → b′. Then by SR (subject reduction), b′ : A ⇒ B. Let a ∈ [A]. Then we have ba ∈ [B]. Since ba → b′a, by (CR2) for [B], we have b′a ∈ [B]. Hence we have b′ ∈ [A ⇒ B].

(CR3) Supose that b : A ⇒ B is neutral and b′ ∈ [A ⇒ B] for all b′ such that b → b′. Let a ∈ [A]. Then a is SN by (CR1) for A. We show by induction on ν(a) that ba ∈ [B]. Now take any c such that ba → c. Since b is neutral c is of the form b′a where b → b′ or ba′ where a → a′. In the first case, we have b′ ∈ [A ⇒ B], so that b′a ∈ [B]. In the second case, since ν(a′) < ν(a), we have ba′ ∈ [B] by induction hypothesis. Therefore by (CR3) for [B], we have ba ∈ [B], so that, we have b ∈ [A ⇒ B].

3. C is a non-empty environment type E:

(CR1) Suppose that e ∈ [E]. Since E is a non-empty environment type we can take a variable x^{A} ∈ E. Then e[[x]] ∈ [A]. So, by (CR1) for [A], e[[x]] is SN. Hence e is also SN.

(CR2) Suppose that e ∈ [E] and e → e′. Let x^{A} ∈ E. Then e[[x]] ∈ [A]. Since e[[x]] → e′[[x]], we have e′[[x]] ∈ [A] by (CR2) for [A]. So, we have e′ ∈ [E].

(CR3) Suppose that e : E is neutral and e′ ∈ [E] for all e′ such that e → e′. Let x^{A} ∈ E. We will show that e[[x]] ∈ [A]. Consider any c such that e[[x]] → c. Since e is neutral and x is normal, c is of the form e′[[x]] where e → e′. Since e′ ∈ [E], we have e′[[x]] ∈ [A]. So by (CR3) for [A], we have e[[x]] ∈ [A]. Therefore, we have e ∈ [E]. ⊓ ⊔

6.1. Decoration Trees and Decorated Terms

Although we can define reducibility in a standard way, we cannot prove the SN of λε in a similar way as in the case of simply typed lambda calculus. The reason is that while substitution is carried out by a single step (β)-rule in the simply typed lambda calculus, in λε we have to compute the substitution internally by moving around environments that carry information about substitution. To cope with this situation, we introduce the notion of a decoration tree which is useful in keeping track of the movements of the environments during the reduction steps.

We define decoration tree (δ) and its type (TY(δ)) inductively as follows.

1. If δ_{1}, …, δ_{n} (n ≥ 0) are decoration trees, then δ ≡ (δ_{1}, …, δ_{n}) is a decoration tree and TY(δ):= TY(δ_{1}) ∪ ⋯ ∪ TY(δ_{n}).

2. If δ is a decoration tree and e is a bindable variable free environment term, then (e, δ) is a decoration tree and TY((e, δ)) := TY(e) ∪ TY(δ).

Note that each leaf of a decoration tree is () or a bindable variable free environment term. A decoration tree is trivial if its leaves are always (). We will use δ, γ, ρ etc. to denote decoration trees.

Let a and ã be terms of type A and δ be a decoration tree. We define a ternary relation ‘ã is a decoration of a by δ’ inductively as follows. In the following definition, δ provides the information about the positions in a which are to be decorated as well as which environments are used to decorate these positions. We will write δ : a ↦ ã for this relation.

{δ : a ↦ ã \atop (e, δ) : a ↦ e[[ã]]}  () : x ↦ x

{δ : b ↦ b̃ \atop (δ) : λx.b ↦ λx.b̃} (∗)  \begin{matrix}δ : b ↦ b̃ & δ′ : a ↦ ã \\ (δ, δ′) : ba ↦ b̃ã \end{matrix}

\begin{matrix}δ_{1} : a_{1} ↦ ã_{1} & ⋯ & δ_{n} : a_{n} ↦ ã_{n} \\ (δ_{1}, …, δ_{n}) : \{a_{1}/x_{1}, …, a_{n}/x_{n}\} ↦ \{ã_{1}/x_{1}, …, ã_{n}/x_{n}\} \end{matrix}

\begin{matrix}δ : e ↦ ẽ & δ′ : a ↦ ã \\ (δ, δ′) : e[[a]] ↦ ẽ[[ã]] \end{matrix} (∗∗)

The rule marked by (∗) may be applied only under the condition that x ∉ TY(δ) and the rule marked by (∗∗) may be applied only when TY(e) ∩ TY(δ′) = ∅.

If δ : c ↦ a holds, we will call the triple (a, c, δ) a decorated term over c, and will simply write a for the decorated term, if c and δ can be inferred from the context.

It is easy to see that if δ : c ↦ a and δ : c ↦ b, then a ≡ b. So, we will write δ(c) for this a. It is also easy to see that for each term a, there is a unique trivial δ such that δ : a ↦ a. We will write ι_{a} for this δ.

If \overline{e} ≡ e_{1}, …, e_{n}, we will write (\overline{e}, δ) for (e_{1}, (e_{2}, ⋯ (e_{n}, δ) ⋯)) and TY(\overline{e}) for ⋃_{i=1}^{n} TY(e_{i}). Suppose that δ : c ↦ a. Then δ can be written uniquely in the form (\overline{e}, γ) where γ is of the form (δ_{1}, …, δ_{n}) (n ≥ 0). In this case, we have a ≡ \overline{e}[[γ(c)]].

Let δ : c ↦ c̃ and π ∈ Π(c̃). We say that π is internal, marginal or external in δ if it can be seen so by the following inductive clauses. At the same time, we also define δ/π which is either a decoration tree or a subterm of some environment term in δ.

1. Λ is internal in (δ_{1}, …, δ_{n}) (n ≥ 0) and (δ_{1}, …, δ_{n})/Λ := (δ_{1}, …, δ_{n}).

2. Λ is marginal in (e, δ) and (e, δ)/Λ := (e, δ).

3. If π ∈ Π(e), then 1π is external in (e, δ) and (e, δ)/1π := e/π.

4. If π is internal, marginal or external in δ, then 2π is internal, marginal or external, respectively, in (e, δ) and (e, δ)/2π := δ/π.

5. If π is internal, marginal or external in δ_{i}, then iπ is internal, marginal or external, respectively, in (δ_{1}, …, δ_{n}) (n ≥ 1) and (δ_{1}, …, δ_{n})/iπ := δ_{i}/π.

Suppose that δ : c ↦ c̃ and π ∈ Π(c̃). The occurrence of c̃/π in c̃ is said to be an internal, marginal or external occurrence with respect to δ if π is internal, marginal or external in δ, respectively. It is easily verified that for any π ∈ Π(c̃), π is either internal, marginal or external in δ and only one of these is the case. This classification can be characterized as follows. π is external if δ/π is a λε-term, π is marginal if δ/π1 is external and δ/π is a decoration tree, and π is internal otherwise. We also note that, if π is marginal in δ, then c̃/π is of the form e[[a]] where e is an environment in δ.

For each decoration tree δ, we define its height h(δ) inductively as follows.

1. h(()) := 1.

2. h((δ_{1}, …, δ_{n})) := max(h(δ_{1}), …, h(δ_{n})) + 1.

3. h((e, δ)) := h(δ) + 1.

A decoration tree δ is strongly normalizing (SN) if each environment term e in δ is SN. Then, for each strongly normalizing δ, we define its weight w(δ) inductively as follows. In the following definition, # denotes the natural sum^{4} of two ordinals.

1. w(()) := 0.

2. w((δ_{1}, …, δ_{n})) := w(δ_{1}) # ⋯ # w(δ_{n}).

3. w((e, δ)) := ω^{h(δ)}(ν(e) + 1) + w(δ).

6.2. Orthogonal Decorations

In this subsection, we introduce orthogonal decorations and show their fundamental properties. We will say that δ : c ↦ c̃ is orthogonal if for each marginal subterm e[[a]] of c̃, TY(e) ∩ FV(a) = ∅ holds. Then we have the following lemmas and proposition which are used in the proof of Proposition 6.11.

Lemma 6.2. If γ : c ↦ c̃ is orthogonal, γ is SN and c̃ → d is obtained by converting an external redex of c̃, then we have an orthogonal decoration γ′ : c ↦ d for some SN γ′ such that w(γ′) < w(γ).

4See, e.g., Takeuti [21] for the definition of natural sum.

Proof: Let c̃/σ be the redex. Then σ is external in γ. We prove the lemma by induction on the inductive definition of ‘σ is external in γ’. We have the following cases. We leave the verification of the orthogonality and strong normalizability of γ′ to the reader.

1. c̃ ≡ e[[c]], γ ≡ (e, δ), σ ≡ 1π and π ∈ Π(e): In this case, we have d ≡ f[[c]] where e → f. Then, putting γ′ := (f, δ), we have γ′ : c ↦ f[[c]] and w(γ′) = ω^{h(δ)}(ν(f) + 1) + w(δ) < ω^{h(δ)}(ν(e) + 1) + w(δ) = w(γ).

2. γ ≡ (δ_{1}, …, δ_{n}), σ ≡ iπ, π is external in δ_{i}, ã ≡ c̃/σ, δ_{i} : a ↦ ã and ã → b: By induction hypothesis, we can find a δ′ such that δ′ : a ↦ b and w(δ′) < w(δ_{i}). So, by putting γ′:= (δ_{1}, …, δ′, …, δ_{n}), we have γ′ : c ↦ d (to see this, we must check that the conditions (∗) and (∗∗) are satisfied) and w(γ′) = w(δ_{1}) # ⋯ # w(δ′) # ⋯ # w(δ_{n}) < w(δ_{1}) # ⋯ # w(δ_{i}) # ⋯ # w(δ_{n}). ⊓ ⊔

Lemma 6.3. If γ : c ↦ c̃ is orthogonal, γ is SN and c̃ → d is obtained by converting a marginal redex of c̃, then we have an orthogonal decoration γ′ : c ↦ d for some SN γ′ such that w(γ′) < w(γ).

Proof: Let c̃/σ be the redex. Then σ is marginal in γ. We prove the lemma by induction on the inductive definition of ‘σ is marginal in γ’. We have the following cases. We leave the verification of the orthogonality and and strong normalizability of γ′ to the reader.

1. σ ≡ Λ, γ ≡ (e, δ), c̃ ≡ e[[δ(c)]] and δ : c ↦ δ(c): We have the following subcases according to the rule used to covert e[[δ(c)]].

1.1. (gc): In this case, we have d ≡ δ(c). So, putting γ′:=δ, we have γ′ : c ↦ d and w(γ′) = w(δ) < w((e, δ)) = w(γ) 1.2. (var): This case is void, since we are considering an orthogonal decoration. 1.3. (abs): In this case, we have c ≡ λx.b, δ ≡ (δ_{1}) and d ≡ λx.e[[δ_{1}(b)]]. So, putting γ′ ≡ ((e, δ_{1})), we have γ′ : c ↦ d (since (∗) is satisfied by the condition on the (abs) rule) and w(γ′) = w((e, δ_{1})) = ω^{h(δ_{1})}(ν(e) + 1) + w(δ_{1}) < ω^{h(δ)}(ν(e) + 1) + w(δ) = w(γ) (since h(δ_{1}) < h(δ)). 1.4. (app): In this case, we have c ≡ ba, δ ≡ (δ_{1}, δ_{2}) and d ≡ e[[δ_{1}(b)]]e[[δ_{2}(a)]]. So, by putting γ′ ≡ ((e, δ_{1}), (e, δ_{2})), we have γ′ : c ↦ d and w(γ′) = w((e, δ_{1}))#w((e, δ_{2})) = (ω^{h(δ_{1})}(ν(e)+ 1) + w(δ_{1})) # (ω^{h(δ_{2})}(ν(e) + 1) + w(δ_{2})) < ω^{h(δ)}(ν(e) + 1) + w(δ) = w(γ), since h(δ_{1}) < h(δ) and h(δ_{2}) < h(δ). 1.5. (env): Similar to the above case. 1.6. (eval): We have two cases here. 1.6.1.c ≡ f[[x]], x ∈ TY(f), δ ≡ (δ_{1}, ι_{x}) and d ≡ e[[δ_{1}(f)]][[x]]: In this case, by putting γ′ := ((e, δ_{1}), ι_{x}), we have γ′ : c ↦ d and w(γ′) = w((e, δ_{1}))#w(ι_{x}) = (ω^{h(δ_{1})}(ν(e)+1)+w(δ_{1}))# w(ι_{x}) = ω^{h(δ_{1})}(ν(e) + 1) + w(δ_{1}) < ω^{h(δ)}(ν(e) + 1) + w(δ) = w(γ) (since h(δ_{1}) < h(δ)). 1.6.2.c ≡ x, x ∈ TY(f), δ ≡ (f, ι_{x}) and d ≡ e[[f]][[x]]: In this case, the fact that x ∈ TY(f) is contradictory to the assumption that γ is orthogonal.

2. σ ≢ Λ: Easy by induction. ⊓ ⊔

Lemma 6.4. If γ : c ↦ c̃ is orthogonal, γ is SN and c̃ → d is obtained by converting an internal redex of c̃, then we have an orthogonal decoration γ′ : c′ ↦ d for some γ′ and c′ such that γ′ is SN and c → c′.

Proof: Let c̃/σ be the redex of the conversion c̃ → d. Then σ is internal in γ. We prove the lemma by induction on the inductive definition of ‘σ is internal in γ’. We have the following cases. We leave the verification of the orthogonality and strong normalizability of γ′ to the reader.

1. σ ≡ Λ: In this case we have the following subcases according to the rule used to convert c̃.

1.1. (λ): In this case, γ ≡ (γ_{1}, γ_{2}), c̃ ≡ (λx.b̃)ã, c ≡ (λx.b)a and d ≡ {ã/x}[[b̃]]. So, putting c′ ≡ {a/x}[[b]] and γ′ ≡ ((γ_{2}), γ_{1}), we have c → c′ and γ′ : c′ ↦ d.

1.2. (gc): In this case, γ ≡ (γ_{1}, γ_{2}), c̃ ≡ ẽ[[ã]], c ≡ e[[a]], TY(ẽ) ∩ FV(ã) = ∅ and d ≡ ã. So, putting c′ ≡ a, we have c → c′ since we have TY(e) ∩ FV(a) = ∅. We also have γ′ : c′ ↦ d, by putting γ′ := γ_{2}.

1.3. (var): In this case, γ ≡ ((γ_{1}, …, γ_{n}), ()), c̃ ≡ {ã_{1}/x_{1}, …, ã_{n}/x_{n}}[[x̃_{i}]], c ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{i}]] and d ≡ ã_{i}. Here, we know that x̃_{i} ≡ x_{i}, since (var) rule is applicable to c̃. So, putting c′ ≡ a_{i} and γ′ := γ_{i}, we have c → c′ and γ′ : c′ ↦ d.

1.4. (abs): In this case, γ ≡ (γ_{1}, (γ_{2})), c̃ ≡ ẽ[[λx.b̃]], c ≡ e[[λx.b]] and d ≡ λx.ẽ[[b̃]]. So, putting c′ := λx.e[[b]] and γ′ := ((γ_{1}, γ_{2})), we have c → c′ and γ′ : c′ ↦ d.

1.5. (app): In this case, γ ≡ (γ_{1}, (γ_{2}, γ_{3})), c̃ ≡ ẽ[[b̃ã]], c ≡ e[[ba]] and d ≡ ẽ[[b̃]]ẽ[[ã]]. So, putting c′ ≡ e[[b]]e[[a]] and γ′ := ((γ_{1}, γ_{2}), (γ_{1}, γ_{3})), we have c → c′ and γ′ : c′ ↦ d.

1.6. (env): Similar to the above case.

1.7. (eval): Here, we have two possibilities.

1.7.1.γ ≡ (γ_{1}, (γ_{2}, ι_{x})), c̃ ≡ γ_{1}(e)[[γ_{2}(f)[[x]]]], c ≡ e[[f[[x]]]] and d ≡ γ_{1}(e)[[γ_{2}(f)]][[x]]: In this case, putting c′ ≡ e[[f]][[x]] and γ′ ≡ ((γ_{1}, γ_{2}), ι_{x}), we have c → c′ and γ′ : c′ ↦ d. 1.7.2.γ ≡ (γ_{1}, (f, ι_{x})), c̃ ≡ γ_{1}(e)[[f[[x]]]], x ∈ TY(f), c ≡ e[[x]] and d ≡ γ_{1}(e)[[f]][[x]]: In this case, x ∈ TY(f) is contradictory to our assumption that γ : c ↦ c̃ is orthogonal.

2. σ ≢ Λ: This case can be proved easily by using IH. ⊓ ⊔

Lemma 6.5. If γ : c ↦ c̃ is orthogonal and c and γ are both SN, then c̃ is also SN.

Proof: By a double induction on ν(c) and w(γ). Take any c̃ → d and let c̃/π be the redex of this conversion. We have the following three cases according to the type of the redex.

1. External: By Lemma 6.2, we have an orthogonal decoration γ′ : c ↦ d such that w(γ′) < w(γ). So, by IH, we see that d is SN.

2. Marginal: By Lemma 6.3, we have an orthogonal decoration γ′ : c ↦ d such that w(γ′) < w(γ). So, by IH, we see that d is SN.

3. Internal: By Lemma 6.4, we can find γ′ and c′ such that γ′ : c′ ↦ d, γ′ is SN and c → c′. Since ν(c′) < ν(c), by IH, we see that d is SN.

Since d is SN in any case, we see that c̃ is SN. ⊓ ⊔

Proposition 6.6. If γ : c ↦ c̃ is orthogonal, γ is SN and c ∈ [C], then c̃ ∈ [C].

Proof: By induction on C.

1. C is atomic or C ≡ {}: In this case, the proposition holds by Lemma 6.5.

2. C ≡ A ⇒ B: Take any a ∈ [A]. Then, we have an orthogonal decoration (γ, ι_{a}) : ca ↦ c̃a where (γ, ι_{a}) is SN. We have also ca ∈ [B], since c ∈ [A ⇒ B]. So, by induction hypothesis, we have c̃a ∈ [B]. Therefore, we have c̃ ∈ [C].

3. C ≡ {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} (n ≥ 1): Take any x^{A} ∈ C. Then, we have an orthogonal decoration (γ, ι_{x}) : c[[x]] ↦ c̃[[x]] where (γ, ι_{x}) is SN. We have also c[[x]] ∈ [A], since c ∈ [{x_{1}^{A_{1}}, …, x_{n}^{A_{n}}}]. So, by induction hypothesis, we see that c̃[[x]] ∈ [A]. Therefore, we have c̃ ∈ [C]. ⊓ ⊔

Discussions on the (eval) rule. Here, we would like to remark that the condition x ∈ TY(f) is essential in proving Lemma 6.5. Recall that the (eval) rule is:

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

Now, let us consider the following rule:

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

This rule is correct in the theory of λε-equality (Proposition 6.7) and more liberal than our (eval) rule. So, we might be tempted to make our calculus more liberal by adopting the (eval′) rule in place of the (eval) rule. However, if we do so, the calculus will not be strongly normalizing. In fact, we have the following counter-example to SN due to Bloo et. al. [6]. (The counter-example in the case of calculus of explicit substitutions was first found by Melliès [17].) Let us put f := {(λx.z)z/x} and e:= {f[[z]]/x} where z is an arbitrary unbindable variable and z and x are of the same type, say, A. Then we can construct an infinite reduction sequence starting from e[[f]]. We also note that both e and f are SN and (e, ι_{f}) : f ↦ e[[f]] is an orthogonal decoration since f is bindable variable free. Hence Lemma 6.5 no longer holds for the extended calculus. Thus we see that the condition x ∈ TY(f) is indispensable in our proof of Lemma 6.5. We can construct an infinite reduction sequence starting from e[[f]] as follows. Let

e_{0} := {(λx.z)z/x}, e_{n+1} := {e_{n}[[z]]/x_{n}} (n = 0, 1, 2, …)

where x_{0} ≡ x and x_{0}, x_{1}, x_{2}, … are distinct bindable variables of the same type. Then, we have the following reduction sequences.

e_{n+1}[[e_{0}]] →^{∗} {e_{n+1}[[λx.z]]e_{n+1}[[z]]/x}
→ {(λx_{n+1}.e_{n+1}[[z]])e_{n+1}[[z]]/x}
→ {{e_{n+1}[[z]]/x_{n+1}}[[e_{n+1}[[z]]]]/x}
≡ {e_{n+2}[[e_{n+1}[[z]]]]/x}
e_{n+1}[[e_{m+1}[[z]]]] → e_{n+1}[[{e_{m}[[z]]/x_{m}}]][[z]]  (by (eval′))
→ {e_{n+1}[[e_{m}[[z]]]]/x_{m}}[[z]]

Masahiko Sato et al. / Explicit Environments 103

By combining these reductions, we have

e_{n+1}[[e_{0}]] →^{∗} ⋯ e_{n+2}[[e_{n+1}[[z]]]] ⋯
→^{∗} ⋯ e_{n+2}[[e_{n}[[z]]]] ⋯ →^{∗} ⋯ e_{n+2}[[e_{n−1}[[z]]]] ⋯
→^{∗} ⋯ e_{n+2}[[e_{0}[[z]]]] ⋯
→ ⋯ e_{n+2}[[e_{0}]][[z]] ⋯  (by (eval′))

Therefore, we have an infinite reduction sequence starting from e[[f]] ≡ e_{1}[[e_{0}]].

Next, consider the rule:

(eval′′) e[[f[[a]]]] ↦_{ε} e[[f]][[a]], if TY(e) ∩ (FV(a) − TY(f)) = ∅. This rule is even more liberal than the (eval′) rule, and if we adopt this rule instead of our (eval) rule, the theory of λε-equality would be unchanged (Proposition 6.7) and we would still have the confluence and the conservativity properties, but we would no longer have SN since SN fails for a less liberal system as we saw above. These are the reasons we have chosen the (eval) rule as it is now. Proposition 6.7. Let =_{ε} be the equivalence relation generated by →_{ε}, namely, the reflexive, symmetric, and transitive closure of →_{ε}, and let a, e, and f be λε-terms. If TY(e) ∩ (FV(a) − TY(f)) = ∅, then we have

e[[f[[a]]]] =_{ε} e[[f]][[a]].

Proof: Without loss of generality, we can assume that a is ε-normal. We prove this proposition by induction on the construction of a.

1. a is a variable x: If x ∈ TY(f), LHS →_{ε} RHS by (eval). Otherwise, we have x ∉ TY(e) by the assumption. Therefore, LHS →^{∗}_{ε} x and RHS →_{ε} x by (gc)s.

2. a ≡ λx.b:

LHS →^{∗}_{ε} λx.e[[f[[b]]]]  (by (abs)s)
RHS →_{ε} λx.e[[f]][[b]]  (by (abs))

By induction hypothesis, we have LHS =_{ε} RHS.

3. a ≡ g[[x]], x ∈ TY(g) and g is not canonical: Since x ∈ TY(g), we can compute as follows.

LHS →_{ε} e[[f[[g]][[x]]]]  (by (eval))
→_{ε} e[[f[[g]]]][[x]]  (by (eval))
RHS →_{ε} e[[f]][[g]][[x]]  (by (eval))

By induction hypothesis, we have LHS =_{ε} RHS.

4. Other cases: Easy by induction.

6.3. Partial Orders on Decorated Terms

In this subsection, for each term c, we define a partial order ⪯_{c} on decorated terms over c. These partial orders play an essential role in our proof of SN.

Let δ : c ↦ c̃ be a decoration, and suppose that π ∈ Π(c) is such that c/π is a variable. Then we define env(c, π, δ) inductively below as a sequence of pairs of the form ⟨e, σ⟩ where e is an environment term in δ and σ ∈ Π(c). In the following definition, if \overline{e} ≡ ⟨e_{1}, σ_{1}⟩, …, ⟨e_{n}, σ_{n}⟩, then k\overline{e} denotes the sequence ⟨e_{1}, kσ_{1}⟩, …, ⟨e_{n}, kσ_{n}⟩.

1. env(x, Λ, ()) := Λ (empty sequence).

2. env(c, kπ, (δ_{1}, …, δ_{n})) := k env(c/k, π, δ_{k}) (1 ≤ k ≤ n).

3. env(c, π, (e, δ)) := env(c, π, δ), ⟨e, Λ⟩.

If δ : c ↦ c̃ and ⟨e, σ⟩ is in the sequence env(c, π, δ), then we will say that the variable c/π at π in c is decorated by e at σ in c. If ⟨e, σ⟩ appears before ⟨e′, σ′⟩ in env(c, π, δ), then we have σ′ ⊑ σ, that is, σ′ is an initial substring of σ. Hence, we see that env(c, π, δ) gives a sorted sequence of environments decorating c/π where the environment closest to c/π is the first element of the sequence.

Here is a simple example. For the decoration

(f, ((e, ι_{y}), ι_{x})) : yx ↦ f[[e[[y]][[x]]]],

we have

env(yx, 1, (f, ((e, ι_{y}), ι_{x})))
≡ env(yx, 1, ((e, ι_{y}), ι_{x})), ⟨f, Λ⟩
≡ 1 env(y, Λ, (e, ι_{y})), ⟨f, Λ⟩
≡ 1(env(y, Λ, ι_{y}), ⟨e, Λ⟩), ⟨f, Λ⟩
≡ 1⟨e, Λ⟩, ⟨f, Λ⟩
≡ ⟨e, 1⟩, ⟨f, Λ⟩

and

env(yx, 2, (f, ((e, ι_{y}), ι_{x})))
≡ env(yx, 2, ((e, ι_{y}), ι_{x})), ⟨f, Λ⟩
≡ 2 env(x, Λ, ι_{x}), ⟨f, Λ⟩
≡ 2Λ, ⟨f, Λ⟩
≡ ⟨f, Λ⟩.

Let \overline{e} ≡ ⟨e_{1}, σ_{1}⟩, …, ⟨e_{m}, σ_{m}⟩ and \overline{e′} ≡ ⟨e′_{1}, σ′_{1}⟩, …, ⟨e′_{n}, σ′_{n}⟩. We write \overline{e} ≤ \overline{e′} if (1) m ≤ n and (2) for each k such that 1 ≤ k ≤ m, e_{k} ≡ e′_{k} and σ_{k} ⊑ σ′_{k} hold. Let a and b be two decorated terms such that γ : c ↦ a and δ : c ↦ b. We write a ⪯_{c} b if, for each occurrence of a variable x ≡ c/π in c, we have env(c, π, γ) ≤ env(c, π, δ). It is easy to see that ⪯_{c} determines a partial order on decorated terms over c and c ≡ (c, c, ι_{c}) ⪯_{c} a holds for any decorated term a over c. We will often simply write a ⪯ b for a ⪯_{c} b. This partial order plays an essential role in our proof of SN.

Masahiko Sato et al. / Explicit Environments 105

Here are some examples. For the decorations

(e, ((δ_{1}), δ_{2})) : (λx.b)a ↦ e[[(λx.b̃)ã]],
((e, (δ_{1})), (e, δ_{2})) : (λx.b)a ↦ e[[λx.b̃]]e[[ã]],
(((e, δ_{1})), (e, δ_{2})) : (λx.b)a ↦ (λx.e[[b̃]])e[[ã]]

where b̃ ≡ δ_{1}(b), ã ≡ δ_{2}(a), and x ∉ TY(e), we have

e[[(λx.b̃)ã]] ⪯ e[[λx.b̃]]e[[ã]] ⪯ (λx.e[[b̃]])e[[ã]].

For the decorations

(e, (δ_{1}, δ_{2})) : f[[a]] ↦ e[[f̃[[ã]]]],
(e, ((e, δ_{1}), δ_{2})) : f[[a]] ↦ e[[e[[f̃]][[ã]]]]

where f̃ ≡ δ_{1}(f) and ã ≡ δ_{2}(a), we have

e[[f̃[[ã]]]] ⪯ e[[e[[f̃]][[ã]]]].

Lemma 6.8. If c_{1} ⪯_{c} c_{2} and c_{2} is SN, then c_{1} is also SN. Proof: See appendix. ⊓ ⊔ We put the proof of the Lemma in appendix, since it is technically complicated and lengthy. However, this Lemma plays an essential role in the proof of the Reducibility Theorem, because the proof of the Reducibility Theorem depends on Proposition 6.9 below, which in turn depends on Lemma 6.8.

We can extend the above Lemma as follows. Proposition 6.9. If c_{1} ⪯_{c} c_{2} and c_{2} ∈ [C], then c_{1} ∈ [C]. Proof: By induction on C. We assume that γ_{1} : c ↦ c_{1} and γ_{2} : c ↦ c_{2}.

1. C is atomic or C ≡ {}: In this case, the proposition holds by Lemma 6.8.

2. C ≡ A ⇒ B: Take any a ∈ [A]. Consider the decorations:

(γ_{i}, ι_{a}) : ca ↦ c_{i}a (i = 1, 2).

Then we have c_{1}a⪯_{ca}c_{2}a. We have also c_{2}a ∈ [B], since c_{2} ∈ [A ⇒ B]. So, by induction hypothesis, we have c_{1}a ∈ [B]. Therefore, we have c_{1} ∈ [C].

3. C ≡ {x_{1}^{A_{1}}, …, x_{n}^{A_{n}}} (n ≥ 1): Take any x^{A} ∈ C. Then, we have

(γ_{i}, ι_{x}) : c[[x]] ↦ c_{i}[[x]] (i = 1, 2).

By these decorations we see that c_{1}[[x]] ⪯_{c[[x]]} c_{2}[[x]]. We have also c_{2}[[x]] ∈ [A], since c_{2} ∈ [{x_{1}^{A_{1}}, …, x_{n}^{A_{n}}}]. So, by induction hypothesis, we see that c_{1}[[x]] ∈ [A]. Therefore, we have c_{1} ∈ [C]. ⊓ ⊔

6.4. Reducibility Theorem

We say that a decoration tree δ is reducible, if each environment term in δ is reducible. In this subsection, we prove the following theorem as the final result of our paper.

Theorem 6.10. (Reducibility) If c : C, (\overline{e}, ι_{c}) : c ↦ \overline{e}[[c]] and (\overline{e}, ι_{c}) is reducible, then \overline{e}[[c]] ∈ [C].

We note that by using an empty sequence as \overline{e} in the theorem, we can conclude that any λε-term is reducible and hence SN. We have to show some more propositions before we can prove the reducibility theorem.

Proposition 6.11. If δ : x^{A} ↦ \overline{e}[[x]] and δ is reducible, then \overline{e}[[x]] ∈ [A].

Proof: By induction on w(δ). Since \overline{e}[[x]] is neutral, we argue by (CR3). Take any d such that \overline{e}[[x]] → d. The redex of this conversion is external, marginal or internal.

1. External: In this case, d is of the form \overline{f}[[x]]. So, we have (\overline{f}, ι_{x}) : x ↦ \overline{f}[[x]] and w((\overline{f}, ι_{x})) < w((\overline{e}, ι_{x})). So, we see that d ∈ [A] by IH.

2. Marginal: We classify according to the rule used in the conversion.

2.1. (gc): In this case, \overline{e} ≡ \overline{f}, e, \overline{g} and we have d ≡ \overline{f}[[\overline{g}[[x]]]]. So, we see that d ∈ [A] similarly as in the external case. 2.2. (var): In this case, \overline{e} ≡ \overline{f}, \{a_{1}/x_{1}, …, a_{n}/x_{n}\} where x ≡ x_{k} for some k (1 ≤ k ≤ n), and d ≡ \overline{f}[[a_{k}]]. Then since each environment term in δ is bindable variable free and reducible, we see that (\overline{f}, ι_{a_{k}}) : a_{k} ↦ \overline{f}[[a_{k}]] is orthogonal, (\overline{f}, ι_{a_{k}}) is SN and that a_{k} ∈ [A]. So, by Proposition 6.6, we see that d ∈ [A]. 2.3. (eval): In this case, \overline{e} ≡ \overline{f}, e, f and d ≡ \overline{f}[[e[[f]][[x]]]] where x ∈ TY(f). Since f is bindable variable free, we have TY(e)∩FV(f) = ∅. Since δ is reducible, we know that e, f are reducible. Hence e[[f]] is reducible by Proposition 6.6. So, by putting γ := (\overline{f}, (e[[f]], ι_{x})), we have the decoration γ : x ↦ d. Here we have w(γ) < w(δ) by a similar computation as in Case 1.6.1. of Lemma 6.3. Hence, we have d ∈ [A] by IH.

3. Internal: This case is void, since the only internal subterm of \overline{e}[[x]] is x.

Since d ∈ [A] in any case, we see that \overline{e}[[x]] ∈ [A] by (CR3). ⊓ ⊔

Proposition 6.12. If a ∈ [A] and {a/x}[[b]] ∈ [B], then (λx.b)a ∈ [B].

Proof: By induction on ν(a) + ν(b). Since (λx.b)a is neutral, we argue by (CR3), by considering any d such that (λx.b)a → d. Here we have the following cases.

1. d ≡ (λx.b′)a and b → b′: In this case, since ν(a) + ν(b′) < ν(a) + ν(b), by IH, we have d ∈ [B].

2. d ≡ (λx.b)a′ and a → a′: In this case, since ν(a′) + ν(b) < ν(a) + ν(b), by IH, we have d ∈ [B].

3. d ≡ {a/x}[[b]]: In this case we have d ∈ [B] by assumption. ⊓ ⊔ Proposition 6.13. If a_{1} ∈ [A_{1}], …, a_{n} ∈ [A_{n}], then {a_{1}/x_{1}, …, a_{n}/x_{n}} ∈ [{x_{1}^{A_{1}}, …, x_{n}^{A_{n}}}].

Proof: Show, by induction on ν(a_{1}) + ⋯ + ν(a_{n}), that {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{i}]] ∈ [A_{i}]. The proof is similar to the previous proposition. ⊓ ⊔

Let c be a term, π_{1}, …, π_{n} ∈ Π(c) be such that x_{i} ≡ c/π_{i} (1 ≤ i ≤ n) are bindable variables free at π_{i} in c and y_{1}, …, y_{n} be unbindable variables such that, for each i (1 ≤ i ≤ n), x_{i} and y_{i} are of the same type. Then we say that c′ ≡ c_{π_{1},...,π_{n}}[y_{1}, …, y_{n}] is a variant of c. If, moreover, c′ is bindable variable free, then we say that c′ is a bindable variable free variant of c. Note that we can always find a bindable variable free variant of c for any c.

Lemma 6.14. If c′ is a variant of c, then c is SN iff c′ is SN.

Proof: Easy. ⊓ ⊔

We can extend this lemma as follows. We omit its proof since the proof is similar to that of Proposition 6.6.

Proposition 6.15. If c′ is a variant of c : C, then c ∈ [C] iff c′ ∈ [C].

Now we can prove the reducibility theorem as follows.

Proof of Theorem 6.10: By induction on the size of the derivation of c : C. We write c̃ for \overline{e}[[c]]. We classify cases according to the last rule applied to derive c : C.

1. (assume): In this case, we have the theorem by Proposition 6.11.

2. (⇒I): In this case, C ≡ A ⇒ B, c ≡ λx.b and c̃ ≡ \overline{e}[[λx.b]]. Here, by α-conversion, we may assume that x ∉ TY(\overline{e}). We put b̃:= \overline{e}[[b]]. We first show that λx.b̃ ∈ [C]. To show this, we take an arbitrary a ∈ [A] and we let a′ be a bindable variable free variant of a. Then, by Proposition 6.15, we have that a′ ∈ [A]. Hence, by Proposition 6.13, we have

γ : b ↦ {a′/x}[[b̃]]

where γ:=(\{a′/x\}, (\overline{e}, ι_{b})) is reducible and bindable variable free. (Note that (\{a/x\}, (\overline{e}, ι_{b})) may not be bindable variable free since FV(a) may contain bindable variables. So, we consider a′ in place of a.) So, by IH, we have {a′/x}[[b̃]] ∈ [B]. Hence by Proposition 6.12, we have (λx.b̃)a′ ∈ [B]. So, by Proposition 6.15, we have (λx.b̃)a ∈ [B]. Therefore, we have λx.b̃ ∈ [C]. Since c̃ ⪯_{λx.b} λx.b̃, we have c̃ ∈ [C] by Proposition 6.9.

3. (⇒E): In this case c ≡ ba where b : A ⇒ C and a : A. We put b̃:= \overline{e}[[b]] and ã:= \overline{e}[[a]]. By induction hypothesis, we have b̃ ∈ [A ⇒ C] and ã ∈ [A]. So, we have b̃ã ∈ [C]. Since c̃ ≡ \overline{e}[[ba]] ⪯_{ba} b̃ã, we have c̃ ∈ [C] by Proposition 6.9.

4. (envI): In this case c ≡ \{a_{1}/x_{1}, …, a_{n}/x_{n}\}. By IH and by Proposition 6.13, we have \{\overline{e}[[a_{1}]]/x_{1}, …,

\overline{e}[[a_{n}]]/x_{n}\} ∈ [C]. Since

c̃ ⪯_{c} \{\overline{e}[[a_{1}]]/x_{1}, …, \overline{e}[[a_{n}]]/x_{n}\},

we have c̃ ∈ [C] by Proposition 6.9.

5. (envE): In this case c ≡ e[[a]] where e : E and a : C. We show that \overline{e}[[e[[a]]]] ∈ [C]. We let e′ be a variant of e such that all free occurrences of bindable variables in e that are not bound by \overline{e} are renamed to unbindable variables. Then, we see that \overline{e}[[e′]] is bindable variable free. Now, consider the decoration:

(\overline{e}, ι_{e′}) : e′ ↦ \overline{e}[[e′]].

Since the size of the derivation of e′ : E is equal to the size of the derivation of e : E, we may appeal to IH for e′. Then, we have \overline{e}[[e′]] ∈ [E]. So, we have the decoration:

(\overline{e}, (\overline{e}[[e′]], ι_{a})) : a ↦ \overline{e}[[\overline{e}[[e′]][[a]]]],

where (\overline{e}, (\overline{e}[[e′]], ι_{a})) is reducible. Hence, by IH for a, we have \overline{e}[[\overline{e}[[e′]][[a]]]] ∈ [C]. Next, we consider the following two decorations.

(\overline{e}, ((\overline{e}, ι_{e′}), ι_{a})) : e′[[a]] ↦ \overline{e}[[\overline{e}[[e′]][[a]]]],
(\overline{e}, (ι_{e′}, ι_{a})) : e′[[a]] ↦ \overline{e}[[e′[[a]]]].

From these decorations, we see that \overline{e}[[e′[[a]]]] ⪯_{e′}_{[[a]]} \overline{e}[[\overline{e}[[e′]][[a]]]]. Hence, by Proposition 6.9, we have \overline{e}[[e′[[a]]]] ∈ [C]. Therefore, by Proposition 6.15 we have \overline{e}[[e[[a]]]] ∈ [C]. ⊓ ⊔

7. Conclusion

We have defined a notion of explicit environments which generalizes explicit substitutions and records, and given a calculus for it which is confluent, SN and conservative extension of the simply typed λβcalculus. The calculus we have presented here is the first such calculus that is conservative over the simply typed λβ-calculus.

We have shown how definition of free and bound variables can be achieved by a suitable type system. This is a form of static analysis.

Now, we explain how our calculus contains records. In λε, we can represent the following basic operations of the record calculus.

• r.x (extraction) — the value corresponding to the label x is extracted from the record r.

• ⟨r | x = a⟩ (extension) — the field of the label x and the value a is added to the record r, if there is no field of label x in r.

• r\x (restriction) — the field of the label x is removed from the record r.

Note that ⟨r\x | x = a⟩ becomes the update operation that updates the value of field x in r to a if there is a field of label x in r or extends r otherwise. A canonical record [x_{1} = a_{1}, …, x_{n} = a_{n}] is represented by the environment {a_{1}/x_{1}, …, a_{n}/x_{n}}, and the above operations can be represented as follows.

r.x := r[[x]],
⟨r | x = a⟩ := {r[[x_{1}]]/x_{1}, …, r[[x_{n}]]/x_{n}, a/x} if x ∉ {x_{1}, …, x_{n}},
r\x := \{ \begin{matrix}\{…, r[[x_{i−1}]]/x_{i−1}, r[[x_{i+1}]]/x_{i+1}, …\} & if x ≡ x_{i} \\ r & if x ∉ \{x_{1}, …, x_{n}\}, \end{matrix}

where TY(r) ≡ {x_{1}, …, x_{n}}. This representation is made possible owing to the fact that λε is a typed system with variable names. It is therefore critical that our calculus has variables with names instead of nameless variables like de Brujin indices, since we insist that an explicit environment must generalize both a record and a substitution. Furthermore, since variables of λ-binders are turned to variables in environment types by (λ), it is natural to use variables with names in λ-binders. Note also that we have defined the representation of extension and restriction operations by case analysis that depends on the type of record r. It is possible because terms of λε are typed terms. However, most record calculi (see, e.g., [7, 8]) consist of untyped terms and type assignment systems that have the notion of subtypes, because they are designed to formulate the features of object oriented languages such as inheritance. Since we cannot represent the notion of subtypes in λε, λε does not contain record calculi in that sense. But we did not extend λε to such a direction because, in this paper, we want to make clear what is the basic system for explicit environments.

There are both named and nameless calculi of explicit substitutions. However, in the case of explicit environments, we have considered only a named calculus for the reason we explained above. Thus, viewed as a calculus of explicit substitution, λε is a named calculus of explicit substitution. We also think it worthwhile to design a nameless version of λε (although such a calculus would no longer contain a calculus of records but instead contain a calculus of tuples), since such a calculus would become a nameless calculus of explicit substitutions that has substitutions as first class values.

It seems possible to design an untyped version of our calculus, which is conservative over the untyped λβ-calculus and preserves SN. The syntax of such a system, however, would have to be an extension of the syntax of untyped λε-terms we have given, since, otherwise, we would not be able to determine free variables correctly. To put it concretely, we give one possible version of untyped λε here. We modify the syntax of the untyped λε-terms given at the beginning of section 3 as follows

a, b, e ::= z | λx.b | ba | {a_{1}/x_{1}, …, a_{n}/x_{n}} | e^{X}[[a]]

where X ranges over sets of bindable variables, and replace the definition of ‘x is free at e[[α]]’ by

x is free at α x is free at e^{X}[[α]] (if x ∉ X).

Then, we define the untyped version of ↦_{λε} by the following rules.

(λ) (λx.b)a ↦_{λ} {a/x}^{{x}}[[b]].
(gc) e^{X}[[a]] ↦_{ε} a, if X ∩ FV(a) = ∅.
(var) {a_{1}/x_{1}, …, a_{n}/x_{n}}^{X}[[x_{i}]] ↦_{ε} a_{i} (1 ≤ i ≤ n), if x_{i} ∈ X.
(abs) e^{X}[[λx.b]] ↦_{ε} λx.e^{X}[[b]], if x ∉ X ∪ FV(e).
(app) e^{X}[[ba]] ↦_{ε} e^{X}[[b]]e^{X}[[a]].
(env) e^{X}[[{a_{1}/x_{1}, …, a_{n}/x_{n}}]] ↦_{ε} {e^{X}[[a_{1}]]/x_{1}, …, e^{X}[[a_{n}]]/x_{n}}.
(eval) e^{X}[[f^{Y} [[x]]]] ↦_{ε} (e^{X}[[f]])^{Y} [[x]], if x ∈ Y.

(Note that {a_{1}/x_{1}, …, a_{n}/x_{n}}^{X}[[y]] where y ∈ X and y ∉ {x_{1}, …, x_{n}} is a normal term if each a_{i} is a normal term.) We can prove the PSN property of this untyped λε using the result by Bloo and Geuvers [5], where they proved PSN of the untyped calculi λx and its extension (see also [6]). Here, we explain λx using our notation for substitutions. The syntax of λx-term is defined by the following grammar

a, b ::= x | λx.b | ba | {b/x}[[a]]

and the reduction rules of λx are (λ), (gc), (var) with n = 1, (abs) and (app), where we read e^{X}[[⋯]] as {c/y}[[⋯]] and X as {y}. In [5], λx is extended by adding the composition rule of substitution

(comp) {b/y}[[{a/x}[[c]]]] → {{b/y}[[a]]/x}[[c]], if x ∈ FV(ε(c)) and y ∉ FV(ε(c))

and its PSN property is proved. The simple terms of untyped λε such that X in e^{X}[[a]] is {Ψ_{1}(e)} (see Theorem 5.8) are essentially λx-terms, because we can assume without loss of generality that {b/y}[[{a/x}]] is reduced to {{b/y}[[a]]/x} as soon as possible. (We omit X in e^{X}[[⋯]] hereafter.) Then, (eval) becomes the rule

(compv) {b/y}[[{a/x}[[x]]]] → {{b/y}[[a]]/x}[[x]],

which is (comp) in the case c ≡ x. Therefore, the untyped λε has PSN property. Furthermore, by this correspondence and Theorem 6.10, we can conclude that typed λx and its extension by (compv) are SN. As far as we know, no composition rule of substitution is ever known that does not break SN when added to typed λx (see, e.g., [9, 14]). Though the form of composition is rather limited, this result is new in that point. But we do not know whether typed λx with (comp) is SN or not.

Also, there are recently growing interests in the calculi of contexts. Among these calculi, a typed calculus of context introduced by Hashimoto and Ohori [12] uses type information to determine the set of free variables for a given term. We feel that we should be able to design a language which has both environments and contexts as first class values.

Other future research directions would be to extend the calculus to a calculus that supports dependent types. We are also considering how to use environments to mimic assignment in imperative programs and hope to do further work in this direction.

Acknowledgements We thank Takayasu Ito and Yukiyoshi Kameyama for helpful comments on earlier versions of the paper. We also thank the anonymous referees for detailed comments and useful suggestions.

Appendix: Proof of Lemma 6.8

For the proof of Lemma 6.8, we introduce the following definitions.

Let δ : c ↦ c̃. Then, this decoration naturally induces a mapping from Π(c) to Π(c̃) as follows. We use δ to denote this mapping. So, for each π ∈ Π(c) we define δ(π) ∈ Π(c̃) inductively as follows.

1. (δ_{1}, …, δ_{n})(Λ) := Λ.

2. (δ_{1}, …, δ_{n})(iπ) := iδ_{i}(π) (1 ≤ i ≤ n).

3. (e, δ)(π) := 2δ(π).

We can easily check that the image of the mapping δ : Π(c) → Π(c̃) is exactly the set of internal positions in δ.

In the same setting as above, we can also define a partial mapping from Π(c̃) to Π(c) as follows. We use δ^{−1} to denote this mapping.

1. δ^{−1}(Λ) := Λ.

2. (δ_{1}, …, δ_{n})^{−1}(iπ) := iδ_{i}^{−1}(π) (1 ≤ i ≤ n).

3. (e, δ)^{−1}(π) := δ^{−1}(π).

We note that the domain of δ^{−1} is the set of internal or marginal positions in δ. We can also see that δ^{−1}(δ(π)) = π for π ∈ Π(c), δ(δ^{−1}(π)) = π for π ∈ Π(c̃) internal in δ, and δ(δ^{−1}(π)) ⊏ π for π ∈ Π(c̃) marginal in δ.

Suppose that γ : c ↦ a, δ : c ↦ b and a ⪯ b. Suppose, further, that σ ∈ Π(a) is marginal in γ and τ ∈ Π(b) is marginal in δ. Then, we write σ ∼ τ (a ⪯ b) if for some π ∈ Π(c) and a natural number i, γ^{−1}(σ) is the second component of the i-th member of env(c, π, γ) and δ^{−1}(τ) is the second component of the i-th member of env(c, π, δ). We see that for any marginal σ in γ, there is at least one τ such that σ ∼ τ (a ⪯ b), and if σ ∼ τ_{1}, σ ∼ τ_{2}, and τ_{1} ≠ τ_{2}, then τ_{1} ⋢ τ_{2} and τ_{2} ⋢ τ_{1}.

Here is an example. Consider the decorations

(e, (δ_{1}, δ_{2})) : ba ↦ e[[b̃ã]]
((e, δ_{1}), (e, δ_{2})) : ba ↦ e[[b̃]]e[[ã]]

where b̃ ≡ δ_{1}(b) and ã ≡ δ_{2}(a). Then, we have

Λ ∼ 1 (e[[b̃ã]] ⪯ e[[b̃]]e[[ã]])
Λ ∼ 2 (e[[b̃ã]] ⪯ e[[b̃]]e[[ã]]).

We use the replacement notation also for decoration trees. If δ : c ↦ c̃, π ∈ Π(c̃) internal or marginal in δ, and γ : d ↦ d̃where d is a subterm of c, then δ_{π}[γ] stands for the decoration tree which is obtained from γ by textually replacing its subdecoration tree δ/π with γ.

Before proving Lemma 6.8, we will explain the idea of the proof. We show that c_{1} is SN by showing that all d_{1} such that c_{1} → d_{1} are SN. We have to classify the redexes by the position and the reduction rule, but the essential cases are proved in the following way: Given d_{1}, we can find d_{2} such that d_{1} ⪯ d_{2} and c_{2} →^{∗} d_{2}. Since we have a measure such that a pair of d_{1} and d_{2} is smaller than a pair of c_{1} and c_{2}, we can appeal to the induction. In the example before Lemma 6.8, if we put c_{1} := e[[(λx.b̃)ã]], c_{2} := (λx.e[[b̃]])e[[ã]] and take e[[{ã/x}[[b̃]]]] as d_{1}, we have {e[[ã]]/x}[[e[[b̃]]]] as d_{2}.

Proof of Lemma 6.8: We assume that γ_{1} : c ↦ c_{1} and γ_{2} : c ↦ c_{2}. We first show that w(γ_{1}) is definable, that is, γ_{1} is SN. Let e be an environment term in γ_{1}. Then e ≡ γ_{1}/π for some π and e is a subterm of c_{1}. Since c_{1} ⪯ c_{2}, we see that e is also a subterm of c_{2}. Since c_{2} is SN, we have that e is SN. Hence γ_{1} is SN. So, we prove the lemma by a double induction on ν(c_{2}) and w(γ_{1}).

We show that d_{1} is SN for all d_{1} such that c_{1} → d_{1}. Take any such d_{1} and let c_{1}/σ_{1} be the redex of the conversion. We classify the redex of this conversion as follows.

1. External: We can find a unique τ_{1} such that τ_{1} is marginal in γ_{1} and τ_{1}1 ⊑ σ_{1}. We put

S := {τ ∈ Π(c_{2}) | τ_{1} ∼ τ (c_{1} ⪯ c_{2})}.

Then, for any τ ∈ S, we have c_{2}/τ1 ≡ c_{1}/τ_{1}1. So, for each τ ∈ S, we apply the same conversion to c_{2}/τ1 as we applied to c_{1}/τ_{1}1, and we let d_{2} be the result of applying these conversions to c_{2}. It is easy to see that d_{1} ⪯ d_{2}. Since S ≠ ∅, we have ν(d_{2}) < ν(c_{2}). So, by IH, we see that d_{1} is SN.

2. Marginal: γ_{1}/σ_{1} is of the form (e, ρ). We put π := γ_{1}^{−1}(σ_{1}2), then the redex is e[[ρ(c/π)]]. We also

put

S := {σ ∈ Π(c_{2}) | σ_{1} ∼ σ (c_{1} ⪯ c_{2})}.

We have the following cases according to the rule used to convert the redex.

2.1. (gc): In this case, γ_{1}/σ_{1} is of the form (e, δ_{1}) and we have c_{1}/σ_{1} ≡ e[[δ_{1}(a)]], c/π ≡ a, TY(e) ∩ FV(δ_{1}(a)) = ∅, and c_{1}/σ_{1} → δ_{1}(a). Let σ ∈ S. Then we have that c_{2}/σ is of the form e[[δ_{2}(b)]] where γ_{2}/σ ≡ (e, δ_{2}) and b is a subterm of a. Since FV(b) ⊆ FV(a), we see that TY(e) ∩ FV(δ_{2}(b)) = ∅. So, we can apply the (gc) rule to c_{2}/σ. Let d_{2} be the result of applying the (gc) rule to all subterms c_{2}/σ in c_{2} for σ ∈ S. Then we have d_{1} ⪯ d_{2}. Moreover, since S ≠ ∅, we have c_{2} →^{+} d_{2} and hence ν(d_{2}) < ν(c_{2}). Therefore, we see that d_{1} is SN by IH.

2.2. (var): In this case, γ_{1}/σ_{1} is of the form ({a_{1}/x_{1}, …, a_{n}/x_{n}}, ι_{x_{k}}) and we have c_{1}/σ_{1} ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{k}]], c/π ≡ x_{k}, and c_{1}/σ_{1} → a_{k}. Since c_{1} ⪯ c_{2}, we see that S is a singleton set, that is S = {σ_{2}}. Then we have that c_{2}/σ_{2} ≡ c_{1}/σ_{1}. So, by applying (var), we have c_{2}/σ_{2} → a_{k}. Let d_{2} be the result of applying these conversions to c_{2}. Then we have ν(d_{2}) < ν(c_{2}) and d_{1} ⪯ d_{2}. Hence, by IH, we see that d_{1} is SN.

2.3. (abs): In this case, γ_{1}/σ_{1} is of the form (e, (δ_{1})) and we have c_{1}/σ_{1} ≡ e[[λx.δ_{1}(b)]], c/π ≡ λx.b, and c_{1}/σ_{1} → λx.e[[δ_{1}(b)]]. Let σ ∈ S. Then we have c_{2}/σ ≡ e[[λx.δ_{2}(b)]] or c_{2}/σ ≡ e[[δ_{2}(b_{2})]] where b_{2} is a subterm of b. We have two cases.

2.3.1.There is some σ ∈ S such that c_{2}/σ ≡ e[[λx.δ_{2}(b)]]: In this case, we have c_{2}/σ → λx.e[[δ_{2}(b)]]. Let d_{2} be the result of applying the same conversions to c_{2}. Then we have ν(d_{2}) < ν(c_{2}) and d_{1} ⪯ d_{2}. Hence, by IH, we see that d_{1} is SN. 2.3.2.Otherwise: We put γ′_{1} := (γ_{1})_{σ_{1}}[((e, δ_{1}))]. Since γ′_{1} : c ↦ d_{1} and γ_{2}(π)1 ⊑ σ, we see that d_{1} ⪯ c_{2}. Hence, noting that w(γ′_{1}) < w(γ_{1}), we see that d_{1} is SN by IH.

2.4. (app), (env): Similar to the (abs) case.

2.5. (eval): In this case, c_{1}/σ_{1} is of the form e[[f[[x]]]], x ∈ TY(f) and c_{1}/σ_{1} → e[[f]][[x]]. Here, we have two cases.

2.5.1.f[[x]] is marginal: In this case, γ_{1}/σ_{1} is of the form (e, (f, ι_{x})). We see that S is a singleton set {σ_{2}} and c_{2}/σ_{2} ≡ e[[f[[x]]]]. We put d_{2} := (c_{2})_{σ_{2}}[e[[f]][[x]]]. Then we have decorations (γ_{1})_{σ_{1}}[(e[[f]], ι_{x})] : c ↦ d_{1} and (γ_{2})_{σ_{2}}[(e[[f]], ι_{x})] : c ↦ d_{2} and have d_{1} ⪯ d_{2}. Since ν(d_{2}) < ν(c_{2}), by IH, we see that d_{1} is SN. 2.5.2.f[[x]] is not marginal: In this case, γ_{1}/σ_{1} is of the form (e, (δ_{1}, ι_{x})). Then c/π is of the form g[[x]] and we have f ≡ δ_{1}(g). Hence we have c_{1}/σ_{1} → e[[δ_{1}(g)]][[x]]. Let σ ∈ S. Then we have c_{2}/σ ≡ e[[γ(a)]], where γ_{2}/σ ≡ (e, γ) and a is a subterm of g[[x]]. Here we have two cases. 2.5.2.1.a ≡ g[[x]] for some σ ∈ S: In this case, there is some σ ∈ S such that c_{2}/σ ≡ e[[δ_{2}(g)[[x]]]]. So, by putting d_{2} ≡ (c_{2})_{σ}[e[[δ_{2}(g)]][[x]]], we get d_{1} ⪯ d_{2}. Since ν(d_{2}) < ν(c_{2}), we see that d_{1} is SN by IH. 2.5.2.2.Otherwise: Since c_{1} ⪯ c_{2}, we see that γ_{2}(c)/γ_{2}(π) is of the form δ_{2}(g)[[\overline{e}[[e[[x]]]]]]. Since x ∈ TY(g), we have x ∉ TY(e) ∪ TY(\overline{e}) by the condition (∗∗) on decoration. So, we have \overline{e}[[e[[x]]]] →^{+} x by applying the (gc) rule several times. Hence, we have c_{2} →^{+} d_{2} where we put d_{2} := (c_{2})_{γ_{2}(π)}[δ_{2}(g)[[x]]]. Now, since c_{1} ⪯_{c} c_{2}, we see that e[[δ_{1}(g)]] ⪯_{g} δ_{2}(g). Therefore, we have d_{1} ⪯_{c} d_{2}. Since ν(d_{2}) < ν(c_{2}), by IH, we see that d_{1} is SN.

3. Internal: In this case, we put π := γ_{1}^{−1}(σ_{1}) ∈ Π(c). Then we put σ_{2} := γ_{2}(π). We note that σ_{2} is internal in γ_{2}. We classify cases according to the rule used to convert c_{1}/σ_{1}.

3.1. (λ): In this case, c/π ≡ (λx.b)a, c_{i}/σ_{i} (i = 1, 2) is of the form \overline{e_{i}}[[λx.δ_{i}(b)]]ρ_{i}(a) where \overline{e_{1}} is empty, and d_{1} ≡ (c_{1})_{σ_{1}}[{ρ_{1}(a)/x}[[δ_{1}(b)]]]. We have two cases.

3.1.1. \overline{e_{2}} is non-empty: We can write \overline{e_{2}} as \overline{f}, f, so that c_{2}/σ_{2} ≡ \overline{f}[[f[[λx.δ_{2}(b)]]]]ρ_{2}(a). Then, by putting

c_{3} := (c_{2})_{σ_{2}}[\overline{f}[[λx.f[[δ_{2}(b)]]]]ρ_{2}(a)],

we have c_{2} ⪯ c_{3} and c_{2} → c_{3}. Since ν(c_{3}) < ν(c_{2}), we see that c_{1} is SN by IH. Hence d_{1} is SN. 3.1.2. \overline{e_{2}} is empty: We put d:= c_{π}[\{a/x\}[[b]]] so that we have c → d and we also put:

d_{2} := (c_{2})_{σ_{2}}[{ρ_{2}(a)/x}[[δ_{2}(b)]]].

Then we have c_{2} → d_{2}, so that ν(d_{2}) < ν(c_{2}). It is also easy to see that d_{1} ⪯_{d} d_{2}. Hence d_{1} is SN.

3.2. (gc): In this case, c/π ≡ e[[a]], TY(e) ∩ FV(a) = ∅, c_{i}/σ_{i} (i = 1, 2) is of the form δ_{i}(e)[[ρ_{i}(a)]] and d_{1} ≡ (c_{1})_{σ_{1}}[ρ_{1}(a)]. We put d:= c_{π}[a] and d_{2} := (c_{2})_{σ_{2}}[ρ_{2}(a)]. Then we can easily check that c → d, c_{2} → d_{2} and d_{1} ⪯_{d} d_{2}. Since ν(d_{2}) < ν(c_{2}), we see that d_{1} is SN by IH.

3.3. (var): In this case, c/π ≡ {a_{1}/x_{1}, …, a_{n}/x_{n}}[[x_{k}]], c_{i}/σ_{i} (i = 1, 2) is of the form {…, δ_{i}^{k}(a_{k})/x_{k}, …\}[[\overline{e_{i}}[[x_{k}]]]] where \overline{e_{1}} is empty, and d_{1} ≡ (c_{1})_{σ_{1}}[δ_{i}^{k}(a_{k})]. We can conclude that d_{1} is SN by an argument similar to the (λ) case.

3.4. (abs), (app), (env): Similar to the (var) case.

3.5. (eval): In this case, we have two possibilities.

3.5.1.c/π ≡ e[[f[[x]]]] and x ∈ TY(f): Here, we have c → c_{π}[e[[f]][[x]]]. Moreover, c_{i}/σ_{i} (i = 1, 2) is of the form δ_{i}(e)[[\overline{e_{i}}[[ρ_{i}(f)[[x]]]]]] where \overline{e_{1}} is empty and d_{1} ≡ (c_{1})_{σ_{1}}[δ_{1}(e)[[ρ_{1}(f)]][[x]]]. 3.5.1.1. \overline{e_{2}} is non-empty: Similar to case 3.1.1.

3.5.1.2. \overline{e_{2}} is empty: We put d_{2} := (c_{2})_{σ_{2}}[δ_{2}(e)[[ρ_{2}(f)]][[x]]]. Then, we see that c_{2} → d_{2}, ν(d_{2}) < ν(c_{2}) and d_{1} ⪯_{d} d_{2}. Hence, by IH, we see that d_{1} is SN.

3.5.2.c/π ≡ e[[x]], c_{1}/σ_{1} ≡ δ_{1}(e)[[f[[x]]]] and x ∈ TY(f): Here, we have d_{1} ≡ (c_{1})_{σ_{1}}[δ_{1}(e)[[f]][[x]]]. Since x ∈ TY(f), by the conditions (∗) and (∗∗) on decoration, we see that the occurrence of x at π2 in c is free. So, since c_{1} ⪯ c_{2}, we see that c_{2}/σ_{2} must be of the form δ_{2}(e)[[\overline{f}[[f[[x]]]]]]. Here, we have two subcases. 3.5.2.1. \overline{f} is non-empty: We first note that env(c, π2, γ_{1}) ≡ ⟨f, π2⟩ and

env(c, π2, γ_{2}) ≡ ⟨f, π2⟩, ⟨f_{m}, π2⟩, …, ⟨f_{1}, π2⟩

where \overline{f} ≡ f_{1}, …, f_{m} (m > 0). Since x ∈ TY(f) and f_{1}, …, f_{m}, f are all bindable variable free, we have the reduction \overline{f}[[f[[x]]]] →^{+} f[[x]] by applying the (gc) rule m times. Moreover, we have c_{1} ⪯ d_{2} where we put d_{2} := (c_{2})_{σ_{2}2}[f[[x]]]. Since ν(d_{2}) < ν(c_{2}), by IH, we see that c_{1} is SN, and hence d_{1} is also SN. 3.5.2.2. \overline{f} is empty: We see that x ∉ TY(e) since x is free in c. So, putting d := c_{π2}[x], we have c → d by (gc). Now we put d_{2} := (c_{2})_{σ_{2}}[δ_{2}(e)[[f]][[x]]]. We also consider d′_{i} := (c_{i})_{σ_{i}}[f[[x]]] (i = 1, 2). From the fact that c_{1} ⪯_{c} c_{2}, we can see that d′_{1} ⪯_{d} d′_{2}. Since f is bindable variable free, we see that TY(e)∩FV(f) = ∅. So, we have d_{2} → d′_{2} by (gc) and hence ν(d′_{2}) < ν(d_{2}) < ν(c_{2}). Hence by IH, we see that d′_{1} is SN. On the other hand, since c_{1} ⪯_{c} c_{2}, we see that δ_{1}(e) ⪯_{e} δ_{2}(e). Here δ_{2}(e) is SN, since it is a subterm of c_{2} which is SN, So, we have ν(δ_{2}(e)) ≤ ν(c_{2}). Moreover, since e is a proper subterm of c, we have w(δ_{1}) < w(γ_{1}). Therefore, by IH, we see that δ_{1}(e) is SN. So, we have the following orthogonal decoration:

(ι_{c_{1}})_{σ_{1}}[(δ_{1}(e), ι_{x})] : d′_{1} ↦ d_{1}

Therefore, by Lemma 6.5, we see that d_{1} is SN.

Since d_{1} is SN in all cases, c_{1} is also SN. ⊓ ⊔

References

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

[2] Abelson, H., Sussman, G. J.: Structure and Interpretation of Computer Programs, The MIT Press, 1985.

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

[4] Benaissa, Z. E. A., Briand, D., Lescanne, P., Maibaum, T. S. E.: λυ, a calculus of explicit substitutions which preserves strong normalization, Journal of Functional Programming, 6, 1996, 699–722.

[5] Bloo, R., Geuvers, H.: Explicit substitution On the edge of strong normalization, Theoretical Computer Science, 211, 1999, 375–395.

[6] Bloo, R., Rose, K.: Preservation of strong normalization in named lambda calculi with explicit substitution and garbage collection, Proc. CSN’95 (Computer Science in Netherlands) (van Vliet J. C., Ed.), 1995.

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

[7] Cardelli, L., Mitchell, J. C.: Operations on records, Mathematical Structures in Computer Science, 1, 1991, 3–48.

[8] Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism, Computing Surveys, 17, 1985, 471–522.

[9] Di Cosmo, R., Kesner, D.: Strong normalization of explicit via cut elimination in proof nets, Proc. 12th IEEE Symposium on Logic in Computer Science, 1997, 35–47.

[10] Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types, Cambridge University Press, 1989.

[11] Hardin, T.: Confluence results for the pure strong categorical combinatory logic CCL: λ-calculi as subsystems of CCL, Theoretical Computer Science, 46, 1986, 305–312.

[12] Hashimoto, M., Ohori, A.: A typed context calculus, Preprint RIMS-1098, Research Institute for Mathematical Sciences, Kyoto University, 1996. (Journal version is to appear in Theoretical Computer Science.)

[13] Kamareddine, F., Ríos, A.: Extending a λ-calculus with explicit substitution which preserves strong normalization into a confluent calculus on open terms, Journal of Functional Programming, 7, 1997, 395–420.

[14] Kamareddine, F., Ríos, A., Wells, J. B.: Calculi of generalized β-reduction and explicit substitutions: The type free and simply typed versions, Journal of Functional and Logic Programming, 1998(5), 1998, 1–44.

[15] Lampson, B., Burstall, R.: Pebble, a kernel language for modules and abstract data types, Information and Computation, 76, 1988, 278–346.

[16] McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I, Comm. ACM, 3, 1960, 184–195.

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

[18] Nishizaki, S.: ML with first-class environments and its type inference algorithm, Logic, Language and Computation, Festschrift in Honor of Satoru Takasu (N. D. Jones, M. Hagiya, M. Sato, Eds.), LNCS 792, 1994, 95–116.

[19] Nishizaki, S.: Simply Typed Lambda Calculus with First-Class Environments, vol. 30(6), Publications of the Research Institute for Mathematical Sciences, Kyoto University, 1994.

[20] Takahashi, M.: Parallel reductions in λ-calculus, Journal of Symbolic Computation, 7, 1989, 113–123.

[21] Takeuti, G.: Proof Theory, North-Holland, 1975.