Previous: Part 2: Syntax of the Lambda Calculus, Next: Part 4: Reductions, Up: Contents

Goals

• To understand the two basic evaluation-strategies of the lambda calculus.
• Understand the difference between pass by reference and pass by value.

Evaluation

In mathematics, the way an expression is evaluated is sometimes the key issue to obtaining the correct answer. It is the same in the Lambda-Calculus. Sometimes the difference in evaluation strategies can mean the difference between an infinite substitution and a terminating solution. There are two basic evaluation principles, on is eager evaluation where one always evaluates the arguments, then instantiates the function. The other concept is that of lazy evaluation, in which one evaluates arguments only when needed.

From these principles two major evaluation strategies have been developed. They are:

• Normal Order, also known as call by name which requires that one always reduce the redex whose lambda appears furthest to the left, an actual parameter is not evaluated before being passed to a function. This strategy is seen in Algol-60 where parameters are passed by name.
• Applicative Order, sometimes called strict evaluation or call by value, which calls for the evaluation of the actual parameter being passes or substituted (always reduce both the function and the argument part first before substituting the latter into the former). This is equivalent to passing parameters by value in languages like Pascal.

Examples

Evaluate the following expression using both normal order and applicative order:

	(\a.\b.a) c ((\d.e) d)

Normal order:

	(\a.\b.a) c ((\d.e) d) ->β (\b.a)[a\c] = ((\d.e) d)
	= \b.c ((\d.e) d) ->β (c)[b\((\d.e) d)] = c

Applicative order:

	(\a.\b.a) c ((\d.e) d) ->β (\a.\b.a) c (e[d\d]) = (\a.\b.a) c (e)
	(\a.\b.a) c (e) ->β (\b.a)[a\c] (e) = (\b.c) e
	(\b.c) e ->β c[b\e] = c

Do we always get the same result from both evaluation strategies? Well, let’s see:

	(\x.a)((\x.x x)(\y.y y))

Normal order:

	(\x.a)((\x.x x)(\y.y y)) ->β a [x\((\x.x x)(\y.y y))] = a

As you can see, normal order evaluation of this expression terminates. Applicative order:

	(\x.a)((\x.x x)(\y.y y)) ->β (\x . a)(xx)[x \ (ly . yy)] = (\x . a)( (ly . yy) (ly . yy))
	(\x . a)( (ly . yy) (ly . yy)) ->β (\x . a)(yy)[ y \ (ly . yy)] = (\x . a)( (ly . yy) (ly . yy))

Applicative order evaluation of this expression results in infinite substitution. So we see that evaluation order does matter. The Church-Rosser theorem states that if an evaluation terminates when applied to an expression, then the normal-order evaluation of that same expression also terminates. It also states that if any two evaluations terminate when applied to the same expression, then they give the same resulting expression, up to an alpha-conversion.

Quiz

1. Verify that both evaluation strategies yield the same result when applied to:

	((\x.\x.y) c (\z.(\w.(\b.(\a.a) c) z) f))

The result should be y.

2. What is the result of reducing the following using both applicative order and normal order evaluation?

	((\a.x) ((\a.a a)(\a.((\b.a b) a))))

Using normal order it should reduce to x. Using applicative order should result in infinite substitution of (\a.a a)(\a.a a).

References

http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/01.Calc.html
http://www.inf.fu-berlin.de/lehre/WS01/ALPI/lambda.pdf
http://www.cs.rpi.edu/~schupp/entries/COURSES/pl/notes/theory1.html