ESOTERIC STANDARD COMMITTEE
     Lambda Calculus Syntax
     ESOSC-2014-A5

     2015-03-11

This standard has been approved by the following members of the ESOSC:
 * nortti
 * Taneb
 * mroman


1 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 [1].

[1] http://en.wikipedia.org/wiki/Lambda_calculus

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


     [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;

     [/GRMR]

If UTF-8 support is readily available then it is recommended to use λ instead of \.

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