Chapter 148Optional

Explicit-Substitution Calculi

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

In the calculi of this book, substitution is an operation of the metalanguage: $β$ -contraction rewrites $(λ x . a) b$ to $a [b / x]$ in one step, and the whole traversal of $a$ happens outside the calculus. An implementation cannot take that step; it must walk the term, and it must be able to stop part-way. Making the traversal into syntax means adding a term former for “ $a$ under a pending substitution” and rules that push the pending substitution one layer inward.

Adding those rules costs nothing by itself. The interesting decision is whether to add one more rule, which composes two pending substitutions into one: $a [s] [t] ⟶ a [s \circ t] .$ The rule is desirable. It makes substitutions an algebra with an associative composition, it lets a machine merge two environments instead of carrying both, and it is what turns the calculus into the algebraic structure that chapter 54 takes as primitive. It is also what this chapter’s central counterexample destroys: with composition, there is a simply typed term, strongly normalizing under ordinary $β$ -reduction, that admits an infinite reduction (theorem 148.8).

Two calculi are therefore developed separately. The first, $λ σ$ , has full composition and is confluent, and the counterexample applies to it. The second, $λ ex$ , has a composition rule guarded by a side condition together with an explicit rule that deletes a substitution nobody uses, and it preserves strong normalization. No theorem proved for one is transferred to the other.

The $λ σ$ -calculus

Definition 148.1 — Syntax ¶

Fix de Bruijn notation: a variable occurrence is a positive integer, and $n$ refers to the variable bound by the $n$ -th enclosing $λ$ . The raw expressions of $λ σ$ are two mutually recursive sorts, $\begin{aligned} terms a, b & ::= 1 ∣ b a ∣ λ a ∣ a [s], \\ substitutions s, t & ::= id ∣ ↑ ∣ a \cdot s ∣ s \circ t . \end{aligned}$ A term $a [s]$ is a closure.

Referenced from 5 locations

Explicit-Substitution Calculi

The intended readings fix every rule below. The substitution $id$ is ${i / i}$ ; the substitution $↑$ is ${i + 1 / i}$ , so that $1 [↑] = 2$ and the index $n + 1$ is written $1 [↑^{n}]$ ; the substitution $a \cdot s$ is ${a / 1, s (i) / i + 1}$ ; and $s \circ t$ is the substitution with $a [s \circ t] = a [s] [t]$ . Only the index $1$ is a primitive term.

Definition 148.2 — The rules ¶

The relation $⟶$ on raw expressions is the compatible closure of $\begin{array}{llcl} B e t a & (λ a) b & ⟶ & a [b \cdot id] \\ V a r I d & 1 [id] & ⟶ & 1 \\ V a r C o n s & 1 [a \cdot s] & ⟶ & a \\ A p p & (b a) [s] & ⟶ & b [s] a [s] \\ A b s & (λ a) [s] & ⟶ & λ a [1 \cdot (s \circ ↑)] \\ C l o s & a [s] [t] & ⟶ & a [s \circ t] \\ I d L & id \circ s & ⟶ & s \\ S h i f t I d & ↑ \circ id & ⟶ & ↑ \\ S h i f t C o n s & ↑ \circ (a \cdot s) & ⟶ & s \\ M a p & (a \cdot s) \circ t & ⟶ & a [t] \cdot (s \circ t) \\ A s s & (s_{1} \circ s_{2}) \circ s_{3} & ⟶ & s_{1} \circ (s_{2} \circ s_{3}) \end{array}$ The ten rules other than Beta are called $σ$ collectively, and $⟶_{σ}$ is the relation they generate.

Referenced from 7 locations

Explicit-Substitution Calculi

Beta is the only rule that removes a $λ$ ; every other rule removes or relocates a substitution. The rule Abs is not a design choice but a calculation. Pushing $s = {s (i) / i}$ under a $λ$ must leave $1$ alone and must protect the free indices of each $s (i)$ from the new binder: $\begin{aligned} (λ c) [s] & \overset{u n d e r λ}{=} λ c {1 / 1, s (i) {i + 1 / i} / i + 1} \\ \overset{d e f . ↑}{=} λ c {1 / 1, s (i) [↑] / i + 1} \\ \overset{d e f . \cdot, \circ}{=} λ c [1 \cdot (s \circ ↑)] . \end{aligned}$ This one rule uses every operator except $id$ , which is what makes the four-operator syntax of definition 148.1 the natural choice rather than an arbitrary one.

Example 148.3 — Substitutions intercept indices ¶

In $(λ 1 [2 \cdot id]) [a \cdot id]$ the occurrence of $1$ is not bound by the displayed $λ$ . The inner substitution intercepts it and returns $2$ ; crossing the $λ$ renames $2$ to $1$ , which the outer substitution sends to $a$ . Reading binding structure off an explicit-substitution term therefore requires computing, not inspecting.

Referenced from 2 locations

Explicit-Substitution Calculi

Proposition 148.4 — σ terminates and is confluent ¶

The relation $⟶_{σ}$ is terminating and confluent, so every raw expression $a$ has a unique $σ$ -normal form, written $σ (a)$ .

Referenced from 4 locations

Explicit-Substitution Calculi

Proof of Proposition 148.4 — σ terminates and is confluent

Proof. Termination is imported. Merging the two sorts and identifying $- [-]$ with $\circ$ translates $σ$ into the rewriting system $SUBST$ of categorical combinators, one $σ$ -step to one $SUBST$ -step; termination of $SUBST$ is the theorem of Hardin and Laville cited by the source (section 148.3). Nothing else in this chapter depends on that import.

Given termination, local confluence suffices, and local confluence is checked on critical pairs. For instance the pair $1 [id] [s] \overset{V a r I d}{⟶} 1 [s], 1 [id] [s] \overset{C l o s}{⟶} 1 [id \circ s] \overset{I d L}{⟶} 1 [s]$ closes with IdL. The remaining overlaps close in the same way, each by one of IdL, ShiftCons, Map or Ass. ◻

Proposition 148.5 — σ -normal forms are ordinary terms ¶

The $σ$ -normal forms are generated by $a, b ::= 1 ∣ 1 [↑^{n}] ∣ b a ∣ λ a, s ::= id ∣ ↑^{n} ∣ a \cdot s .$ In particular a term in $σ$ -normal form contains no closure except the codings $1 [↑^{n}]$ of de Bruijn indices, so it is a term of the ordinary $λ$ -calculus.

Referenced from 6 locations

Explicit-Substitution Calculi

Proof of Proposition 148.5 — σ -normal forms are ordinary terms

Proof. A normal substitution cannot be a composition: the outermost composition $s \circ t$ is a redex for one of IdL, ShiftId, ShiftCons, Map or Ass according to the shape of $s$ , and these five cases exhaust the productions for $s$ . So a normal substitution is $id$ , $↑$ , or $a \cdot s$ with $a, s$ normal, and iterating the last clause gives the displayed grammar with $↑^{n}$ written for the $n$ -fold composition, itself normal only when its associativity has been fixed. A normal term cannot be a closure $a [s]$ unless $a = 1$ and $s$ is a composition of shifts: if $a$ is an application, an abstraction or a closure, one of App, Abs, Clos applies, and if $a = 1$ then VarId or VarCons applies unless $s$ is $↑^{n}$ . ◻

Theorem 148.6 — Simulation of β ¶

Let $a {a_{1} / 1, a_{2} / 2, \dots} = b$ be derivable in the metalevel substitution calculus for de Bruijn terms, and suppose there are $m$ and $p$ with $a_{m + q} = p + q$ for all $q \geq 1$ . Then $σ (a [a_{1} \cdot a_{2} \dots a_{m} \cdot ↑^{p}]) = b .$ Consequently one $β$ -step is simulated by one Beta-step followed by $σ$ -reduction to normal form.

Referenced from 6 locations

Explicit-Substitution Calculi

Proof of Theorem 148.6 — Simulation of β

Proof. Induction on the derivation, strengthening the claim so that every intermediate expression satisfies the hypothesis on the $a_{i}$ .

Index. For $n {a_{1} / 1, \dots} = a_{n}$ : if $n \leq m$ then $n [a_{1} \dots a_{m} \cdot ↑^{p}]$ $σ$ -reduces to $a_{n}$ by $n - 1$ uses of ShiftCons followed by VarCons; if $n > m$ it reduces to $n - m + p$ , and the hypothesis gives $a_{n} = a_{m + (n - m)} = n - m + p$ .

Application. Both sides distribute by App and the two induction hypotheses apply to the immediate subterms.

Abstraction. For $(λ a) {a_{1} / 1, \dots} = λ a^{'}$ , the metalevel rule first lifts each $a_{i}$ , giving $a_{i}^{'}$ with $σ (a_{i} [↑]) = a_{i}^{'}$ by the induction hypothesis at $m = 0$ , $p = 1$ . The induction hypothesis for $a$ at $m + 1$ and $p + 1$ gives $σ (a [1 \cdot a_{1}^{'} \dots a_{m}^{'} \cdot ↑^{p + 1}]) = a^{'}$ . On the other side, Abs produces $a [1 \cdot ((a_{1} \dots a_{m} \cdot ↑^{p}) \circ ↑)]$ , and repeated Map gives $(a_{1} \dots a_{m} \cdot ↑^{p}) \circ ↑ \overset{M a p}{⟶^{*}} a_{1} [↑] \dots a_{m} [↑] \cdot ↑^{p + 1},$ whose $σ$ -normal form is $a_{1}^{'} \dots a_{m}^{'} \cdot ↑^{p + 1}$ . The two sides therefore have the same $σ$ -normal form. ◻

Theorem 148.7 — Confluence of λ σ ¶

The relation generated by Beta together with $σ$ is confluent.

Referenced from 5 locations

Explicit-Substitution Calculi

Proof of Theorem 148.7 — Confluence of λ σ

Proof. The proof does not go through the Knuth–Bendix test, which $B e t a + σ$ fails, and instead uses Hardin’s interpretation method: if $R$ is terminating and confluent with normal-form map $R (-)$ , if $S_{R}$ is a relation on $R$ -normal forms contained in $(R \cup S)^{*}$ , and if $S (x, y)$ implies $S_{R}^{*} (R (x), R (y))$ , then confluence of $S_{R}$ gives confluence of $R \cup S$ .

Take $R : = σ$ , which is terminating and confluent by proposition 148.4, and $S_{R} : = β$ on $σ$ -normal forms. Two facts are then needed. First, $β$ is confluent on $σ$ -normal forms: by proposition 148.5 those are ordinary $λ$ -terms, on which $β$ is the ordinary $β$ by theorem 148.6, and ordinary $β$ is confluent; on substitutions in normal form the reductions are independent reductions in the components. Second, a Beta-step projects: if $a \overset{B e t a}{⟶} b$ then $σ (a) {⟶^{*}}_{β} σ (b)$ , and likewise for substitutions. That projection is proved by induction on the pair consisting of the length of the longest $σ$ -reduction out of the expression and its size, with cases for applications, abstractions, closures and compositions; the source carries it out in full. Hardin’s method then yields the theorem. ◻

Exercise 148.1 ¶

★☆☆ Reduce $(λ (2 1)) [a \cdot id]$ to $σ$ -normal form, naming the rule at each step. Recall that $2$ abbreviates $1 [↑]$ .

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.2 ¶

★★☆ Check local confluence for the critical pair between Map and Ass on $((a \cdot s_{1}) \circ s_{2}) \circ s_{3}$ , displaying both reducts and their common reduct.

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.3 ¶

★★☆ Show that $σ$ alone does not prove $1 [s] \cdot (↑ \circ s) = s$ for an arbitrary substitution variable $s$ , although the equation holds for every closed normal $s$ . Which rule would have to be added, and what does its absence say about the difference between the equational theory and the rewriting system?

Referenced from 2 locations

Explicit-Substitution Calculi

Composition destroys strong normalization

$λ σ$ is confluent. It does not follow that a term which cannot diverge under ordinary $β$ -reduction cannot diverge in $λ σ$ , and it is false.

The failure is easiest to display with named variables, in a calculus with single substitutions. Write $t ⟨ x : = u ⟩$ for a pending substitution and consider the single composition rule $t ⟨ x : = u ⟩ ⟨ y : = v ⟩ ⇝ t ⟨ x : = u ⟨ y : = v ⟩ ⟩ if y \notin FV (t) .$ The side condition says the outer substitution is garbage for $t$ : nothing in $t$ uses $y$ . The rule does not delete it; it pushes it into the body of the inner substitution. Equation 148.1 is weaker than the Clos/Map pair of definition 148.2, which implement the parallel form of the same move, so a divergence built from it is a divergence of $λ σ$ .

Theorem 148.8 — Composition breaks preservation of strong normalization ¶

There is a term, strongly normalizing under $β$ -reduction, that admits an infinite reduction using $β$ , the substitution-propagation rules, and (148.1).

Referenced from 14 locations

Explicit-Substitution Calculi

Proof of Theorem 148.8 — Composition breaks preservation of strong normalization

Proof. Let $a, b, y, y^{'}$ be four distinct variables and define $S_{0} : = ⟨ y : = (λ y . a) b ⟩, S_{n + 1} : = ⟨ y : = b S_{n} ⟩ .$ Start from $M : = (λ y . (λ y^{'} . a) ((λ y . a) b)) ((λ y . a) b)$ and compute: $\begin{aligned} M & ⟶ a ⟨ y^{'} : = (λ y . a) b ⟩ ⟨ y : = (λ y . a) b ⟩ & two Beta steps \\ ⇝ a ⟨ y^{'} : = ((λ y . a) b) ⟨ y : = (λ y . a) b ⟩ ⟩ & (148.1), since y \notin FV (a) \\ ⟶ a ⟨ y^{'} : = (λ y . a S_{0}) (b S_{0}) ⟩ & propagation into the application \\ ⟶ a ⟨ y^{'} : = a S_{0} ⟨ y : = b S_{0} ⟩ ⟩ & Beta, \end{aligned}$ and the last expression is $a ⟨ y^{'} : = a S_{0} S_{1} ⟩$ . $\begin{matrix} \end{matrix}$ The same four moves applied to $a S_{0} S_{m + 1}$ give $a S_{0} S_{m + 1} ⇝ \dots ⟶ a ⟨ y^{'} : = a S_{m + 1} S_{m + 2} ⟩,$ and for the mixed indices $\begin{aligned} a S_{m + 1} S_{n + 1} & = a ⟨ y^{'} : = b S_{m} ⟩ ⟨ y : = b S_{n} ⟩ \\ ⇝ a ⟨ y^{'} : = b S_{m} ⟨ y : = b S_{n} ⟩ ⟩ = a ⟨ y^{'} : = b S_{m} S_{n + 1} ⟩ . \end{aligned}$ Chaining these three schemes produces $\begin{aligned} M & ⟶ \dots S_{0} S_{1} \dots ⟶ \dots S_{1} S_{2} \dots ⟶ \dots S_{0} S_{2} \dots \\ ⟶ \dots S_{2} S_{3} \dots ⟶ \dots S_{1} S_{3} \dots ⟶ \dots S_{0} S_{3} \dots ⟶ \dots, \end{aligned}$ an infinite reduction, since the index pair strictly increases along the displayed schedule and no expression repeats.

The term $M$ is strongly normalizing under $β$ : every $β$ -redex of $M$ has a body in which the bound variable does not occur, so each contraction erases its argument and strictly decreases the number of $λ$ ’s. The original counterexample uses the simply typable term $λ x . (λ y . I (I y)) (I x)$ with $I : = λ z . z$ , for which the same schedule runs and the type assignment is displayed in the source. ◻

Remark 148.9 — Where the divergence lives ¶

Every step after the first three takes place inside a substitution that no free variable of the body uses. The reduction never produces a term whose $σ$ -normal form is new; by theorem 148.6 the projection of the whole sequence to ordinary $λ$ -terms is finite. What diverges is the bookkeeping, not the computation. Two repairs suggest themselves: forbid pushing a substitution into garbage, or delete garbage instead of pushing it. The calculus of the next section does both, with one side condition and one rule.

Referenced from 2 locations

Explicit-Substitution Calculi

Remark 148.10 — Confluence and normalization are independent ¶

Theorem 148.7 and theorem 148.8 hold of the same calculus. Confluence says that the results of terminating computations agree; it says nothing about which computations terminate. Neither theorem may be used to weaken the other, and neither transfers to a different explicit-substitution calculus without a proof for that calculus.

Referenced from 2 locations

Explicit-Substitution Calculi

Safe composition: the $λ ex$ -calculus

Definition 148.11 — Syntax and equation ¶

Terms are generated by $T ::= x ∣ T T ∣ λ x . T ∣ T [x / T]$ , with $λ x . t$ and $t [x / u]$ both binding $x$ in $t$ ; free variables are as usual, with $FV (t [x / u]) = (FV (t) ∖ {x}) \cup FV (u)$ . Metalevel substitution $t {x / u}$ is defined as usual and additionally by $t [y / u] {x / v} : = t {x / v} [y / u {x / v}]$ . The equation $C t [x / u] [y / v] = t [y / v] [x / u] if y \notin FV (u) and x \notin FV (v)$ together with $α$ -conversion generates an equivalence $=_{e}$ on terms.

Referenced from 5 locations

Explicit-Substitution Calculi

Definition 148.12 — The rules ¶

$\begin{array}{llcll} B & (λ x . t) u & ⟶ & t [x / u] \\ V a r & x [x / u] & ⟶ & u \\ G c & t [x / u] & ⟶ & t & if x \notin FV (t) \\ A p p & (t u) [x / v] & ⟶ & t [x / v] u [x / v] \\ L a m b & (λ y . t) [x / v] & ⟶ & λ y . t [x / v] \\ C o m p & t [x / u] [y / v] & ⟶ & t [y / v] [x / u [y / v]] & if y \in FV (u) \end{array}$ Write $⟶_{x}$ for the relation generated by the five rules other than B, and let $⟶_{λ ex}$ be $⟶$ modulo $=_{e}$ : that is, $t ⟶_{λ ex} t^{'}$ when $t =_{e} s ⟶ s^{'} =_{e} t^{'}$ for some $s, s^{'}$ .

Referenced from 6 locations

Explicit-Substitution Calculi

Two features distinguish definition 148.12 from definition 148.2. The composition rule Comp fires only when $y \in FV (u)$ , that is, only when the outer substitution has something to do inside the inner one. And Gc deletes a substitution whose variable does not occur. Together they remove exactly the move (148.1) used in theorem 148.8: when $y \notin FV (t)$ and $y \notin FV (u)$ the substitution is deleted, and when $y \in FV (u)$ it is composed, which is not pushing into garbage.

Theorem 148.13 — Full composition ¶

For all terms $t, u$ , $t [x / u] {⟶^{*}}_{λ ex} t {x / u}$ .

Referenced from 6 locations

Explicit-Substitution Calculi

Proof of Theorem 148.13 — Full composition

Proof. Induction on $t$ .

$t = x$ . $x [x / u] \overset{V a r}{⟶} u = x {x / u}$ .

$t = y \neq x$ . $x \notin FV (y)$ , so $y [x / u] \overset{G c}{⟶} y = y {x / u}$ .

$t = t_{1} t_{2}$ . By App, $(t_{1} t_{2}) [x / u] ⟶ t_{1} [x / u] t_{2} [x / u]$ ; the two induction hypotheses then give $⟶^{*} t_{1} {x / u} t_{2} {x / u}$ , which is $(t_{1} t_{2}) {x / u}$ .

$t = λ y . s$ . Choose $y \notin FV (u) \cup {x}$ by $α$ -conversion. Then $(λ y . s) [x / u] \overset{L a m b}{⟶} λ y . s [x / u] \overset{I H}{⟶^{*}} λ y . s {x / u} = (λ y . s) {x / u} .$

$t = s [y / v]$ . Choose $y \notin FV (u) \cup {x}$ . Two cases. If $x \in FV (v)$ , then Comp applies to $s [y / v] [x / u]$ and gives $s [x / u] [y / v [x / u]]$ ; the induction hypotheses for $s$ and $v$ reduce this to $s {x / u} [y / v {x / u}]$ , which is $(s [y / v]) {x / u}$ by definition 148.11. If $x \notin FV (v)$ , then $v {x / u} = v$ and the equation C applies, since $y \notin FV (u)$ and $x \notin FV (v)$ : $s [y / v] [x / u] =_{e} s [x / u] [y / v] ⟶^{*} s {x / u} [y / v] = (s [y / v]) {x / u} .$ ◻

Corollary 148.14 — Simulation ¶

If $t ⟶_{β} t^{'}$ for $λ$ -terms $t, t^{'}$ , then $t {⟶^{*}}_{λ ex} t^{'}$ .

Referenced from 4 locations

Explicit-Substitution Calculi

Proof of Corollary 148.14 — Simulation

Proof. A $β$ -step contracts $(λ x . s) u$ to $s {x / u}$ in some context. By B the same context reduces to $s [x / u]$ , and by theorem 148.13 that reduces to $s {x / u}$ . Reduction is compatible with contexts. ◻

Proposition 148.15 — The counterexample is blocked ¶

In $λ ex$ the term $M$ of theorem 148.8 reduces in four steps to the normal form $a$ .

Referenced from 4 locations

Explicit-Substitution Calculi

Proof of Proposition 148.15 — The counterexample is blocked

Proof. Two B steps are available; take the outer one first: $M \overset{B}{⟶} ((λ y^{'} . a) ((λ y . a) b)) [y / (λ y . a) b] .$ Now $FV ((λ y^{'} . a) ((λ y . a) b)) = {a, b}$ , which does not contain $y$ , so Gc applies and Comp does not: Comp would require a substitution immediately inside, and the body is an application. Hence $\overset{G c}{⟶} (λ y^{'} . a) ((λ y . a) b) \overset{B}{⟶} a [y^{'} / (λ y . a) b] \overset{G c}{⟶} a,$ the last step because $y^{'} \notin FV (a) = {a}$ . The divergence of theorem 148.8 is created by the step from $a ⟨ y^{'} : = \dots ⟩ ⟨ y : = \dots ⟩$ to $a ⟨ y^{'} : = \dots ⟨ y : = \dots ⟩ ⟩$ . In $λ ex$ that redex would be Comp at the term $a [y^{'} / (λ y . a) b] [y / (λ y . a) b]$ , and its side condition asks for $y \in FV ((λ y . a) b)$ , a set equal to ${a, b}$ ; the condition fails. ◻

Theorem 148.16 — Imported properties of λ ex ¶

The following hold for $λ ex$ and are imported at the exact signature stated.

Perpetuality. There is a deterministic many-step strategy $⇉$ on terms such that $t ⇉ t^{'}$ implies $t ⟶_{λ ex}^{+} t^{'}$ , and such that $t ⇉ t^{'}$ with $t^{'}$ strongly normalizing implies $t$ strongly normalizing.
Preservation of strong normalization. If a $λ$ -term $t$ is strongly normalizing for $β$ , then $t$ is strongly normalizing for $λ ex$ .
Confluence. The relation $⟶_{λ ex}$ is confluent on metaterms, that is, on terms extended by metavariables carrying a list of delayed substitutions.
Typed strong normalization. Every simply typed $λ ex$ -term is strongly normalizing.

Referenced from 3 locations

Explicit-Substitution Calculi

The proofs are not reproduced. Clause (1) is proved by induction on the strategy and depends on a separate property of the substitution calculus; clause (2) follows from (1) through an inductive characterization of the strongly normalizing terms; clause (3) is proved by exhibiting a superdevelopment map with van Oostrom’s Z-property, and clause (4) by a modular normalization theorem applied to a translation into a calculus with weakening. Locators for all four are in section 148.3. What is proved locally is theorem 148.13, corollary 148.14 and proposition 148.15; these do not depend on clauses (1)–(4), and clauses (1)–(4) are not transferred to $λ σ$ , where (2) is false by theorem 148.8.

Exercise 148.4 ¶

★★☆ Show that Gc is not derivable from the other five rules of definition 148.12: exhibit a term $t [x / u]$ with $x \notin FV (t)$ that is a normal form for ${B, V a r, A p p, L a m b, C o m p}$ modulo $=_{e}$ .

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.5 ¶

★★☆ Drop the side condition $y \in FV (u)$ from Comp and show that the resulting calculus admits the infinite reduction of theorem 148.8, by writing the first four steps in the notation of definition 148.12.

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.6 ¶

★★☆ State and prove the analogue of theorem 148.13 for $λ σ$ : for every term $a$ , $σ (a [b \cdot id])$ is the de Bruijn metasubstitution of $b$ into $a$ . Which theorem of section 148.1 is this?

Referenced from 2 locations

Explicit-Substitution Calculi

Suggested first pass.

Begin with exercise 148.7 and exercise 148.8, then complete exercise 148.11.

Exercise 148.7 ¶

★★☆ Reduce $(λ (λ (2 1))) [a \cdot id]$ to $σ$ -normal form in $λ σ$ , naming every rule. Then perform the same computation with named variables in $λ ex$ and compare the number of steps.

Referenced from 3 locations

Explicit-Substitution Calculi

Exercise 148.8 ¶

★★★ Verify the schedule displayed at the end of the proof of theorem 148.8 by computing the first three transitions $\dots S_{0} S_{1} \dots ⟶ \dots S_{1} S_{2} \dots ⟶ \dots S_{0} S_{2} \dots$ in full, and prove that no expression occurs twice, using the pair $(m, n)$ of indices as a measure.

Referenced from 3 locations

Explicit-Substitution Calculi

Exercise 148.9 ¶

★★☆ Theorem 148.7 is proved for the untyped calculus. Explain why adding the simple typing rules of chapter 2 to $λ σ$ does not by itself repair theorem 148.8, and identify the exact clause of the counterexample that typing would have to exclude.

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.10 ¶

★★★ Compare definition 148.2 with the CwF equations of definition 54.16: match $id$ , $↑$ , $a \cdot s$ and $s \circ t$ with the identity, $p$ , $⟨ γ, a ⟩$ and composition, and identify which of the ten $σ$ rules become CwF equations and which become derived facts. State precisely one $σ$ rule that is an orientation choice with no counterpart in definition 54.16, and say what is lost by orienting it the other way.

Referenced from 2 locations

Explicit-Substitution Calculi

Exercise 148.11 ¶

★★★ Practical project.explicit-substitution-reducer Implement a reducer for both calculi and a divergence detector. The program takes a term in one of two input syntaxes — de Bruijn $λ σ$ expressions over the grammar of definition 148.1, or named-variable $λ ex$ terms over the grammar of definition 148.11 — a rule set, a reduction strategy (leftmost-outermost or a supplied rule order), and a step budget.

Invariant. Every state is a well-formed expression of the declared sort: in $λ σ$ , terms and substitutions are never confused, and every rule instance is applied at a subexpression of the matching sort; in $λ ex$ , the side conditions of Gc and Comp are recomputed from the current free-variable sets at each step and never cached across a rewrite. The program checks the invariant before each step and aborts, printing the offending subexpression, rather than continuing.

Concrete result. The program prints the numbered trace, each line carrying the rule name and the redex position, and terminates with normal form: followed by the expression, or with budget exhausted followed by the last expression and the multiset of rule names used.

Acceptance test. In $λ σ$ , reducing $(λ (2 1)) [a \cdot id]$ with the $σ$ rules must reach a normal form containing no closure other than the codings $1 [↑^{n}]$ , as proposition 148.5 requires. Running the term $M$ of theorem 148.8 in $λ ex$ under the leftmost-outermost strategy must print normal form: a after exactly four steps, with the rule sequence B, Gc, B, Gc, matching proposition 148.15. Finally, run the same $M$ under the rule order that deletes the side condition $y \in FV (u)$ from Comp, removes Gc, and prefers Comp to every congruence step; that is the calculus of (148.1), and the run must print budget exhausted. A run that still reports a normal form under that order has cached a free-variable set instead of recomputing it, or has kept Gc; either is the defect this test detects.

The divergence of theorem 148.8 is one reduction sequence, not every one, so no acceptance clause asks a leftmost-outermost reducer to find it in $λ σ$ : the rule order is part of the input for exactly this reason.

Referenced from 3 locations

Explicit-Substitution Calculi

Sources. Definition 148.1, Definition 148.2, proposition 148.4, proposition 148.5, theorem 148.6 and theorem 148.7 follow M. Abadi, L. Cardelli, P.-L. Curien and J.-J. Lévy, Explicit substitutions, Journal of Functional Programming 1 (1991), 375–416. The de Bruijn discussion and the derivation of Abs are on physical pages 4–7 of the authors’ preprint; the rule table of definition 148.2 is on physical page 12; the simulation statement proved here as theorem 148.6 is their Proposition 3.1 on physical page 13; confluence is their Theorem 3.2 and the termination and confluence of $σ$ their Proposition 3.3, both on physical page 14, the termination being credited there to Hardin and Laville; the normal-form grammar of proposition 148.5 and Hardin’s interpretation method are on physical pages 14–15. Theorem 148.8 is P.-A. Melliès, Typed lambda-calculi with explicit substitutions may not terminate, TLCA 1995, LNCS 902, 328–334 [Mel95]; the simplified form displayed here, together with the schedule and the remark that the original term is the typable $λ x . (λ y . I (I y)) (I x)$ , is Figure 1.2 and Remark 1.2.1 of K. H. Rose, Explicit substitution: tutorial and survey, BRICS Lecture Series LS-96-3, 1996 [Ros96], physical pages 26–28. Definition 148.11, Definition 148.12 are Figure 1 of D. Kesner, A theory of explicit substitutions with safe and full composition, Logical Methods in Computer Science 5(3:1) (2009), 1–29, physical pages 5–6; theorem 148.13 and corollary 148.14 are her full-composition property and Lemma 2.3 on physical page 7; the four imported clauses of theorem 148.16 are her Theorem 3.3 (physical page 7), Theorem 3.6 (physical page 8), Corollary 8.13 (physical page 24) and the typed strong-normalization result of Section 7 (physical page 20). The algebraic reading of the same operators, in which the $σ$ equations become the equations of a category with families rather than rewrite rules, is chapter 54; the telescopic presentation that preceded both is de Bruijn’s.

The 𝜆𝜎λσ-calculus

Composition destroys strong normalization

Safe composition: the 𝜆exλex-calculus

Suggested first pass.

The $λ σ$ -calculus

Safe composition: the $λ ex$ -calculus