lambda

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.

9/17/19

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.

9/17/19

 

λ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 *)

9/17/19

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

9/17/19

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.

9/17/19

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

9/16/19

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). [An expression is considered to be a subexpression of itself.]

9/13/19

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.

9/16/2019

Definition 

In an abstraction λ<variable>.<expr> the <expr> is known as the scope of the abstraction.

Egs. λx.λy.(m x) has scope λy.(m x), and λy.(m x) has scope (m x)

Definition 

An occurrence of a variable v in a lambda expression is bound if it is within the scope of an λv.<expr> abstraction.

Eg. in λx.λy.(m x) the occurrence of x is bound, but the occurrence of m is not bound.

There are widely differing conventions for notation. Let me explain what the problems are and some of the suggestions. We have to capture three types of thing... variables, abstractions, and applications and the problem is that many even quite simple expressions will contain lots of these. So if brackets are used, say with applications and abstractions, there will be lots of them or a bracket omitting convention will be needed coupled with left or right associativity.