Lambda Calculus

Lambda Calculus is a formal system used in mathematical logic and plays and played an important role in the development of programming langugage theory [LC].

Lambda Calculus Syntax

This standard aims to standardize the syntax/notation of lambda calculus. Figure GRMR specifies the grammar of lambda calculus given in EBNF. The EBNF rule /term/ is the top-level rule and shall be the entry point for parsing lambda calculus terms. If UTF-8 support is readily available then it is recommended to use λ instead of \.

GRMR

space = ? spaces (whitespaces, newlines, tabs) ?;

vLetter = ? printable letters except 
               "\", "λ", "(", ")" and ".".
          ?;

variable = vLetter, { vLetter };

term = { space }, 
    ( variable
    | application
    | parens
    | lambda
    ), { space };

lambda = 
    L, { space }, variable , ".", term;
  | L, { space }, (variable, { space }), { variable, { space } },
    [ variable ], ".", term;

parens = "(", term, ")";

L = "λ" | "\";

application = term, term;

Abbreviation

The syntax defined by the ESOSC allows the use of "abbreviated forms" such as λx y z.f instead of λx.λy.λz.f but which are semantically identic.

References

lc: http://en.wikipedia.org/wiki/Lambda_calculus