(How) does lambda calculus encode/use associativity of function composition

category-theoryfunctionslambda-calculus

I'm just learning about Lambda Calculus, so apologies if this is an obvious question, but given how useful and fundamental the associativity property of function composition is, (how) is this associativity encoded/utilized in lambda calculus (which is apparently designed to abstract important patterns of functions)?

I'm not asking about the convention of left (or right) associativity in lambda or type notation, but the genuine and general associativity property of function composition, i.e. the general identity $f(gh)=(fg)h$.

The Hindley and Seldin bible on lambda calculus doesn't even mention associativity.

Best Answer

In general it is not the case that given lambda terms $f,g,h$, then $(fg)h = f(gh)$. For example, let $I=\lambda x.x$, and take $$f =\lambda x.\lambda y.x,\quad g=h = I$$ then $(fg)h = I$, however $f(gh) = \lambda y.I$.

However, you could define a composition term $$c = \lambda f.\lambda g.\lambda x.f(gx)$$ and show that $$((c((cf)g))h) = ((cf)((cg)h)).$$ Notice that this notation is hard to read, and for this reason it is common to associate application of lambda terms to the left, that is we can instead write $$c(cfg)h = cf(cgh).$$

To show this we just expand $c$ as follows: \begin{align*} c(cfg)h &= \lambda x.(cfg)(hx)\\ &=\lambda x.(\lambda x.f(gx))(hx)\\ &=\lambda x. f(g(hx))\\ &=\lambda x.f((\lambda x.g(hx))x)\\ &=\lambda x.f((cgh)x)\\ &=cf(cgh). \end{align*}

Related Question