An EBNF Grammar for Lambda Expressions.

• Terminal symbols: 'λ', ., (, ), and the letters a through z .
• Nonterminal symbols: <expression>, <variable>, <application>, <primary> .
  
• The starting symbol is: <expression> .
  
• Derivation rules:
  1. variable ::= <letter> .
     
  2. expression ::= 'λ' <variable> '.' <application> | <application> .
  3. application ::= <application> <primary> | <primary>
  4. primary ::= <variable> | '(' <expression> ')'

Notes on this Grammar. In rule 2, we can the part before the dot corresponds to a function header and parameter list. The part between the dot and the vertical bar is the body of the function. An application corresponds to a function call.

Rule 3 says that application associates to the left, like + and * in C (and unlike =). In practice, this means that the expression     a b c     means     (a b) c     instead of     a (b c), where a, b, and c are all expressions. Parentheses may be used to override this association.

Rules 2, 3, and 4, taken together, mean that parentheses may be freely added around any expression. Parentheses may also be dropped when they are redundant. For example:
((a b)) c     can be simplified to     (a b) c

Renaming. As in any programming language, you can change the name of a parameter is all references to that parameter are also changed. Thus, there are many equivalent ways to write the number 1, including these:    1 = λx.λy.xy     and     1 = λp.λq.pq

Binding and scope. Each λ creates one parameter (bound variable). The scope of a binding is from the lambda that declares it to the end of the formula, or to the parenthesis that closes the function by matching the paren just before the lambda. For example, there are three bound variables in this formula:     (λn.(λx.λy.nx(xy))) p(pq)     The scope of n is (λx.λy.nx(xy)), the scope of x is λy.nx(xy), and the scope of y is nx(xy).

When a binding for the variable x is nested inside an expression that has another binding for x, the familiar scoping rule applies: each reference to x is bound by the most recent open binding. For example, there are two bindings for x in the following expression:
       ( λx.xy( λx.nx(xy )xn )
The inner binding (colored blue) binds the two referrences to x that follow it. The outer binding (colored red) binds the x before the inner binding and the x after the paren that closes the inner function.

Free variables. A variable can occur in an expression without any binding. We call these "free variables". They cannot be renamed, because the renaming rule requires that variable and binding must be renamed simultaneously.

A Lambda Application: calculate the successor of 1.

• The number 1:   1 = λp.λq.pq
• The successor function, which is named 1+ in FORTH:   S = λn.(λx.λy.nx(xy))
  
• Calculating the successor of 1:
  

  (S 1)	Apply S to 1.
  ( λn.(λx.λy.n x (xy))  1 )	Substitute 1 for n, drop λn
  ((λx.λy.1 x (xy)))	Expand 1.
  ((λx.λy. ( λp.λq.pq )  x (xy) ))	Apply 1 to x, drop the λp.
  ((λx.λy. ( λq.xq ) (xy) ))	Apply result to (xy), drop the λq
  (λx.λy. ( x(xy) ))	Drop redundant parentheses.
  λx.λy. x(xy)	The answer is 2.