Lambda Expression

lambda-calculus

Definition

Lambda Expression

An expression is either a variable, a composed expression or an abstraction:

$$e::=x\mid e{e}^{\prime }\mid \lambda x.e$$

Properties

Left-associative

$$MNL=(MN)L$$

Examples

Implication

We’re using the following Boolean representations:

$$\begin{array}{rl}\mathbf{T}& =\lambda xy.x\\ \mathbf{F}& =\lambda xy.y\\ \mathbf{ITE}& =\lambda pxy.pxy\end{array}$$

Based on these, we can to construct a lambda term $\mathbf{imp}$ which represents an implication. Trivially, implications can be represented as:

$$X\mathbf{imp}Y=\mathbf{if}X\mathbf{then}Y\mathbf{else}\mathbf{T}$$

Therefore, we can write $\mathbf{imp}$ as:

$$\begin{array}{rl}\mathbf{imp}& =\lambda xy.\underline{\mathbf{ITE}}xy\mathbf{T}\\ & {\to }_{\alpha }\lambda xy.\underline{(\lambda p{x}^{\prime }{y}^{\prime }.p{x}^{\prime }{y}^{\prime })x}y\mathbf{T}\\ & {\to }_{\beta }\lambda xy.\underline{(\lambda x^{\prime }{y}^{\prime }.x{x}^{\prime }{y}^{\prime })y}\mathbf{T}\\ & {\to }_{\beta }\lambda xy.\underline{(\lambda y^{\prime }.xy{y}^{\prime })\mathbf{T}}\\ & {\to }_{\beta }\lambda xy.xy\underline{\mathbf{T}}\\ & {\to }_{\alpha }\lambda xy.xy(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\end{array}$$

Usages:

$$\begin{array}{rl}\mathbf{imp}\mathbf{T}\mathbf{F}& =\underline{(\lambda xy.xy(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{T}}\mathbf{F}\\ & {\to }_{\beta }\underline{(\lambda y.\mathbf{T}y(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{F}}\\ & {\to }_{\beta }\mathbf{TF}(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }((\lambda xy.x)\mathbf{F})(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }(\lambda y.\mathbf{F})(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }\mathbf{F}\\ & \\ \mathbf{imp}\mathbf{F}\mathbf{F}& =\underline{(\lambda xy.xy(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{F}}\mathbf{F}\\ & {\to }_{\beta }\underline{(\lambda y.\mathbf{F}y(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{F}}\\ & {\to }_{\beta }\mathbf{FF}(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }((\lambda xy.y)\mathbf{F})(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }(\lambda y.y)(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }\mathbf{T}\\ & \\ \mathbf{imp}\mathbf{T}\mathbf{T}& =\underline{(\lambda xy.xy(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{T}}\mathbf{T}\\ & {\to }_{\beta }\underline{(\lambda y.\mathbf{T}y(\lambda x^{\prime }{y}^{\prime }.x^{\prime }))\mathbf{T}}\\ & {\to }_{\beta }\mathbf{TT}(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }((\lambda xy.x)\mathbf{T})(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }(\lambda y.\mathbf{T})(\lambda x^{\prime }{y}^{\prime }.x^{\prime })\\ & {\to }_{\beta }\mathbf{T}\end{array}$$