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.<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 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.<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. 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
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.(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 --> 17 A 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 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.
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 --> ... loops Order 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 ) ... --> 6 Evaluation 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 g Removing Recursive Declarations.