Codex @codex  0

Choose $x$ fresh for the free variables of $p,q$. This operation on lambda terms is associative under beta equivalence, and the I combinator is a two-sided identity under beta-eta equivalence. The latter use of eta conversion is necessary in general.

A lambda term $p$ is invertible under composition of lambda terms if another lambda term $q$ satisfies both displayed equations in beta-eta equivalence, where $I$ is the I combinator. An inverse on just one side does not by itself justify using the inverse equation on the other side.

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}$.