ch:simple-types: ch:simple-types

The inserted conditional has free variable $y$, so rename the displayed binder to a fresh $u$ before substituting: The two displayed occurrences of $y$, one in each inserted copy, are free; the binder binds only $u$.

For the second term, the binder shadows the substitution variable. The stopping equation for substitution therefore gives $$(\lambda x:\mathbf{2}.x)[\mathsf{tt}/x]=\lambda x:\mathbf{2}.x,$$ not $\lambda x:\mathbf{2}.\mathsf{tt}$. Substitution replaces free occurrences only.

Let $\mathrm{\Gamma }=x:\mathbf{2},y:\mathbf{2}$. The full derivation for $\mathit{or}$ is $$\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(x:\mathbf{2})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{\mathrm{\Gamma }⊢\mathsf{tt}:\mathbf{2}}}\mathrm{True}\\ {\displaystyle \frac{(y:\mathbf{2})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢y:\mathbf{2}}}\mathrm{Var}\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(x;\mathsf{tt};y):\mathbf{2}}}\mathrm{If}}{x:\mathbf{2}⊢\lambda y:\mathbf{2}.\mathsf{if}(x;\mathsf{tt};y):\mathbf{2}\to \mathbf{2}}}\mathrm{Lam}}{\cdot ⊢\mathit{or}:\mathbf{2}\to \mathbf{2}\to \mathbf{2}}\mathrm{Lam}.$$

Take $$\mathit{xor}:=\lambda x:\mathbf{2}.\lambda y:\mathbf{2}.\mathsf{if}(x;\mathsf{if}(y;\mathsf{ff};\mathsf{tt});y).$$ Its body derivation is the complete tree $$\mathcal{X}=\frac{\begin{array}{c}{\displaystyle \frac{(x:\mathbf{2})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(y:\mathbf{2})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢y:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{\mathrm{\Gamma }⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\\ {\displaystyle \frac{\phantom{X}}{\mathrm{\Gamma }⊢\mathsf{tt}:\mathbf{2}}}\mathrm{True}\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(y;\mathsf{ff};\mathsf{tt}):\mathbf{2}}}\mathrm{If}\\ {\displaystyle \frac{(y:\mathbf{2})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢y:\mathbf{2}}}\mathrm{Var}\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(x;\mathsf{if}(y;\mathsf{ff};\mathsf{tt});y):\mathbf{2}}\mathrm{If}.$$ The two abstraction nodes complete the typing derivation: $$\frac{{\displaystyle \frac{\mathcal{X}}{x:\mathbf{2}⊢\lambda y:\mathbf{2}.\mathsf{if}(x;\mathsf{if}(y;\mathsf{ff};\mathsf{tt});y):\mathbf{2}\to \mathbf{2}}}\mathrm{Lam}}{\cdot ⊢\mathit{xor}:\mathbf{2}\to \mathbf{2}\to \mathbf{2}}\mathrm{Lam}.$$

Any typing of $\mathsf{if}(\lambda x:\mathbf{2}.x;\mathsf{tt};\mathsf{ff})$ must end in If. Its guard premise would require $$\mathrm{\Gamma }⊢\lambda x:\mathbf{2}.x:\mathbf{2}.$$ But the only final rule for an abstraction is Lam, whose result type is an arrow, here $\mathbf{2}\to \mathbf{2}$, never $\mathbf{2}$. Thus the guard premise fails.

Any typing of $\mathsf{ff}(\lambda x:\mathbf{2}.x)$ must end in App. Its function premise requires $\mathrm{\Gamma }⊢\mathsf{ff}:A\to C$ for some $A,C$. The only final rule for $\mathsf{ff}$ is False, which assigns $\mathbf{2}$, not an arrow. Hence that premise fails in every context.

Renaming the three variable leaves and rebuilding the conditional gives $$\frac{\begin{array}{c}{\displaystyle \frac{(y:\mathbf{2})\in y:\mathbf{2}}{y:\mathbf{2}⊢y:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{(y:\mathbf{2})\in y:\mathbf{2}}{y:\mathbf{2}⊢y:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{y:\mathbf{2}⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\end{array}}{y:\mathbf{2}⊢\mathsf{if}(y;y;\mathsf{ff}):\mathbf{2}}\mathrm{If}.$$ Every node is the image of the corresponding node in the original tree.

The premise in example 2.6 is displayed under $x:\mathbf{2}$. Renaming $x$ to fresh $u$ gives $$\frac{\begin{array}{c}{\displaystyle \frac{u:\mathbf{2}\in u:\mathbf{2}}{u:\mathbf{2}⊢u:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{u:\mathbf{2}⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\\ {\displaystyle \frac{\phantom{X}}{u:\mathbf{2}⊢\mathsf{tt}:\mathbf{2}}}\mathrm{True}\end{array}}{u:\mathbf{2}⊢\mathsf{if}(u;\mathsf{ff};\mathsf{tt}):\mathbf{2}}\mathrm{If}.$$ Applying Lam produces $\lambda u:\mathbf{2}.\mathsf{if}(u;\mathsf{ff};\mathsf{tt})$, which is alpha-equivalent to the original $\lambda x:\mathbf{2}.\mathsf{if}(x;\mathsf{ff};\mathsf{tt})$.

Let $a=\mathsf{if}(\mathsf{tt};\mathsf{ff};\mathsf{tt})$. The two premise derivations for typed substitution are $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{x:\mathbf{2}\in x:\mathbf{2},y:\mathbf{2}}{x:\mathbf{2},y:\mathbf{2}⊢x:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{y:\mathbf{2}\in x:\mathbf{2},y:\mathbf{2}}{x:\mathbf{2},y:\mathbf{2}⊢y:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{x:\mathbf{2},y:\mathbf{2}⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\end{array}}{x:\mathbf{2},y:\mathbf{2}⊢\mathsf{if}(x;y;\mathsf{ff}):\mathbf{2}}}\mathrm{If}}{x:\mathbf{2}⊢\lambda y:\mathbf{2}.\mathsf{if}(x;y;\mathsf{ff}):\mathbf{2}\to \mathbf{2}}\mathrm{Lam},$$ and $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\cdot ⊢\mathsf{tt}:\mathbf{2}}}\mathrm{True}\\ {\displaystyle \frac{\phantom{X}}{\cdot ⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\\ {\displaystyle \frac{\phantom{X}}{\cdot ⊢\mathsf{tt}:\mathbf{2}}}\mathrm{True}\end{array}}{\cdot ⊢a:\mathbf{2}}\mathrm{If}.$$ Weakening the second tree inserts $y:\mathbf{2}$, giving the same If tree with all three constant conclusions under $y:\mathbf{2}$; call it ${\mathcal{A}}_y:y:\mathbf{2}⊢a:\mathbf{2}$. Substitution replaces the first guard leaf, while the $y$-leaf and false branch remain: $$\frac{{\displaystyle \frac{\begin{array}{c}{\mathcal{A}}_y\\ {\displaystyle \frac{y:\mathbf{2}\in y:\mathbf{2}}{y:\mathbf{2}⊢y:\mathbf{2}}}\mathrm{Var}\\ {\displaystyle \frac{\phantom{X}}{y:\mathbf{2}⊢\mathsf{ff}:\mathbf{2}}}\mathrm{False}\end{array}}{y:\mathbf{2}⊢\mathsf{if}(a;y;\mathsf{ff}):\mathbf{2}}}\mathrm{If}}{\cdot ⊢\lambda y:\mathbf{2}.\mathsf{if}(a;y;\mathsf{ff}):\mathbf{2}\to \mathbf{2}}\mathrm{Lam}.$$ The first premise of the rebuilt If is precisely the weakened inserted derivation.

For guard congruence, typing inversion and the induction hypothesis transform the tree as follows: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e:\mathbf{2}\\ \mathrm{\Gamma }⊢e_1:C\\ \mathrm{\Gamma }⊢e_2:C\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(e;e_1;e_2):C}\mathrm{If}$$ When $e⟼e^{\prime }$, the induction hypothesis changes the first premise and the rebuilt tree is $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e^{\prime }:\mathbf{2}\\ \mathrm{\Gamma }⊢e_1:C\\ \mathrm{\Gamma }⊢e_2:C\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(e^{\prime };e_1;e_2):C}\mathrm{If}.$$ All three premises of the rebuilt rule are displayed.

For the two root contractions, inversion already contains the selected branch: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\mathsf{tt}:\mathbf{2}\\ \boxed{{\displaystyle \mathrm{\Gamma }⊢e_1:C}}\\ \mathrm{\Gamma }⊢e_2:C\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(\mathsf{tt};e_1;e_2):C}\mathrm{If}⇝\boxed{\mathrm{\Gamma }⊢e_1:C},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\mathsf{ff}:\mathbf{2}\\ \mathrm{\Gamma }⊢e_1:C\\ \boxed{{\displaystyle \mathrm{\Gamma }⊢e_2:C}}\end{array}}{\mathrm{\Gamma }⊢\mathsf{if}(\mathsf{ff};e_1;e_2):C}\mathrm{If}⇝\boxed{\mathrm{\Gamma }⊢e_2:C}.$$ Both arrows are metalevel transformations of derivation trees, not term steps. Thus every conditional rule preserves the result type $C$.

The complete derivation is the zero-premise introduction instance $$\frac{\phantom{X}}{x:A⊢\star :\mathbf{1}}\mathrm{Unit}-\mathrm{I}.$$ If a closed value $v$ has type $\mathbf{1}$, inspect its value form and invert its typing. A lambda has an arrow type, a Boolean has type $\mathbf{2}$, a pair has a product type, and an injection has a sum type. Disjointness of type constructors excludes all four possibilities, leaving $v=\star$.

For $A\mathsf{type}$, the required derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{(x:\mathbf{0})\in (x:\mathbf{0},y:A)}{x:\mathbf{0},y:A⊢x:\mathbf{0}}}\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}A\mathsf{type}\\ {\displaystyle \frac{\phantom{X}}{\mathbf{2}\mathsf{type}}}\mathrm{Ty}-\mathrm{Bool}\end{array}}{A\times \mathbf{2}\mathsf{type}}}\mathrm{Ty}-\mathrm{Prod}\end{array}}{x:\mathbf{0},y:A⊢{\mathsf{abort}}_{A\times \mathbf{2}}(x):A\times \mathbf{2}}\mathrm{Empty}-\mathrm{E}.$$ Abort is not a value form. Its only evaluation rule is E-Abort, whose premise would require a step from the variable $x$; no evaluation rule has a variable source. Hence this open neutral term has no root or congruence step.

Recall $\mathsf{Color}=\mathbf{1}+(\mathbf{1}+\mathbf{1})$, with red the outer left injection, amber the outer-right/inner-left injection, and green the outer-right/inner-right injection. Abbreviate $$K(u):=\mathsf{case}(u;a.\mathsf{red};g.\mathsf{amber}),L(c):=\mathsf{case}(c;r.\mathsf{green};u.K(u)),$$ and define $\mathit{next}:=\lambda c:\mathsf{Color}.L(c)$. For any context $\mathrm{\Theta }$, let ${\mathcal{R}}_{\mathrm{\Theta }}$, ${\mathcal{A}}_{\mathrm{\Theta }}$, and ${\mathcal{G}}_{\mathrm{\Theta }}$ be the following complete constructor derivations. Here $\mathcal{U}$ is the axiom $\mathbf{1}\mathsf{type}$, while $\mathcal{S}$ is Ty-Sum applied to two copies of $\mathcal{U}$, deriving $\mathbf{1}+\mathbf{1}\mathsf{type}$: $${\mathcal{R}}_{\mathrm{\Theta }}=\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\mathrm{\Theta }⊢\star :\mathbf{1}}}\mathrm{Unit}-\mathrm{I}\\ \mathcal{S}\end{array}}{\mathrm{\Theta }⊢\mathsf{red}:\mathsf{Color}}\mathrm{Inl},$$ $${\mathcal{A}}_{\mathrm{\Theta }}=\frac{\begin{array}{c}\mathcal{U}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{\mathrm{\Theta }⊢\star :\mathbf{1}}}\mathrm{Unit}-\mathrm{I}\\ \mathcal{U}\end{array}}{\mathrm{\Theta }⊢\mathsf{inl}(\star ):\mathbf{1}+\mathbf{1}}}\mathrm{Inl}\end{array}}{\mathrm{\Theta }⊢\mathsf{amber}:\mathsf{Color}}\mathrm{Inr},$$ and $${\mathcal{G}}_{\mathrm{\Theta }}=\frac{\begin{array}{c}\mathcal{U}\\ {\displaystyle \frac{\begin{array}{c}\mathcal{U}\\ {\displaystyle \frac{\phantom{X}}{\mathrm{\Theta }⊢\star :\mathbf{1}}}\mathrm{Unit}-\mathrm{I}\end{array}}{\mathrm{\Theta }⊢\mathsf{inr}(\star ):\mathbf{1}+\mathbf{1}}}\mathrm{Inr}\end{array}}{\mathrm{\Theta }⊢\mathsf{green}:\mathsf{Color}}\mathrm{Inr}.$$ Put $\mathrm{\Gamma }=c:\mathsf{Color}$ and $\mathrm{\Delta }=\mathrm{\Gamma },u:\mathbf{1}+\mathbf{1}$. These constructor trees make every premise in the typing derivation explicit: $$\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(c:\mathsf{Color})\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢c:\mathsf{Color}}}\mathrm{Var}\\ {\mathcal{G}}_{\mathrm{\Gamma },r:\mathbf{1}}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(u:\mathbf{1}+\mathbf{1})\in \mathrm{\Delta }}{\mathrm{\Delta }⊢u:\mathbf{1}+\mathbf{1}}}\mathrm{Var}\\ {\mathcal{R}}_{\mathrm{\Delta },a:\mathbf{1}}\\ {\mathcal{A}}_{\mathrm{\Delta },g:\mathbf{1}}\end{array}}{\mathrm{\Delta }⊢K(u):\mathsf{Color}}}\mathrm{Case}\end{array}}{\mathrm{\Gamma }⊢L(c):\mathsf{Color}}}\mathrm{Case}}{\cdot ⊢\mathit{next}:\mathsf{Color}\to \mathsf{Color}}\mathrm{Lam}.$$

The reductions are The first step of each line is beta; the remaining steps are the appropriate case contractions.

For the right contraction, inversion of the typing derivation before the step gives $$\mathrm{\Gamma }⊢\mathsf{inr}(v):A+B,\mathrm{\Gamma },x:A⊢e_1:C,\mathrm{\Gamma },y:B⊢e_2:C.$$ Inverting the injection premise gives $\mathrm{\Gamma }⊢v:B$. The source of the complete derivation transformation is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}A\mathsf{type}\\ \mathrm{\Gamma }⊢v:B\end{array}}{\mathrm{\Gamma }⊢\mathsf{inr}(v):A+B}}\mathrm{Inr}\\ \mathrm{\Gamma },x:A⊢e_1:C\\ \mathrm{\Gamma },y:B⊢e_2:C\end{array}}{\mathrm{\Gamma }⊢\mathsf{case}(\mathsf{inr}(v);x.e_1;y.e_2):C}\mathrm{Case}.$$ Its target is $$\frac{\begin{array}{c}\mathrm{\Gamma },y:B⊢e_2:C\\ \mathrm{\Gamma }⊢v:B\end{array}}{\mathrm{\Gamma }⊢e_2[v/y]:C}\mathrm{Substitution}.$$ This is a metalevel transformation of derivation trees, not a term evaluation step. For scrutinee congruence, inversion gives $\mathrm{\Gamma }⊢e:A+B$ and the same two branch premises. The induction hypothesis changes the first premise to $\mathrm{\Gamma }⊢e^{\prime }:A+B$; reapplying Case yields $\mathrm{\Gamma }⊢\mathsf{case}(e^{\prime };x.e_1;y.e_2):C$.

Let $a=(\lambda y.y)\mathsf{tt}$. Call by value evaluates the argument first: $$(\lambda x.xx)a{⟼}_{\mathrm{v}}(\lambda x.xx)\mathsf{tt}{⟼}_{\mathrm{v}}\mathsf{tt}\mathsf{tt}.$$ The endpoint is stuck because its function is a boolean value rather than an abstraction.

Call by name substitutes the unevaluated argument twice and then evaluates the function position: $$(\lambda x.xx)a{⟼}_{\mathrm{n}}aa{⟼}_{\mathrm{n}}\mathsf{tt}a.$$ This endpoint is stuck; call by name has no context that evaluates the argument after a nonlambda function has become final.

If $x:X$ typed $xx:C$, App would require the function occurrence to have $D\to C$ and the argument occurrence to have $D$. Both occurrences refer to the same declaration, so uniqueness of types gives $X=D\to C$ and $X=D$, hence $D=D\to C$. No finite type tree is equal to a proper arrow tree containing itself as a subtree, so no simple type solves these equations.

Put $F=A\Rightarrow B$, $G=B\Rightarrow C$, $T=F\Rightarrow G\Rightarrow (A\Rightarrow C)$, and $\mathrm{\Delta }=f:F,g:G,x:A$. The complete natural-deduction tree is $$\frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{g:G\in \mathrm{\Delta }}{\mathrm{\Delta }{⊢}_{\mathsf{N}}G}}\mathrm{Hyp}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{f:F\in \mathrm{\Delta }}{\mathrm{\Delta }{⊢}_{\mathsf{N}}F}}\mathrm{Hyp}\\ {\displaystyle \frac{x:A\in \mathrm{\Delta }}{\mathrm{\Delta }{⊢}_{\mathsf{N}}A}}\mathrm{Hyp}\end{array}}{\mathrm{\Delta }{⊢}_{\mathsf{N}}B}}\end{array}}{\mathrm{\Delta }{⊢}_{\mathsf{N}}C}}}{f:F,g:G{⊢}_{\mathsf{N}}A\Rightarrow C}}}{f:F{⊢}_{\mathsf{N}}G\Rightarrow (A\Rightarrow C)}}}{\cdot {⊢}_{\mathsf{N}}T}.$$ Decorating the three Hyp leaves by variables, the two elimination nodes by App, and the three discharge nodes by Lam gives the complete typing tree for $$\lambda f:A\to B.\lambda g:B\to C.\lambda x:A.g(fx).$$ Every node in this arrow-only example has the corresponding typing node and there are no extra formation premises. Skeleton erasure therefore recovers the displayed natural-deduction tree node for node.

Let $F$ be the proof term from example 2.35. The injection $\mathsf{inl}(a)$ has type $A+B$ because $a:A$ and $B$ is a formed type. Write $p_0=(f,g)$. Compatible proof reduction gives The first beta step occurs compatibly in function position of the outer application. The second is the outer application itself. Subject reduction assigns type $C$ to every displayed line: $f:A\to C$, $g:B\to C$, and $a:A$ are unchanged throughout.

Suppose $e\in {\mathcal{R}}_{A\times B}$ and $e{⟶}_{\mathsf{p}}{e}^{\prime }$. By definition, $\mathsf{fst}(e)\in {\mathcal{R}}_A$ and $\mathsf{snd}(e)\in {\mathcal{R}}_B$. The proof contexts $\mathsf{fst}([-])$ and $\mathsf{snd}([-])$ give $$\mathsf{fst}(e){⟶}_{\mathsf{p}}\mathsf{fst}(e^{\prime }),\mathsf{snd}(e){⟶}_{\mathsf{p}}\mathsf{snd}(e^{\prime }).$$ Reduction closure at $A$ and $B$ gives both defining conditions for $e^{\prime }\in {\mathcal{R}}_{A\times B}$.

Now let $a\in {\mathcal{R}}_A$ and $b\in {\mathcal{R}}_B$. Saturation clause 1 makes both strongly normalizing. The root contractions $$\mathsf{fst}((a,b)){⟶}_{\mathsf{p}}a,\mathsf{snd}((a,b)){⟶}_{\mathsf{p}}b$$ have reducible contracta and strongly normalizing proper arguments. Principal expansion makes the two projections reducible, and the product clause gives $(a,b)\in {\mathcal{R}}_{A\times B}$.

The two identity derivations are $$\frac{{\displaystyle \frac{(x:\mathbf{2})\in x:\mathbf{2}}{x:\mathbf{2}⊢x:\mathbf{2}}}\mathrm{Var}}{\cdot ⊢{\mathit{id}}_{\mathbf{2}}:\mathbf{2}\to \mathbf{2}}\mathrm{Lam},$$ and $$\frac{{\displaystyle \frac{(x:\mathbf{1})\in x:\mathbf{1}}{x:\mathbf{1}⊢x:\mathbf{1}}}\mathrm{Var}}{\cdot ⊢{\mathit{id}}_{\mathbf{1}}:\mathbf{1}\to \mathbf{1}}\mathrm{Lam}.$$ One term using each twice is $$(({\mathit{id}}_{\mathbf{2}}\mathsf{tt},{\mathit{id}}_{\mathbf{2}}\mathsf{ff}),({\mathit{id}}_{\mathbf{1}}\star ,{\mathit{id}}_{\mathbf{1}}\star )),$$ of type $(\mathbf{2}\times \mathbf{2})\times (\mathbf{1}\times \mathbf{1})$.

If one simply typed variable $i$ replaced both definitions, its boolean uses would require $i:\mathbf{2}\to \mathbf{2}$, while its unit uses would require $i:\mathbf{1}\to \mathbf{1}$. Uniqueness of typing for a variable in a fixed context would identify these two arrow types, and arrow injectivity would then give $\mathbf{2}=\mathbf{1}$, impossible. A single monomorphic declaration cannot serve both uses.

Extend the old evaluation contexts by The side metavariable $v$ ranges over values. The new basic redexes are the two projections of a value pair and the two case expressions whose scrutinee is a value injection.

We prove the value/redex/stuck trichotomy by structural induction on a closed term, without assuming that it is typed. A variable case is impossible by closedness; a Boolean, lambda, or the Unit constructor $\star$ is a value. In an application, first apply the induction hypothesis to the function. Its step or stuck outcome lifts to the application. If it is a value, apply the hypothesis to the argument; an argument step or stuck outcome lifts, while two values form a beta redex exactly when the function is a lambda and otherwise form a stuck application. In a conditional, the guard’s step or stuck outcome lifts; a true or false guard determines its unique root contraction, and any other value guard makes the conditional stuck.

For a pair, decompose the left component first; only when it is a value decompose the right. If both are values, the pair is a value. In a projection, decompose the scrutinee. A value pair has the corresponding projection redex; every other value scrutinee makes the projection stuck. In an injection, decompose its payload; the injection becomes a value exactly when the payload does. In a case, decompose the scrutinee. A value left or right injection determines the corresponding contraction, while every other value scrutinee makes the case stuck. Abort decomposes its scrutinee; any value scrutinee makes the abort stuck. These clauses also propagate a stuck selected subterm to a stuck whole term.

For uniqueness, structural induction compares two proposed decompositions. The Unit constructor has no decomposition because it is already a value. In an application, the argument frame requires a value function, whereas the function frame contains a reducible function; a value has no step. The induction hypotheses make the selected function or argument decomposition unique, and a beta root has both subterms values, so it cannot overlap either nonempty frame. A conditional root has a Boolean value guard and cannot overlap its guard frame. In a pair, the right frame requires the left component to be a value, whereas the left frame requires that component to decompose; no value steps. A projection, injection, case, or abort has only the displayed frame for its outer constructor, and the induction hypothesis makes the selected child decomposition unique. At the empty context, projection and case roots are separated by their outer constructors, and the two case roots are separated because an injection cannot be both left and right. The outer constructor $\star$ is disjoint from every redex and from every nonempty frame. A root redex cannot also have a nonempty decomposition: every subterm at an earlier selected position is a value, while plugging a basic redex into a context produces a step and no value steps.

These cases exhaust the grammar and establish exactly one of value, unique context-and-redex decomposition, or stuckness. If $e⟼e_1$ and $e⟼e_2$, both derivations therefore expose the same context and basic redex. Every basic redex has one contractum, and filling the common context yields $e_1=e_2$.

The substituend $(x,y)$ has both $x$ and $y$ free. Freshen the left branch binder $x$ to $u$, and the right branch binder $y$ to $v$: The occurrences of $x,y$ inside both inserted pairs are free, as is the scrutinee variable $z$; $u,v$ are bound in their respective branches. Retaining the original left binder would bind the inserted $x$ in that branch. Retaining the original right binder would similarly bind the inserted $y$. Both freshening steps are therefore necessary.

Define $$N:=\lambda h:(A+B)\to \mathbf{0}.(\lambda a:A.h\mathsf{inl}(a),\lambda b:B.h\mathsf{inr}(b)).$$ Put $H=h:(A+B)\to \mathbf{0}$, ${\mathrm{\Gamma }}_A=H,a:A$, and ${\mathrm{\Gamma }}_B=H,b:B$. The two component derivations are $${\mathcal{D}}_A=\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(h:(A+B)\to \mathbf{0})\in {\mathrm{\Gamma }}_A}{{\mathrm{\Gamma }}_A⊢h:(A+B)\to \mathbf{0}}}\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(a:A)\in {\mathrm{\Gamma }}_A}{{\mathrm{\Gamma }}_A⊢a:A}}\mathrm{Var}\\ B\mathsf{type}\end{array}}{{\mathrm{\Gamma }}_A⊢\mathsf{inl}(a):A+B}}\mathrm{Inl}\end{array}}{{\mathrm{\Gamma }}_A⊢h\mathsf{inl}(a):\mathbf{0}}}\mathrm{App}}{h:(A+B)\to \mathbf{0}⊢\lambda a:A.h\mathsf{inl}(a):A\to \mathbf{0}}\mathrm{Lam}.$$ The right component is not left implicit: $${\mathcal{D}}_B=\frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{(h:(A+B)\to \mathbf{0})\in {\mathrm{\Gamma }}_B}{{\mathrm{\Gamma }}_B⊢h:(A+B)\to \mathbf{0}}}\mathrm{Var}\\ {\displaystyle \frac{\begin{array}{c}A\mathsf{type}\\ {\displaystyle \frac{(b:B)\in {\mathrm{\Gamma }}_B}{{\mathrm{\Gamma }}_B⊢b:B}}\mathrm{Var}\end{array}}{{\mathrm{\Gamma }}_B⊢\mathsf{inr}(b):A+B}}\mathrm{Inr}\end{array}}{{\mathrm{\Gamma }}_B⊢h\mathsf{inr}(b):\mathbf{0}}}\mathrm{App}}{H⊢\lambda b:B.h\mathsf{inr}(b):B\to \mathbf{0}}\mathrm{Lam}.$$ The remaining Pair and Lam nodes give the complete outer tree: $$\frac{{\displaystyle \frac{\begin{array}{c}{\mathcal{D}}_A\\ {\mathcal{D}}_B\end{array}}{H⊢(\lambda a:A.h\mathsf{inl}(a),\lambda b:B.h\mathsf{inr}(b)):(A\to \mathbf{0})\times (B\to \mathbf{0})}}\mathrm{Pair}}{\cdot ⊢N:((A+B)\to \mathbf{0})\to ((A\to \mathbf{0})\times (B\to \mathbf{0}))}\mathrm{Lam}.$$

For the converse define $$M:=\lambda p:(A\to \mathbf{0})\times (B\to \mathbf{0}).\lambda s:A+B.\mathsf{case}(s;a.\mathsf{fst}(p)a;b.\mathsf{snd}(p)b).$$ Let $P=p:(A\to \mathbf{0})\times (B\to \mathbf{0})$, $\mathrm{\Sigma }=P,s:A+B$, ${\mathrm{\Sigma }}_A=\mathrm{\Sigma },a:A$, and ${\mathrm{\Sigma }}_B=\mathrm{\Sigma },b:B$. The complete branch trees are $${\mathcal{E}}_A=\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{P\in {\mathrm{\Sigma }}_A}{{\mathrm{\Sigma }}_A⊢p:(A\to \mathbf{0})\times (B\to \mathbf{0})}}\mathrm{Var}}{{\mathrm{\Sigma }}_A⊢\mathsf{fst}(p):A\to \mathbf{0}}}\mathrm{Fst}\\ {\displaystyle \frac{(a:A)\in {\mathrm{\Sigma }}_A}{{\mathrm{\Sigma }}_A⊢a:A}}\mathrm{Var}\end{array}}{{\mathrm{\Sigma }}_A⊢\mathsf{fst}(p)a:\mathbf{0}}\mathrm{App},$$ and $${\mathcal{E}}_B=\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{P\in {\mathrm{\Sigma }}_B}{{\mathrm{\Sigma }}_B⊢p:(A\to \mathbf{0})\times (B\to \mathbf{0})}}\mathrm{Var}}{{\mathrm{\Sigma }}_B⊢\mathsf{snd}(p):B\to \mathbf{0}}}\mathrm{Snd}\\ {\displaystyle \frac{(b:B)\in {\mathrm{\Sigma }}_B}{{\mathrm{\Sigma }}_B⊢b:B}}\mathrm{Var}\end{array}}{{\mathrm{\Sigma }}_B⊢\mathsf{snd}(p)b:\mathbf{0}}\mathrm{App}.$$ Thus the case and abstraction nodes are $$\mathcal{E}=\frac{\begin{array}{c}{\displaystyle \frac{(s:A+B)\in \mathrm{\Sigma }}{\mathrm{\Sigma }⊢s:A+B}}\mathrm{Var}\\ {\mathcal{E}}_A\\ {\mathcal{E}}_B\end{array}}{\mathrm{\Sigma }⊢\mathsf{case}(s;a.\mathsf{fst}(p)a;b.\mathsf{snd}(p)b):\mathbf{0}}\mathrm{Case},$$ $$\frac{{\displaystyle \frac{\mathcal{E}}{P⊢\lambda s:A+B.\mathsf{case}(s;a.\mathsf{fst}(p)a;b.\mathsf{snd}(p)b):(A+B)\to \mathbf{0}}}\mathrm{Lam}}{\cdot ⊢M:((A\to \mathbf{0})\times (B\to \mathbf{0}))\to ((A+B)\to \mathbf{0})}\mathrm{Lam}.$$

On constructor inputs, with $f:A\to \mathbf{0}$ and $g:B\to \mathbf{0}$, put $p_0=(f,g)$. Then while the other injection has its own complete trace

Define $$d:=\lambda p:A\times (B+C).\mathsf{case}(\mathsf{snd}(p);b.\mathsf{inl}((\mathsf{fst}(p),b));c.\mathsf{inr}((\mathsf{fst}(p),c))).$$ In the other direction, define $$u_B(q):=(\mathsf{fst}(q),\mathsf{inl}(\mathsf{snd}(q))),u_C(r):=(\mathsf{fst}(r),\mathsf{inr}(\mathsf{snd}(r))).$$ Then $$u:=\lambda s:(A\times B)+(A\times C).\mathsf{case}(s;q.u_B(q);r.u_C(r)).$$ Product inversion gives $\mathsf{fst}(p):A$ and $\mathsf{snd}(p):B+C$; the two branches of $d$ have the common type $(A\times B)+(A\times C)$. Conversely, each branch of $u$ has type $A\times (B+C)$. The Case, Pair, projection, and injection rules therefore give the two advertised arrow typings.

Put $$p_B=(a,\mathsf{inl}(b)),q_B=(a,b),p_C=(a,\mathsf{inr}(c)),q_C=(a,c).$$ For a fixed product term $p$, abbreviate the fully displayed case context by $$D_p(t):=\mathsf{case}(t;b^{\prime }.\mathsf{inl}((\mathsf{fst}(p),b^{\prime }));c^{\prime }.\mathsf{inr}((\mathsf{fst}(p),c^{\prime }))),$$ and put $U(t):=\mathsf{case}(t;q.u_B(q);r.u_C(r))$. All contractions needed by both composites are the following four calculations: For the right constructors: Thus $u(d(p_B))$ and $u(d(p_C))$ concatenate respectively the first and second chains in each display and return $p_B,p_C$. Conversely, $d(u(\mathsf{inl}(q_B)))$ and $d(u(\mathsf{inr}(q_C)))$ concatenate the same chains in the opposite order and return $\mathsf{inl}(q_B),\mathsf{inr}(q_C)$. Every step is beta, projection, or case contraction; no eta law has been used.

We reconstruct, rather than cite, neutral expansion. For each type $A$, let $N(A)$ assert: if $n$ is neutral and every immediate reduct of $n$ lies in ${\mathcal{R}}_A$, then $n\in {\mathcal{R}}_A$. We prove $N(A)$ by structural induction on $A$, using only normalization and reduction closure at proper component types.

At $P,\mathbf{2},\mathbf{1},\mathbf{0}$, every immediate reduct is strongly normalizing. There are finitely many, so adjoining the root $n$ produces no infinite branch. Hence $\mathsf{SN}(n)$ and the base candidate contains $n$.

Let $A=B\to C$ and fix $a\in {\mathcal{R}}_B$. Normalization at $B$ gives $\nu (a)$. By induction on $\nu (a)$ we show $na\in {\mathcal{R}}_C$. Its immediate reducts have exactly two forms. If $n{⟶}_{\mathsf{p}}{n}^{\prime }$, the premise of $N(A)$ gives $n^{\prime }\in {\mathcal{R}}_{B\to C}$, and the arrow clause gives $n^{\prime }a\in {\mathcal{R}}_C$. If $a{⟶}_{\mathsf{p}}{a}^{\prime }$, reduction closure at $B$ gives $a^{\prime }\in {\mathcal{R}}_B$ and the height induction gives $n{a}^{\prime }\in {\mathcal{R}}_C$. The outer induction hypothesis $N(C)$ now admits $na$. Since $a$ was arbitrary, the arrow clause admits $n$.

Let $A=B\times C$. The term $\mathsf{fst}(n)$ is neutral, and each of its immediate reducts is $\mathsf{fst}(n^{\prime })$ for an immediate $n^{\prime }$ of $n$. The premise gives $n^{\prime }\in {\mathcal{R}}_{B\times C}$, hence $\mathsf{fst}(n^{\prime })\in {\mathcal{R}}_B$. The outer induction hypothesis $N(B)$ admits $\mathsf{fst}(n)$. Replacing $B,\mathsf{fst}$ by $C,\mathsf{snd}$ proves the second projection condition, so the product clause admits $n$.

Let $A=B+C$. Every immediate $n^{\prime }$ is reducible and therefore strongly normalizing; finite branching makes $n$ strongly normalizing. A reduction from neutral $n$ to $\mathsf{inl}(b)$ has positive length and factors through an immediate $n^{\prime }\in {\mathcal{R}}_{B+C}$, whose canonical-reduct condition gives $b\in {\mathcal{R}}_B$. A reduction to $\mathsf{inr}(c)$ factors the same way and the right condition of $n^{\prime }$ gives $c\in {\mathcal{R}}_C$. Thus the sum clause admits $n$.

This completes the proof of $N(A)$ without invoking saturation clause 3. A variable $x$ is neutral and has no immediate reducts, so the premise of $N(A)$ is vacuous and $x\in {\mathcal{R}}_A$ for every type $A$.

Let $e\in {\mathcal{R}}_{\mathbf{2}}$ and $b,c\in {\mathcal{R}}_C$. Saturation normalization gives finite heights $\nu (e),\nu (b),\nu (c)$. Induct on their sum. The conditional is neutral. Its complete list of immediate reducts is In the first three cases, saturation reduction closure keeps the changed component in its candidate, and its reduction height strictly decreases. The induction hypothesis therefore places the resulting conditional in ${\mathcal{R}}_C$. In the last two cases the reduct is respectively $b$ or $c$, reducible by assumption. Thus every immediate reduct is in ${\mathcal{R}}_C$; saturation neutral expansion gives $\mathsf{if}(e;b;c)\in {\mathcal{R}}_C$.

Finally, ${\mathcal{R}}_{\mathbf{2}}=\{e\mid \mathsf{SN}(e)\}$. Neither $\mathsf{tt}$ nor $\mathsf{ff}$ has an immediate proof reduct, hence neither begins an infinite reduction. Therefore $\mathsf{tt},\mathsf{ff}\in {\mathcal{R}}_{\mathbf{2}}$ directly from the base definition.