Abstracción

$$\begin{aligned} M &:= x\\ &\mid \app{M}{M}\\ &\mid \highlight{\lam{x}{M}} \end{aligned}$$

De la tercera parte de la gramática sabemos que, dado un término $M$ y un identificador $x$, la expresión $\lam{x}{M}$ es un término válido.

Para representar la abstracción o lambda $\lam{x}{M}$ en un árbol sintáctico, necesitamos un nodo que tenga un solo hijo, para el término $M$. El identificador $x$ se representa como información adicional en el nodo de la abstracción. El identificador $x$ no es un subtérmino.

Por ejemplo, la expresión $\lam{x}{x}$ se puede representar como un nodo de abstracción con un solo hijo, que es el término $x$.

\ x. x

Creemos un árbol sintáctico para la expresión $\lam{x}{(\app{f}{x})}$.

Con esto ya tenemos las tres formas del cálculo lambda: variable, aplicación y abstracción. Aunque todavía no sabemos qué significan.