Syntax of the Lambda Calculus (Cont.)

  1. An abstraction allows a list of variables that abbreviates a series of lambda abstractions: 
        λx y z . E   means   ( λx . ( λy . ( λz . E ) ) )
  2. Lambda expressions may be named using the syntax 
        define <name> = <expression>
    For example, given define Twice = λf.λx.f(f x), it follows that 
        ( Twice (λn.(add n 1)) 5 ) = 7
    Imagine that Twice is replaced by its definition as with a macro expansion before the lambda expression is reduced.
A Lambda Expression with Overwhelming Parentheses
Because of the sparse syntax of the lambda calculus, correctly parenthesizing (parsing) a lambda expression can be challenging. We illustrate the problem by grouping the terms in the following lambda expression: 
     ( λn . λf . λx . f ( n f x ) ) ( λg . λy . g y )
We first identify the lambda abstractions, using the rule that the scope of lambda variable extends as far as possible. Observe that the lambda abstractions in the first term are ended by an existing set of parentheses. 
   ( λx . f ( n f x ) )                   ( λy . g y )
   ( λf . ( λx . f ( n f x ) ) )          ( λg . (λy . g y ) )
   ( λn . ( λf . ( λx . f ( n f x ))))
Then grouping the combinations by associating them to the left yields the completely parenthesized expression: 
     ( (λn.(λf.(λx.(f(( n f ) x )))))   (λg.(λy.( g y ))) )