Proof completion: if $Y$ is a closed term in strong nf, then $Yx$ weakly reduces to a strong nf $Z$

Question

I am self-studying Hindley & Seldin's Lambda-Calculus and Combinators. I would appreciate some help with filling in a final detail for a proof for the following statement regarding combinatory logic:

Claim. If a closed term $Y$ is in strong nf, then $Yx$ weakly reduces to a strong nf $Z$.

Weak reduction (notation: $\rhd_w$) is defined as usual: $X \rhd_w Y$ iff there exists a (possibly empty) series of $\mathsf{I}, \mathsf{K}, \mathsf{S}$ contractions from $X$ to $Y$. For completeness, the single contractions are as follows:

• $\mathsf{I}x \rhd_{1w} x$
• $\mathsf{K}xy \rhd_{1w} x$
• $\mathsf{S}xyz \rhd_{1w} xz(yz)$

The book states that the claim can be proven by induction on the following definition:

Definition 1. (Strong normal forms)

1. All atoms other than $\mathsf{I}$, $\mathsf{K}$ and $\mathsf{S}$ are in strong normal form;
2. if $X_1, \ldots, X_n$ are in strong normal form and $a$ is any atom $\not \equiv \mathsf{I}, \mathsf{K}, \mathsf{S}$, then $aX_1\ldots X_n$ is in strong normal form;
3. if $X$ is in strong nf, then so is $[x].X$.

Here, $[x]$ is the pseudoabstractor (also denoted by $\lambda^*$ in other literature), defined as follows:

Definition 2. (Abstraction) For every CL-term $M$ and every variable $x$, a CL-term called $[x].M$ is defined by induction on $M$, thus:

1. $[x].M \equiv \mathsf{K}M$ $\hspace{29.8mm}$if $x \not\in FV(M)$
2. $[x].x \equiv \mathsf{I}$
3. $[x].Ux \equiv U$ $\hspace{33mm}$if $x \not\in FV(U)$
4. $[x].UV \equiv \mathsf{S}([x].U)([x].V)$ $\hspace{6mm}$if neither (1) nor (3) applies

Note that $\equiv$ denotes syntactical equivalence.

This is what I have so far:

Proof. Assume that the closed term $Y$ is in strong nf. The cases are as follows according to Def. 1.

1. $Y \equiv a$ (with $a$ some variable). Then $Yx \equiv ax \rhd_{w} ax$. By Def. 1.1, $x$ is in strong nf. By Def 1.2, and the preceding fact, $ax$ is in strong nf.

2. $Y \equiv aX_1...X_n$ with $X_1,\ldots,X_n$ in strong nf. Then $Yx \equiv aX_1...X_nx \rhd_{w} aX_1...X_n x$. Since $X_1, \ldots, X_n, x$ are all in strong nf, so is $aX_1\ldots X_nx$ by Def 1.2.

3. $Y \equiv [x].X$ with $X$ in strong nf. Then the cases must be distinguished according to Def. 2.

   a. $x \not\in FV(X)$. Then $Yx \equiv \mathsf{K}Xx \rhd_{w} X$. $X$ is in strong nf by hypothesis.

   b. $X \equiv x$. Then $Yx \equiv \mathsf{I}x \rhd_{w} x$. $x$ is in strong nf by Def 1.1.

   c. $X \equiv Ux$ with $x \not\in FV(U)$. Then $Yx \equiv ([x].Ux)x \equiv Ux \equiv X \rhd_w X$. $X$ is in strong nf by hypothesis.

   Now for the final case, which gives me trouble:

   d. $X \equiv UV$ with $x \in FV(UV)$ and $V \not\equiv x$. Then $$Yx \equiv \mathsf{S}([x].U)([x].V)x \rhd_{w} ([x].U)x(([x].V)x)$$By the IH, both $([x].U)x$ and $([x].V)x$ weakly reduce to strong nfs $Z_1$ and $Z_2$.

   Question: Should I now argue that $Z_1Z_2$ weakly reduces to a strong normal form, or that $Z_1Z_2$ is a strong normal form? If the former, how do I properly complete this argument without falling into the trap of infinite regress?

Let me know if you require additional information.

Answer 1

To prove that for every strong nf $X$ the expression $([y]X)x$ weakly reduce to a strong nf I think you should use induction over definition of strong nf not over abstraction.

To prove this we procede by induction over definition of strong nf:

• if $X \equiv y$ then by definition $[y]X=[y]y=I$ and so $([y]X)x=x$ which is a strong nf;
• if $X \equiv a$ with $a$ an atom different than $S$, $I$, $K$ and $y$ then $[y]X=KX$ and so $([y]X)x=X$ which is strong nf by hypothesis;
• if $X \equiv a X_1 \dots X_n$ with $a$ being atom different by $S$, $I$ and $K$ and the $X_i$ being all strong nf then by definition of abstraction we have that $[y]X=[y]aX_1\dots X_{n-1}X_n\equiv S([y]aX_1\dots X_{n-1})([y]X_n)$ and so $([y]X)x \equiv ([y]aX_1 \dots X_{n-1})x(([y]X_n)x)$ which is equal (this can be easily proved by induction on the number $n$ of terms applied to $a$) to $$[([y]a)x][([y]X_1)x][([y]X_2)x]\dots[([y]X_n)[x]]$$ since all $X_i$ a strong nf by inductive hypothesis each $([y]X_i)x\rhd_w Z_i$ and similarily $([y]a)x \rhd_w A$ where the $Z_i$ are strong nf while $A$ is either $x$ (if $a\equiv y$) or $a$ (so $A$ is an atom), so by applying the substitution lemma $$([y]X)x\equiv [([y]a)x][([y]X_1)x]\dots[([y]X_n)x] \rhd_w AZ_1\dots Z_n$$

where $AZ_1 \dots Z_n$ is a strong nf since all the $Z_i$ are Strong nf and $A$ is an atom.

This proves the point 3 and so conclude your proof.