Exercises 2: Termination of $β$reduction and Simple Type Theory
Teacher: Gilles Dowek
Ex1: ST $λ$calculus: termination of $β$reduction
1.
 Onestep $β$reduction:

$u ⟶_β v$ iff there exists context $C$ such that $u = C[(λx.t)u’]$ and $v = C[(u’/x)t]$
 Termination of $β$reduction:

if the rewriting system over ST $λ$terms comprised of the $β$reduction rule is weakly normalizing (for every ST $λ$term $u$, there exists there exists a finite reduction sequence from $u$ to a normal form).
 Strong termination of $β$reduction:

if the rewriting system over ST $λ$terms comprised of the $β$reduction rule is strongly normalizing (for every ST $λ$term $u$, all reduction sequences from $u$ are finite).
2.
This proof is wrong because the application $(t \, u)$ creates a new $β$redex if $t$ is a $λ$abstraction (counterexample: in untyped $λ$calculus: set $t = u ≝ λx.(xx)$)
3.
Let $x$ be a variable or a constant. By case analysis over $A$, let us show that ∀A, \, x ∈ R_A

if $A ∈ \lbrace ι, o\rbrace$: $x ∈ R_A$ is clear as $x$ is a normal form.

if $A ≝ B → C$: $x ∈ R_A$ because
 it strongly terminates
 it does not reduce to a term of the form $λx^B.u$
4.
Let $t ∈ R_A$ and $t ⟶^\ast t’$. Let’s show that $t’ ∈ R_A$ by case analysis over $A$:

if $A ∈ \lbrace ι, o\rbrace$: $t ∈ R_A$ is clear as $t’$ strongly terminates, since $t$ does (if they were an infinite reduction sequence from $t’ ⟶ ⋯$, then $t ⟶^\ast t ⟶ ⋯$ would be an infinite reduction from $t$ as well)

if $A ≝ B → C$: $t’ ∈ R_A$ because
 it strongly terminates
 if $t’$ reduces to an abstraction $λx^B.u$, then so does $t$, and as $t ∈ R_A$: for every term $v ∈ R_B$, $(v/x)u ∈ R_C$
5.
 $t$ strongly terminates: $t ⟶ t’ ⟶ ⋯$ impossible, as $t’ ∈ R_A$
 if $A ∈ \lbrace ι, o\rbrace$: $t ∈ R_A$ by the previous point
 if $A ≝ B → C$: assume $t ⟶^\ast λx^B.u$. As $t$ is an application, it’s not an abstraction, and this reduction sequence has at least one step: $t ⟶ t’ ⟶^\ast λx^B.u$, and as $t’ ∈ R_A$ by the previous lemma, we’re done.
6.
$t_1$ and $t_2$ strongly terminate by definition of $R_{A → B}$ and $R_A$
NB: the reduction tree of $t_1$ is a finitely branching one, so by König’s lemma, $n_1$ and $n_2$ are welldefined.
Using the previous question, it suffices to show that all the one reducts from $t_1 \, t_2$ are in $R_B$.
By induction on $n_1+n_2$:

if $n_1 + n_2 = 0$: then see last point
 $t_1 \, t_2 ⟶ t_1’ \, t_2$: IH
 $t_1 \, t_2 ⟶ t_1 \, t_2’$: IH
 $(λx^A.t) \, t_2 ⟶ (t_2/x) t$: since $(λx^A.t) ∈ R_{A → B}$ and $t_2 ∈ R_B$, it comes that $(t_2/x)t ∈ R_B$
Leave a comment