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$.

Application $MN$ applies the lambda term $M$ to the lambda term $N$. It associates to the left: $MNP=(MN)P$. Together with variables and lambda abstraction, it generates all lambda terms.

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the lambda term $t$. In the simply typed lambda calculus, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the implication introduction rule under the Curry-Howard correspondence.