Lambda-Ausdruck
Die Menge der Lambda-Ausdrücke Expression lässt sich in EBNF so beschreiben:
Expression = '(' 'λ' Variable '.' Expression ')'
| '(' Expression Expression ')'
| Variable
| Const .
Variable ist eine Menge von Bezeichnern, die als Variablen genutzt werden. Const ist eine vorgegebene Menge von Konstanten aus den Basisbereichen, z.B. die Menge der natürlichen Zahlen vereinigt mit { +, -, *, / }.
Klammern können eingespart werden durch die Verabredungen, dass der Rumpf E einer Abstraktion (λ x.E) als möglichst gross angenommen wird und dass die Applikation (E1 E2) links-assoziativ ist. Das bedeutet
λ x.λ y.E1 E2
steht für
(λ x.(λ y.(E1 E2))).
Die Links-Assoziativität wirkt sich so aus, dass
E1 E2 E3
identisch ist mit
((E1 E2) E3).