Notes |
Lambda CalculusLet'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 Encoding Lambda calculus in ML
Boolean values and operators
Church numerals
Lambda Calculus as a basis for functional programming languages
|
Lambda calculus is a formal model of computation. Others include
|
Basics:
For example:
|
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 |
ReductionsReduction == 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 L y ((+ x) y) 1) 4) --> (L y ((+ 1) y) 4) --> ((+ 1) 4) --> 5Here 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 yto 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...
|
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
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 )
Integers
Lists/pairs
|
Integers
1 == L f L x ( f x )
( 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 )
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 ) )
Mult
M*N == L z ( M ( N z ) )
Exponentiation
A ^ 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:
|