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

Choose all auxiliary bound variables fresh for the free variables of $p,q,r$; alpha equivalence permits this. The operation $\bullet$ is composition of lambda terms, so expand its definition and use beta reduction:The two lambda terms have the same reduct, up to alpha equivalence, hence they are related by beta equivalence:No eta conversion is needed for this associativity calculation.

Write $I\equiv \lambda u.u$ for the I combinator, and choose $x$ outside the free variables of $p$. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:The freshness condition is exactly the side condition for eta conversion, which contracts $\lambda x.px$ to $p$. ThereforeHere eta conversion matters: a free variable $p$ is already in beta-normal form, as is $\lambda x.px$, and beta equivalence alone does not equate them.

The argument order in $p$ is a cyclic permutation. Undo it by rotating in the other direction. For $n\ge 1$, choose the lambda termUse fresh bound variables throughout. Substituting $qz$ for the first argument of $p$ and then performing beta reduction givesIndeed, the arguments received by $qz$ are $y_1=x_2,\dots ,y_{n-1}=x_n,y_n=x_1$, so its last argument moves back to the front. Apply eta conversion successively, starting with the innermost lambda abstraction. At each step the bound variable being removed is absent from the preceding expression. Thus the last expression is related to $z$ by beta-eta equivalence, and consequentlyFor the induction needed in the next part, also compute the reverse composition of lambda terms:So this $q$ is a two-sided inverse. The empty argument list at $n=0$ means $p=\lambda z.z$; choose $q=I$. For $n=1$, both displayed rotations give $\lambda z{y}_1.z{y}_1$, which is also related to $I$ by eta conversion. These boundary cases require no exceptional inverse construction.

Use structural induction on the construction of $p\in \mathcal{R}$, with the stronger induction claim that $p$ is an invertible lambda term: there is a lambda term $q$ satisfying bothThe base constructor has exactly the two-sided inverse proved in part (c). Strengthening the claim is useful because the inductive construction needs inverses of its constituent lambda terms in both orders.

For the inductive constructor, let $t_i$ be the two-sided inverse supplied for $s_i$. Thus, for a fresh variable $u$, beta-eta equivalence givesFor $n\ge 1$, defineThis lambda term reverses the cyclic permutation and applies the appropriate inverse to each argument. First use beta reduction to expand one order of composition of lambda terms:For the other order, beta reduction givesThese computations close the stronger induction. For $n=1$, each formula has the single argument involving $s_1$ and $t_1$; for $n=0$, the constructor is $I$ and its inverse is $I$. Every construction is finite, so the inverse is a finite lambda term. There is no requirement that this inverse itself belong to $\mathcal{R}$.