Chapter 60Core route

The Lambda Cube and Pure Type Systems

Three binders have appeared with three separate typing rules. In the simply typed calculus of chapter 2, $λ x : A . x$ abstracts a term variable. The uniform PTS syntax writes the same abstraction as $λ (x : A) . x$ . In System F (chapter 5), $Λ X . λ (x : X) . x : \forall X . X \to X$ abstracts a type variable in a term. In $F_{ω}$ (chapter 9), the expression $λ X :: Ty . X \to X$ abstracts a type variable in a type operator. The three rules differ only in the classes of the domain, the body, and the resulting product. A uniform product rule must therefore expose all three classes; one structural argument can then cover every admitted triple.

One product rule with three classifiers

Write $*$ for the class of ordinary types and $◻$ for the class of kinds. These two symbols are sorts: primitive classifiers that may occur on the right of a typing judgment. A product whose domain has sort $s_{1}$ , whose codomain has sort $s_{2}$ , and which itself has sort $s_{3}$ is controlled by the triple $(s_{1}, s_{2}, s_{3})$ .

Example 60.1 — The baseline and the optional directions ¶

Let $A : *$ and $Nat : *$ . The following products separate the baseline from two optional directions. $\begin{aligned} \prod_{a : A} A & : * & uses (*, *, *), \\ \prod_{X : *} X & : * & uses (◻, *, *), \\ \prod_{F : *} * & : ◻ & uses (◻, ◻, ◻) . \end{aligned}$ The second product classifies polymorphic terms. The third classifies type operators. A fourth possibility, $(*, ◻, ◻)$ , allows a type or kind to depend on a term. For example, the declaration $Vec : \prod_{n : Nat} *$ requires that fourth triple. The word direction records dependency: it does not assert that every well-sorted body mentions its bound variable.

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

The examples force a syntax in which terms, types, and kinds are not separate grammatical categories.

Definition 60.2 — Pure-type-system specification ¶

Fix a set $C$ of constants. A pure-type-system specification, abbreviated PTS specification, is a triple $S = (S, A, R)$ consisting of:

a set $S \subseteq C$ of sorts;
a set $A \subseteq C \times S$ of axioms, written $c : s$ ;
a set $R \subseteq S \times S \times S$ of product triples.

For every $s \in S$ , fix an infinite set $V_{s}$ of variables. The sets $C, V_{s}$ are pairwise disjoint, and $V : = ⋃_{s \in S} V_{s}$ . Here $R$ is the PTS product-triple set; it is unrelated to the rule sets and reducibility candidates denoted by the same calligraphic letter in earlier chapters. The pseudo-terms of $S$ are generated by $M, N, A, B ::= x ∣ c ∣ M N ∣ λ (x : A) . M ∣ \prod_{x : A} B .$ Here $x \in V$ and $c \in C$ . The binder $x$ binds in $M$ or $B$ , respectively. Expressions identify alpha-equivalent pseudo-terms. We write $M [N / x]$ for capture-avoiding replacement of the free occurrences of $x$ in $M$ by $N$ , renaming bound variables first when necessary. When $x \notin FV (B)$ , write $A \to B$ for $\prod_{x : A} B$ . Compatible beta-reduction is the least relation closed under every pseudo-term constructor and containing $\frac{}{(λ (x : A) . M) N ⟶_{β} M [N / x]} Beta .$ Write $⟶_{β}^{*}$ for its reflexive-transitive closure and $M =_{β} N$ when $M$ and $N$ are related by the equivalence relation it generates.

Referenced from 5 locations

Allowing $c : s$ with $c \in C$ is intentional. It is the general PTS schema of [Bar92], not a later signature extension, and permits a base-type constant such as $Nat : *$ . The common sort-only specialization has $A \subseteq S \times S$ . The lambda-cube instances below use that specialization with the sole axiom $* : ◻$ ; adding a base-type constant changes the signature but not its cube vertex.

The typography of a name does not determine whether it is a constant or a variable. Thus a displayed family name such as $Vec$ may denote a member of some $V_{s}$ ; its context declaration must then be justified by Var. It may occur in $A$ only when its declared type is a sort. This distinction prevents a family declaration such as $Vec : \prod_{n : Nat} *$ from bypassing Prod.

In this chapter, the letter $M$ ranges over arbitrary PTS expressions, not merely program terms.

Definition 60.3 — PTS typing ¶

For a specification $S = (S, A, R)$ , the judgment $Γ ⊢_{S} M : A$ is generated by the following rules. Contexts are finite lists of declarations with distinct subjects. $\frac{c : s \in A}{\cdot ⊢_{S} c : s} Ax \frac{\begin{matrix} Γ ⊢_{S} A : s \\ x \in V_{s} \\ x \notin dom (Γ) \end{matrix}}{Γ, x : A ⊢_{S} x : A} Var$ $\frac{\begin{matrix} Γ ⊢_{S} M : A \\ Γ ⊢_{S} B : s \\ x \in V_{s} \\ x \notin dom (Γ) \end{matrix}}{Γ, x : B ⊢_{S} M : A} Weak$ $\frac{\begin{matrix} Γ ⊢_{S} A : s_{1} \\ Γ, x : A ⊢_{S} B : s_{2} \\ (s_{1}, s_{2}, s_{3}) \in R \end{matrix}}{Γ ⊢_{S} \prod_{x : A} B : s_{3}} Prod$ $\frac{\begin{matrix} Γ, x : A ⊢_{S} M : B \\ Γ ⊢_{S} \prod_{x : A} B : s \end{matrix}}{Γ ⊢_{S} λ (x : A) . M : \prod_{x : A} B} Lam$ $\frac{\begin{matrix} Γ ⊢_{S} F : \prod_{x : A} B \\ Γ ⊢_{S} N : A \end{matrix}}{Γ ⊢_{S} F N : B [N / x]} App$ $\frac{\begin{matrix} Γ ⊢_{S} M : A \\ Γ ⊢_{S} B : s \\ A =_{β} B \end{matrix}}{Γ ⊢_{S} M : B} Conv$ The specification determines which instances of Prod exist; the other rules are fixed.

Referenced from 8 locations

The sort premise in Conv prevents an unclassified expression from being installed as a type. Removing it leaves a well-formed rule, but destroys the presupposition that the right side of every typing judgment is a sort or has a sort.

Example 60.4 — The polymorphic identity ¶

Let $S = {*, ◻}, A = {* : ◻}, R = {(*, *, *), (◻, *, *)} .$ Write the short subderivations $\begin{aligned} D_{X} & : = \frac{\frac{* : ◻ \in A}{\cdot ⊢_{S} * : ◻} Ax}{X : * ⊢_{S} X : *} Var, \\ D_{X}^{+ x} & : = \frac{\begin{matrix} D_{X} \\ D_{X} x \neq X \end{matrix}}{X : *, x : X ⊢_{S} X : *} Weak, \\ D_{Π} & : = \frac{\begin{matrix} D_{X} \\ D_{X}^{+ x} \\ (*, *, *) \in R \end{matrix}}{X : * ⊢_{S} \prod_{x : X} X : *} Prod, \\ D_{id} & : = \frac{\begin{matrix} \frac{D_{X}}{X : *, x : X ⊢_{S} x : X} Var \\ D_{Π} \end{matrix}}{X : * ⊢_{S} λ (x : X) . x : \prod_{x : X} X} Lam, \\ D_{\forall id} & : = \frac{\begin{matrix} \frac{* : ◻ \in A}{\cdot ⊢_{S} * : ◻} Ax \\ D_{Π} \\ (◻, *, *) \in R \end{matrix}}{\cdot ⊢_{S} \prod_{X : *} \prod_{x : X} X : *} Prod . \end{aligned}$ Every leaf of the required derivation is now visible: $\frac{\begin{matrix} D_{id} \\ D_{\forall id} \end{matrix}}{\cdot ⊢_{S} λ (X : *) . λ (x : X) . x : \prod_{X : *} \prod_{x : X} X} Lam .$ The outer product uses $(◻, *, *)$ ; the inner product uses $(*, *, *)$ . Thus the derivation records exactly which axis polymorphism requires.

Referenced from 5 locations

The Lambda Cube and Pure Type Systems

The application rule can now be read on a closed constructor. Put $I : = λ (X : *) . λ (x : X) . x,$ and work in the legal context $A : *, a : A$ . Weakening the final judgment of example 60.4 into this context and applying App gives $\frac{\begin{matrix} A : *, a : A ⊢_{S} I : \prod_{X : *} \prod_{x : X} X \\ A : *, a : A ⊢_{S} A : * \end{matrix}}{A : *, a : A ⊢_{S} I A : \prod_{x : A} A} App .$ A second use of App derives $A : *, a : A ⊢_{S} I A a : A .$ The corresponding computation performs two compatible beta-steps: $I A a \overset{B e t a}{⟶_{β}} (λ (x : A) . x) a \overset{B e t a}{⟶_{β}} a .$ Conversion should do real work rather than rename an alpha-bound variable. In $λ_{2 ω}$ , put $F_{0} : = λ (Y : *) . Y \to Y .$ The triple $(◻, ◻, ◻)$ forms the outer product in the type of $F_{0}$ , while $(*, *, *)$ forms its body $Y \to Y$ ; hence $F_{0} : \prod_{Y : *} *$ . In the legal context $A : *, a : A, g : \prod_{Y : *} F_{0} Y,$ rule App first derives $g A : F_{0} A$ . Since $F_{0} A ⟶_{β} A \to A,$ and $A \to A : *$ , rule Conv derives $g A : A \to A$ ; another application derives $g A a : A$ . This is conversion at a type-level beta-redex.

By contrast, in a legal context containing $f : \prod_{y : A} B$ and $N : A$ , the application $f N$ is neutral: App gives it type $B [N / y]$ , but no beta-step applies because its head is the variable $f$ .

Exercise 60.1 ¶

★☆☆ Delete $(◻, *, *)$ from the specification in example 60.4. Mark the first premise in its derivation that can no longer be discharged. Verify that the monomorphic term $λ (x : X) . x$ remains typable in the context $X : *$ . (Six lines.)

Referenced from 3 locations

The eight vertices

For the lambda cube, fix $S = {*, ◻}$ and $A = {* : ◻}$ . Write $\begin{aligned} r_{\to} & : = (*, *, *), & r_{2} & : = (◻, *, *), \\ r_{ω} & : = (◻, ◻, ◻), & r_{P} & : = (*, ◻, ◻) . \end{aligned}$ The baseline $r_{\to}$ forms ordinary function types. Adding $r_{2}$ permits terms to depend on types, adding $r_{ω}$ permits type operators to depend on types, and adding $r_{P}$ permits types to depend on terms. All four cube triples satisfy $s_{3} = s_{2}$ ; general PTS specifications need not have that property.

Definition 60.5 — Lambda-cube systems ¶

For $I \subseteq {2, ω, P}$ , let $λ_{I}$ be the PTS with product triples ${r_{\to}} \cup {r_{i} ∣ i \in I}$ . We use the following compact subscripts throughout this chapter: $\begin{array}{ccc} I & system & R \\ \emptyset & λ_{\to} & r_{\to} \\ {2} & λ_{2} & r_{\to}, r_{2} \\ {ω} & λ_{ω} & r_{\to}, r_{ω} \\ {P} & λ_{P} & r_{\to}, r_{P} \\ {2, ω} & λ_{2 ω} & r_{\to}, r_{2}, r_{ω} \\ {2, P} & λ_{P 2} & r_{\to}, r_{2}, r_{P} \\ {ω, P} & λ_{P ω} & r_{\to}, r_{ω}, r_{P} \\ {2, ω, P} & λ_{C} & r_{\to}, r_{2}, r_{ω}, r_{P} . \end{array}$ The top system $λ_{C}$ is the Calculus of Constructions. Barendregt’s conventional names distinguish the vertices by writing $λ \underset{―}{ω}$ for our $λ_{ω}$ , $λ ω$ for our $λ_{2 ω}$ , $λ P \underset{―}{ω}$ for our $λ_{P ω}$ , and $λ P ω = λ C$ for the top vertex [Bar92]. Thus our subscript $P ω$ is a set-valued axis label, not Barendregt’s name $λ P ω$ .

Referenced from 6 locations

Lemma 60.6 — Monotonicity in product triples ¶

Let $S = (S, A, R)$ and $S^{'} = (S, A, R^{'})$ , with $R \subseteq R^{'}$ . Then $Γ ⊢_{S} M : A ⟹ Γ ⊢_{S^{'}} M : A .$

Referenced from 5 locations

Proof of Lemma 60.6 — Monotonicity in product triples

Proof. Induct on the displayed derivation. Rebuild every rule with the induction hypotheses. In the Prod case, its triple lies in $R^{'}$ by the inclusion; no other rule inspects the product-triple set. ◻

The cube below records these inclusions. A solid edge labeled $2$ or $ω$ adds the indicated triple; a dashed edge labeled $P$ adds $r_{P}$ . A crossing without a node is not a vertex. If $I \subseteq J \subseteq K$ , write $ι_{I, J}$ for the inclusion proved by lemma 60.6; each square asserts $ι_{J, K} \circ ι_{I, J} = ι_{I, K} .$ Both sides preserve the same derivation tree and merely regard every Prod membership witness in the larger set. Mathematical diagram Diagram

Proposition 60.7 — Recovery of the familiar systems ¶

The syntax translations from Church-style STLC with type variables, System F, and $F_{ω}$ with term polymorphism into $λ_{\to}$ , $λ_{2}$ , and $λ_{2 ω}$ , respectively, preserve typing and beta-reduction. Conversely, a derivation-directed decoding maps every derivable judgment in the image of one of these translations back to its source calculus, up to alpha-equivalence, and maps beta-steps between such image expressions to source beta-steps. The top vertex $λ_{C}$ is exactly the PTS presentation of the Calculus of Constructions.

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

Proof of Proposition 60.7 — Recovery of the familiar systems

Proof. Map every arrow $A \to B$ to $\prod_{x : A} B$ with $x \notin FV (B)$ , every term abstraction to the PTS abstraction, every System F type abstraction $Λ X . M$ to $λ (X : *) . M$ , and every kind abstraction to the same PTS constructor. Applications are unchanged; type application becomes ordinary application.

For preservation, rule induction on the source derivation replaces each source formation rule by the indicated product triple. The three non-structural cases are $\begin{array}{cc} source rule & PTS triple \\ A \to B type & r_{\to} \\ \forall X . B type & r_{2} \\ K \to K^{'} kind & r_{ω} \end{array}$ The abstraction and application rules then coincide with Lam and App. Substitution is unchanged, so source beta-contraction maps to PTS beta-contraction.

For reflection, do not attempt to invert the translation on arbitrary pseudo-terms. Define the decoding simultaneously on PTS derivations and their premises. Its invariant assigns each decoded expression the source syntactic class determined by its typing derivation and returns a source derivation whose translation is alpha-equivalent to the PTS conclusion.

Rules Ax, Var, and Weak decode their premises and reconstruct the corresponding source rules. In a Prod derivation in the translated fragment, the final triple is one row of the table, so it determines whether the source constructor is an ordinary arrow, a universal type, or a kind arrow. In a Lam derivation, its product premise has fixed the class of the bound variable and the body. In an App derivation, the decoded product type of the function determines whether the source step is term application, type application, or kind application; this resolves the two applications present in $λ_{2}$ . Rule Conv reconstructs source conversion after decoding its sort premise. These clauses cover every rule whose conclusion is in the translated fragment and preserve the invariant.

A legal beta-redex is an application whose function derivation decodes to an abstraction with the same source class for its binder and argument. Decoding its contraction therefore gives source capture-avoiding substitution, and the source beta-rule translates back to the original PTS contraction. Congruence cases follow by decoding the derivation of the reduced subexpression. This proves reflection without claiming a syntactic inverse on untyped pseudo-terms. ◻

The qualification with type variables is necessary at the bottom vertex. The axiom $* : ◻$ permits declarations $X : *$ . A fixed-base STLC is obtained by restricting contexts and adding named base-type constants; that restriction is not a different cube vertex.

The fourth clause is not an adequacy theorem for a separately defined surface language. Rather, $λ_{C}$ is the PTS presentation called the Calculus of Constructions in [Bar92]. The primary presentation of the calculus, with dependent products and two classifier levels, is [CH88]. Relating either presentation to a different surface language would require a separate encoding theorem.

Example 60.8 — A term-indexed family at the P-vertex ¶

Extend the constant axioms by $Nat : *$ , and work in $λ_{P}$ . Choose $n \in V_{*}$ . The family kind is derived by $\frac{\begin{matrix} \cdot ⊢ Nat : * \\ n : Nat ⊢ * : ◻ \\ r_{P} = (*, ◻, ◻) \end{matrix}}{\cdot ⊢ \prod_{n : Nat} * : ◻} Prod .$ The middle premise is Weak applied to $\cdot ⊢ * : ◻$ . Consequently a context declaration $Vec : \prod_{n : Nat} *$ , with $Vec \in V_{◻}$ , is legal only when the $P$ -axis is present. Choose a fresh $v \in V_{*}$ , with $Vec, n, v$ pairwise distinct, and put $Γ_{0} : = (Vec : \prod_{n : Nat} *), n : Nat, Γ_{1} : = Γ_{0}, v : Vec n .$ Rules Var, App, Prod, and Lam derive $Γ_{1} ⊢ v : Vec n, Γ_{0} ⊢ λ (v : Vec n) . v : \prod_{v : Vec n} Vec n .$ The type depends on the neutral term $n$ ; no beta-step removes that dependency. Abstracting $n$ once more gives the displayed dependent judgment $Vec : \prod_{n : Nat} * ⊢ λ (n : Nat) . λ (v : Vec n) . v : \prod_{n : Nat} \prod_{v : Vec n} Vec n .$ The inner and outer term abstractions use $r_{\to}$ , while formation of the family’s context declaration uses $r_{P}$ . The only constant added to the axiom set is $Nat : *$ ; $Vec$ enters the context through Var, not Ax.

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Exercise 60.2 ¶

★★☆ For each of the following products, give the least vertex of the lambda cube in which it is formable and name the decisive product triple: $\begin{matrix} \prod_{X : *} X \to X, \\ \prod_{F : (* \to *)} \prod_{X : *} F X \to F X, \\ \prod_{n : Nat} Vec n \to Vec n . \end{matrix}$ A name may be added as an axiom only with a sort on its right. Every other declaration must have its type derived in the candidate vertex; in particular, derive $Vec : \prod_{n : Nat} *$ as in example 60.8. Prove minimality by deleting one triple in each case and use lemma 60.6 for the upward inclusions. (Half a page.)

Referenced from 6 locations

Structural metatheory

The PTS rules are uniform enough that their structural proofs use only capture-avoiding substitution and the placement of declarations in a context. No normalization hypothesis is needed.

Definition 60.9 — Legal PTS expressions ¶

A context $Γ$ is legal when it occurs in a derivable judgment. An expression $M$ is legal in $Γ$ when either $Γ ⊢_{S} M : A$ or $Γ ⊢_{S} A : M$ for some expression $A$ .

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

Lemma 60.10 — Context validity ¶

If $x_{1} : A_{1}, \dots, x_{n} : A_{n}$ is legal, then for every $i$ there is a sort $s_{i}$ such that $x_{1} : A_{1}, \dots, x_{i - 1} : A_{i - 1} ⊢_{S} A_{i} : s_{i} .$

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.10 — Context validity

Proof. Choose a derivation in which the context occurs and induct on that derivation. Rules Ax, Prod, Lam, App, and Conv either have empty context or have a premise with the same context; apply the induction hypothesis to that premise. A final Var has context $Θ, x : A$ and premise $Θ ⊢ A : s$ . A final Weak has context $Θ, x : B$ , first premise in $Θ$ , and declaration premise $Θ ⊢ B : s$ . In either case the induction hypothesis gives the claims for $Θ$ , and the declaration premise gives the last claim. These are all possible final rules. ◻

Lemma 60.11 — Free variables ¶

If $Γ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ and $Γ ⊢_{S} M : B$ , then

the variables $x_{1}, \dots, x_{n}$ are pairwise distinct;
$FV (M) \cup FV (B) \subseteq {x_{1}, \dots, x_{n}}$ ;
$FV (A_{i}) \subseteq {x_{1}, \dots, x_{i - 1}}$ for every $1 \leq i \leq n$ .

Referenced from 5 locations

Proof of Lemma 60.11 — Free variables

Proof. Proceed by rule induction on the typing derivation. Rule Ax has empty context. Rules Var and Weak append a name outside the context domain, and their sort premise gives the induction hypotheses for the new declaration. Rules Prod and Lam bind $x$ in the second premise; removing $x$ from that premise’s free-variable set gives the claimed set for the conclusion. Rule App takes the union of the two premise bounds and then substitutes $N$ for $x$ ; the capture-avoiding substitution equation $FV (B [N / x]) \subseteq (FV (B) ∖ {x}) \cup FV (N)$ gives the result. Rule Conv uses the two premise bounds. These are all rule families. ◻

Lemma 60.12 — Composition of substitution ¶

Capture-avoiding substitution on pseudo-terms satisfies $D [N / x] [P [N / x] / y] = D [P / y] [N / x] (y \notin FV (N) \cup {x}) .$

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.12 — Composition of substitution

Proof. This equation follows by structural induction on $D$ ; at either binder, first choose a representative whose bound name avoids $FV (N) \cup FV (P) \cup {x, y}$ . ◻

Lemma 60.13 — Beta-equivalence and substitution ¶

Capture-avoiding substitution respects beta-equivalence in both inputs: $\begin{aligned} M =_{β} N & ⟹ M [P / x] =_{β} N [P / x], \\ P =_{β} Q & ⟹ M [P / x] =_{β} M [Q / x] . \end{aligned}$

Referenced from 5 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.13 — Beta-equivalence and substitution

Proof. For the first implication, induct over the compatible beta reductions and their symmetric, transitive closure. A contracted redex is preserved after choosing its binder fresh; lemma 60.12 identifies the contractum. Congruence reconstructs every surrounding constructor. For the second implication, perform structural induction on $M$ . Each free occurrence of $x$ contributes the given beta-equivalence, while constructor congruence combines the induction hypotheses; at a binder, first choose its name fresh for $P$ and $Q$ . ◻

Lemma 60.14 — Weakening ¶

Suppose $Γ, Δ ⊢_{S} M : A$ and $Γ ⊢_{S} B : s$ . If $x \notin dom (Γ, Δ)$ , then $Γ, x : B, Δ ⊢_{S} M : A .$

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.14 — Weakening

Proof. Generalize over the split $Γ, Δ$ and perform rule induction on the first derivation. Keep the declaration-legality derivation $Γ ⊢ B : s$ as an explicit second input.

Rules Prod, Lam, App, and Conv are reconstructed after applying the induction hypothesis to every premise with context $Γ, Δ$ . In a product or lambda premise under $y : C$ , choose $y \notin FV (B) \cup {x} \cup dom (Γ, Δ)$ and apply the induction hypothesis at the enlarged suffix $Δ, y : C$ . This inserts $x : B$ before that binder, as required.

The two context-extending rules expose why the split was generalized. If a final Var concludes in $Γ, Δ_{0}, y : C$ with $Δ = Δ_{0}, y : C$ , apply the induction hypothesis to its premise $Γ, Δ_{0} ⊢ C : s_{C}$ and then reapply Var: $\frac{Γ, x : B, Δ_{0} ⊢ C : s_{C} y \notin dom (Γ, x : B, Δ_{0})}{Γ, x : B, Δ_{0}, y : C ⊢ y : C} Var .$ A final Weak with the same nonempty suffix is identical: apply the two induction hypotheses to its typing and declaration-sort premises and reapply Weak. If $Δ$ is empty, either final rule already has conclusion in $Γ$ ; one application of Weak, justified by the fixed premise $Γ ⊢ B : s$ , appends $x : B$ to that conclusion.

Finally, an Ax conclusion has empty context, so both parts of the split are empty. Reapply Weak to Ax using $\cdot ⊢ B : s$ . Every recursive call is on a proper premise of the original derivation, and the freshness condition follows from the theorem’s hypothesis. This exhausts the typing rules. ◻

Theorem 60.15 — Substitution ¶

If $Γ, x : A, Δ ⊢_{S} M : B and Γ ⊢_{S} N : A,$ then $Γ, Δ [N / x] ⊢_{S} M [N / x] : B [N / x] .$ The simultaneous substitution $Δ [N / x]$ acts on every declaration type.

Referenced from 5 locations

The Lambda Cube and Pure Type Systems

Proof of Theorem 60.15 — Substitution

Proof. The proof is by rule induction on the first derivation. Keep the second derivation fixed.

Variable cases. If the conclusion selects $x : A$ , substitution changes it to $N : A$ , which is the fixed second premise: a final Var selecting $x$ forces $Δ = \cdot$ . Moreover, lemma 60.11 gives $x \notin FV (A)$ , so $A [N / x] = A$ . If the conclusion selects a different declaration $y : C$ , the induction hypothesis for the derivation of $C : s$ gives $C [N / x] : s$ ; Var derives $y : C [N / x]$ in the substituted context.

Product case. The last rule has premises $Γ, x : A, Δ ⊢ C : s_{1}, Γ, x : A, Δ, y : C ⊢ D : s_{2},$ and $(s_{1}, s_{2}, s_{3}) \in R$ . Choose the representative with $y \notin FV (N) \cup {x} \cup dom (Γ, Δ) .$ The induction hypotheses give $Γ, Δ [N / x] ⊢ C [N / x] : s_{1}, Γ, Δ [N / x], y : C [N / x] ⊢ D [N / x] : s_{2} .$ Rule Prod yields the required product. The fresh choice gives $\prod_{y : C [N / x]} D [N / x] = (\prod_{y : C} D) [N / x] .$

Abstraction case. Use the same fresh choice for the bound variable $y$ . The induction hypotheses derive the substituted body and the substituted product. Rule Lam then derives $Γ, Δ [N / x] ⊢ λ (y : C [N / x]) . M_{0} [N / x] : \prod_{y : C [N / x]} D [N / x] .$

Application case. Suppose the final premises type $F : \prod_{y : C} D$ and $P : C$ . The induction hypotheses type $F [N / x]$ and $P [N / x]$ . Rule App gives the type $D [N / x] [P [N / x] / y] \overset{e q u a t i o n 60.2}{=} D [P / y] [N / x],$ where the representative has $y \notin FV (N) \cup {x}$ .

Weakening and conversion cases. A final Ax is impossible because the context of the first derivation contains the declaration $x : A$ . Suppose a final Weak appends $y : C$ . If $y \neq x$ , then the context has the form $Γ, x : A, Δ_{0}, y : C$ ; the two induction hypotheses type the weakened judgment and $C [N / x]$ , and Weak reconstructs the conclusion. If the appended declaration is $x : A$ , then $Δ$ is empty and the premise of Weak is the required target judgment. Indeed, lemma 60.11 gives $x \notin FV (M) \cup FV (B)$ , so $M [N / x] = M$ and $B [N / x] = B$ . For Conv, the induction hypotheses give the substituted typing and sort premises; lemma 60.13 gives $C [N / x] =_{β} D [N / x]$ , so Conv applies. These cases exhaust the typing rules. ◻

Exercise 60.3 ¶

★☆☆ Let $Γ$ be legal and contain $F : \prod_{y : A} D$ . Assume $Γ ⊢ A : s$ , $Γ ⊢ N : A$ , and $x \notin dom (Γ)$ , choosing $y \notin FV (N) \cup {x}$ . Instantiate theorem 60.15 with $M : = F x$ . Write the complete derivation of $F N : D [N / y]$ , including the weakening needed to type $F$ in the source context. Name the free-variable fact that simplifies the substituted result type. (Ten lines.)

Referenced from 3 locations

Lemma 60.16 — Generation ¶

Suppose the displayed judgment is derivable.

If $Γ ⊢ c : C$ , then $c : s \in A$ and $C =_{β} s$ for some $s \in S$ .
If $Γ ⊢ x : C$ , then $x : A \in Γ$ and $C =_{β} A$ for some $A$ with $Γ ⊢ A : s$ .
If $Γ ⊢ \prod_{x : A} B : C$ , then for some $(s_{1}, s_{2}, s_{3}) \in R$ , $Γ ⊢ A : s_{1}, Γ, x : A ⊢ B : s_{2}, C =_{β} s_{3} .$
If $Γ ⊢ λ (x : A) . M : C$ , then for some $B$ and $s$ , $Γ, x : A ⊢ M : B, Γ ⊢ \prod_{x : A} B : s, C =_{β} \prod_{x : A} B .$
If $Γ ⊢ F N : C$ , then for some $A, B$ , $Γ ⊢ F : \prod_{x : A} B, Γ ⊢ N : A, C =_{β} B [N / x] .$

The subscripts $S$ are suppressed in this statement.

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.16 — Generation

Proof. Follow the derivation upward past every final Weak or Conv; neither rule changes the subject. The first rule that constructs the subject must be Ax, Var, Prod, Lam, or App, respectively. Its premises give the displayed judgments. Each skipped Conv contributes one beta-equality, whose composite gives the asserted equality. For each skipped Weak, the constructing rule’s premises hold in a prefix $Γ_{0}$ of $Γ$ ; repeated applications of lemma 60.14 reinsert the declarations of $Γ ∖ Γ_{0}$ in their original order. The required sort premises are the declaration premises of those skipped Weak rules, equivalently the corresponding instances of lemma 60.10. This proves all five clauses. ◻

Lemma 60.17 — Correctness of types ¶

If $Γ ⊢_{S} M : A$ , then either $A \in S$ or there is a sort $s \in S$ such that $Γ ⊢_{S} A : s .$

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.17 — Correctness of types

Proof. Proceed by rule induction. Rule Ax concludes with the sort on the right, and Prod concludes with its result sort. The declaration-sort premise of Var gives the second alternative. In Weak, the induction hypothesis either says that the unchanged type is a sort or gives its sort derivation; in the second case, Weak extends that derivation.

The product premise of Lam gives the sort of its result type. In App, the function type is a product expression and therefore is not a sort constant. The induction hypothesis for the function premise must therefore give a sort derivation for that product. Generation applied to that derivation gives $Γ ⊢ A : s_{1}, Γ, x : A ⊢ B : s_{2} .$ The argument premise and theorem 60.15 therefore give $Γ ⊢ B [N / x] : s_{2}$ . Finally, the sort premise of Conv gives the second alternative directly. Notice that the Ax branch may end at a top sort with no classifier; this is why the statement has two alternatives. ◻

Lemma 60.18 — Confluence of beta-reduction on pseudo-terms ¶

For the pseudo-terms of definition 60.2, if $M ⟶_{β}^{*} N_{1}$ and $M ⟶_{β}^{*} N_{2}$ , then some pseudo-term $P$ satisfies $N_{1} ⟶_{β}^{*} P and N_{2} ⟶_{β}^{*} P .$ No typing hypothesis is required.

Referenced from 4 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.18 — Confluence of beta-reduction on pseudo-terms

Proof. Define $M par N$ , read as parallel reduction from $M$ to $N$ , by reflexivity on variables and constants, componentwise clauses for application, annotated abstraction, and product, and the contracting clause $\frac{A par A^{'} M par M^{'} N par N^{'}}{(λ (x : A) . M) N par M^{'} [N^{'} / x]} .$ The only binder side condition is the choice of an alpha-representative whose bound variable avoids the free variables of the substituted argument. Structural induction proves the substitution property $M par M^{'} \land N par N^{'} ⟹ M [N / x] par M^{'} [N^{'} / x] .$ The abstraction and product cases choose the same fresh representative on both sides; the variable, constant, and application cases are the defining clauses.

Define the complete development $M^{⋆}$ recursively by developing every component and contracting every redex visible in $M$ . Thus $((λ (x : A) . M) N)^{⋆} : = M^{⋆} [N^{⋆} / x],$ while a non-redex application develops its two components, and abstractions and products develop their annotations and bodies. Induction on a derivation of $M par N$ , using the substitution property in the contracting case, gives the triangle property $M par N ⟹ N par M^{⋆} .$ Hence parallel reduction is diamond. One beta-step is a parallel step, and every parallel step is a finite compatible beta-reduction, as induction on its derivation shows. Replacing the two finite beta-reductions by their parallel factorizations and using the diamond property proves the stated confluence. ◻

Corollary 60.19 — Church–Rosser ¶

If $M =_{β} N$ , then some $P$ satisfies $M ⟶_{β}^{*} P and N ⟶_{β}^{*} P .$

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Corollary 60.19 — Church–Rosser

Proof. Induct on the length of a reflexive, symmetric, transitive beta-conversion chain from $M$ to $N$ . The reflexive case chooses $P = M$ . For one more forward or backward beta segment, apply lemma 60.18 to the common endpoint obtained by the induction hypothesis. This tiles the new segment with a common reduct. ◻

Lemma 60.20 — Product compatibility ¶

If $\prod_{x : A} B =_{β} \prod_{x : A^{'}} B^{'}$ , then $A =_{β} A^{'}$ and $B =_{β} B^{'}$ .

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Lemma 60.20 — Product compatibility

Proof. By corollary 60.19, the two products reduce to a common expression $P$ . No beta-step removes an outer product constructor, so $P = \prod_{x : C} D$ for some $C, D$ . The left reductions give $A ⟶_{β}^{*} C$ and $B ⟶_{β}^{*} D$ ; the right reductions give $A^{'} ⟶_{β}^{*} C$ and $B^{'} ⟶_{β}^{*} D$ . The two beta-equalities follow. ◻

Subject reduction must account for reduction in a context declaration as well as reduction in the subject. The mutual statement makes that dependency explicit.

Theorem 60.21 — Subject reduction ¶

For every PTS specification $S$ :

if $Γ ⊢_{S} M : A$ and $M ⟶_{β} M^{'}$ , then $Γ ⊢_{S} M^{'} : A$ ;
if $Γ ⊢_{S} M : A$ and one declaration type in $Γ$ takes a beta-step, producing a legal context $Γ^{'}$ , then $Γ^{'} ⊢_{S} M : A$ .

Referenced from 5 locations

The Lambda Cube and Pure Type Systems

Proof of Theorem 60.21 — Subject reduction

Proof. Prove the two clauses simultaneously by rule induction on the typing derivation. For every proper premise derivation, the first induction hypothesis preserves its type after one compatible step in its subject. The second preserves the judgment after one declaration type in its context steps, provided the resulting context is legal. We display computation, product, abstraction, application, conversion, and context-extension cases.

Beta-redex. Suppose the final App has premises $Γ ⊢ λ (x : A_{0}) . M_{0} : \prod_{x : C} D, Γ ⊢ N : C,$ and its subject contracts to $M_{0} [N / x]$ . Generation for the abstraction gives a family $B$ and a sort $s$ such that $Γ, x : A_{0} ⊢ M_{0} : B, Γ ⊢ \prod_{x : A_{0}} B : s, \prod_{x : A_{0}} B =_{β} \prod_{x : C} D .$ Product compatibility gives $A_{0} =_{β} C$ and $B =_{β} D$ . Generation for the displayed product gives $Γ ⊢ A_{0} : s_{0}$ , so Conv derives $Γ ⊢ N : A_{0}$ . Substitution gives $Γ ⊢ M_{0} [N / x] : B [N / x] .$ The type $\prod_{x : C} D$ is not a sort, so lemma 60.17 applied to the function premise gives $Γ ⊢ \prod_{x : C} D : s^{'}$ . Generation and substitution with $Γ ⊢ N : C$ then give $Γ ⊢ D [N / x] : s_{D}$ . By lemma 60.13, $B [N / x] =_{β} D [N / x] (B =_{β} D) .$ Rule Conv, with the derived sort premise for $D [N / x]$ , restores the exact App result type.

Product formation. Suppose the final rule derives $Γ ⊢ \prod_{x : A} B : s_{3}$ . If $A ⟶_{β} A^{'}$ , the first induction hypothesis gives $Γ ⊢ A^{'} : s_{1}$ . Rule Var establishes that $Γ, x : A^{'}$ legal, so the second induction hypothesis changes the codomain premise to $Γ, x : A^{'} ⊢ B : s_{2}$ . Reapplying Prod gives $Γ ⊢ \prod_{x : A^{'}} B : s_{3} .$ If the step is in $B$ , the first induction hypothesis on the codomain premise followed by Prod gives the result. If a declaration in $Γ$ steps, the second induction hypothesis repairs both formation premises before Prod is reapplied.

Lambda annotation. Suppose $A ⟶_{β} A^{'}$ inside $λ (x : A) . M$ . The first induction hypothesis on the product premise changes $Γ ⊢ \prod_{x : A} B : s to Γ ⊢ \prod_{x : A^{'}} B : s .$ Generation of the latter judgment shows that $Γ, x : A^{'}$ is legal. The second mutual induction hypothesis therefore changes the body premise from $Γ, x : A ⊢ M : B$ to $Γ, x : A^{'} ⊢ M : B$ . Rule Lam derives $Γ ⊢ λ (x : A^{'}) . M : \prod_{x : A^{'}} B .$ Because $\prod_{x : A^{'}} B =_{β} \prod_{x : A} B$ , Conv restores the original type, using the original product premise as its required sort premise. Reduction in the body uses the first induction hypothesis under the freshly chosen binder.

For App, a step in the function is handled by the first induction hypothesis and reapplication of App. If the argument changes from $N$ to $N^{'}$ , the first induction hypothesis and App derive $Γ ⊢ F N^{'} : B [N^{'} / x]$ . Correctness of types for $F : \prod_{x : A} B$ , followed by generation and substitution with $N : A$ , gives $Γ ⊢ B [N / x] : s_{B}$ . Since $B [N^{'} / x] =_{β} B [N / x]$ , Conv restores the stated type. Rules Ax and Var have no principal redex in the subject-reduction clause.

For the context-reduction clause, Var has one additional principal case. Suppose its selected declaration changes from $x : C$ to $x : C^{'}$ with $C ⟶_{β} C^{'}$ . Subject reduction on the declaration-sort premise gives $Θ ⊢ C^{'} : s$ . Hence Var gives $Θ, x : C^{'} ⊢ x : C^{'}$ . Weakening the old sort derivation $Θ ⊢ C : s$ across $x : C^{'}$ gives $Θ, x : C^{'} ⊢ C : s$ , and Conv, using $C^{'} =_{β} C$ , restores $Θ, x : C^{'} ⊢ x : C .$ If the changed declaration is earlier than the selected one, the mutual induction hypothesis first repairs the selected declaration’s sort premise and Var is reapplied. For a final Weak, distinguish a change in its newly appended declaration from a change in its prefix. In the former case subject reduction repairs its declaration-sort premise; in the latter the mutual induction hypotheses repair both premises. Rule Ax has empty context. For clause 1, Weak applies the first induction hypothesis to its typing premise and reattaches the unchanged declaration. Rule Conv applies the first induction hypothesis to its typing premise and, if the step is in the chosen result type, to its sort premise before reapplying conversion. For clause 2, both rules use the second induction hypothesis on every premise with the changed context. These cases exhaust compatible beta-reduction in subjects and contexts. ◻

Corollary 60.22 — Legality under declaration reduction ¶

Suppose $Γ$ is legal and one declaration type in $Γ$ takes a beta-step, producing $Γ^{'}$ . Then $Γ^{'}$ is legal. Moreover, $Γ ⊢_{S} M : A ⟹ Γ^{'} ⊢_{S} M : A .$

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

Proof of Corollary 60.22 — Legality under declaration reduction

Proof. Write $Γ = Θ, x : C, Δ, Γ^{'} = Θ, x : C^{'}, Δ, C ⟶_{β} C^{'} .$ Context validity gives $Θ ⊢ C : s$ , and the first clause of theorem 60.21 gives $Θ ⊢ C^{'} : s$ . Hence $Θ, x : C^{'}$ is legal.

Proceed from left to right through the declarations of $Δ$ . Suppose the target prefix constructed so far is legal. Context validity gives a sort derivation for the next declaration type in the corresponding source prefix. The second clause of theorem 60.21, applied to that derivation and the legal target prefix, gives the same declaration-sort judgment in the target prefix. Appending it preserves legality. Induction on the length of $Δ$ proves that $Γ^{'}$ is legal. The second clause of theorem 60.21 now gives the final implication. ◻

Exercise 60.4 ¶

★★☆ Complete the App argument-reduction case in the subject-reduction proof. If $N ⟶_{β} N^{'}$ , derive the type $B [N^{'} / x]$ of $F N^{'}$ and then derive the original type $B [N / x]$ . Put the reason for the final conversion on the equality step. (Half a page.)

Referenced from 3 locations

Normalization and decisions belong to instances

The rules of definition 60.3 also describe specifications with $* : *$ . Structural uniformity therefore cannot imply normalization.

Theorem 60.23 — Strong normalization of the lambda cube ¶

For each of the eight systems $λ_{I}$ of definition 60.5, if $Γ ⊢_{λ_{I}} M : A$ , then every compatible beta-reduction sequence from $M$ , $A$ , or a declaration type in $Γ$ is finite.

Referenced from 6 locations

Proof of Theorem 60.23 — Strong normalization of the lambda cube

Proof. This is the exact strong-normalization theorem for the lambda cube proved by Barendregt, [Bar92]. Its proof interprets the strongest vertex $λ_{C}$ in a marked calculus, proves normalization of the marked constructors and objects, and transfers the result to every subsystem. The import applies here because definition 60.5 has the same sorts, axiom, four product triples, compatible beta-reduction, and Church-style typing rules. No claim about an arbitrary triple $(S, A, R)$ is imported. ◻

The schema itself admits the one-sort specification $S = {*}, A = {* : *}, R = {(*, *, *)} .$ It is not a lambda-cube vertex. Its circular axiom invalidates the reducibility construction used by the theorem.

Theorem 60.24 — Girard's boundary for the one-sort PTS ¶

In the displayed one-sort specification there is a closed term $G$ such that $\cdot ⊢ G : \prod_{A : *} A .$ Consequently every type of sort $*$ is inhabited. In addition, some typable term has no beta-normal form. Thus the specification is logically inconsistent under propositions-as-types and is not strongly normalizing.

Referenced from 3 locations

The Lambda Cube and Pure Type Systems

Proof of Theorem 60.24 — Girard's boundary for the one-sort PTS

Proof. This is the contraction to $λ *$ of Girard’s paradox, imported with the exact one-sort signature from [Bar92]. The contraction from Girard’s system $λ U$ to $λ *$ preserves the displayed inhabitation result; the same corollary separately states that $λ *$ has typable terms without normal form. We do not use Proposition 5.2.31, whose hypothesis requires an extension of $λ_{2}$ . No claim about a different $* : *$ specification is imported. ◻

Definition 60.25 — Functional and lookup-effective specifications ¶

A PTS specification is functional when each constant has at most one axiom sort and every pair $(s_{1}, s_{2})$ has at most one product-result sort $s_{3}$ . It is lookup-effective when equality of constants and sorts is decidable and there are total computable procedures $\begin{aligned} isSort & : C \to Bool, \\ axiomSort & : C \to Option (S), \\ productSort & : S \times S \to Option (S) \end{aligned}$ such that $isSort (c)$ is true exactly when $c \in S$ , $axiomSort (c) = some (s)$ exactly when $(c, s) \in A$ , and $productSort (s_{1}, s_{2}) = some (s_{3})$ exactly when $(s_{1}, s_{2}, s_{3}) \in R$ . Every lookup-effective specification is functional: the last two biconditionals imply uniqueness because each procedure returns at most one option value.

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

The partition $V = ⋃_{s} V_{s}$ and the side conditions on Var and Weak are exactly the naming convention of Barendregt’s Section 5.2 presentation. Consequently the uniqueness and decidability results cited below apply to the displayed rules directly; no erasure or renaming transfer is being assumed.

Lemma 60.26 — Uniqueness of types modulo beta ¶

If $S$ is functional, $Γ ⊢_{S} M : A$ , and $Γ ⊢_{S} M : B$ , then $A =_{β} B$ .

Referenced from 5 locations

Proof of Lemma 60.26 — Uniqueness of types modulo beta

Proof. This is Barendregt’s uniqueness lemma for functional PTSs [Bar92]; our functionality and typing rules are its hypotheses. Its induction is on the structure of the common subject $M$ , not on either derivation. Apply lemma 60.16 to both derivations. Constants and variables select the same axiom or context declaration; products use functionality after their domain and codomain sorts have been identified; applications use lemma 60.20 and lemma 60.13; abstractions use generation on both bodies. Final Weak and Conv steps have already been absorbed by generation. This yields $A =_{β} B$ without a context-condensing premise. ◻

Theorem 60.27 — Conditional decidable checking ¶

Let $S$ be lookup-effective and let $S$ be finite. Assume every legal expression is strongly beta-normalizing. There is a total computable procedure that, on input finite encodings of $Γ$ , $M$ , and $A$ , decides whether $Γ ⊢_{S} M : A$ is derivable. Consequently, type checking is decidable at every lambda-cube vertex.

Referenced from 3 locations

Proof of Theorem 60.27 — Conditional decidable checking

Proof. The imported result is Corollary 5.2.18 of Barendregt’s treatment [Bar92]. Here is the decision procedure under our more explicit effectiveness hypotheses. First validate the context from left to right. For each declaration, recursively synthesize an actual sort for its type, then extend the already validated prefix; an untyped top sort cannot be a declaration type. On terms, synthesize by the outer constructor. Constants and variables use the two finite lookups. A product synthesizes sorts for its domain and codomain and consults $productSort$ . An abstraction first classifies its annotation, synthesizes its body in the extended context, and consults the same product table for the type thereby assembled. An application synthesizes its function, normalizes that already legal type to product form, checks the argument against the domain, and returns the substituted codomain. Checking first synthesizes, validates the proposed type as either a sort itself or an expression having a synthesized sort, and then compares the two types modulo beta. The terminal “is a sort” alternative is needed here because a derivable right-hand side may be the untyped top sort; it is not used when validating context declarations or binder annotations.

This mutual synthesis-and-classification procedure recurses on proper raw subterms. Its only subsidiary computation is normalization of expressions already established to be legal, which terminates by hypothesis; beta confluence from lemma 60.18 makes comparison of their normal forms decisive. Soundness rebuilds the rules of definition 60.3. Generation proves completeness constructor by constructor, product compatibility handles the application case, and lemma 60.26 proves completeness of the final conversion test. Thus the paragraph supplies a syntax-directed reconstruction of the corollary, not an attribution of this algorithm to one of the source’s intermediate lemmas.

Barendregt attributes the unprinted proof of the corollary to van Benthem Jutting’s method for the preceding condensing lemma; the statement of that lemma is not an algorithm or a termination measure. The source also leaves effective access to $A$ and $R$ implicit. Our lookup-effective hypothesis makes those finite decisions explicit.

Each cube system has finite lookup tables, and theorem 60.23 discharges the normalization hypothesis. ◻

Functionality is used only in completeness of synthesis. Without it, one subject may have two non-convertible product sorts, so an algorithm returning a single inferred type need not find the requested derivation. A finite search algorithm can still decide some nonfunctional specifications, but that is a different theorem. The normalization hypothesis is essential: type checking for the one-sort system $λ *$ is undecidable [Bar92].

Exercise 60.5 ¶

★★☆ Construct a finite PTS with sorts $s_{0}, s_{1}, s_{2}, s_{3}$ , decidable membership in its three specification sets, and two triples $(s_{0}, s_{1}, s_{2})$ and $(s_{0}, s_{1}, s_{3})$ such that one product receives both $s_{2}$ and $s_{3}$ . Identify the exact step of lemma 60.26 that fails. Do not use $s : s$ . (Half a page.)

Referenced from 3 locations

The boundary of the classification

Proposition 60.28 — What a cube placement does not establish ¶

For a PTS specification $S$ , the data $(S, A, R)$ and a derivation $Γ ⊢_{S} M : A$ establish only formation and typing by the PTS rules. They do not, without separate rules and proofs, establish:

adequacy of an encoding of another syntax or logic;
formation or elimination principles for inductive or indexed families;
an intensional identity type and its path-induction eliminator;
a cumulative hierarchy of Martin–Löf universes or large elimination;
a particular judgmental computation discipline beyond beta-conversion;
normalization, consistency, canonicity, or decidable checking for an arbitrary PTS specification.

Referenced from 2 locations

The Lambda Cube and Pure Type Systems

Proof of Proposition 60.28 — What a cube placement does not establish

Proof. The conclusion is about what follows from the displayed signature, not about what can be encoded by its terms. For example, an impredicative vertex may form Church data or Leibniz equality, but the PTS rules give those encodings no primitive induction rule, large eliminator, or judgmental computation rule beyond beta. Establishing that an encoding represents exactly the intended objects and eliminations is a separate adequacy theorem.

Likewise, neither $A$ nor $R$ contains induction constructors, an identity eliminator, or universe levels. Such rules must be added to a larger signature and their metatheory proved there. Theorem 60.24 separates the arbitrary PTS schema from the normalizing cube instances of theorem 60.23. Hence the last group of properties also requires instance hypotheses rather than cube placement alone. ◻

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 60.6, then complete exercise 60.9.

Exercise 60.6 ¶

★★☆ Choose one term witnessing each of the three optional cube axes. Give its complete PTS derivation, then delete the corresponding product triple and prove by generation that the term is no longer typable at that vertex.

Referenced from 4 locations

Exercise 60.7 ¶

★★☆ Reconstruct the beta-redex case of subject reduction without suppressing the types $A_{0}, A, B, C, D$ . Mark the uses of product compatibility, conversion, and substitution. Then give a malformed variant obtained by deleting the sort premise from Conv and identify the presupposition that fails.

Referenced from 3 locations

Exercise 60.8 ¶

★★☆ Compare $λ_{C}$ with the one-sort system $* : *$ at the level of specifications. Exhibit the common product rule and the differing axiom, and explain why inclusion in the PTS schema transfers theorem 60.15 but not theorem 60.23.

Referenced from 3 locations

Exercise 60.9 ¶

★★★ Practical project.pts-cube-checker Implement in Agda or Kappa two bounded entry points. The first checks the finite, beta-normal fragment of the lambda-cube specifications in definition 60.3; the second admits one declared conversion stage in which visible type redexes are developed once. Globally fresh numeric binder names may stand for alpha-classes; state and check that invariant on every input, and use alpha-aware structural comparison for the beta-normal entry point. Preserve the invariant that every synthesized right-hand side is either a sort or has a derived sort. The program must print a trace annotated by the product triple used at each binder. It must accept the polymorphic identity of example 60.4 in $λ_{2}$ , reject it in $λ_{\to}$ at the outer product, accept the second product of exercise 60.2 in $λ_{2 ω}$ , and reject the family declaration $Vec : \prod_{n : Nat} *$ required by the third product when $r_{P}$ is absent. Finally, admit one redex in a type, develop it, and accept an application whose argument type agrees with its domain only after that conversion. These five outcomes are the decidable acceptance test.

Referenced from 6 locations

Sources. The PTS specification, generation and substitution arguments, subject reduction, cube vertices, and instance normalization theorem follow the exact systems in [Bar92]. A modern derivational route through the cube is given by [NG14, Geu09]. These references provide provenance and the imported strong-normalization theorem; the structural proofs used in this chapter are printed above. Barendregt’s earlier generalized-type- system paper gives the historical three-part specification and cube classification [Bar91]; its displayed rule sheet is not substituted for the 1992 PTS rules fixed in definition 60.3.

A bounded strength comparison.

Setzer analyzes Martin–Löf type theory with one universe and W-types, not a PTS or the Calculus of Constructions. For ${ML}_{J}$ , ${ML}_{[T D]}$ , and their two auxiliary presentations, Theorem 4.41 proves transfinite induction below $ψ_{Ω_{1}} (Ω_{I + n})$ for every $n \in N$ . Corollary 4.42 then includes the stated extensional extension and uses the separately cited upper bound to obtain the exact ordinal $ψ_{Ω_{1}} (Ω_{I + ω})$ , where $I$ belongs to the paper’s notation system. The theorem and corollary cover the named intensional and extensional presentations. Setzer’s abstract separately states the same strength for the Tarski- and Russell-style universe presentations [Set98]. The well-ordering construction is not reproduced here, and no book result depends on it.