 Bracket abstraction

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.