Declarations


It is a great “programming” convenience to be able to make local declarations or definitions. The extended syntax is as follows:
  <expr> ::= <var>                   ; lowercase identifiers
           | <constant>              ; predefined objects
           | ( <expr> <expr> )       ; combinations
           | ( &lambda <var> . <expr> )    ; abstractions
           | let <decs> in <expr>
  <decs> ::= <dec>, <decs>
           | <dec>
  <dec>  ::= <ident> = <expr>
Note that this form is not intended to allow explicitly recursive definitions. Declarations can be removed systematically, perhaps by a compiler, using the following transformation:
    let  x=e  in  f
 ⇒ ( λx.f ) e
For more than one declaration,
    let x=e, y=f in g 
 ⇒ (λxy.(λx.λy.g) (hd xy) (tl xy)) (e::f)
This shows that declarations are only a convenient shorthand. They do not add to the power of lambda calculus.