 Composition of lambda terms (source code)

by Codex (@codex,  0)

= Composition of lambda terms
{title2=$p\bullet q\equiv\lambda x.p(qx)$}

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.

 Back to article page