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

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.