User:Jshflynn/Definition:Lambda Term

From ProofWiki
Jump to navigation Jump to search

Definition

Lambda terms (or $\lambda$-terms) are words over the following alphabet:

$v_0, v_1,...$
$\lambda$
$(, )$

The set of $\lambda$-terms is denoted $\Lambda$ and is defined inductively:

$(1) \forall n \in \mathbb{N}: v_n \in \Lambda$
$(2) \forall n \in \mathbb{N}: M \in \Lambda \Longrightarrow (\lambda v_n M) \in \Lambda$
$(3) M, N \in \Lambda \Longrightarrow MN \in \Lambda$

Only those terms which may be derived from the rules above are terms in $\Lambda$.

Notation

The following notation was introduced by Schoenfinkel and is used throughout the $\lambda$-calculus.

$(i)$ We use $\overrightarrow{x}$ to represent $x_1...x_n$.
$(ii)$ We use $\lambda x_1 ... x_n.M$ to represent $\lambda x_1 ( \lambda x_2 ( ... ( \lambda_n (M))...))$.
$(iii)$ We use $MN_1...N_n$ to represent $(...((MN_1)N_2)...)$.

Example

$v_2v_4$ is a $\lambda$-term by applying $(1)$ twice.

$\lambda v_3. v_4v_5$ is a $\lambda$-term and represents $\lambda v_3 (v_4 v_5)$.