Chapter 2Core route

Simple Types, Curry–Howard, Safety, and Normalization

Example 1.79 exhibited a closed term that is not a value and cannot take a step. In the language of booleans and functions, the application $tt ff,$ a constant in function position, has the same two properties. The evaluator can report the failure only after inspecting the application. The first task is therefore to define a finite static check that rejects $tt ff$ before execution and whose answer is preserved by every evaluation step.

A typed language of booleans and functions

Definition 2.1 — Simple types ¶

Fix effective enumerations $P_{0}, P_{1}, \dots$ of atomic type constants and $x_{0}, x_{1}, \dots$ of variables. Equality of two indices, and hence equality of atomic constants and variables, is decidable. We continue to write $P, Q, \dots$ and $x, y, z, \dots$ when their numerical codes are irrelevant. The simple types are the expressions generated by the judgment $A type$ below:

2 type

Ty-Bool

P type

Ty-Atom

A type

B type

A \to B type

Ty-Arr

Equivalently, as a grammar: $A, B ::= P ∣ 2 ∣ A \to B$ . The atomic constants are not type variables and admit no substitution. Types are finite trees whose atomic leaves carry decidable codes, so their constructors are disjoint and injective: $A \to B = A^{'} \to B^{'}$ implies $A = A^{'}$ and $B = B^{'}$ , and an arrow type equals neither $2$ nor an atomic type. Equality of these trees means equality of the root label and, recursively, of the ordered children. Hence an arrow has two uniquely determined children and cannot equal the nullary Boolean constructor. We write $2$ for the two-element Boolean type and its values as $tt$ and $ff$ .

Referenced from 5 locations

Simple Types, Curry–Howard, Safety, and Normalization

The rules already calculate a nontrivial type, the type of two-argument boolean operations:

2 type

Ty-Bool

2 type

Ty-Bool

2 type

Ty-Bool

2 \to 2 type

Ty-Arr

2 \to (2 \to 2) type

Ty-Arr

As usual, $\to$ associates to the right: $2 \to 2 \to 2$ means $2 \to (2 \to 2)$ . In a formation judgment, the whole expression to the left of $type$ is its subject; thus $A \to B type$ means $(A \to B) type$ .

Definition 2.2 — Raw terms ¶

Using the effective variable enumeration fixed above, raw terms are given by the grammar $e ::= x ∣ λ x : A . e ∣ e_{1} e_{2} ∣ tt ∣ ff ∣ if (e; e_{1}; e_{2}),$ where the abstraction $λ x : A . e$ binds $x$ in $e$ and $A$ ranges over the types of definition 2.1. The free variables of a raw term are computed by structural recursion: $\begin{aligned} FV (x) & = {x}, & FV (tt) & = FV (ff) = \emptyset, \\ FV (e_{1} e_{2}) & = FV (e_{1}) \cup FV (e_{2}), & FV (λ x : A . e) & = FV (e) ∖ {x}, \end{aligned}$ and $FV (if (e; e_{1}; e_{2})) = FV (e) \cup FV (e_{1}) \cup FV (e_{2})$ . Write $Names (e)$ for the finite set of every free or bound variable name in $e$ , and $BN (e)$ for its finite set of binder labels, using the constructor-wise clauses of definition 1.50. A term is closed when its free-variable set is empty.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

The binding apparatus of chapter 1 was built for a grammar with one binding constructor: abstraction. It consists of fresh renaming, alpha-equivalence, and capture-avoiding substitution. Every proof proceeds constructor by constructor. For example, renaming in an application recurses in both subterms, while renaming under $λ x : A . e$ first chooses a representative with a fresh binder. Compared with definition 1.50, this grammar drops the arithmetic constructors $0$ , $suc$ , and $add$ , retains $tt$ , $ff$ , and $if$ , and adds a type annotation to the binder. Binding ignores the annotation, and each retained nonbinding constructor recurses in its immediate subterms. These clauses give the six binding consequences recorded next.

Convention 2.3 — Terms, binding, and substitution ¶

Unless “raw term” is stated explicitly, term means an alpha-equivalence class of raw terms, using the size-recursive common-opening definition of definition 1.53. A written raw expression is one representative of that class. We import from that construction, extended constructor-wise to the present grammar:

fresh renaming $e ⟨ y / x ⟩$ on a raw representative, defined when $y \notin Names (e)$ , with its free-variable, size, composition, and commutation equations;
the alpha-invariants: alpha-equivalent terms have the same outer constructor, the same constructor count, the same free variables, and the same binder annotations. In particular, $λ x : A . b =_{α} λ y : B . c$ requires $A = B$ and, for one common fresh $z$ , $b ⟨ z / x ⟩ =_{α} c ⟨ z / y ⟩$ ;
fresh representatives and common opening: for every finite set $X$ , every raw term $e$ has a representative $e_{X}$ with $e =_{α} e_{X}$ , whose binder labels are pairwise distinct and satisfy $BN (e_{X}) \cap X = \emptyset$ ; two alpha-equivalent abstractions have alpha-equivalent bodies after opening with any one name absent from both displayed raw representatives;
a capture-avoiding substitution $e [a / x]$ , well defined on alpha-classes, satisfying $\begin{aligned} x [a / x] & = a, & y [a / x] & = y (y \neq x), \\ tt [a / x] & = tt, & ff [a / x] & = ff, \\ (e_{1} e_{2}) [a / x] & = e_{1} [a / x] e_{2} [a / x], \\ if (e; e_{1}; e_{2}) [a / x] & = if (e [a / x]; \\ e_{1} [a / x]; e_{2} [a / x]), \\ (λ y : B . b) [a / x] & = λ y : B . b [a / x], \\ (λ x : B . b) [a / x] & = λ x : B . b . \end{aligned}$ The penultimate equation assumes $y \neq x$ and $y \notin FV (a)$ . The same clause carries the free-variable equation: if $x \in FV (e)$ then $FV (e [a / x]) = (FV (e) ∖ {x}) \cup FV (a),$ and $e [a / x] = e$ when $x \notin FV (e)$ ;
substitution by a fresh variable agrees with fresh renaming: if $z \notin FV (e)$ , choose a representative of $e$ whose binders are fresh for $z$ ; then $e [z / x] = e ⟨ z / x ⟩$ .
fresh renaming can be cancelled: if $x \neq z$ and $z \notin Names (e)$ , then $e ⟨ z / x ⟩ [x / z] = e .$ Indeed, the fresh-opening cancellation lemma of lemma 1.63, specialized to the variable $x$ , gives the left side as $e [x / x]$ ; substitution clause (B4) makes the latter term $e$ .

Here $=_{α}$ compares raw representatives, while ordinary equality compares their alpha-classes. Every term constructor obeys one of two substitution clauses: substitution is componentwise at a nonbinding argument, while a binding argument uses the fresh-binder clause (B4). Each extension of the term grammar states which arguments bind. Typing judgments have alpha-classes as subjects. A rule instance may use any representative whose binders are fresh for the terms being substituted; changing only those bound names changes neither the judgment nor its derivation. An algorithm recurses on one such raw representative and returns a judgment about its alpha-class.

Referenced from 12 locations

Two calculations show the convention at work. Substitution passes through $if$ componentwise, $if (x; ff; x) [tt / x] = if (tt; ff; tt),$ while a binder equal to a free variable of the inserted term must first be freshened: for distinct $x, y, z$ , $(λ y : 2 . x) [y / x] \overset{f r e s h e n b i n d e r}{=} (λ z : 2 . x) [y / x] \overset{s u b s t i t u t i o n c l a u s e}{=} λ z : 2 . y .$ Textual replacement without the renaming would produce $λ y : 2 . y$ and capture the inserted variable.

Exercise 2.1 ¶

★☆☆ Let $x, y, z$ be distinct. Compute $(λ y : 2 . if (x; y; x)) [if (y; tt; ff) / x]$ after alpha-renaming its binder fresh for the substituend, and mark every free occurrence of $y$ in the result. Then compute $(λ x : 2 . x) [tt / x]$ and explain, from the equations of convention 2.3, why the answer is not $λ x : 2 . tt$ .

Referenced from 3 locations

Definition 2.4 — Contexts ¶

The judgment $Γ ctx$ is inductively defined by

\cdot ctx

Cx-Emp

Γ ctx

A type

x \notin dom (Γ)

Γ, x : A ctx

Cx-Ext

The symbol $\cdot$ denotes the empty context. A context is an ordered list of distinct declarations; $Γ, x : A$ appends one declaration, and $Γ_{1}, Γ_{2}$ denotes list concatenation when the domains are disjoint. Thus an insertion between two declarations has a definite place, and the declaration introduced for a lambda body is the final one. We write $dom (Γ)$ for the set of variables $Γ$ declares and $(x : A) \in Γ$ for the occurrence of the declaration $x : A$ in $Γ$ . Whenever we write $Γ, x : A$ , the side condition $x \notin dom (Γ)$ is understood; in particular a context never declares a variable twice. A well-formed context $Γ^{'}$ is a declaration-preserving extension of $Γ$ when it is obtained from $Γ$ by finitely many insertions of fresh declarations, without changing the order or type of any declaration already present. Zero insertions give reflexivity, and concatenating insertion sequences gives transitivity. If $Γ^{'}$ extends $Γ$ and $x \notin dom (Γ^{'})$ , then $Γ^{'}, x : A$ extends $Γ, x : A$ : perform the same insertions before the common final declaration.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

For example, $x : 2, f : 2 \to 2$ is a context. The freshness formulas printed above bars in this tree are metalevel checks on rule instances, not new judgment forms; the layout merely keeps each check beside the premise it restricts.

\cdot ctx

Cx-Emp

2 type

x \notin \emptyset

x : 2 ctx

Cx-Ext

2 \to 2 type

f \neq x

x : 2, f : 2 \to 2 ctx

Cx-Ext

Definition 2.5 — Typing ¶

The typing judgment $Γ ⊢ e : A$ , for $Γ ctx$ and $A type$ , is inductively defined by

(x : A) \in Γ

Γ ⊢ x : A

Var

Γ ⊢ tt : 2

True

Γ ⊢ ff : 2

False

Γ ⊢ e : 2

Γ ⊢ e_{1} : C

Γ ⊢ e_{2} : C

Γ ⊢ if (e; e_{1}; e_{2}) : C

Γ, x : A ⊢ e : B

Γ ⊢ λ x : A . e : A \to B

Lam

Γ ⊢ e_{1} : A \to B

Γ ⊢ e_{2} : A

Γ ⊢ e_{1} e_{2} : B

App

Rule instances range only over well-formed contexts and displayed types. In Lam, context formation requires $x \notin dom (Γ)$ . Context membership and binder freshness are metalevel side conditions, not additional judgment forms. The premise of If types both branches by the same $C$ because either branch may be the result. When the context is empty, we may abbreviate $\cdot ⊢ e : A$ by $⊢ e : A$ ; these are the same judgment.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

The typing rules are the static counterpart of the evaluator: they inspect a program constructor by constructor without running it. We type the two boolean programs that will serve as test inputs throughout the chapter.

Example 2.6 — Negation ¶

Let $not : = λ x : 2 . if (x; ff; tt)$ . Then $\cdot ⊢ not : 2 \to 2$ :

(x : 2) \in x : 2

x : 2 ⊢ x : 2

Var

x : 2 ⊢ ff : 2

False

x : 2 ⊢ tt : 2

True

x : 2 ⊢ if (x; ff; tt) : 2

\cdot ⊢ λ x : 2 . if (x; ff; tt) : 2 \to 2

Lam

Referenced from 5 locations

Example 2.7 — Conjunction ¶

Let $and : = λ x : 2 . λ y : 2 . if (x; y; ff)$ and $Γ : = x : 2, y : 2$ . Reading upward, each abstraction extends the context by one declaration:

(x : 2) \in Γ

Γ ⊢ x : 2

Var

(y : 2) \in Γ

Γ ⊢ y : 2

Var

Γ ⊢ ff : 2

False

Γ ⊢ if (x; y; ff) : 2

x : 2 ⊢ λ y : 2 . if (x; y; ff) : 2 \to 2

Lam

\cdot ⊢ and : 2 \to 2 \to 2

Lam

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Exercise 2.2 ¶

★★☆ Define $or : = λ x : 2 . λ y : 2 . if (x; tt; y)$ and exhibit its full typing derivation at $2 \to 2 \to 2$ , labeling every node with its rule. Then write a term $xor$ of the same type whose $if$ has another $if$ in one branch, and type it.

Referenced from 3 locations

We can now carry out the calculation promised at the head of the chapter: the search for a typing of the stuck term fails, and the failure is located at one specific premise. Any derivation of $\cdot ⊢ tt ff : C$ would have to end

\cdot ⊢ tt : A \to C

\cdot ⊢ ff : A

\cdot ⊢ tt ff : C

App

for some type $A$ . The right premise is derivable, with $A = 2$ , by False. The left premise is not derivable for any $A$ : it demands an arrow type for $tt$ , and the only rule that concludes a typing of the subject $tt$ assigns it $2$ .

Proposition 2.8 — The stuck term is untypable ¶

There are no $Γ$ , $C$ for which $Γ ⊢ tt ff : C$ is derivable.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Proposition 2.8 — The stuck term is untypable

Proof. We inspect final rules, as in chapter 1. The subjects of the six typing rules have pairwise distinct outer constructors—a variable, an abstraction, an application, the two constants, and $if$ —and by (B2) of convention 2.3 alpha-equivalence preserves the outer constructor. A derivation of $Γ ⊢ tt ff : C$ therefore ends with App, whose first premise is $Γ ⊢ tt : A \to C$ for some $A$ . A derivation of that premise must end with the only rule whose subject is $tt$ , namely True, whose conclusion type is $2$ . Since types are finite trees (definition 2.1), $2 \neq A \to C$ . So no derivation exists. ◻

The rejection required no execution: it is a finite failed search through rule instances. The search terminates here because the syntax determines the only possible final typing rule, and every recursive premise concerns a strict subterm. Thus final-rule inspection rejects the term without running it.

Exercise 2.3 ¶

★☆☆ Show by final-rule inspection that neither term $if (λ x : 2 . x; tt; ff) ff (λ x : 2 . x)$ is typable in any context. For the conditional, locate the premise of If that fails. For the application, locate the premise of App that fails.

Referenced from 3 locations

Renaming, weakening, and substitution

The typing rules contain no rule that inserts an unused declaration and no rule that replaces a variable by a term. Both operations are forced on us by the safety proof: when a $β$ -step replaces a bound variable by an argument, the type of the contractum is computed by substituting one derivation into another, and substitution in turn needs weakening. We prove that both are admissible rules in the sense of chapter 1. Renaming comes first because it repairs a name collision that weakening creates.

Here is the collision. Suppose a typing derivation ends in $\frac{Γ, z : B_{1} ⊢ b : B_{2}}{Γ ⊢ λ z : B_{1} . b : B_{1} \to B_{2}} Lam$ To insert $x : A$ into $Γ$ , we would like to insert it into the premise as well. If the displayed binder happens to be $z = x$ , the proposed context declares $x$ twice. We must first rename the binder. Renaming preserves the conclusion and does not increase derivation height. Weakening can therefore recurse on the smaller renamed premise even though it is not a literal subtree of the original derivation. We formalize this with complete induction on derivation height $h (D)$ (chapter 1).

In a ground instance, let $x \neq y$ and start from $x : 2 ⊢ λ y : 2 . x : 2 \to 2$ , and try to rename $x$ to $y$ . The captured term $λ y : 2 . y$ is wrong. Choose $z \notin {x, y}$ and first represent the subject as $λ z : 2 . x$ ; renaming then gives $y : 2 ⊢ λ z : 2 . y : 2 \to 2 .$ This two-stage calculation is the abstraction case of lemma 2.9.

Lemma 2.9 — Renaming ¶

Suppose $D :: Γ_{1}, x : A, Γ_{2} ⊢ e : B$ with $h (D) = h$ , and let $x^{'}$ be a variable with $x^{'} \neq x$ and $x^{'} \notin dom (Γ_{1}) \cup dom (Γ_{2}) \cup FV (e)$ . Then $Γ_{1}, x^{'} : A, Γ_{2} ⊢ e [x^{'} / x] : B$ has a derivation of height at most $h$ .

Referenced from 7 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.9 — Renaming

Proof. By complete induction on $h$ , with cases on the final rule of $D$ .

Case Var: $e = y$ with $(y : B) \in Γ_{1}, x : A, Γ_{2}$ . If $y = x$ , then $B = A$ because contexts declare distinct variables, $e [x^{'} / x] = x^{'}$ , and Var concludes $Γ_{1}, x^{'} : A, Γ_{2} ⊢ x^{'} : A$ . If $y \neq x$ , then $(y : B)$ occurs in $Γ_{1}$ or $Γ_{2}$ , $e [x^{'} / x] = y$ , and Var applies unchanged.

Cases True, False: the subject is a constant, unchanged by substitution, and the same axiom applies in the renamed context.

Case Lam: $e = λ z : B_{1} . b$ and $B = B_{1} \to B_{2}$ , with premise $D^{'} :: Γ_{1}, x : A, Γ_{2}, z : B_{1} ⊢ b : B_{2}$ of height $h - 1$ ; by context formation in the premise, $z \notin dom (Γ_{1}) \cup {x} \cup dom (Γ_{2})$ .

If $z \neq x^{'}$ , the inductive hypothesis applies to $D^{'}$ , renaming $x$ to $x^{'}$ ; here $x^{'} \notin FV (b)$ because $x^{'} \notin FV (e) = FV (b) ∖ {z}$ and $x^{'} \neq z$ . It yields $Γ_{1}, x^{'} : A, Γ_{2}, z : B_{1} ⊢ b [x^{'} / x] : B_{2}$ at height at most $h - 1$ , and Lam concludes, with $λ z : B_{1} . b [x^{'} / x] = (λ z : B_{1} . b) [x^{'} / x]$ by the abstraction equation of convention 2.3 ( $z \neq x$ , $z \neq x^{'}$ ).

If $z = x^{'}$ , choose $z^{″}$ outside $dom (Γ_{1}) \cup dom (Γ_{2}) \cup {x, x^{'}}$ and outside the finite set of all variable names occurring in $b$ . Two uses of the inductive hypothesis, both on derivations of height at most $h - 1$ , transform the premise: $\begin{aligned} Γ_{1}, x : A, Γ_{2}, z : B_{1} & ⊢ b : B_{2} \\ ⟹ Γ_{1}, x : A, Γ_{2}, z^{″} : B_{1} ⊢ b [z^{″} / z] : B_{2} \\ ⟹ Γ_{1}, x^{'} : A, Γ_{2}, z^{″} : B_{1} ⊢ b [z^{″} / z] [x^{'} / x] : B_{2} . \end{aligned}$ The first use freshens the binder. For the second, recall that $x^{'} = z$ : by the free-variable equation in substitution clause (B4), $FV (b [z^{″} / z]) \subseteq (FV (b) ∖ {z}) \cup {z^{″}}$ , so $x^{'} = z$ is not free in the renamed body, and the remaining freshness conditions follow from the choice of $z^{″}$ and context formation. Rule Lam now concludes with subject $λ z^{″} : B_{1} . b [z^{″} / z] [x^{'} / x]$ . To identify this subject with $(λ z : B_{1} . b) [x^{'} / x]$ : by fresh-substitution clause (B5) the substitution $b [z^{″} / z]$ is the fresh renaming $b ⟨ z^{″} / z ⟩$ , so the common-opening clause (B3) gives $λ z : B_{1} . b = λ z^{″} : B_{1} . b ⟨ z^{″} / z ⟩$ as terms; substituting $x^{'}$ for $x$ on both displays—the right display is clean, since $z^{″} \notin {x, x^{'}}$ and $z^{″} \notin FV (x^{'})$ —and using the abstraction equation of substitution clause (B4) on the right yields exactly the displayed subject.

Cases If, App: apply the inductive hypothesis to every premise derivation, each of height at most $h - 1$ and with the same decomposition of the context, and re-apply the rule. Substitution commutes with both constructors by substitution clause (B4), so the re-applied rule has the required subject $e [x^{'} / x]$ . ◻

Exercise 2.4 ¶

★★☆ Carry out lemma 2.9 on the derivation of $x : 2 ⊢ if (x; x; ff) : 2$ , renaming $x$ to $y$ : display the resulting derivation node by node. Then apply the lemma to the premise of example 2.6 with $x^{'} =$ a fresh $u$ and confirm that the conclusion of Lam denotes the same alpha-class as the original abstraction, even though its premise is displayed with binder $u$ .

Referenced from 3 locations

Corollary 2.10 — Opening an abstraction ¶

Suppose $Γ ⊢ λ x : A . b : C$ is derivable, and choose $z$ distinct from $x$ , outside $dom (Γ)$ , and occurring nowhere in $b$ . Then $C = A \to B$ for some $B$ , and $Γ, z : A ⊢ b ⟨ z / x ⟩ : B$ is derivable. Thus the typing of an abstraction does not depend on the bound name used to display it.

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Corollary 2.10 — Opening an abstraction

Proof. The final rule must be Lam, since by alpha-invariance clause (B2) alpha-equivalence preserves the outer constructor and the annotation. The derivation may, however, end with another display $λ y : A . c$ of the same term, giving a premise $Γ, y : A ⊢ c : B$ and the conclusion type $A \to B$ . We cannot assume the requested $z$ fresh for the hidden body $c$ . Choose $w$ outside the finite set ${x, y, z} \cup dom (Γ) \cup Names (b) \cup Names (c)$ .

Renaming the premise from $y$ to $w$ (lemma 2.9) gives $Γ, w : A ⊢ c [w / y] : B$ , and $c [w / y] = c ⟨ w / y ⟩$ by fresh-substitution clause (B5). Common-opening clause (B3), applied to the equality of terms $λ x : A . b = λ y : A . c$ , gives $c ⟨ w / y ⟩ = b ⟨ w / x ⟩$ . Now rename once more, from $w$ to $z$ : the target $z$ is absent from the opened body because it is absent from $b$ and distinct from $w$ , so lemma 2.9 and fresh-substitution clause (B5) give $Γ, z : A ⊢ b ⟨ w / x ⟩ ⟨ z / w ⟩ : B,$ and the fresh-renaming composition equation (B1) computes $b ⟨ w / x ⟩ ⟨ z / w ⟩ = b ⟨ z / x ⟩ .$ ◻

Corollary 2.11 — Typing respects alpha-equivalence ¶

If raw terms $e$ and $e^{'}$ are alpha-equivalent, then $Γ ⊢ e : A$ is derivable if and only if $Γ ⊢ e^{'} : A$ is. Moreover the premise derivations of two displays of one abstraction can be opened with a single common fresh binder.

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Corollary 2.11 — Typing respects alpha-equivalence

Proof. The subjects denote the same term under convention 2.3, so the same derivation tree serves for both; the second assertion is corollary 2.10 applied to each display, followed by the common-opening clause (B3) of the two premise subjects. ◻

Convention 2.12 — Fresh binders in displays ¶

By the fresh-representative clause (B3) and corollary 2.11, every statement and proof uses representatives whose bound names are mutually distinct, absent from the variables declared in the ambient contexts, and absent from the free variables of the other terms under discussion, except when a collision is itself the object of the calculation.

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Lemma 2.13 — Scope ¶

If $Γ ⊢ e : A$ , then $FV (e) \subseteq dom (Γ)$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.13 — Scope

Proof. By induction on the displayed typing derivation. The Var case is context membership. Constants have no free variables. The application and conditional cases follow by taking unions and applying the induction hypotheses. In the abstraction case the induction hypothesis gives $FV (b) \subseteq dom (Γ) \cup {x}$ ; deleting the bound name $x$ leaves $FV (λ x : A . b) \subseteq dom (Γ)$ . ◻

Weakening permits insertion at any well-formed position in a context.

Lemma 2.14 — Weakening ¶

Suppose $Γ_{1}, Γ_{2} ⊢ e : B$ and $Γ_{1}, x : A, Γ_{2} ctx$ . Then $Γ_{1}, x : A, Γ_{2} ⊢ e : B .$

Referenced from 5 locations

Proof of Lemma 2.14 — Weakening

Proof. Use complete induction on the height of the given typing derivation. The variable case follows because the original declaration remains in $Γ_{1}, x : A, Γ_{2}$ . Constants require no premises. For App and If, weaken each premise and reapply its final rule.

Suppose the last rule is $\frac{Γ_{1}, Γ_{2}, z : C ⊢ b : D}{Γ_{1}, Γ_{2} ⊢ λ z : C . b : C \to D} Lam .$ Choose $w$ outside the finite set $FV (b) \cup dom (Γ_{1}, x : A, Γ_{2}) \cup {z}$ . By convention 2.12, lemma 2.9, alpha-renaming the binder transports the premise, without increasing its height, to $Γ_{1}, Γ_{2}, w : C ⊢ b ⟨ w / z ⟩ : D .$ The induction hypothesis inserts $x : A$ before $Γ_{2}$ in this smaller premise. Rule Lam yields $λ w : C . b ⟨ w / z ⟩ : C \to D$ under the enlarged context; this term is alpha-equivalent to the displayed conclusion. ◻

Corollary 2.15 — Weakening by a telescope ¶

If $Γ ⊢ e : B$ and $Γ, Δ ctx$ , then $Γ, Δ ⊢ e : B$ .

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Corollary 2.15 — Weakening by a telescope

Proof. Induct on the length of $Δ$ , applying lemma 2.14 at the end of the context at each step. ◻

Theorem 2.16 — Substitution ¶

Suppose $Γ_{1}, x : A, Γ_{2} ⊢ e : B and Γ_{1}, Γ_{2} ⊢ a : A .$ Then $Γ_{1}, Γ_{2} ⊢ e [a / x] : B$ .

Referenced from 3 locations

Proof of Theorem 2.16 — Substitution

Proof. Induct on the first derivation, keeping the displayed context split in the induction assertion. In the Var case the subject is a variable $y$ . If $y = x$ , context uniqueness gives $B = A$ , and the second hypothesis is the desired conclusion. If $y \neq x$ , then $(y : B)$ remains in $Γ_{1}, Γ_{2}$ , substitution leaves $y$ unchanged, and Var applies. The constants are unchanged. The App and If cases follow by applying the induction hypotheses to all premises and rebuilding the final rule.

For Lam, use convention 2.12 to write its subject as $λ y : C . b$ with $y \neq x$ and $y \notin FV (a)$ . Its premise is $Γ_{1}, x : A, Γ_{2}, y : C ⊢ b : D .$ Weakening the second hypothesis at the end gives $Γ_{1}, Γ_{2}, y : C ⊢ a : A$ . The induction hypothesis, with $Γ_{2}, y : C$ as the right part of the split, gives $Γ_{1}, Γ_{2}, y : C ⊢ b [a / x] : D$ . Rule Lam concludes $Γ_{1}, Γ_{2} ⊢ λ y : C . b [a / x] : C \to D .$ Substitution clause (B4) gives $λ y : C . b [a / x] =_{α} (λ y : C . b) [a / x],$ so the derived subject is the required substitution. ◻

Example 2.17 — Substituting a derivation ¶

Let $b = if (x; ff; tt)$ and $a = if (tt; ff; tt)$ . We have $x : 2 ⊢ b : 2$ and $⊢ a : 2$ . Substitution therefore derives $\cdot ⊢ if (if (tt; ff; tt); ff; tt) : 2 .$ At the unique Var leaf for $x$ , the entire derivation of $a$ is inserted; all other rule nodes are copied. Thus substitution on terms is the visible trace of substitution on derivation trees.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Exercise 2.5 ¶

★★☆ Write the two premise derivations and the resulting derivation tree for $(λ y : 2 . if (x; y; ff)) [if (tt; ff; tt) / x] .$ Point to the weakening step used to type the inserted term under $y : 2$ .

Referenced from 3 locations

Reading typing derivations backward

The structural lemmas transform derivations. Safety also requires information in the opposite direction: the outer form of a term tells us what the final rule of any typing derivation must have been.

Lemma 2.18 — Inversion ¶

The following implications hold.

If $Γ ⊢ x : A$ , then $(x : A) \in Γ$ .
If $Γ ⊢ λ x : C . b : A$ , then $A = C \to D$ for some $D$ . For every $z$ outside the finite set $dom (Γ) \cup FV (b) \cup {x}$ , $Γ, z : C ⊢ b ⟨ z / x ⟩ : D$ .
If $Γ ⊢ e_{1} e_{2} : B$ , then for some $A$ , $Γ ⊢ e_{1} : A \to B$ and $Γ ⊢ e_{2} : A$ .
If $Γ ⊢ if (e; e_{1}; e_{2}) : C$ , then $Γ ⊢ e : 2$ and $Γ ⊢ e_{1} : C$ and $Γ ⊢ e_{2} : C$ .
If $Γ ⊢ tt : A$ or $Γ ⊢ ff : A$ , then $A = 2$ .

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.18 — Inversion

Proof. Inspect the final rule. By the alpha-invariants (B2), its subject has the same outer constructor as the displayed subject, so exactly the matching typing rule is possible. Read off that rule’s premises and result type. The abstraction premise is put under the requested displayed binder by corollary 2.10. ◻

Lemma 2.19 — Uniqueness of types ¶

If $Γ ⊢ e : A$ and $Γ ⊢ e : B$ , then $A = B$ .

Referenced from 4 locations

Proof of Lemma 2.19 — Uniqueness of types

Proof. Use complete induction on the constructor count of a representative of $e$ whose binders are fresh for $Γ$ , using lemma 2.18 on both derivations. A variable has one declaration in a well-formed context. Both constants have type $2$ . For an abstraction, inversion gives $A = C \to A^{'}$ and $B = C \to B^{'}$ and two typings of the same opened body; the induction hypothesis gives $A^{'} = B^{'}$ . For an application, inversion gives $Γ ⊢ e_{1} : C \to A$ and $Γ ⊢ e_{1} : D \to B$ ; the induction hypothesis for $e_{1}$ gives $C \to A = D \to B$ , hence $A = B$ by injectivity of the arrow constructor. For a conditional, either branch has both result types, so its induction hypothesis gives $A = B$ . ◻

Proposition 2.20 — Type synthesis ¶

There is an algorithm which, given a finite well-formed context $Γ$ and a finite raw representative $e$ , either returns the unique type of its alpha-class and a derivation of $Γ ⊢ e : A$ , or correctly reports that no such type exists.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Proposition 2.20 — Type synthesis

Proof. First clean the input’s binders from $dom (Γ)$ , processing sibling subterms from left to right as in lemma 1.56. At each binder choose the least variable code outside the ambient avoidance set, the names of its body, and the old binder; after cleaning a subterm, add its new binder names to the avoidance set used for later siblings. The effective enumeration and decidable equality make every such finite-set choice deterministic. Recurse on the cleaned syntax. A variable succeeds exactly when it has a context declaration. The constants return $2$ . For $λ x : A . b$ , first check $A type$ and synthesize $B$ for $b$ under $Γ, x : A$ ; return $A \to B$ . For $e_{1} e_{2}$ , synthesize both types, require the first to be $A \to B$ and the second to equal $A$ , and return $B$ . For a conditional, require the guard’s synthesized type to be $2$ and the two branch types to be equal; return their common type. Every recursive call is on an immediate subterm, so structural recursion on the finite raw input terminates. Context membership is decidable because a context is a finite list with decidable variable equality. Type equality is decidable by recursion on the two finite type trees, using decidable equality of their atomic codes.

Each successful clause builds the corresponding typing rule, proving soundness. Conversely, lemma 2.18 says that any derivation has exactly the premises tested by its constructor’s clause; structural induction on $e$ therefore proves completeness. Uniqueness is lemma 2.19. Finally, let $e_{1}$ and $e_{2}$ be two raw representatives of the same term. Soundness makes every successful result a typing of their common alpha-class, and completeness makes success or failure the same for both. When both succeed, uniqueness gives the same result type. Thus the returned judgment is independent of the supplied representative, although its displayed derivation may use the deterministic cleaned names. ◻

Dynamics and safety

The evaluator is call-by-value. Function position is evaluated before argument position; a beta-redex fires only when its argument is a value.

Definition 2.21 — Values and one-step evaluation ¶

Values, the completed results of evaluation, and the one-step relation $e ⟼ e^{'}$ are generated by $v ::= tt ∣ ff ∣ λ x : A . e$ and the rules

e_{1} ⟼ e_{1}^{'}

e_{1} e_{2} ⟼ e_{1}^{'} e_{2}

E-AppL

v_{1} value

e_{2} ⟼ e_{2}^{'}

v_{1} e_{2} ⟼ v_{1} e_{2}^{'}

E-AppR

v value

(λ x : A . b) v ⟼ b [v / x]

E-Beta

e ⟼ e^{'}

if (e; e_{1}; e_{2}) ⟼ if (e^{'}; e_{1}; e_{2})

E-If

if (tt; e_{1}; e_{2}) ⟼ e_{1}

E-True

if (ff; e_{1}; e_{2}) ⟼ e_{2}

E-False

The many-step relation is generated by

e ⟼^{*} e

M-Refl

e ⟼ e_{1}

e_{1} ⟼^{*} e_{2}

e ⟼^{*} e_{2}

M-Step

Here $v$ ranges over the displayed value grammar, and $v value$ is the corresponding grammar-membership judgment. Writing that premise explicitly in both E-AppR and E-Beta avoids making the evaluation order depend on a metavariable letter. After erasing lambda annotations, this presentation is equivalent to the boolean-and-function part of the value rules of definition 1.61; the numeral alternatives were removed with the arithmetic fragment at the chapter boundary. We use the shorter grammar because it has only three alternatives. In the Boolean-and-function fragment, E-AppL and E-AppR restrict chapter 1’s E-App-L and E-App-R; E-True and E-False restrict E-If-T and E-If-F. Likewise, $v value$ restricts that chapter’s $v val$ to functions and booleans.

Referenced from 4 locations

For example, with $not$ from example 2.6, $not (if (ff; ff; tt)) \overset{E - F a l s e / E - A p p R}{⟼} not tt \overset{E - B e t a}{⟼} if (tt; ff; tt) \overset{E - T r u e}{⟼} ff .$ The value restriction on E-Beta fixes this order.

Lemma 2.22 — Canonical forms ¶

Let $v$ be a closed value.

If $\cdot ⊢ v : 2$ , then $v$ is $tt$ or $ff$ .
If $\cdot ⊢ v : A \to B$ , then $v = λ x : A . b$ for some $x, b$ .

Referenced from 3 locations

Proof of Lemma 2.22 — Canonical forms

Proof. There are three value forms. Inversion assigns $2$ to the two constants and an arrow type to an abstraction. Disjointness of the type constructors excludes the other forms in each clause; arrow injectivity equates the abstraction’s domain annotation with the displayed domain in the second. ◻

Theorem 2.23 — Preservation ¶

If $Γ ⊢ e : A$ and $e ⟼ e^{'}$ , then $Γ ⊢ e^{'} : A$ .

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Theorem 2.23 — Preservation

Proof. Induct on the evaluation derivation.

For E-AppL, inversion of the typing of $e_{1} e_{2}$ gives $Γ ⊢ e_{1} : B \to A$ and $Γ ⊢ e_{2} : B$ . Apply the induction hypothesis to the first premise and rebuild App. The E-AppR case is the same with the second premise.

For E-Beta, inversion first gives $Γ ⊢ λ x : B . b : B \to A$ and $Γ ⊢ v : B$ ; abstraction inversion gives $Γ, x : B ⊢ b : A$ . The substitution theorem yields $Γ ⊢ b [v / x] : A$ .

For E-If, inversion gives $Γ ⊢ e : 2$ , $Γ ⊢ b : A$ , and $Γ ⊢ c : A$ ; apply the induction hypothesis to the guard and rebuild If. In the E-True and E-False cases, inversion says respectively that the selected first or second branch already has the result type. ◻

Theorem 2.24 — Progress ¶

If $\cdot ⊢ e : A$ , then either $e$ is a value or there exists $e^{'}$ with $e ⟼ e^{'}$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Theorem 2.24 — Progress

Proof. Induct on the typing derivation with the property “if its context is empty, then its subject is a value or takes a step.” Variables cannot occur when the context is empty. Constants and abstractions are values; in particular, the Lam case does not use its induction hypothesis because an abstraction is already a value. For an application $e_{1} e_{2}$ , the induction hypothesis for $e_{1}$ either gives an E-AppL step or says $e_{1}$ is a value. In the latter case, the induction hypothesis for $e_{2}$ either gives an E-AppR step or says $e_{2}$ is a value. By lemma 2.13, the typing in the empty context makes $e_{1}$ closed. Now $e_{1}$ is a closed value of arrow type, so canonical forms writes it as an abstraction; E-Beta applies.

For $if (e; e_{1}; e_{2})$ , a step of $e$ gives E-If. Otherwise $e$ is a closed value of type $2$ , hence is $tt$ or $ff$ by canonical forms, and E-True or E-False applies. ◻

Corollary 2.25 — Type safety ¶

If $\cdot ⊢ e : A$ and $e ⟼^{*} e^{'}$ , then $e^{'}$ is not stuck. Equivalently, it is a value or it can take another step.

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Corollary 2.25 — Type safety

Proof. First prove by induction on the displayed many-step derivation the strengthened assertion $\cdot ⊢ e : A \land e ⟼^{*} e^{'} ⟹ \cdot ⊢ e^{'} : A .$ The M-Refl case uses the given typing. In the M-Step case, preservation types the one-step target, and the induction hypothesis types the final endpoint. Progress applied to $\cdot ⊢ e^{'} : A$ gives the result. ◻

Safety says that evaluation does not go wrong. It does not yet say that evaluation ends. A well-typed language can be safe and still contain a well-typed looping construct; normalization will require a different proof.

Exercise 2.6 ¶

★★☆ Write the complete preservation proof for the three conditional evaluation rules as three displayed derivation transformations. In the congruence case show every premise of the rebuilt If rule.

Referenced from 3 locations

Products, sums, truth, and falsity

Functions and booleans suffice to state safety, but they cannot package two results, distinguish two alternatives carrying different payload types, or express a type with exactly one or no constructor values. We therefore add four type constructors. A product packages two results; a sum marks which of two alternatives was chosen; $1$ has one canonical inhabitant, meaning one constructor value of that type; and $0$ has none. A term of a type is also called an inhabitant of it. Rules that build a value of a connective are its introduction rules; rules that inspect or use such a value are its elimination rules.

Definition 2.26 — The propositional extension ¶

Extend types and terms by $A, B ::= \dots ∣ A \times B, e ::= \dots ∣ (e_{1}, e_{2}) ∣ fst (e) ∣ snd (e) .$ The formation, introduction, and elimination rules are

A type

B type

A \times B type

Ty-Prod

Γ ⊢ e_{1} : A

Γ ⊢ e_{2} : B

Γ ⊢ (e_{1}, e_{2}) : A \times B

Pair

Γ ⊢ e : A \times B

Γ ⊢ fst (e) : A

Fst

Γ ⊢ e : A \times B

Γ ⊢ snd (e) : B

Snd

A pair is a value exactly when both components are values. Its left-to-right evaluation and the two projection contractions are generated by

e_{1} ⟼ e_{1}^{'}

(e_{1}, e_{2}) ⟼ (e_{1}^{'}, e_{2})

E-PairL

v_{1} value

e_{2} ⟼ e_{2}^{'}

(v_{1}, e_{2}) ⟼ (v_{1}, e_{2}^{'})

E-PairR

e ⟼ e^{'}

fst (e) ⟼ fst (e^{'})

E-Fst

v_{1} value

v_{2} value

fst ((v_{1}, v_{2})) ⟼ v_{1}

E-Fst-Pair

e ⟼ e^{'}

snd (e) ⟼ snd (e^{'})

E-Snd

v_{1} value

v_{2} value

snd ((v_{1}, v_{2})) ⟼ v_{2}

E-Snd-Pair

Fresh renaming is componentwise, and substitution satisfies $\begin{aligned} (e_{1}, e_{2}) [a / z] & = (e_{1} [a / z], e_{2} [a / z]), & fst (e) [a / z] & = fst (e [a / z]), \\ snd (e) [a / z] & = snd (e [a / z]) . \end{aligned}$ The name and binder-label sets take unions over the displayed arguments. The equation $(fst (p), snd (p)) = p$ would remove a pair constructor placed immediately around the two projections of $p$ . Such an equation is called a product eta contraction; it is not a reduction rule of this calculus.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

The term inspected by a projection is its scrutinee. The first projection computes immediately, while one with a variable scrutinee remains stuck: $fst ((tt, ff)) \overset{E - F s t - P a i r}{⟼} tt, fst (x) has no step.$

Example 2.27 — A product program ¶

The term ${swap}_{A, B} : = λ p : A \times B . (snd (p), fst (p))$ has type $(A \times B) \to (B \times A)$ . The body derivation is

(p : A \times B) \in (p : A \times B)

p : A \times B ⊢ p : A \times B

Var

p : A \times B ⊢ snd (p) : B

Snd

(p : A \times B) \in (p : A \times B)

p : A \times B ⊢ p : A \times B

Var

p : A \times B ⊢ fst (p) : A

Fst

p : A \times B ⊢ (snd (p), fst (p)) : B \times A

Pair

One application of Lam derives the advertised type.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Definition 2.28 — Sum types ¶

Extend types and terms by $\begin{aligned} A, B & ::= \dots ∣ A + B, \\ e & ::= \dots ∣ inl (e) ∣ inr (e) ∣ case (e; x . e_{1}; y . e_{2}) . \end{aligned}$ The notation $x . e_{1}$ marks $x$ as bound in the left branch body, and $y . e_{2}$ marks $y$ as bound in the right branch body. The formation, introduction, and elimination rules are

A type

B type

A + B type

Ty-Sum

Γ ⊢ e : A

B type

Γ ⊢ inl (e) : A + B

Inl

A type

Γ ⊢ e : B

Γ ⊢ inr (e) : A + B

Inr

Γ ⊢ e : A + B

Γ, x : A ⊢ e_{1} : C

Γ, y : B ⊢ e_{2} : C

Γ ⊢ case (e; x . e_{1}; y . e_{2}) : C

Case

The unused summand is printed as a formation premise in each introduction rule because the payload cannot determine it. A left or right injection is a value exactly when its payload is a value. Evaluation uses

e ⟼ e^{'}

inl (e) ⟼ inl (e^{'})

E-Inl

e ⟼ e^{'}

inr (e) ⟼ inr (e^{'})

E-Inr

e ⟼ e^{'}

case (e; x . e_{1}; y . e_{2}) ⟼ case (e^{'}; x . e_{1}; y . e_{2})

E-Case

v value

case (inl (v); x . e_{1}; y . e_{2}) ⟼ e_{1} [v / x]

E-Case-L

v value

case (inr (v); x . e_{1}; y . e_{2}) ⟼ e_{2} [v / y]

E-Case-R

Fresh renaming and substitution are componentwise on injections. For a case, choose $x^{'}$ and then $y^{'}$ outside $Names (a) \cup Names (e_{1}) \cup Names (e_{2}) \cup {x, y, z},$ with $x^{'} \neq y^{'}$ . Rename the two branch binders independently and define $\begin{aligned} case (e; x . e_{1}; y . e_{2}) [a / z] \\ = case (e [a / z]; x^{'} . e_{1} [x^{'} / x] [a / z]; y^{'} . e_{2} [y^{'} / y] [a / z]) . \end{aligned}$ Two permitted choices give the same alpha-class. Open both left branches at one common fresh name and both right branches at a second common fresh name. Structural induction on the two branch bodies identifies the opened results; the definition of alpha-equivalence for each binding argument then identifies the two case terms. Thus this definition is independent of the displayed branch labels. For name bookkeeping, $Names (case (e; x . e_{1}; y . e_{2}))$ is the union of the three body name sets with ${x, y}$ ; its binder-label set adds $x, y$ to the three body binder-label sets. Injections retain the two sets of their payloads.

Referenced from 6 locations

Simple Types, Curry–Howard, Safety, and Normalization

Example 2.28 — Eliminating a sum ¶

For arbitrary types $A, B$ , define ${tag}_{A, B} : = λ s : A + B . case (s; x . tt; y . ff) .$ The two branch derivations use True and False under their extended contexts, so Case types the body by $2$ and Lam gives ${tag}_{A, B} : (A + B) \to 2$ . This is a genuine elimination: the program is allowed to inspect which introduction rule built its argument. The body derivation is

s : A + B \in s : A + B

s : A + B ⊢ s : A + B

Var

s : A + B, x : A ⊢ tt : 2

True

s : A + B, y : B ⊢ ff : 2

False

s : A + B ⊢ case (s; x . tt; y . ff) : 2

Case

For values $a : A$ and $b : B$ , the two computation clauses are visible in the complete traces $\begin{aligned} {tag}_{A, B} inl (a) & ⟼ case (inl (a); x . tt; y . ff) ⟼ tt, \\ {tag}_{A, B} inr (b) & ⟼ case (inr (b); x . tt; y . ff) ⟼ ff . \end{aligned}$

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Definition 2.30 — Unit ¶

Extend types by $1$ , terms by $⋆$ , and the rules by

1 type

Ty-Unit

Γ ⊢ ⋆ : 1

Unit-I

The constructor $⋆$ is a value and substitution leaves it fixed. The name and binder-label sets of $⋆$ are empty. The display itself is a complete constructor derivation in every well-formed context. By final-rule inspection, every closed value of type $1$ is $⋆$ ; Unit has no eliminator or root contraction in this calculus.

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Exercise 2.7 ¶

★☆☆ Let $Γ = x : A$ be well formed. Display the derivation of $Γ ⊢ ⋆ : 1$ , and use final-rule inspection to show that a closed value $v : 1$ cannot be a lambda, Boolean, pair, or injection.

Referenced from 3 locations

Definition 2.31 — Void ¶

Extend types by $0$ , terms by ${abort}_{C} (e)$ , and the rules by

0 type

Ty-Empty

Γ ⊢ e : 0

C type

Γ ⊢ {abort}_{C} (e) : C

Empty-E

e ⟼ e^{'}

{abort}_{C} (e) ⟼ {abort}_{C} (e^{'})

E-Abort

The result annotation makes the eliminator syntax directed. There is no Void constructor, no value of type $0$ , and no root contraction for $abort$ . The following open stuck term has the exact derivation

(x : 0) \in (x : 0)

x : 0 ⊢ x : 0

Var

2 type

x : 0 ⊢ {abort}_{2} (x) : 2

Empty-E

It is not a value and cannot step because its variable argument cannot step. Substitution satisfies ${abort}_{C} (e) [a / z] = {abort}_{C} (e [a / z])$ . Abort retains the name and binder-label sets of its argument.

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Exercise 2.8 ¶

★☆☆ For a formed type $A$ , derive $x : 0, y : A ⊢ {abort}_{A \times 2} (x) : A \times 2$ . Explain from the displayed dynamics why the open term has neither a root step nor value status.

Referenced from 3 locations

Finite algebraic data now require no new metatheory. For instance, set $\begin{aligned} Color & : = 1 + (1 + 1), & red & : = inl (⋆), \\ amber & : = inr (inl (⋆)), & green & : = inr (inr (⋆)) . \end{aligned}$ A three-way case analysis is two nested Case rules. Thus a finite list of constructors is represented by a nested sum of copies of $1$ ; a constructor with several fields uses a product in its summand.

Exercise 2.7 ¶

★★☆ Write $next : Color \to Color$ sending red to green, green to amber, and amber to red. Give its typing derivation and calculate the reductions of $next red$ , $next amber$ , and $next green$ to constructor values.

Referenced from 3 locations

Definition 2.32 — Injection-free terms ¶

The injection-free terms are generated recursively by $\begin{aligned} i ::= & x ∣ λ x : A . i ∣ i_{1} i_{2} ∣ tt ∣ ff ∣ if (i_{0}; i_{1}; i_{2}) \\ ∣ (i_{1}, i_{2}) ∣ fst (i) ∣ snd (i) ∣ ⋆ ∣ case (i_{0}; x . i_{1}; y . i_{2}) ∣ {abort}_{A} (i) . \end{aligned}$ Thus neither $inl (e)$ nor $inr (e)$ may occur at any depth. In particular, a lambda is injection free exactly when its body is injection free, and a case is injection free exactly when its scrutinee and both branch bodies are injection free.

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proposition 2.29 — Structural metatheory survives the extension ¶

For the extended grammar the following statements hold.

If $Γ ⊢ e : A$ , then $FV (e) \subseteq dom (Γ)$ .
If $Γ ⊢ e : A$ and $Γ^{'}$ is a declaration-preserving extension of $Γ$ , then $Γ^{'} ⊢ e : A$ .
If $Γ_{1}, z : D, Γ_{2} ⊢ e : A$ and $Γ_{1}, Γ_{2} ⊢ a : D,$ then $Γ_{1}, Γ_{2} ⊢ e [a / z] : A .$
Typing inversion has exactly the premises displayed in definition 2.26, definition 2.28, definition 2.30, definition 2.31; for Case, inversion gives a type $A + B$ for the scrutinee and branch typings at the same $C$ under $x : A$ and $y : B$ .
Types are unique and synthesis is defined for the injection-free terms of definition 2.32. Given an expected type $A + B$ , checking $inl (e)$ reduces to checking $e$ at $A$ , and checking $inr (e)$ reduces to checking $e$ at $B$ .

Uniqueness and synthesis do not extend to unannotated injections: $⊢ inl (tt) : 2 + 1 and ⊢ inl (tt) : 2 + 0 .$ An injection can instead be checked against a given sum type.

Referenced from 4 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Proposition 2.29 — Structural metatheory survives the extension

Proof. For item 1, induction on typing adds eight rule families. Pair takes the union of the two induction-hypothesis inclusions; projections, injections, and abort retain the inclusion of their premise; Unit-I has empty free-variable set. For Case, the induction hypotheses give $FV (e) \subseteq dom (Γ), FV (e_{1}) ∖ {x} \subseteq dom (Γ), FV (e_{2}) ∖ {y} \subseteq dom (Γ),$ which is precisely the free-variable clause for the case expression.

For item 2, first prove the one-insertion assertion $Γ_{1}, Γ_{2} ⊢ e : A ⟹ Γ_{1}, w : E, Γ_{2} ⊢ e : A$ whenever the enlarged context is well formed. Induct on the displayed extended typing derivation while retaining the insertion position $Γ_{1} ∣ Γ_{2}$ . A variable keeps its declaration. The two Boolean constants and Unit-I have no term premises. Rules App and If, and every nonbinding added constructor, receive the induction hypothesis at each term premise and are rebuilt by their typing rules.

For Lam, display the binder $x$ fresh for the enlarged context. If the last rule is $\frac{Γ_{1}, Γ_{2}, x : B ⊢ e_{0} : C}{Γ_{1}, Γ_{2} ⊢ λ x : B . e_{0} : B \to C} Lam,$ the induction hypothesis with right suffix $Γ_{2}, x : B$ gives $Γ_{1}, w : E, Γ_{2}, x : B ⊢ e_{0} : C .$ Rule Lam then gives $Γ_{1}, w : E, Γ_{2} ⊢ λ x : B . e_{0} : B \to C .$ For Case, display both branch binders fresh for the enlarged context. Apply the induction hypothesis to the scrutinee at the original split, to the left branch at right suffix $Γ_{2}, x : B$ , and to the right branch at right suffix $Γ_{2}, y : C$ ; then rebuild Case. This proves one insertion for every extended rule. Induction on the finite insertion sequence proves item 2.

For item 3, induct on the first derivation while retaining the arbitrary split $Γ_{1}, z : D, Γ_{2}$ . In the variable case, the subject is $z$ , or its declaration remains in $Γ_{1}, Γ_{2}$ . Constants are unchanged. Every nonbinding constructor receives the induction hypothesis at each term premise and is rebuilt by the same typing rule.

For Lam, display its binder $x$ outside $FV (a) \cup dom (Γ_{1}, z : D, Γ_{2})$ . Its last rule is $\frac{Γ_{1}, z : D, Γ_{2}, x : B ⊢ e_{0} : C}{Γ_{1}, z : D, Γ_{2} ⊢ λ x : B . e_{0} : B \to C} Lam .$ Item 2 types $a$ under $Γ_{1}, Γ_{2}, x : B$ ; the induction hypothesis with right suffix $Γ_{2}, x : B$ gives the premise of $\frac{Γ_{1}, Γ_{2}, x : B ⊢ e_{0} [a / z] : C}{Γ_{1}, Γ_{2} ⊢ λ x : B . e_{0} [a / z] : B \to C} Lam .$ Because $x \notin FV (a)$ , the right conclusion is the substitution of the left conclusion.

For Case, display distinct binders $x, y$ outside the same set and each other. The final rule has the form $\frac{\begin{matrix} Γ_{1}, z : D, Γ_{2} ⊢ s : B + C \\ Γ_{1}, z : D, Γ_{2}, x : B ⊢ e_{1} : F \\ Γ_{1}, z : D, Γ_{2}, y : C ⊢ e_{2} : F \end{matrix}}{Γ_{1}, z : D, Γ_{2} ⊢ case (s; x . e_{1}; y . e_{2}) : F} Case .$ Item 2 types $a$ under both branch contexts without $z : D$ . The three induction hypotheses, using right suffixes $Γ_{2}$ , $Γ_{2}, x : B$ , and $Γ_{2}, y : C$ , give $Γ_{1}, Γ_{2} ⊢ case (s [a / z]; x . e_{1} [a / z]; y . e_{2} [a / z]) : F .$ Because $x, y \notin FV (a)$ , this subject is the capture-avoiding substitution specified in definition 2.28.

For item 4, inspect the final rule. Outer constructors are disjoint, so a pair ends only in Pair, a projection in its corresponding projection rule, a unit term in Unit-I, an injection in its corresponding introduction, a case in Case, and an abort in Empty-E. Reading the premises gives the asserted clauses, including the formed unused summand of an injection and the formed result type of abort.

For uniqueness in item 5, induct on the first typing derivation and invert the second. Pair uses both induction hypotheses and injectivity of $\times$ . Fst and Snd use uniqueness of the premise product, then its selected component. Case uses uniqueness on the scrutinee to identify the summands and on a branch to identify the common result type. Unit-I has result $1$ , while Empty-E obtains its result from the syntax annotation ${abort}_{C}$ . For synthesis, recurse on the grammar of definition 2.32. Each constructor uses the corresponding inversion clause: a case first synthesizes a sum type for its scrutinee and then synthesizes both branches in the contexts determined by those summands. Because the grammar excludes injections at every depth, no recursive call encounters an introduction whose unused summand is unknown.

For an injection, however, its payload determines only one summand. The two displayed judgments are derived by Inl with different choices of the unused summand, so their result types are unequal. Thus there is no unique type for a synthesis algorithm to return. If checking starts with expected type $A + B$ , inversion of Inl says exactly that its payload checks at $A$ ; rebuilding Inl, with formed type $B$ , proves soundness. Inversion and rebuilding Inr give the corresponding equivalence at $B$ . In either case the conclusion retains both summands, although the payload determines only the selected one. ◻

Definition 2.30 — Extended values and computation ¶

The extended value judgment is generated by the three core value rules and the four additional forms $⋆$ , $(v_{1}, v_{2})$ , $inl (v)$ , and $inr (v)$ , with the displayed components required to be values. The extended step relation is generated by the core rules together with the six product rules of definition 2.26, five sum rules of definition 2.28, and the abort congruence of definition 2.31: exactly twelve new rules. These rules evaluate constructor arguments from left to right. More generally, an eliminator inspects its scrutinee to select an elimination clause. Abort has no root contraction.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

The same stuck boundary holds for a case whose scrutinee is a variable: the open term has no step until a value injection is substituted for that variable.

Lemma 2.35 — Extended canonical forms ¶

If $v$ is a closed well-typed value, then $\begin{array}{cc} type of v & form of v \\ A \times B & (v_{1}, v_{2}) with \cdot ⊢ v_{1} : A and \cdot ⊢ v_{2} : B \\ A + B & inl (v_{1}) with \cdot ⊢ v_{1} : A, or inr (v_{2}) with \cdot ⊢ v_{2} : B \\ 1 & ⋆ \\ 0 & no form. \end{array}$

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.35 — Extended canonical forms

Proof. Inspect the four extended value forms and invert their typing derivations. Disjointness of $\times, +, 1, 0$ removes all rows except the one named by the result type. By product and sum inversion, the payloads have the displayed types. No value-typing rule concludes at $0$ , proving the last row. ◻

Theorem 2.31 — Safety for the propositional extension ¶

The extended language satisfies preservation and progress. Consequently, the type-safety conclusion of corollary 2.25 remains valid.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Theorem 2.31 — Safety for the propositional extension

Proof. For preservation, induct on the displayed evaluation step. The congruence rules E-PairL and E-PairR invert Pair, apply the induction hypothesis to the changed component, and rebuild Pair; the value premise of E-PairR is retained. Rules E-Fst, E-Snd, E-Inl, E-Inr, and E-Abort perform the same three operations with their respective typing rules. E-Case inverts Case, changes only the scrutinee premise by the induction hypothesis, and rebuilds Case with the two unchanged branch premises.

For E-Fst-Pair, inversion first gives $Γ ⊢ (v_{1}, v_{2}) : A \times B$ and then $Γ ⊢ v_{1} : A$ , the type of the reduct. The E-Snd-Pair case uses the second premise of the same Pair inversion and concludes $Γ ⊢ v_{2} : B$ . For E-Case-L, inversion of the source typing gives $Γ ⊢ inl (v) : A + B, Γ, x : A ⊢ e_{1} : C, Γ, y : B ⊢ e_{2} : C .$ Inverting the first judgment gives $Γ ⊢ v : A$ ; substitution gives $Γ ⊢ e_{1} [v / x] : C$ . For E-Case-R, inversion instead gives $Γ ⊢ v : B$ and the right branch $Γ, y : B ⊢ e_{2} : C$ ; substitution concludes $Γ ⊢ e_{2} [v / y] : C$ . These are all twelve new rules.

For progress, induct on the typing derivation. In Pair, apply the left induction hypothesis; a step gives E-PairL. If the left component is a value, apply the right hypothesis; a step gives E-PairR, and two values make the pair a value. In Inl and Inr, a payload step lifts by the corresponding congruence rule and a payload value makes an injection value. The unit introduction is a value.

For Fst and Snd, a scrutinee step lifts by the matching congruence rule. Otherwise the scrutinee is a closed product value, so lemma 2.35 makes it a pair of values and the matching projection contraction applies. In Case, a scrutinee step gives E-Case; otherwise the closed sum value is a left or right injection by extended canonical forms, so E-Case-L or E-Case-R applies. In Empty-E, the scrutinee induction hypothesis gives a step or a value. The first lifts by E-Abort; the second contradicts the $0$ row of extended canonical forms. The core typing rules retain the proof of theorem 2.24.

Finally, induction on a many-step derivation iterates preservation; progress at the endpoint proves the stated safety conclusion. ◻

Exercise 2.8 ¶

★★☆ Prove preservation for the right sum contraction, showing the inversion and substitution derivations explicitly. Then prove the congruence case in which the scrutinee of a case expression takes a step.

Referenced from 3 locations

Call-by-value and call-by-name

Typing does not choose an evaluation order. Our safety theorem used call-by-value because E-AppR evaluates the argument and E-Beta requires a value. To see the alternative without overloading the typed metatheory, return briefly to the untyped lambda terms of chapter 1.

Definition 2.32 — Call-by-name ¶

Call-by-name evaluation uses contexts $F ::= [-] ∣ F e ∣ if (F; e_{1}; e_{2})$ and contracts $(λ x . b) a$ to $b [a / x]$ without first evaluating $a$ . Boolean case contractions are unchanged. Write $⟼_{n}$ for this relation and $⟼_{v}$ for the call-by-value relation of definition 2.21 after the structural erasure $\begin{aligned} erase (x) & = x, \\ erase (λ x : A . b) & = λ x . erase (b), \\ erase (e_{1} e_{2}) & = erase (e_{1}) erase (e_{2}), \end{aligned}$ extended identically through booleans and conditionals. Thus both relations act on the same erased Boolean-and-function grammar.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

On the terminating term $t : = (λ x . tt) ((λ y . y) ff)$ the two strategies reveal their order: $\begin{array}{rcl} t & ⟼_{v} (λ x . tt) ff ⟼_{v} tt, \\ t & ⟼_{n} tt . \end{array}$ Call-by-name does not evaluate an argument that the body discards.

Now let $Ω : = (λ z . z z) (λ z . z z) .$ This is the application $ω ω$ from exercise 1.17, where the earlier lowercase $ω = λ x . x x$ named only the abstraction; uppercase $Ω$ names the complete looping application. Its unique beta contraction reproduces $Ω$ . Consequently $(λ x . tt) Ω ⟼_{n} tt, (λ x . tt) Ω ⟼_{v} (λ x . tt) Ω ⟼_{v} \dots .$ The source term is not typable in the simply typed lambda calculus (STLC): typing $z z$ would require the type of $z$ to be both an arrow and its own domain. Thus the example separates evaluation strategies outside the language to which the safety theorem applies.

Exercise 2.9 ¶

★★☆ Calculate both strategies on $(λ x . x x) ((λ y . y) tt)$ until a value or a stuck term is reached. Then suppose the self-applied variable $x$ had a simple type $X$ . Use the application rule to derive the two incompatible requirements $X = D \to C$ and $X = D$ , and explain why no finite simple type satisfies them. No annotations need be invented for the untyped trace.

Referenced from 3 locations

Propositions as types, derivations as programs

A propositional letter $P$ is an atomic formula. The propositional formulas used here are generated by $F ::= P ∣ ⊤ ∣ ⊥ ∣ F \land F ∣ F \lor F ∣ F \Rightarrow F .$ Suppose $f : A \to B$ , $g : B \to C$ , and $a : A$ are typed terms. Two applications form the term $g (f a) : C$ . Replacing each type arrow by the formula connective $\Rightarrow$ turns those two applications into two uses of implication elimination: first derive $B$ from $f : A \Rightarrow B$ and $a : A$ , then derive $C$ from $g : B \Rightarrow C$ and that result. The problem is whether every proof rule admits such a term decoration and whether erasing the terms recovers the proof.

The Curry–Howard translation fixes propositional letters $P, Q, \dots$ as atomic types and maps these formulas by $\begin{array}{ccccccc} formula & P & ⊤ & ⊥ & A \land B & A \lor B & A \Rightarrow B \\ type & P & 1 & 0 & A \times B & A + B & A \to B . \end{array}$ These are the atomic types fixed in definition 2.1; no grammar extension occurs here. An assumption $A$ is given a label $h$ , written $h : A$ . These names are proof labels, not terms in the formula language; translation turns them into term variables.

Definition 2.38 — Intuitionistic propositional natural deduction ¶

A judgment $Δ ⊢_{N} A$ says that $A$ follows from the finite list $Δ$ of named assumptions. Assumption labels in this list are distinct; accordingly $Δ, h : A$ in a rule premise requires $h \notin dom (Δ)$ , and the two labels introduced by $\lor E$ are also distinct from each other. The system is intuitionistic: each judgment has exactly one conclusion, and it has no independent rule asserting either excluded middle, the formula $A \lor (A \Rightarrow ⊥)$ or double-negation elimination, the formula $((A \Rightarrow ⊥) \Rightarrow ⊥) \Rightarrow A .$ Its rules are

(h : A) \in Δ

Δ ⊢_{N} A

Hyp

Δ ⊢_{N} ⊤

→p I

Δ ⊢_{N} ⊥

Δ ⊢_{N} C

Δ ⊢_{N} A

Δ ⊢_{N} B

Δ ⊢_{N} A \land B

Δ ⊢_{N} A \land B

Δ ⊢_{N} A

E_1

Δ ⊢_{N} A \land B

Δ ⊢_{N} B

E_2

Δ, h : A ⊢_{N} B

Δ ⊢_{N} A \Rightarrow B

Δ ⊢_{N} A \Rightarrow B

Δ ⊢_{N} A

Δ ⊢_{N} B

Δ ⊢_{N} A

Δ ⊢_{N} A \lor B

I_1

Δ ⊢_{N} B

Δ ⊢_{N} A \lor B

I_2

Δ ⊢_{N} A \lor B

Δ, h : A ⊢_{N} C

Δ, k : B ⊢_{N} C

Δ ⊢_{N} C

The letters I and E abbreviate introduction and elimination. In $\Rightarrow I$ , the assumption $h : A$ is open in the premise and discharged in the conclusion: the conclusion no longer depends on it. The two branch assumptions of $\lor E$ are likewise local and discharged at the rule.

Referenced from 4 locations

The motivating calculation is now a derivation in the displayed system: $\frac{g : B \Rightarrow C \frac{f : A \Rightarrow B a : A}{B}}{C} .$ Decorating its assumption leaves by variables and its two $\Rightarrow E$ nodes by application produces the term $g (f a)$ .

Proposition 2.33 — Natural deduction is typing ¶

For intuitionistic natural deduction with implication, conjunction, disjunction, truth, and falsity, every introduction or elimination rule is respectively one of the typing rules in this table: $\begin{array}{ccc} connective & introduction & elimination \\ \Rightarrow & L a m & A p p \\ \land & P a i r & F s t, S n d \\ \lor & I n l, I n r & C a s e \\ ⊤ & U n i t - I & none \\ ⊥ & none & E m p t y - E \end{array}$ Translation of a derivation of $Δ ⊢_{N} A$ using only Hyp and the displayed connective rules produces a term $e$ . Here every formula in $Δ$ is a formed type, and each assumption label is used as the corresponding term variable, so the named-assumption list is a well-formed typing context. The translation produces a derivation $Δ ⊢ e : A$ ; conversely, erasing terms from a typing derivation generated by the corresponding rules, after erasing lambda annotations, produces a natural-deduction derivation of $Δ ⊢_{N} A$ . Let the logical skeleton of a typing derivation be the tree obtained by deleting the type-formation premises printed by Inl, Inr, and Empty-E, then replacing each remaining typing rule by the corresponding natural-deduction rule. Starting with a natural-deduction derivation and erasing its decoration recovers that derivation exactly. Starting with a typing derivation recovers its term up to alpha-equivalence and its logical skeleton exactly. The full typing tree has extra formation premises and therefore is not literally the same tree.

Referenced from 5 locations

Proof of Proposition 2.33 — Natural deduction is typing

Proof. For a natural-deduction derivation $D$ , write $T (D)$ for its term decoration. For a typing derivation $T$ , write $E (T)$ for its erasure.

At an introduction rule, $T$ uses the assumption label as the bound term variable. Induct on the derivation in either direction. We display the two cases that discharge hypotheses or combine alternatives.

Implication introduction transforms $\frac{Δ, h : A ⊢_{N} B}{Δ ⊢_{N} A \Rightarrow B} into \frac{Δ, x : A ⊢ b : B}{Δ ⊢ λ x : A . b : A \to B} Lam .$ Here choose $x = h$ ; the term variable therefore records exactly the logical assumption label that was discharged. A preliminary alpha-renaming makes the label fresh for the surrounding context when necessary.

Disjunction elimination transforms $\frac{\begin{matrix} Δ ⊢_{N} A \lor B \\ Δ, h : A ⊢_{N} C \\ Δ, k : B ⊢_{N} C \end{matrix}}{Δ ⊢_{N} C}$ into Case; its two branch binders record the two temporary assumptions. The product, arrow, unit, and assumption rules agree premise for premise with their displayed typing rules. For $\lor I_{1}$ , translation inserts the formed-type premise for the unused right summand; $\lor I_{2}$ inserts the corresponding left premise. For $⊥ E$ , translation inserts formation of the chosen result type. Skeleton erasure deletes precisely these premises. In the reverse direction, the outer term constructor fixes the final typing rule, and skeleton erasure yields the logical rule with the same logical premises.

The same induction proves the two round trips: $\begin{aligned} E (T (D)) & = D, \\ term (T (E (T))) & =_{α} term (T), \\ skel (T (E (T))) & = skel (T) . \end{aligned}$ For the first equation, every case reapplies the same logical rule to the inductively identical logical premises; erasure deletes the three kinds of inserted formation premise. For the second, every nonbinding case reapplies the same term constructor to alpha-equivalent premises. At $\Rightarrow I$ , erasure records the lambda binder as the discharged assumption label, and translation reuses it; changing the preliminary fresh representative changes only that binder name. The two branch binders of $\lor E$ are each recorded by erasure as the label discharged in that branch, and translation reuses each recorded label. Changing either fresh representative therefore alpha-renames only its own branch binder. These are all binding cases. At injection and empty-elimination nodes, canonical rebuilding may choose a different derivation of the same type-formation judgment, but skeleton erasure deletes it. This proves exactly the displayed claims about the second round trip. ◻

Exercise 2.10 ¶

★★☆ Give both a natural-deduction tree and a typing derivation for $(A \Rightarrow B) \Rightarrow (B \Rightarrow C) \Rightarrow (A \Rightarrow C) .$ Then erase the term labels from your typing derivation and verify node by node that the original natural-deduction tree is recovered.

Referenced from 3 locations

Example 2.34 — Commutativity of conjunction ¶

The natural-deduction proof of $A \land B \Rightarrow B \land A$ is represented by the already typed program ${swap}_{A, B}$ . Here are the two trees node for node: $\frac{\frac{\begin{matrix} \frac{\frac{p : A \land B \in p : A \land B}{p : A \land B ⊢_{N} A \land B} Hyp}{p : A \land B ⊢_{N} B} E_{2} \\ \frac{\frac{p : A \land B \in p : A \land B}{p : A \land B ⊢_{N} A \land B} Hyp}{p : A \land B ⊢_{N} A} E_{1} \end{matrix}}{p : A \land B ⊢_{N} B \land A} I}{\cdot ⊢_{N} (A \land B) \Rightarrow (B \land A)} I$ and $\frac{\frac{\begin{matrix} \frac{\frac{p : A \times B \in p : A \times B}{p : A \times B ⊢ p : A \times B} Var}{p : A \times B ⊢ snd (p) : B} Snd \\ \frac{\frac{p : A \times B \in p : A \times B}{p : A \times B ⊢ p : A \times B} Var}{p : A \times B ⊢ fst (p) : A} Fst \end{matrix}}{p : A \times B ⊢ (snd (p), fst (p)) : B \times A} Pair}{\cdot ⊢ λ p : A \times B . (snd (p), fst (p)) : (A \times B) \to (B \times A)} Lam .$ Erasing terms and reading the connectives through the table gives the first tree exactly.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

Example 2.35 — Distributing implication over alternatives ¶

The formula $(A \Rightarrow C) \land (B \Rightarrow C) \Rightarrow (A \lor B \Rightarrow C)$ has proof term $λ p : (A \to C) \times (B \to C) . λ s : A + B . case (s; x . fst (p) x; y . snd (p) y) .$ In the left branch, Fst derives a proof of $A \Rightarrow C$ , which App applies to the temporary proof $x : A$ . In the right branch, Snd derives $B \Rightarrow C$ and App applies it to $y : B$ . The common branch type is $C$ , exactly the side condition of disjunction elimination.

Referenced from 4 locations

Proof reduction and subject reduction

Evaluation models a machine strategy. Proof reduction has a different purpose: it removes an introduction immediately followed by its matching elimination, wherever that detour occurs in a proof. It therefore reduces under lambdas and in both branches of a case.

Definition 2.36 — Compatible proof reduction ¶

The root relation $r ⇝_{p} q$ consists of $\begin{array}{rcl} (λ x : A . b) a & ⇝_{p} & b [a / x], \\ fst ((a, b)) & ⇝_{p} & a, \\ snd ((a, b)) & ⇝_{p} & b, \\ case (inl (a); x . b; y . c) & ⇝_{p} & b [a / x], \\ case (inr (a); x . b; y . c) & ⇝_{p} & c [a / y], \\ if (tt; b; c) & ⇝_{p} & b, \\ if (ff; b; c) & ⇝_{p} & c . \end{array}$ A proof context is a term with one hole, generated by $\begin{aligned} K ::= & [-] ∣ λ x : A . K ∣ K e ∣ e K \\ ∣ if (K; e_{1}; e_{2}) ∣ if (e; K; e_{2}) ∣ if (e; e_{1}; K) \\ ∣ (K, e) ∣ (e, K) ∣ fst (K) ∣ snd (K) \\ ∣ inl (K) ∣ inr (K) ∣ case (K; x . e_{1}; y . e_{2}) \\ ∣ case (e; x . K; y . e_{2}) ∣ case (e; x . e_{1}; y . K) ∣ {abort}_{A} (K) . \end{aligned}$ Plugging is capture-permitting at the displayed hole: $K [e]$ denotes the literal replacement of the hole by $e$ . Bound names in $K$ are chosen fresh for the root step before plugging, which makes the construction well-defined on alpha-classes. The one-step relation has the single closure rule $\frac{r ⇝_{p} q}{K [r] ⟶_{p} K [q]} P - Ctx .$ Thus the grammar explicitly includes lambda bodies, both application positions, all three conditional positions, both pair components, every unary constructor, the case scrutinee, and both case branches. Write $⟶_{p}^{*}$ for reflexive transitive closure.

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof reduction can contract below a binder where call-by-value evaluation cannot enter: $λ x : 2 . (λ y : 2 . y) x \overset{b e t a, c o m p a t i b l e c l o s u r e}{⟶_{p}} λ x : 2 . x .$

Theorem 2.37 — Subject reduction ¶

If $Γ ⊢ e : A$ and $e ⟶_{p} e^{'}$ , then $Γ ⊢ e^{'} : A$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Theorem 2.37 — Subject reduction

Proof. First type each of the seven root contractions. The beta contraction is item 3 of proposition 2.29. The two projection contractions follow by two inversions of the typing derivation of the projection: the premise pair has type $B \times C$ , so its selected component already has the required type.

For the left sum contraction, inversion gives $Γ ⊢ a : B$ and $Γ, x : B ⊢ b : A$ ; item 3 of proposition 2.29 gives $Γ ⊢ b [a / x] : A$ . For the right contraction, interchange the two summands and branch binders in that derivation: inversion gives $Γ ⊢ a : C$ and $Γ, y : C ⊢ c : A$ , so the same extended substitution result gives $Γ ⊢ c [a / y] : A$ . This interchange preserves the common branch result type. Conditional inversion says both branches already have the result type, so selecting either preserves it. These cases exhaust the root relation.

Now induct on the grammar of the proof context $K$ . The hole case is the root result. For $λ x : A . K$ , invert Lam, apply the induction hypothesis under $Γ, x : A$ , and rebuild Lam. For $K e$ and $e K$ , invert App, change respectively its function or argument premise, and rebuild App. The three conditional contexts change the guard, first branch, or second branch premise of If; the two pair contexts change the corresponding premise of Pair. Each unary context for a projection, injection, or abort changes its unique term premise and rebuilds the same rule. Finally, the three case contexts change respectively the scrutinee premise, the left branch under $x : B$ , or the right branch under $y : C$ , and rebuild Case. These alternatives are exactly the context grammar, so $Γ ⊢ K [q] : A$ follows from $Γ ⊢ K [r] : A$ in every case. ◻

Corollary 2.44 — Many-step subject reduction ¶

If $Γ ⊢ e : A$ and $e ⟶_{p}^{*} e^{'}$ , then $Γ ⊢ e^{'} : A$ .

Referenced from 5 locations

Proof of Corollary 2.44 — Many-step subject reduction

Proof. Induct on the many-step derivation. Reflexivity preserves the given typing. At a step followed by a tail, apply theorem 2.37 to the first step and the induction hypothesis to the tail. ◻

The beta step above does not require its argument to be a value. Thus proof reduction includes every machine beta step but is not itself the evaluator. Its normal forms are proofs without local introduction–elimination detours.

Exercise 2.11 ¶

★★☆ Reduce the proof term of example 2.35 after applying it to $(f, g)$ and then to $inl (a)$ in the context $f : A \to C, g : B \to C, a : A$ . Check the injection against $A + B$ . Label the projection, case, and beta contractions. Use subject reduction to write the common type $C$ after each step.

Referenced from 3 locations

Strong normalization by reducibility

Structural induction on a typing derivation cannot prove termination of an application. Its premises tell us that the function and argument terminate separately, but a terminating function applied to a terminating argument may create a new beta-redex. The missing invariant must say how a term behaves when eliminated at its type. The arrow reducibility candidate requires a function to remain reducible after application to every reducible argument.

Indeed, with $P (Γ ⊢ e : A) : = SN (e)$ , the application case would have only $SN (e_{1}), SN (e_{2}) ⟹̸ SN (e_{1} e_{2}) .$ When $e_{1} = λ x : A . b$ and $e_{2} = v$ , the new reduct is $b [v / x]$ ; it is a subterm of neither premise, so the two induction hypotheses give it no bound. We therefore build a type-indexed family that is closed under elimination. Finite reduction height supports induction on reducts; reduction closure proves reducibility of reducts, and the expansion clause puts a redex back into the candidate once all of its immediate reducts are there. The fundamental lemma places every typed term in the family; its normalization clause gives the desired theorem. The dependency chain is $\begin{matrix} l e m m a 2.47 \\ supports the height inductions in \\ l e m m a 2.40 \\ whose clauses prove \\ \begin{matrix} l e m m a 2.52 \\ l e m m a 2.53 \end{matrix} \\ which discharge the typing cases of \\ t h e o r e m 2.42 \\ whose normalization clause yields \\ t h e o r e m 2.43 . \end{matrix}$ Each vertical phrase states the named use made by the box below it; the display is bookkeeping, not a proof.

Definition 2.38 — Strong normalization and neutral terms ¶

Strong normalization, written $SN (e)$ , is the property that there is no infinite chain $e = e_{0} ⟶_{p} e_{1} ⟶_{p} \dots$ . The introduction forms are $λ x : A . b, tt, ff, ⋆, (a, b), inl (a), inr (b) .$ A neutral term is not an introduction form. Thus a variable and an elimination headed by a variable are neutral, but so is a principal redex such as $(λ x : A . b) a$ . This broader notion is needed for expansion: a principal redex is admitted after all of its immediate reducts have been admitted.

Referenced from 2 locations

Simple Types, Curry–Howard, Safety, and Normalization

The narrower attempt “neutral means variable-headed” would exclude every principal redex. Then the neutral-expansion clause below could not recover $(λ x : A . b) a$ from its contractum, so the beta case of the fundamental lemma would stop at exactly the redex that typing creates.

Convention 2.46 — Finitely branching choice ¶

The normalization proof uses the following classical metatheoretic principle: if a finitely branching rooted tree has nodes at every finite depth, then it has an infinite branch. Equivalently, a finitely branching tree with no infinite branch has a finite height. This is the finitely branching form of König’s lemma; it is the only choice principle used below.

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Lemma 2.47 — Finite reduction height ¶

Every term has finitely many immediate proof reducts. If $SN (e)$ , there is a finite maximum length $ν (e)$ of a reduction beginning at $e$ , and every step $e ⟶_{p} e^{'}$ satisfies $ν (e^{'}) < ν (e)$ .

Referenced from 4 locations

Proof of Lemma 2.47 — Finite reduction height

Proof. Finite branching is structural induction on $e$ . Each constructor has finitely many immediate children, each child has finitely many reducts by induction, and the outer term has at most one additional root contraction.

Now suppose $e$ is strongly normalizing. If its finite reduction tree had branches of unbounded finite length, one of the finitely many first reducts would again have branches of unbounded length. Repeating that choice would construct an infinite reduction, contradicting $SN (e)$ . Hence a maximum branch length $ν (e)$ exists. A step to $e^{'}$ removes the first edge from every continuation, so $ν (e^{'}) < ν (e)$ . The selection of an unbounded successor at each stage is exactly the principle declared in convention 2.46; its contrapositive gives the required bound. ◻

Reducibility is defined for raw, possibly open terms. This is essential: a fresh variable is the test argument which reveals whether a function itself can reduce forever. Typing enters only in the fundamental lemma.

Definition 2.39 — Reducible terms ¶

For every type $A$ , the reducible terms $R_{A}$ are defined by structural recursion on $A$ . At atomic and nullary types, reducibility is strong normalization: $R_{P} = R_{2} = R_{1} = R_{0} = {e ∣ SN (e)} .$ The arrow and product clauses use only their immediate component types: $\begin{aligned} e \in R_{A \to B} & ⟺ for every a \in R_{A}, e a \in R_{B}, \\ e \in R_{A \times B} & ⟺ fst (e) \in R_{A} and snd (e) \in R_{B} . \end{aligned}$ A sum has no single eliminator until a result candidate and two branch bodies have been chosen. Its structural clause records the canonical information that any later case analysis will need. Thus $e \in R_{A + B}$ exactly when $SN (e)$ and both canonical-reduct conditions hold: $\begin{array}{ll} e ⟶_{p}^{*} inl (a) & ⟹ a \in R_{A}, \\ e ⟶_{p}^{*} inr (b) & ⟹ b \in R_{B} . \end{array}$

Referenced from 4 locations

The compound clauses express behavior under elimination. Arrows are tested by application and products by projection; the base clauses impose only strong normalization. The sum clause records the reducibility of every payload reached at an injection.

Every recursive occurrence in this definition is indexed by a proper subexpression of the current type. In particular, the $2$ and $0$ clauses do not quantify over an arbitrary $R_{C}$ ; elimination closure is a property of the completed structurally defined family, not a clause in its definition. The tempting alternative would define the Boolean clause by $e \in R_{2}^{?} ⟺ if (e; b_{1}; b_{2}) \in R_{C} for every type C and b_{1}, b_{2} \in R_{C} .$ Taking $C = 2 \to 2$ already asks for a candidate at a type larger than $2$ while defining the Boolean candidate. This is not structural recursion on the current type. The displayed definition instead uses strong normalization at $2$ and recurses only through proper component types.

The three closure properties below fill each candidate with all of its reducts and with every neutral term whose possible next states are already present. We call the clauses normalization, reduction closure, and neutral expansion, respectively.

Lemma 2.40 — Saturation ¶

For every type $A$ :

if $e \in R_{A}$ , then $SN (e)$ ;
if $e \in R_{A}$ and $e ⟶_{p} e^{'}$ , then $e^{'} \in R_{A}$ ;
if $n$ is neutral and every immediate reduct of $n$ belongs to $R_{A}$ , then $n \in R_{A}$ .

Referenced from 4 locations

Proof of Lemma 2.40 — Saturation

Proof. Induct on the structure of $A$ , proving the clauses in their displayed order at each type.

Base types.

For $P, 2, 1, 0$ , clause 1 is the definition. Clause 2 follows because a reduct of a strongly normalizing term is strongly normalizing. For clause 3, every immediate reduct of $n$ has a well-founded reduction tree. There are finitely many of them, so adjoining the root $n$ gives another well-founded tree.

Arrow types.

Suppose $A = B \to C$ . Any variable $z$ belongs to $R_{B}$ by neutral expansion at the smaller type: it is neutral and the requirement on all of its immediate reducts holds vacuously because it has none. If $e \in R_{B \to C}$ , then $e z \in R_{C}$ , hence $e z$ is strongly normalizing by clause 1 at $C$ . An infinite reduction of $e$ would lift by application congruence to one of $e z$ , proving clause 1 at the arrow. If $e ⟶_{p} e^{'}$ and $a \in R_{B}$ , then $e a ⟶_{p} e^{'} a$ ; clause 2 at $C$ proves $e^{'} a \in R_{C}$ , which proves clause 2 at the arrow.

For neutral expansion at $B \to C$ , fix $a \in R_{B}$ and perform a second, inner induction on $ν (a)$ . The outer induction hypotheses concern the smaller types $B, C$ ; the inner hypothesis concerns arguments of smaller reduction height. The application $n a$ is neutral because an application is not an introduction form. It has no root beta contraction because the neutral term $n$ is not an abstraction. An immediate reduct is $n^{'} a$ , where the hypothesis gives $n^{'} \in R_{B \to C}$ , or $n a^{'}$ , where $ν (a^{'}) < ν (a)$ . Reduction closure at the smaller type $B$ gives $a^{'} \in R_{B}$ . The arrow clause and the induction hypothesis place these two reducts in $R_{C}$ : the arrow clause handles $n^{'} a$ , and the inner height induction, with this membership of $a^{'}$ , handles $n a^{'}$ . Neutral expansion at the smaller type $C$ gives $n a \in R_{C}$ . Since $a$ was arbitrary, $n$ belongs to the arrow candidate.

Product types.

Suppose $A = B \times C$ . If $e$ reduced forever, so would $fst (e)$ ; clause 1 at $B$ therefore proves clause 1 for $e$ . For clause 2, place $e ⟶_{p} e^{'}$ under each projection and use clause 2 at $B$ and $C$ . For clause 3, $fst (n)$ is neutral because $n$ is not a pair. Its immediate reducts are exactly $fst (n^{'})$ for immediate reducts $n^{'}$ of $n$ ; each belongs to $R_{B}$ by the hypothesis and the product clause. Clause 3 at $B$ gives the first projection condition. For the second, replace the smaller target type $B$ by $C$ and the context $fst ([-])$ by $snd ([-])$ . For every immediate reduct $n^{'}$ of $n$ , the product hypothesis gives $snd (n^{'}) \in R_{C}$ ; clause 3 at $C$ therefore gives $snd (n) \in R_{C}$ . Both projection conditions hold, so $n \in R_{B \times C}$ .

Sum types.

Suppose $A = B + C$ . Clause 1 is part of the definition. For clause 2, $e ⟶_{p} e^{'}$ preserves strong normalization; moreover any reduction $e^{'} ⟶_{p}^{*} inl (b)$ extends to one from $e$ , so $b \in R_{B}$ . Exchanging the left and right summands gives the required payload in $R_{C}$ for a reachable right injection.

For clause 3, every immediate reduct $n^{'}$ is in $R_{B + C}$ and hence is strongly normalizing by clause 1 just proved. Finite branching therefore gives $SN (n)$ . If $n ⟶_{p}^{*} inl (b)$ , the path has positive length because $n$ is not an introduction. Its first step reaches some $n^{'} \in R_{B + C}$ , whose canonical-reduct condition gives $b \in R_{B}$ . For a reduction to $inr (c)$ , the same positive-length factorization reaches an immediate $n^{'} \in R_{B + C}$ , whose right canonical-reduct condition gives $c \in R_{C}$ . Thus all parts of the sum definition hold. ◻

Lemma 2.50 — Fresh-renaming invariance ¶

For a term $t$ with $z \notin FV (t)$ , choose a raw representative $\bar{t}$ with $z \notin Names (\bar{t})$ , and define $t ⟨ z / x ⟩$ to be the alpha-class of $\bar{t} ⟨ z / x ⟩$ . This definition is independent of the chosen representative. If $z \notin FV (e) \cup FV (e^{'}) \cup {x}$ , then $e ⟶_{p} e^{'} ⟺ e ⟨ z / x ⟩ ⟶_{p} e^{'} ⟨ z / x ⟩, SN (e) ⟺ SN (e ⟨ z / x ⟩) .$ The same equivalences hold with $⟶_{p}$ replaced by $⟶_{p}^{*}$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.50 — Fresh-renaming invariance

Proof. First, fresh-representative clause (B3) gives the required $\bar{t}$ . Fresh-substitution clause (B5) identifies the alpha-class of its raw renaming with the quotient substitution $t [z / x]$ . Well-definedness of substitution, clause (B4), therefore proves independence of $\bar{t}$ .

For preservation of one step, write it as $K [r] ⟶_{p} K [q]$ and use clause (B3) to choose representatives of the complete source and target whose binders avoid ${x, z}$ . Renaming distributes over the context and over each of the seven root equations. In the beta root, for example, $(b [a / y]) ⟨ z / x ⟩ = b ⟨ z / x ⟩ [a ⟨ z / x ⟩ / y]$ because $y$ was chosen outside ${x, z}$ ; the two case roots use the same equation separately for their branch binders. The other roots are componentwise. For reflection, first choose representatives of the renamed terms whose binders avoid $x$ , then apply preservation to the inverse renaming $z \mapsto x$ . Cancellation clause (B6), once for $e$ and once for $e^{'}$ , says that the two inverse renamings recover the original alpha-classes. Induction on length gives the many-step equivalence. Applying preservation or reflection pointwise to an infinite chain gives an infinite chain on the other side, proving the two directions of strong-normalization invariance. ◻

Lemma 2.51 — Reduction and substitution compatibility ¶

The following hold.

If $b ⟶_{p} b^{'}$ , then $b [a / x] ⟶_{p} b^{'} [a / x]$ .
If $a ⟶_{p} a^{'}$ , then $b [a / x] ⟶_{p}^{*} b [a^{'} / x]$ .
If $x \neq y$ and $y \notin FV (d)$ , then $(b [a / y]) [d / x] = b [d / x] [a [d / x] / y] .$

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.51 — Reduction and substitution compatibility

Proof. Prove item 3 first by structural induction on $b$ . Variables split into $x$ , $y$ , and every other name; direct calculation gives the equation in each case. Nonbinding constructors apply the induction hypotheses to their arguments. At an abstraction or case branch, choose every displayed binder outside $FV (a) \cup FV (d) \cup {x, y}$ . Both sequential substitutions pass under that same binder; apply the body induction hypothesis and reattach it. The representative-independence argument in definition 2.28 shows that the resulting equation is on alpha-classes.

For item 1, write the step as $K [r] ⟶_{p} K [q]$ , freshen the binders of $K, r, q$ outside $FV (a) \cup {x}$ , and induct on $K$ . Substitution rebuilds the same context around the substituted root. At a beta root $(λ y . b) c ⇝_{p} b [c / y]$ , item 3 gives $(b [c / y]) [a / x] = b [a / x] [c [a / x] / y],$ which is the contractum of the substituted beta redex. The left and right case roots use the same equation with their selected branch binder. Every other root is componentwise.

For item 2, choose a representative of $b$ whose binders lie outside the finite set $FV (a) \cup FV (a^{'}) \cup {x}$ , and use structural induction on that representative. A variable different from $x$ gives reflexivity; the variable $x$ gives the assumed step. For each nonbinding constructor, reduce the copied occurrences one at a time and compose the resulting many-step derivations. At a binder, choose its name outside $FV (a) \cup FV (a^{'}) \cup {x}$ and apply the induction hypothesis to the body; the proof-context grammar lifts the resulting sequence under that binder. For a case, perform this argument independently in the scrutinee and the two branch bodies; the independent freshness choices ensure that neither copied sequence captures a free variable of $a$ or $a^{'}$ . ◻

Strong normalization supplies reduction heights, reduction closure handles a step in an argument, and neutral expansion admits the rebuilt eliminator. The following lemma records the resulting closure properties.

Lemma 2.52 — Eliminator closure ¶

The following closure properties hold for the reducibility interpretation.

If $e \in R_{2}$ and $b, c \in R_{C}$ , then $if (e; b; c) \in R_{C}$ .
If $e \in R_{A + B}$ and $\forall a \in R_{A}, b [a / x] \in R_{C}, \forall d \in R_{B}, c [d / y] \in R_{C},$ then $case (e; x . b; y . c) \in R_{C}$ .
If $e \in R_{0}$ , then ${abort}_{C} (e) \in R_{C}$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.52 — Eliminator closure

Proof. We use lemma 2.51 throughout.

For item 1, induct on $ν (e) + ν (b) + ν (c)$ . The conditional is neutral. Its root reduct is $b$ when $e = tt$ and $c$ when $e = ff$ , hence is reducible by hypothesis. Its immediate reducts are exactly $\begin{array}{ll} if (e^{'}; b; c) & e ⟶_{p} e^{'}, \\ if (e; b^{'}; c) & b ⟶_{p} b^{'}, \\ if (e; b; c^{'}) & c ⟶_{p} c^{'}, \\ b & e = tt, \\ c & e = ff . \end{array}$ Thus every nonroot immediate step reduces exactly one of $e, b, c$ . Saturation clause 2 puts the changed immediate subterm in its candidate. Its reduction height is smaller, so the induction hypothesis gives membership of the new conditional in $R_{C}$ . Saturation clause 3 now gives the result.

For item 2, choose distinct variables $z, w$ outside the finite set $FV (b) \cup FV (c) \cup {x, y}$ . Saturation clause 3 gives $z \in R_{A}$ and $w \in R_{B}$ . Hence $b [z / x], c [w / y] \in R_{C}$ , so both are strongly normalizing. Fresh renaming preserves the reduction tree, and therefore $b$ and $c$ themselves are strongly normalizing.

Induct on $ν (e) + ν (b) + ν (c)$ . The case term is neutral. If $e = inl (a)$ , the zero-step canonical-reduct condition in $R_{A + B}$ gives $a \in R_{A}$ , so the root reduct $b [a / x]$ is reducible. If $e = inr (d)$ , its right canonical-reduct condition gives $d \in R_{B}$ , so the root reduct $c [d / y]$ is reducible by the right-branch hypothesis. A step in $e$ uses saturation clause 2 and the induction hypothesis. If $b ⟶_{p} b^{'}$ , then $b [a / x] ⟶_{p} b^{'} [a / x]$ for every reducible $a$ ; saturation clause 2 therefore establishes the left-branch hypothesis for $b^{'}$ . The measure decreases, so the induction hypothesis applies. If $c ⟶_{p} c^{'}$ , compatibility gives $c [d / y] ⟶_{p} c^{'} [d / y]$ for every $d \in R_{B}$ ; reduction closure establishes the right-branch hypothesis for $c^{'}$ , and the decreased height allows the induction hypothesis. Thus every immediate reduct of the case term lies in $R_{C}$ , and saturation clause 3 concludes.

For item 3, induct on $ν (e)$ . The abort term is neutral and has no root contraction. Every immediate reduct is ${abort}_{C} (e^{'})$ with $e^{'} \in R_{0}$ by saturation clause 2 and $ν (e^{'}) < ν (e)$ ; the induction hypothesis and saturation clause 3 finish the proof. ◻

Principal expansion is a different closure property. It starts from the contractum, whereas eliminator closure starts from the scrutinee. The proper immediate term arguments of a root redex are the terms immediately carried by its introduction and elimination forms: $\begin{array}{cc} root redex & proper arguments \\ (λ x : A . b) a & b, a \\ fst ((a, b)), snd ((a, b)) & a, b \\ case (inl (a); x . b; y . c), case (inr (a); x . b; y . c) & a, b, c \\ if (tt; b; c), if (ff; b; c) & b, c . \end{array}$ This table defines the phrase for all seven root contractions.

Lemma 2.53 — Principal expansion ¶

Let $r ⟶_{p} q$ be one of the seven root contractions in definition 2.36. If $q \in R_{C}$ and every proper immediate term argument of $r$ is strongly normalizing, then $r \in R_{C}$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.53 — Principal expansion

Proof. Induct on the sum of the reduction heights of the proper arguments. The redex $r$ is neutral. Its root reduct $q$ is reducible by hypothesis. Any other immediate step reduces one proper argument and leaves a principal redex $r^{'}$ of the same kind. Its root contractum $q^{'}$ is reachable from $q$ by zero or more compatible steps: a step in an unused branch leaves $q$ unchanged; a step in a selected body gives one compatible step; and a step $a ⟶_{p} a^{'}$ in a substituted argument gives $b [a / x] ⟶_{p}^{*} b [a^{'} / x]$ by the compatibility fact above. Repeated use of saturation clause 2 gives $q^{'} \in R_{C}$ . The height sum has decreased, so the induction hypothesis gives $r^{'} \in R_{C}$ . Every immediate reduct of $r$ is now reducible, and saturation clause 3 gives $r \in R_{C}$ . ◻

For example, if $b [a / x] \in R_{C}$ and both $b$ and $a$ are strongly normalizing, principal expansion gives $(λ x : A . b) a \in R_{C} .$ The strong-normalization premise for $b$ matters because proof reduction is compatible under lambda bodies.

A complete calculation is already visible at Boolean type. The two values $tt$ and $ff$ belong to $R_{2}$ . If $a \in R_{2}$ , eliminator closure gives $if (a; ff; tt) \in R_{2} .$ The abstraction body is strongly normalizing, so principal expansion applied to an arbitrary such $a$ yields $(λ x : 2 . if (x; ff; tt)) a \in R_{2} .$ Therefore Boolean negation belongs to $R_{2 \to 2}$ , exactly by the arrow clause.

Definition 2.41 — Reducible substitution ¶

For $Γ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ , a simultaneous substitution $σ$ is a finite map from the declared variables $x_{i}$ to terms. It acts simultaneously and capture-avoidingly on $e$ ; variables outside its domain are left unchanged. Write $FV (rng (σ)) : = ⋃_{x \in dom (σ)} FV (σ (x)) .$ Constants are fixed, and the nonbinding clauses are $\begin{aligned} x [σ] & = {\begin{cases} σ (x) & x \in dom (σ), \\ x & otherwise, \end{cases} & (e_{1} e_{2}) [σ] & = e_{1} [σ] e_{2} [σ], \\ if (e; e_{1}; e_{2}) [σ] & = if (e [σ]; e_{1} [σ]; e_{2} [σ]), \\ (e_{1}, e_{2}) [σ] & = (e_{1} [σ], e_{2} [σ]), & fst (e) [σ] & = fst (e [σ]), \\ snd (e) [σ] & = snd (e [σ]), & inl (e) [σ] & = inl (e [σ]), \\ inr (e) [σ] & = inr (e [σ]), & {abort}_{C} (e) [σ] & = {abort}_{C} (e [σ]) . \end{aligned}$ Here $tt, ff, ⋆$ are the fixed constants. For an abstraction, choose a representative with $x \notin FV (rng (σ))$ and define $(λ x : A . b) [σ] = λ x : A . b [σ ∖ x] .$ For a case choose its two binders independently outside $FV (rng (σ))$ and each other, then define $\begin{aligned} case (e; x . e_{1}; y . e_{2}) [σ] \\ = case (e [σ]; x . e_{1} [σ ∖ x]; y . e_{2} [σ ∖ y]) . \end{aligned}$ These clauses are independent of representatives. Fix raw representatives of the finitely many terms in the range of $σ$ . For two displayed abstraction representatives, choose one name $u$ outside the name sets of both bodies and of all those range representatives. Clause (B3) permits both abstractions to be opened at $u$ . Structural induction identifies the two substituted opened bodies, and rebuilding the common binder $u$ identifies the output abstractions up to alpha-equivalence.

For two displayed case representatives, choose distinct names $u, v$ outside the name sets of both complete case representatives and all range representatives. Clause (B3) opens both left branches at $u$ and both right branches at $v$ . Structural induction identifies the substituted scrutinees and the two pairs of substituted opened branch bodies. Rebuilding the common branch binders $u, v$ identifies the output cases up to alpha-equivalence. Thus simultaneous substitution is well-defined on alpha-classes.

In particular, if $x \notin dom (σ)$ and is fresh for the range of $σ$ , then $b [σ, x \mapsto a] = b [σ] [a / x] .$ This equation is proved by structural induction on $b$ . The variable and nonbinding cases are the displayed clauses. For an abstraction choose its binder $y$ outside $FV (rng (σ)) \cup FV (a) \cup {x}$ ; both sides reattach $λ y$ to the body equation. For a case choose distinct branch binders $y, z$ outside the same finite set. Both sides use the same substituted scrutinee and reattach $y$ and $z$ to the two induction-hypothesis equations. This treats every constructor and proves equation 2.1 before it is used in the fundamental lemma.

The substitution is reducible for $Γ$ when $σ (x_{i}) \in R_{A_{i}}$ for every $i$ . Write $e [σ]$ for simultaneous capture-avoiding substitution. The empty substitution is reducible for the empty context. Write $σ, x \mapsto a$ for the map which agrees with $σ$ away from $x$ and sends $x$ to $a$ .

Referenced from 9 locations

Theorem 2.42 — Fundamental lemma ¶

If $Γ ⊢ e : A$ and $σ$ is reducible for $Γ$ , then $e [σ] \in R_{A}$ .

Referenced from 3 locations

Proof of Theorem 2.42 — Fundamental lemma

Proof. Induct on the typing derivation. Before a binder case, display its bound name outside the finite set $FV (rng (σ)) \cup dom (Γ)$ and outside the other case binder when there are two; convention 2.3 permits this choice.

For Var, the assertion is the corresponding component of $σ$ . For Lam, choose $z$ outside $FV (b [σ]) \cup FV (rng (σ)) \cup dom (Γ) \cup {x}$ and map $x$ first to $z$ . Saturation clause 3 and the induction hypothesis give $b [σ, x \mapsto z] \in R_{B}$ . This term is a fresh renaming of $b [σ]$ ; saturation clause 1 and lemma 2.50 therefore give $SN (b [σ])$ in both renaming directions.

For arbitrary $a \in R_{A}$ , the induction hypothesis under $σ, x \mapsto a$ gives the beta contractum $b [σ, x \mapsto a] \in R_{B}$ . Saturation clause 1 gives $SN (a)$ , so principal expansion admits $(λ x : A . b [σ]) a$ : its contractum is the same alpha-class by equation 2.1. The arrow clause now admits the abstraction. The App case is that clause’s elimination condition.

For Pair, the induction hypotheses give reducible, hence strongly normalizing, components. Principal expansion admits both projections; the product clause then admits the pair. The Fst and Snd cases are the two defining product tests.

For Inl, the induction hypothesis gives $a \in R_{A}$ , hence $SN (a)$ and $SN (inl (a))$ . Every canonical reduct $inl (a^{'})$ comes from $a ⟶_{p}^{*} a^{'}$ , so saturation clause 2 gives $a^{'} \in R_{A}$ ; no right injection is reachable. Thus $inl (a) \in R_{A + B}$ . In Inr, the induction hypothesis gives $b \in R_{B}$ and hence $SN (inr (b))$ ; every reachable $inr (b^{'})$ has $b^{'} \in R_{B}$ by reduction closure, while no left injection is reachable. Therefore $inr (b) \in R_{A + B}$ .

In the Case case, extend $σ$ by an arbitrary reducible branch argument. The two branch induction hypotheses give $\forall a \in R_{A}, e_{1} [σ] [a / x] \in R_{C}, \forall d \in R_{B}, e_{2} [σ] [d / y] \in R_{C} .$ The scrutinee induction hypothesis and eliminator closure item 2 now give the substituted case term.

The constants $tt, ff, ⋆$ lie in their base candidates. The If case is eliminator closure item 1, and Empty-E is item 3. There is no introduction case for $0$ . ◻

Theorem 2.43 — Strong normalization ¶

Every well-typed term of the extended STLC is strongly normalizing for $⟶_{p}$ .

Referenced from 7 locations

Proof of Theorem 2.43 — Strong normalization

Proof. Map every variable $x : A$ in $Γ$ to itself. Variables are reducible by neutral expansion, so this identity substitution is reducible for $Γ$ . The fundamental lemma gives $e \in R_{A}$ , and saturation clause 1 gives $SN (e)$ . ◻

Lemma 2.57 — Machine steps are proof steps ¶

If $e ⟼ e^{'}$ , then $e ⟶_{p} e^{'}$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Lemma 2.57 — Machine steps are proof steps

Proof. Induct on the call-by-value step. Each beta, Boolean, projection, or case contraction is one of the seven proof roots; its value premise only restricts when that root may be used. Every congruence rule selects a position in the proof-context grammar: applications use $K e$ or $v K$ , conditionals use their guard, pairs use either component, projections, injections, and abort use their unary argument, and cases use their scrutinee. Apply P-Ctx to the induction-hypothesis step in each congruence case. ◻

Corollary 2.58 — Call-by-value normalization ¶

If $\cdot ⊢ e : A$ , then there is a value $v$ such that $e ⟼^{*} v$ and $\cdot ⊢ v : A$ .

Referenced from 3 locations

Simple Types, Curry–Howard, Safety, and Normalization

Proof of Corollary 2.58 — Call-by-value normalization

Proof. Strong normalization gives the finite height $ν (e)$ . If $e$ is not a value, by extended progress there is a step $e ⟼ e_{1}$ ; by lemma 2.57, $ν (e_{1}) < ν (e)$ . Well-founded induction on this natural number therefore reaches a term $v$ with no call-by-value step. Progress makes $v$ a value. Composing the selected steps gives $e ⟼^{*} v$ , and iterated preservation gives $\cdot ⊢ v : A$ . ◻

Exercise 2.12 ¶

★★☆ Assume $e \in R_{A \times B}$ and $e ⟶_{p} e^{'}$ . Display the two lifted steps $fst (e) ⟶_{p} fst (e^{'})$ and $snd (e) ⟶_{p} snd (e^{'})$ , apply reduction closure at $A$ and $B$ , and conclude $e^{'} \in R_{A \times B}$ . Then prove directly from definition 2.39, lemma 2.53 that if $a \in R_{A}$ and $b \in R_{B}$ , then $(a, b) \in R_{A \times B}$ .

Referenced from 3 locations

Lemma 2.59 — Typed normal forms ¶

Suppose $Γ ⊢ n : A$ and $n$ has no $⟶_{p}$ reduct. Then exactly one of the following holds:

$n$ is an introduction form;
$n$ is variable-headed, according to the grammar $\begin{aligned} h ::= & x ∣ h e ∣ fst (h) ∣ snd (h) ∣ if (h; e_{1}; e_{2}) \\ ∣ case (h; x . e_{1}; y . e_{2}) ∣ {abort}_{A} (h), \end{aligned}$ and its head variable has a declaration in $Γ$ .

Referenced from 6 locations

Proof of Lemma 2.59 — Typed normal forms

Proof. Induct on the structure of $n$ . A variable is in the second class by typing inversion; every introduction form is in the first. It remains to consider an elimination.

For $n = e_{1} e_{2}$ , both subterms are normal. Apply the induction hypothesis to the well-typed function $e_{1}$ . If it is variable-headed, then so is $n$ . If it is an introduction, typing inversion at an arrow type forces it to be an abstraction, making $n$ a beta-redex, contrary to normality. For $fst (e)$ and $snd (e)$ , an introductory $e$ of product type must be a pair and would create a projection redex; otherwise the variable head is preserved.

For a case expression, an introductory scrutinee of sum type must be an injection, and either form creates a case redex. For a conditional, an introductory scrutinee of type $2$ must be $tt$ or $ff$ , again creating a redex. Finally, an introductory term cannot have type $0$ : the introduction rules conclude only at $2$ , an arrow, a product, a sum, or $1$ . Thus the scrutinee of ${abort}_{C} (e)$ must be variable-headed. These cases exhaust the term grammar. The two classes are disjoint by their outer forms. ◻

Under proposition 2.33, a logic is consistent when it has no derivation of falsity from no assumptions.

Corollary 2.44 — Consistency ¶

There is no closed term $e$ with $\cdot ⊢ e : 0$ .

Referenced from 3 locations

Proof of Corollary 2.44 — Consistency

Proof. Assume such an $e$ . Strong normalization and lemma 2.47 give the natural-number measure $ν (e)$ . While a reduct exists, choose one; its measure is strictly smaller, so after finitely many choices a normal form $n$ is reached. Many-step subject reduction, corollary 2.44, gives $⊢ n : 0$ . By lemma 2.59, $n$ is an introduction form or is headed by a variable declared in the empty context. The second alternative is impossible. The first is also impossible: inspection of the introduction rules shows that none concludes at $0$ . Thus no such normal form exists, a contradiction. ◻

Safety alone would not prove this corollary. It permits an infinite, well-typed computation, because an infinite computation is never stuck. Corollary 2.58 gives $e ⟼^{*} v$ for a value $v : 0$ ; extended canonical forms shows that no such $v$ exists. Translating a hypothetical natural-deduction derivation of $⊥$ from no assumptions would give a closed term of $0$ , contradicting the corollary. Hence the uninhabitedness statement is the promised logical consistency theorem.

The first pressure for polymorphism

The identity program has to be copied when its type changes: ${id}_{2} : = λ x : 2 . x : 2 \to 2, {id}_{1} : = λ x : 1 . x : 1 \to 1 .$ Their erased lambda bodies are identical, yet the grammar contains no type that gives one simply typed term both displayed arrow types. Writing two definitions works; expressing them as one uniform definition does not. A single identity usable at both types requires quantification over its type.

Exercise 2.13 ¶

★★☆ Type the two identities above and use each twice in one product term. Then attempt to bind a single simply typed variable $i$ and use $i$ at both types. Use uniqueness of types to prove that the two required arrow types for $i$ would have to be equal, and exhibit the unequal domain or codomain that contradicts this equality.

Referenced from 3 locations

Suggested first pass.

Do exercise 2.15, exercise 2.14, exercise 2.16, in that order: binding calculation, proof reconstruction, and the Curry–Howard boundary. Continue in printed order for the full pass.

Exercise 2.15 ¶

★★☆ Let $w, x, y, z$ be distinct. Compute, with every freshening step shown, $case (z; x . (x, w); y . (w, y)) [(x, y) / w] .$ Mark the free occurrences in the result. Explain why retaining the left binder would capture the inserted $x$ , while retaining the right binder would capture the inserted $y$ .

Referenced from 4 locations

Exercise 2.14 ¶

★★★ Begin with the call-by-value function-and-Boolean STLC frames, obtained by restricting definition 1.67: $E ::= [-] ∣ E e ∣ v E ∣ if (E; e_{1}; e_{2}) .$ Add frames for products, projections, injections, the case scrutinee, and ${abort}_{A} (E)$ ; do not import the arithmetic frames of chapter 1. Prove unique decomposition for the extended language, including the two injection contractions of a case, and derive determinism.

Referenced from 4 locations

Exercise 2.16 ¶

★★★ Put $\neg A : = A \to 0$ . Give proof terms and complete typing derivations for $\neg (A + B) \to (\neg A \times \neg B) and (\neg A \times \neg B) \to \neg (A + B) .$ Reduce the second term on both injection forms.

Referenced from 4 locations

Exercise 2.17 ¶

★★★ Construct both directions of $A \times (B + C) ⟷ (A \times B) + (A \times C) .$ Show every beta, projection, and case contraction in each composite on constructor inputs. Do not add either of the following equations as a computation rule: $(fst (p), snd (p)) = p, λ x : A . f x = f (x \notin FV (f)) .$

Referenced from 3 locations

The next two problems form one normalization reconstruction: the first rebuilds neutral expansion, and the second applies the resulting saturation mechanism to Boolean elimination.

Exercise 2.18 ¶

★★★ For every type $A$ , let $N (A)$ be the assertion that every neutral term $n$ belongs to $R_{A}$ whenever all immediate reducts of $n$ belong to $R_{A}$ . Prove $N (A)$ by structural induction on $A$ , without citing clause 3 of lemma 2.40. At a proper component type you may use clauses 1 and 2 of that lemma together with the corresponding outer induction hypothesis $N (B)$ or $N (C)$ . In the arrow case, fix a reducible argument and use well-founded induction on its reduction height. State separately the outer type induction hypothesis and the inner height induction hypothesis. Finally, apply $N (A)$ to a variable, which is neutral and has no immediate reducts, to derive $x \in R_{A}$ .

Referenced from 3 locations

Exercise 2.19 ¶

★★★ Prove item 1 of lemma 2.52 in full. Use induction on $ν (e) + ν (b) + ν (c)$ , list the possible immediate reductions of $if (e; b; c)$ , and identify where each saturation clause is used. Then prove directly that $tt, ff \in R_{2}$ .

Referenced from 3 locations

Exercise 2.22 ¶

★★★ Practical project.stlc-safety-checker Implement the syntax-directed checker and call-by-value evaluator for the Boolean-and-function fragment in the following stages.

Define datatypes for types, raw terms, and typing derivations. Make the checker return a type together with a derivation, rather than a Boolean. Write a second traversal that validates every node of the returned derivation against the rules of section 2.1.
Implement free-name calculation, deterministic fresh-name selection, and capture-avoiding substitution. On the body $λ y : 2 . x$ , substitute the free variable $y$ for $x$ . Check that the implementation freshens the binder and that naive textual replacement would capture the inserted $y$ .
Implement values, the six call-by-value one-step rules, and a fueled driver that distinguishes a normal form from exhausted fuel. Use enough fuel to finish every named run below.
Accept $not ff$ at $2$ , validate its returned derivation, and evaluate the same source term to $tt$ . Also evaluate $not tt$ to $ff$ . Reject $tt ff$ and $λ x : 2 . x x$ .
Treat finite raw terms as the executable input. Reject $λ x : 2 . λ x : 2 . x$ because its nested binder duplicates a context declaration; an alpha-fresh representative is a separate valid input. Add a regression that fails if either inference or derivation validation accepts the duplicate declaration.

Finally, give the size argument showing that no simple type $A$ can annotate $λ x : A . x x$ : typing the body would force $A = A \to B$ for some $B$ . The executable checks the finite named outcomes; it is not a test of this universal argument.

Submit the program together with a short execution record containing the following five items.

Print the complete validated derivation returned for $not ff$ , including the context at every Var node.
Print its call-by-value trace from the named source through the beta and conditional contractions to $tt$ . Beside each term, print the type returned by a fresh checker run.
Give a table with one row for each named input above and columns for checker result, evidence-validation result, final value or rejection, and remaining fuel. A rejected term has no fabricated derivation or final value.
Replace capture-avoiding substitution by textual replacement only for the capture witness of stage 2 above. Record the captured output and the failed witness assertion, then restore the correct implementation before running the acceptance cases.
Explain which observations are finite tests and which claim is proved only by the size argument. In particular, rejection of the displayed self-application is evidence for one raw input, not a normalization or untypability theorem for an unspecified language.

Referenced from 5 locations