 Lambda term

A lambda term is a variable, an abstraction $\lambda x.M$, or an application $MN$, formed recursively from lambda terms $M$ and $N$.