lambda

10 Software

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).

10 Software

We are going to want to deal with lists, numbers, and suchlike. To do this we have to choose representations. Let me warn you that some of this is going to appear too too clever (this is not my doing). It is also not unique. There are many different ways of doing this, all of which achieve the same ends.

For lists we will need a constructor, an empty list, accessors for the head and tail, and a predicate to tell us whether a list is empty.

10 Software

We will take the doing of lambda calculus in the system to the level of writing one recursive function.

A lambda expression without any free variables is a closed lambda expression or a combinator.
Combinators can have free variables in its sub-expressions. We like combinators, simply because they do not require any external context for their evaluation (there are no free variables to worry about).

Some important combinators.

λx.x (* IDENTITY *)

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

10 Software

Our main weapon is going to be beta-reduction (i.e. simple function application). The sub-expression which gets reduced is known as a redex. When you keep beta-reducing an expression you may reach the stage where there are no further reductions to be done.

Definition.

A lambda expression is in normal form if no subexpression of it has the form (λx.P Q).

That is, it is in normal form if no further beta reductions can be done.

There are other concepts too, which will be important later.

10 Software

Alpha conversion (Rewrite of bound variables):-

Any abstraction λ<variable1>.<expr> can be converted to λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.

10 Software

The basic grammar for Lambda expressions is:

<expression> := <variable> | <function> | <application>
<function> := λ<variable>.<scope>
<application> := (<function expression> <argument expression>)
<scope>:= <expression>
<function expression>:= <expression>
<argument expression>:= <expression>
<variable>:= any string of characters (excepting ( λ . )) starting with a lower case letter

9/18/19

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...

9/18/19

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.