Slide 12.13: Declarations

Slide 12.12: Reduction strategies (cont.)
Slide 12.14: Recursive functions
Home

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)

hd: the head function such as the Lisp car. For example,
```
     ( hd e::f ) = e
```
tl: the tail function such as the Lisp cdr. For example,
```
     ( tl e::f ) = f
```
“::”: the cons function such as the Lisp cons.

This shows that declarations are only a convenient shorthand. They do not add to the power of lambda calculus.