# 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$

Tags:

Updated:
{"extraction_info": {"found_math": true, "script_math_tex": 1, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.9482487440109253, "perplexity": 1062.166751581918}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2019-13/segments/1552912201329.40/warc/CC-MAIN-20190318132220-20190318153621-00023.warc.gz"}