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 lambdaexpressions  
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 lambdacalculus(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 betaredexes is important...Consider this lexp:( 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 betaredex 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 betaredex 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 Nfold 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 ) )

Lexp to try:
