Bracket abstraction ($[x]x=I,[x]T=KT(x\notin FV(T)),[x](PQ)=S([x]P)([x]Q)$)

Bracket abstraction removes a free variable from a combinatory logic term. The displayed clauses are applied in that order, giving $FV([x]T)=FV(T)\setminus \{x\}$ and $([x]T)A{\to }^{\ast }T[x:=A]$. Under the standard lambda expansions of $S,K,I$, the result is beta-equivalent to $\lambda x.T$. The recursive translation of lambda terms therefore preserves variables and application and reflects weak equivalence, but need not preserve all beta equivalences.