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).