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.

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.

Take an infinite supply of variables and the two distinguished constants of combinatory logic, the K combinator and the S combinator. The combinatory logic terms are exactly the finite expressions generated byThus every variable and each distinguished constant is a combinatory logic term, and the application of two combinatory logic terms is a combinatory logic term. Nothing else is a combinatory logic term. Application associates to the left, so $ABC$ means $(AB)C$; it is not assumed to be associative. The I combinator can be used as the abbreviation $\mathbf{I}\equiv \mathbf{SKK}$, without adding a new primitive constant.

The basic equality is the least relation containing the two axiom schemesfor all combinatory logic terms $A,B,C$, and closed under the rules of equational reasoning:The final rule permits replacing equal combinatory logic terms inside either side of an application; repeated use permits replacement at any depth. Uniform substitution of combinatory logic terms for variables preserves equality, either included as a rule or proved by induction on these derivations, since the displayed axioms are schemes. No rule equating two combinatory logic terms merely because they agree after an extra argument belongs to this basic theory. Its equality is the symmetric, reflexive and transitive closure of weak combinatory reduction.

Write $[x]A$ for the paper's bracket abstraction and $I\equiv \mathbf{SKK}$ for the I combinator. Prove the result by structural induction following the three clauses of bracket abstraction.

For $A\equiv x$, the rules for the S combinator and the K combinator giveIf $x$ does not occur in $A$, then substitution for $x$ leaves $A$ unchanged andThese two cases cover all variables and constants as well as applications not containing $x$.

In the remaining case, $A\equiv CD$ and $x$ occurs in at least one of $C,D$. The bracket abstraction clause, the rule for the S combinator, the induction hypotheses and compatibility of equality with application giveThe last line is the defining application clause of substitution. ThereforeThe conclusion is equality in combinatory logic; it need not be literal identity of strings. There are no binders in a combinatory logic term, so this substitution introduces no variable capture.

Successive bracket abstractions are processed from the inside out: $[x][y]((\mathbf{K}x)y)$. Retain $I\equiv (\mathbf{SK})\mathbf{K}$ only as a temporary abbreviation for the I combinator. Since $y$ is absent from $\mathbf{K}x$, the first bracket abstraction isFor the outer bracket abstraction, $x$ is absent from $I$ and the S combinator, while it occurs in $\mathbf{K}(\mathbf{K}x)$. HenceSubstituting upward and then expanding $I$ gives the following fully bracketed string, consisting solely of the S combinator, the K combinator and parentheses:For readability, the same result with the usual left association convention and the temporary abbreviation isThe syntactic result comes from the specified bracket abstraction algorithm. Replacing it by the shorter K combinator, despite agreement after two arguments, would not answer the requested computation. As a check using the result of part (b), applying the computed combinatory logic term to $u,v$ gives $\mathbf{K}uv=u$.