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
Lambda calculus is a formal model of computation. Others include
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.
((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
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...
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 )
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
M + N == L f L z ( ( M f ) ( ( N f ) z ) )
M*N == L z ( M ( N z ) )
A ^ B == ( B A )
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: