Gramática

La gramática del cálculo lambda con booleanos es la que resulta de agregar tres reglas a la gramática del cálculo lambda básico:

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

En lugar de repetir toda la gramática, podemos escribir solo las partes que se agregan, siempre y cuando quede claro qué lenguaje estamos extendiendo.

$$\begin{aligned}M &:= \ldots \\ &\mid \true \\ &\mid \false \\ &\mid \ifthenelse{M}{M}{M} \end{aligned}$$