Explicit Environments (Extended abstract)

Masahiko Sato^{1}, Takafumi Sakurai^{2}, and Rod Burstall^{3}

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

2 Department of Mathematics and Informatics, Chiba University

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

3 Department of Computer Science, University of Edinburgh 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 a set 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.

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 have explicit environments. The Pebble language of Lampson and Burstall [8] also treated explicit environments (bindings). It used dependent types and no confluence result was obtained. Nishizaki [9, 10] 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–3, 7], 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.

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 introduce a typed language λε by introducing typing rules for terms that will determine the (typable) terms of the language. In section 3, we give reduction rules of the λε-calculus and prove the subject reduction theorem for the calculus. In section 4, we prove the confluence of λε and prove that the λε-calculus is a conservative extension of the simply typed λβ-calculus. In section 5, 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 6, we give concluding remarks. Due to lack of space, we have omitted some lemmas and almost all proofs. A full version of this paper with proofs is accessible at

http://www.sato.kuis.kyoto-u.ac.jp/~masahiko/index-e.html.

Acknowledgements We thank Takayasu Ito and Yukiyoshi Kameyama for helpful comments on earlier versions of the paper.

2 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. 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/π.

1 ε is for environment.

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 sequence x_{1}^{A_{1}}, …, x_{n}^{A_{n}} of declarations. We use Γ, Δ etc. as meta variables for contexts. As notational conventions, we will write Γ, Δ for the concatenation of the contexts Γ and Δ. Also, Γ − E will denote the context obtained from Γ by removing all the elements in E from Γ.

A typing judgment is an expression of the form Γ ⊢ a : A where Γ is a context, a is a (typed) λε-term 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 {}.

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

α-congruence. Let a and b be terms and x, y be bindable variables of the same type such that y is fresh for 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}.

2 It 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). An 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}.

By the above typing, we see that the two occurrences of x in {y/x}[[x]] are both bound while the only one occurrence of y in this term is free.

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

3 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. 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 garbage collection rule (gc) collects e as a garbage. 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.

We introduced the last rule (eval) to take care of the nested evaluation. 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 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 5.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 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.

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

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

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 2 (Subject Reduction). If Γ ⊢ a : A and a →_{λε} b, then Δ ⊢ b : A for some subcontext Δ of Γ.

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}[[{double add2/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}.

4 Confluence and Conservativity

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

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

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}, 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 2-5.

Lemma 2. If a ⇒ b, then a →^{∗} b.

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

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

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

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

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 4 (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 by 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 6 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)].

Lemma 6. Let a be a simple λs-term. If a →_{λε} b, then b is also simple and

Φ(a) →^{∗}_{β} Φ(b).

Proof of Theorem 4. Only if part is trivial and if part follows from Lemma 6 by noting that Φ is identity on λβ-terms. □

5 Strong Normalizability

In this section we prove the strong normalizability of the λε-calculus using the reducibility argument. (See, e.g., [4].) So, for each type A, we define a set [A] of reducible terms of type A as follows.

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

Proposition 1. (CR1) If a ∈ [A], then a is SN. (CR2) If a ∈ [A] and a → a′, then a′ ∈ [A]. (CR3) If a : A is neutral and a′ ∈ [A] for all a′ such that a → a′, then a ∈ [A].

5.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}, then we will write (\overline{e}, δ) for (e_{1}, (e_{2}, ⋯ (e_{n}, δ) ⋯)) and \overline{e}[[a]] for e_{1}[[⋯ e_{n}[[a]] ⋯]]. 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 ã/π in ã 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 internal otherwise.

Suppose that δ : c ↦ c̃ and σ is external in δ. Then we can find a unique π such that π is marginal in δ and π1 ≤ σ. In this case, we say that π is the root of σ in δ.

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 δ. If π̃ ≡ δ(π), then we write δ^{−1}(π̃) for π.

Let δ : c ↦ c̃, so that c̃ is of the form \overline{e}[[γ(c)]] where γ ≡ (δ_{1}, …, δ_{n}). Then, for each π ∈ Π(c), we define a decoration tree δ|π as follows. If π ≡ Λ, we put δ|π := γ. If π ≡ iσ, we put δ|π := δ_{i}|σ. We can then see that for each π ∈ Π(c), we have δ|π : c/π ↦ c̃/π̃ where π̃ ≡ δ(π). We will call c̃/π̃ the image of c/π under δ.

A decoration tree δ is strongly normalizing (SN) if each environment term e in δ is SN.

5.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 proposition which is used in the proof of Proposition 4.

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

Discussions on the (eval) rule. Here, we would like to remark that the condition x ∈ TY(f) is essential in proving Proposition 2. 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 a semantically correct and more liberal rule 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. [3]. 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 Proposition 2 no longer holds for the extended calculus. Thus we see that the condition x ∈ TY(f) is indispensable in our proof of Proposition 2.

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

5.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})) := kenv(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 and at δ(σ) in c̃. We note that, here, δ(σ) is marginal in δ and c̃/δ(σ) ≡ e[[a]] for some a. If ⟨e, σ⟩ appears before ⟨e′, σ′⟩ in env(c, π, δ), then we have σ ≥ σ′ and δ(σ) > δ(σ′). 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. Let δ ≡ (f, ((e, ι_{y}), ι_{x})). For the decoration δ : yx ↦ f[[e[[y]][[x]]]], we have env(yx, 1, δ) ≡ ⟨e, 1⟩, ⟨f, Λ⟩ and env(yx, 2, δ) ≡ ⟨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. Proposition 3. If c_{1} ⪯_{c} c_{2} and c_{2} ∈ [C], then c_{1} ∈ [C].

5.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 5 (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 4. If δ : x^{A} ↦ \overline{e}[[x]] and δ is reducible, then \overline{e}[[x]] ∈ [A].

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

Proposition 6. 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}}}].

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. Proposition 7. If c′ is a variant of c : C, then c ∈ [C] iff c′ ∈ [C].

Now we can prove the reducibility theorem as follows. Proof. 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. We treat only two cases.

1. (⇒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(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 7, we have that a′ ∈ [A]. Hence, by Proposition 6, 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 5, we have (λx.b̃)a′ ∈ [B]. So, by Proposition 7, we have (λx.b̃)a ∈ [B]. Therefore, we have λx.b̃ ∈ [C]. Since c̃ ⪯_{λx.b} λx.b̃, we have c̃ ∈ [C] by Proposition 3.

2. (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. 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 3, we have \overline{e}[[e′[[a]]]] ∈ [C]. Therefore, by Proposition 7 we have \overline{e}[[e[[a]]]] ∈ [C]. □

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

Due to lack of space, we have not been able to explain how our calculus contains records. We only note here that a canonical record [x_{1} = a_{1}, …, x_{n} = a_{n}] may be represented by the environment {a_{1}/x_{1}, …, a_{n}/x_{n}}, and that accessing to the x field of a record r may be achieved by r[[x]]. This representation is made possible owing to the fact that λε is a system with variable names. It is therefore critical that our calculus has variables with names, since we insist that an explicit environment must generalize both a record and a substitution.

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.

Also, there are recently growing interests in the calculi of contexts. Among these calculi, a typed calculus of context introduced by Hashimoto and Ohori [6] 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.

References

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

2. Benaissa, Z.E.A., Briand, D., Lescanne, P. and Maibaum, T.S.E., λυ, a calculus of explicit substitutions which preserves strong normalization pp. 699-722, Journal of Functional Programming, 6, 1996.

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

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

4. Girard, J.-Y., Lafont, Y. and Taylor, P., Proofs and Types, Cambridge University Press, 1989.

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

6. Hashimoto, M. and Ohori, A., A typed context calculus, Preprint RIMS-1098, Res. Inst. for Math. Sci., Kyoto Univ., 1996. Available at: http:

//www.kurims.kyoto-u.ac.jp/~ohori/list.html.

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

8. Lampson, B. and Burstall, R., Pebble, a Kernel Language for Modules and Abstract Data Types, pp. 278-346, Information and Computation, 76, 1988.

9. Nishizaki, S., Simply Typed Lambda Calculus with First-Class Environments, Publications of the Research Institute for Mathematical Sciences, Kyoto University, Vol. 30, No. 6, 1994.

10. Nishizaki, S., ML with First-Class Environments and its Type Inference Algorithm, pp. 95-116, Logic, Language and Computation, Festschrift in Honor of Satoru Takasu, Lecture Notes in Computer Science 792, Jones, N. D., Hagiya, M. and Sato, M. (eds.), Springer-Verlag, 1994.

11. Takahashi, M., Parallel Reductions in λ-calculus, J. Symbolic Computation, 7, pp. 113-123, 1989.