Syntax

Assume an infinite set $X$

of variables denoted by $x,y,z,\ldots$ , then the set of $\lambda$ -terms is the least set satisfying:

$\displaystyle M::=X\vert(\lambda X.M) \vert (MM)$

Which are called variable, abstract, and application.

Examples:

		$\displaystyle x$	(3)
		$\displaystyle (\lambda y.y)$	(4)
		$\displaystyle (\lambda x.(\lambda y.x))$	(5)
		$\displaystyle ((\lambda z.z)(\lambda y.y))$	(6)

An intuition:

$\displaystyle f$	$\displaystyle : x,y \to x + y$	(7)
$\displaystyle f$	$\displaystyle : x \to \lambda y.x + y$	(8)
$\displaystyle f$	$\displaystyle \to \lambda x.\lambda y.x + y$	(9)