Exercises 2: Termination of $β$-reduction and Simple Type Theory

Teacher: Gilles Dowek

Ex1: ST $λ$-calculus: termination of $β$-reduction

1.

\[(λx^A.t) u ⟶ (u/x)t\]

One-step $β$-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 (counter-example: 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 well-defined.

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$