Do λ-terms form a group with composition?

68 Views Asked by At

Consider obviously as composition the well known combinator $\circ := \lambda f g.\lambda x.f(g x)$. It is easy to see that it associates ($\circ(\circ f g)h \equiv \circ f(\circ g h)$), and that it does have an identity element ($1 := \lambda x.x$), is there some reason why every λ-term should have an inverse? Intuitively one may think no, but being λ-calculus this magical place where every term has a fixed point, and being Google quite silent about, I'd rather ask.

1

There are 1 best solutions below

2
On

It's easy to see that there are lambda terms that are not invertible.

let $f=\lambda x.(\lambda y.y)$. We then have $f(1)=id$ and $f(2)=id$ so $f^{-1}(id)$ can't exist