Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 3 / c

Again write $[x]A$ for bracket abstraction. In combinatory logic, all variable occurrences are free variables. Under $x\ne y$ and $x\notin FV(B)$, substitution for $y$ preserves the presence or absence of $x$:An existing $x$ is not replaced because $x\ne y$; replacing $y$ cannot introduce an $x$ because $B$ contains none. This ensures that the same clause of bracket abstraction applies before and after substitution.

Use structural induction on $A$, respecting those clauses. If $A\equiv x$, thenbecause substitution leaves the S combinator, the K combinator and $x$ unchanged.

If $x$ is absent from $A$, it is also absent from $A[B/y]$. ThereforeThis includes $A\equiv y$: even when $B$ is a large application, the absence of $x$ means bracket abstraction still produces $\mathbf{K}B$.

Finally, let $A\equiv CD$ with $x$ occurring in $C$ or $D$. By the occurrence observation, $x$ also occurs in $C[B/y]$ or $D[B/y]$, so the application clause applies on both sides. Apply the induction hypotheses:Every step uses the definitions of substitution and bracket abstraction, without applying the equality axioms for the S combinator or the K combinator. Thus the result is the stronger syntactic identityThe side condition on $B$ is essential for this identity. For example, substituting $x$ for $y$ in $[x]y\equiv \mathbf{K}y$ gives $\mathbf{K}x$, whereas $[x](y[x/y])\equiv [x]x\equiv \mathbf{SKK}$, a different string.