Lambda Calculus

Lambda Calculus Interpreter

Fun to try after you learn the basics of the syntax

Notes

Lambda Calculus

Let's examine some of the theoretical foundations of computation, specifically functional computation.

You may wish to read early parts of this paper:

Notes we will refer to

Lambda calculus is a formal model of computation. Others include
• Turing Machine
• Post production system (phrase-structure, unrestricted, type-0 grammars)
• Graph/Net models
• Petri-nets with inhibitor arcs
• predicate/transition nets
• debit-nets under forced anihilation
• Relational model (resolution/unification, Prolog basis)
• Theory of recursive functions

Basics:

• variables are lambda-expressions (lexp)
• lambda abstractions (function definitions) are lexp
• function applications are lexp

For example:

• variables: a, x, foo, bar
• lambda abstraction: lambda x 2*x
• function application: ( (lambda x 2*x) 5 ) specifies value 10

Syntax examples for lambda-expressions

x a single variable
lambda x x a function abstraction with one argument (x) and the body "x"
(x y) function application where function lexp "x" is applied to arg lexp "y"
(lambda x x y) function "lambda x x" applied to "y"
lambda x (x y) function abstraction with one variable "x" and body "(x y)" which is a function application
(lambda x x lambda y y) function application: "lambda x x" is applied to "lambda y y" as an argument
lambda x (x (y x)) function abstraction: body is "(x (y x))" which is an application
lambda x lambda y x function abstraction defining function of one variable "x" with body "lambda y x" which is another function abstraction.
lambda x lambda y (x lambda x lambda y y) good and strange

Reductions

Reduction == computation in lambda-calculus

(lambda x M A) can be reduced by substituting A into M for all free occurrances of x.

Examples:

• (L x x (y z)) --> (y z)
• ( L x x L x x ) --> L x x
• (L x (x y) L z z) --> L z z y --> y
• (L x (x x) L x (x x)) --> (L x (x x) L x (x x)) --> ... nonterminating
Example with abbreviations:
```  ((L x L y ((+ x) y) 1) 4)
--> (L y ((+ 1) y) 4)
--> ((+ 1) 4)
--> 5
```
Here we depend on some externally supplied semantics for the symbol "+" which appears where a lambda abstraction must be

```  (L x L y (x y) (y z)) --> ...?? need renaming here to avoid conflicts

naieve approach:

--> L y ((y z) y)    this "captures" the y in (y z) which
was previously unbound

rename:

(L x L k (x k) (y z)) -->  L k ((y z) k)

which is a different function from L k ((k z) k)

```

Order of evaluation of beta-redexes is important...

Consider this l-exp:
```  ( L x (x x) L x (x x) )
```
This expression has no normal form, i.e., there is no way to reduce it so that reduction will terminate.

Now consider this one:

```  ( L x y ( L x (x x) L x (x x) ) )
```
Here's how this one works... it is an application of the function
```  L x y
```
to the argument
```  ( L x (x x) L x (x x) )   <--- this is a function application
that will not terminate... it
takes it's argument and replicates
it...
```
so if you use an eval order that tries to eval the argument before you call the outermost function you will not terminate.

However, the outermost function ignores it's argument and just returns "y" no matter what the argument is. So normal order eval (outermost, left most first) will reduce fine to "y" as the normal form... applicative order will never reduce.

Normal Order Reduction

(underlining indicated the beta-redex for each step)
```     ( L x y ( L x (x x) L x (x x) ) )
-----
```
so we plug the arg "( L x (x x) L x (x x ) )" into all occurrances of the bound var "x" in the body of the function "L x y"... and there are no such occurrance so the problematic arg goes away... leaving
```     y
```

Applicative Order Reduction

(underlining indicated the beta-redex for each step)
```     ( L x y ( L x (x x) L x (x x) ) )
-----------------------
```
so we plug the arg "(L x x x)" in for each of the "x" in the body if the function "(L x x x)"... we get
```     ( L x y ( L x (x x) L x (x x) ) )
-----------------------
```
and we have the same problem back... and continue... ad infinitum..

We know these things...

1. some l-exps do not terminate when reduced

2. some l-exps fail to terminate when reduced one way, but reduce successfully when reduced a different way

3. (Church-Rosser) for a given l-exp, all terminating reduction sequences end in the same reduced l-exp

4. If you choose Normal order reduction (outer-most, left-most redex first) you will get a terminating reduction sequence *if one exists*... this models lazy evaluation in functional languages
 Booleans boolean (truth) values are functions of two arguments... "true" returns the first arg, and "false" returns the second arg. T == L x L y x F == L x L y y Then boolean operators can be defined... NOT simple reverses the sense of its arg... so if you do (NOT T) you get F... NOT == L x ( ( x F ) T ) AND == L x L y ( ( x y ) F ) OR == L x L y ( ( x T ) y ) in class, do XOR Integers go over function ZEROP, SUCC, ADD in class, do MULT Lists/pairs from text Integers 1 == L f L x ( f x ) 2 == L f L x ( f ( f x ) ) N == L f L x ( f .... ( f x ) ... ) f applied N times ( N f ) is L x ( f ... ( f x ) ... ) which is a function abstraction ( N f ) b ) is (f ... ( f b ) ... ) is an N-fold application, a value Try this: apply ( M f ) to ( ( N f ) b ) ( ( M f ) ( ( N f ) b ) ) ```gives ( f ... f ( f ... f ( f b ) ... ) ... ) with M+N f's in the list M here N here ``` ADDITION: M+N == L f L x ( ( M f ) ( ( N f ) x ) ) ADDITION: + == L A L B L f L x ( ( A f ) ( ( B f ) x ) ) The second form is fully abstracted for the two numbers being added so it is the operation itself Addition M + N == L f L z ( ( M f ) ( ( N f ) z ) ) + == L A L B L f L z ( ( A f ) ( ( B f ) z ) ) Mult M*N == L z ( M ( N z ) ) * == L A L B L z ( A ( B z ) ) Exponentiation A ^ B == ( B A ) ^ == L A L B ( B A ) Pairs pair == L a L b L f ( f ( a b )) head == L g ( g ( L a L b a ) ) tail == L g ( g ( L a L b b ) ) L-exp to try: XOR one that lengthens... maybe triples Lx ( x ( x x )) Lx ( x ( x x )) one that differs in semantics if evaled L-R vs. R-L