<Exp> ::= <ident> |
<constant> |
lambda <ident> . <Exp> | -- function abstraction
<Exp> <Exp> | -- function application
( <Exp> )
Grammar for Lambda Calculus.
A function abstraction is an expression for a function.
The identifier is the name of the parameter; it is said to be bound.
An unbound identifier is free.
The function itself has no name.
Application is left associative, f x y=(f x)y.
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.
<Exp> ::= ... as before ... |
<unopr> <Exp> |
<Exp> <binopr> <Exp> |
if <Exp> then <Exp> else <Exp>
Extended Grammar to include Operators.
This chapter considers list processing applications
which require a list constructor,
often called cons,
and written as an infix operator `::'.
The constant `nil' represents the empty list.
Unary operators `hd' (head) and `tl' (tail) dismantle a list
and `null' tests for the empty list.
Conventionally a list is terminated by nil,
but this is not essential.
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. A strict function evaluates all of its arguments; the conditional is therefore a non-strict function.hd (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 = error List and Conditional Operators.
The process of evaluating a lambda expression is called reduction. Each operator must have an evaluation rule but the interesting case is the application of functions.hd (if true then 1::2::nil else nil) --> 1
(lambda x.e)f
--> e[f/x]
Application; Beta-Reduction.
The actual parameter f is substituted for the formal parameter x
throughout the function body, e[f/x].
This is called beta-reduction.
A precise definition of substitution is given shortly.
eg.
(lambda n. n*2+3) 7
--> (n*2+3)[7/n]
--> 7*2+3
--> 14+3
--> 17
A Function Application.
The actual parameter 7 is substituted for n.
The modified body is then evaluated.
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 e Name 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 the scope rule of lambda calculus in avoiding this problem. It is essentially the same as the scope rule in Pascal or other block-structured programming languages - this is where those programming languages got the idea.eg. 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 an evaluation rule. A familiar evaluation rule is variously known as strict evaluation or call by value. It requires the evaluation of an actual parameter before it is passed to, or substituted in, a function. It corresponds to passing parameters by value in a programming language such as Pascal. A second rule is known as normal-order evaluation or as call by name. It specifies that the left-most, outer-most application of an expression be carried out at each step. An actual parameter is not evaluated before being passed to a function. This corresponds to passing parameters by name, as in Algol-60.x, 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.
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
--> ... loops
Order of Evaluation.
In the example, normal-order evaluation terminates but
strict evaluation does not.
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.
<Exp> ::= ... as before ... |
let <decs> in <Exp>
<Decs> ::= <Dec>, <Decs> | <Dec>
<Dec> ::= <ident> = <Exp>
Extended Grammar including Declarations.
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.
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.
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 )
Using this observation it is possible to evaluate factorial(3)
as follows.
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 )
...
--> 6
Evaluation of factorial(3).
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.
<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 g
Removing Recursive Declarations.