Reduction Strategies


Much of what is presented here applies both to the lambda calculus and to combinatory logic.

There is often a choice of reduction order, for example

(λx.(+ x x) (+ 1 2))

do we want to go λx.(+ x x) (+ 1 2) -> (+ (+ 1 2) (+ 1 2)) -> (+ 3 3) -> 6 or should we prefer λx.(+ x x) (+ 1 2) -> λx.(+ x x) 3 -> (+ 3 3) -> 6 ?

Some definitions...


Combinatory Logic I


Combinatory logic is 'simplified' way of doing the lambda calculus. In the lambda calculus there are variables and constants, applications, and abstractions; combinatory logic makes do with variables and constants, and applications only—abstractions are done away with. There are more rules for reduction in combinatory logic, but since all variables are free there are none of the complications of capturing, sound substitutions, and name rewrites.

Translating Functional Programming Constructs into Lambda Calculus


One has to be of an extremely unusual disposition to wish to work in the bare lambda calculus.

What is standard is to extend its expressions by adding various constants, and extend its reduction rules by adding reduction rules under the rubric of delta-reduction rules. These constants are understood to name familiar constants or familiar functions; for example, integers may be added and the function PLUS; then if an expression amounts to a suitable application, for example, PLUS 1 2, then the appropriate delta rule can be brought in to reduce this to 3.

Operational and Denotational Semantics


What has been provided thus far are the rules for reducing expressions-- this amounts to the operational semantics of the lambda calculus.

We can also provide a denotational semantics for it. That is, for every expression in the λ-calculus we can say what value it should denote. This can be done by producing a mathematical function Eval[[]] which will take expressions to values. We do this by cases for the three types of l-expression.


Normal Order and Applicative Order Reduction


As we have seen, often a lambda expression can be reduced in different ways ie there will be more than one reduction that could be applied, at some stage in the reduction, and so, among the possible reductions, there is a choice as to which reduction to apply first.

There are a variety of reduction strategies (left to right, right to left, random, in to out, out to in, in to out left to right, etc.). Among these, two are prominent.

Review of Lambda Combinators



λx.x (* IDENTITY *)

λx.(x x) (* SELF APPLICATION *)


λx.λy.λz.(x (y z)) (* COMPOSITION *)
λfirst.λsecond.λargument.(first (second argument))) (* composition, again *)


λx.λy.x (* TRUE *)
λfirst.λsecond.first (* true, again *)


λx.λy.y (* FALSE *)
λfirst.λsecond.second (* false, again *)

Lambda Combinators III: Recursion and the Fixpoint Combinator


Now we can attempt to write a recursive function. Let us try for a length of list function. Something like

length(list) = df. If (list is empty) then 0 else succ(length(tail(list)))

we can do all this with the materials we have apart from the fact that the name 'length' appears in the body of the function and in lambda calculus there are no names.

This obstacle is overcome by what is known as a fix-point combinator (and the next little piece is something with intellectual content).