A function abstraction is an expression for a function. The identifier is the name of the parameter; it is said to be<Exp> ::= <ident> | <constant> | lambda <ident> . <Exp> | -- function abstraction <Exp> <Exp> | -- function application ( <Exp> ) Grammar for Lambda Calculus.

The clause for constants can be omitted because constants can be defined with what is left but this is inconvenient and does not aid our purpose. (But see [ints], [bool] and [list] if interested.) The constants certainly include true, false, integers, some functions such as plus, minus, and a conditional function (if). Just what the set of constants contains is not crucial; it is a parameter of the lambda calculus rather than a central part of it, and the set can be varied from application to application.

The previous grammar forces the use of prefix notation. It costs nothing to extend the grammar to include prefix and infix operators. The gain is purely in convenience not in power or difficulty of implementation.

This chapter considers list processing applications which require a list constructor, often called<Exp> ::= ... as before ... | <unopr> <Exp> | <Exp> <binopr> <Exp> | if <Exp> then <Exp> else <Exp>Extended Grammar to include Operators.

Note that the conditional expression evaluates either its true or its false branch but not both, thus the expression below evaluates to 1 and is not in error. Ahd (a::b) = a | hd x = error tl (a::b) = b | tl x = error null (a::b) = false | null nil = true | null x = error if true then a else b = a | if false then a else b = b | if x then a else b = errorList and Conditional Operators.

The process of evaluating a lambda expression is calledhd (if true then 1::2::nil else nil) --> 1

The actual parameter f is(lambda x.e)f --> e[f/x]Application; Beta-Reduction.

The actual parameter 7 is substituted for n. The modified body is then evaluated.eg. (lambda n. n*2+3) 7 --> (n*2+3)[7/n] --> 7*2+3 --> 14+3 --> 17A Function Application.

The choice of a variable name is not important.
A name can be changed provided this is done "systematically".
This is called *alpha-conversion*.

Renaming can be used to prevent name clashes.(lambda x.e) = (lambda y.e[y/x]) provided y not free in eName Changing; Alpha-Conversion.

We can now define substitution properly in terms of the original simple grammar. The most difficult case involves substitution in functions. There could be a name clash and the rule for functions effectively defines theeg. lambda x. (lambda x. x) = lambda x. (lambda y. y)

There may be a choice of two or more applications in an expression. The strategy for determining which application to carry out next is called anx, y, y' :ident; c :constant; e, e', a :Exp x[a/x] --> a y[a/x] --> y if y!=x c[a/x] --> c (lambda y.e)[a/x] --> lambda y.e if y=x --> lambda y'.(e[y'/y][a/x]) if y!=x, x free in e, y free in a, new y' --> lambda y.(e[a/x]) otherwise (e e')[a/x] --> (e[a/x])(e'[a/x]) (e)[a/x] --> (e[a/x])Definition of Substitution.

In the example, normal-order evaluation terminates but strict evaluation does not.eg. (lambda x. 7) ((lambda x. x x)(lambda y. y y)) either --> 7 normal-order terminates or --> (lambda x. 7) ((lambda y. y y)(lambda y. y y)) strict --> ... loopsOrder of Evaluation.

The Church-Rosser theorem states
firstly that if any evaluation rule terminates
when applied to a particular expression then normal-order evaluation
also terminates.
Secondly, if any two evaluation rules terminate then
they give the same result, up to alpha-conversion.
Thus, normal-order evaluation is the most general evaluation rule of all.
A functional programming language having the effect of normal-order
evaluation is often called *lazy*.
There is an efficient implementation of normal-order evaluation
called *call by need*
which can be used in functional languages.
The idea is to pass an actual parameter to a function in unevaluated form.
If the function *needs* to evaluate the parameter, it does so
but it also overwrites the parameter so that it need not be reevaluated later.
A small interpreter using this technique is described later.

It is a great "programming" convenience
to be able to make local *declarations* or definitions.
The extended syntax is easy.

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.<Exp> ::= ... as before ... | let <decs> in <Exp> <Decs> ::= <Dec>, <Decs> | <Dec> <Dec> ::= <ident> = <Exp>Extended Grammar including Declarations.

This shows that declarations are only a convenient shorthand. They do not add to the power of lambda calculus.let x=e in f --> (lambda x.f)e let x=e, y=f in g --> (lambda xy. (lambda x. lambda y. g) (hd xy) (tl xy)) (e::f)Removing Declarations.

Recursive or self-referential definitions
are not needed to write a recursive
function in lambda calculus!
The function *Y* gives the effect of recursion.
Y is known as the *paradoxical operator*
or as the *fixed-point operator*.

For example, a factorial program can be written with no recursive declarations, in fact with no declarations at all. First note that YF=F(YF); YF is a fixed-point of F.Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))The Paradoxical Operator.

Using this observation it is possible to evaluate factorial(3) as follows.Y F = (lambda G. (lambda g.G(g g)) (lambda g.G(g g))) F --> (lambda g. F(g g)) (lambda g. F(g g)) --> F( (lambda g. F(g g)) (lambda g. F(g g)) ) = F( Y F )

The existence of Y means that recursive declarations can be introduced for free. Any such declaration can be converted to a non-recursive one by the use of Y and can then be removed as before.let F = lambda f. lambda n. if n=0 then 1 else n*f(n-1) in Y F 3 --> Y (lambda f. lambda n. if n=0 then 1 else n*f(n-1)) 3 --> F(Y F) 3 = (lambda f.lambda n.if n=0 then 1 else n*f(n-1)) (Y F) 3 --> (lambda n. if n=0 then 1 else n*(Y F)(n-1)) 3 normal-order! --> if 3=0 then 1 else 3*( (Y F 2) ) --> 3*( Y F 2 ) ... --> 6Evaluation of factorial(3).

<Exp> ::= ... as before ... | let [rec] <decs> in <Exp>Extended Grammar for Recursive Declarations.

let rec x=e in f --> let x=Y(lambda x.e) in f let rec x=e, y=f in g --> let rec xy= let x=hd xy, y=tl xy in e::f in let x=hd xy, y=tl xy in gRemoving Recursive Declarations.

[Previous Page] [Next Page] [Index] © L. Allison, Dept. of Computer Science, Monash University