added lambda lecture

lectures/lambda.md

@@ -0,0 +1,60 @@
+## Back to the Future
+In 1933, Kurt Goedel invented the notion of the general recursive functions.
+In 1936, Alonzo Church invented a logical language known as Lambda calculus.
+In 1936, Alan Turing invented an automaton known as the Turing machine.
+It was not a long period of time before it was possible to prove the equivalence of these three different ideas. Because these three different approaches end up defining the same class of functions, there was a desire to associate that class of functions with those that could be called the computable functions.
+
+## The Church-Turing Thesis
+The **Church-Turing Thesis** states that the functions defined by lambda calculus and turing machines are precisely those that we call computable. This hasn't been proven, so it is a very famous thesis in the theory of computing and computer languages.
+
+## The Grammar of Lambda
+```
+Lambda ::= Variable | Group | Abstraction | Application;
+Variable ::= <letter> 
+Group ::= '(' Lambda ')';
+Abstraction ::= 'λ' <variable> '.' Lambda;
+Application ::= Lambda Lambda
+```
+
+That is the entire grammar for the language of the computable functions. Now, what does it mean?
+
+Lambda expressions always are **left associative**, e.g.  mnp == (mn)p.
+
+In the lambda expression λx.abcxjxxk  we say that the parameter x is **bound**. Note that parameter bindings nest lexically.
+
+An unbound variable in a lambda expression is said to be **free**.
+
+A lambda expression with no free variables is said to be **closed**.
+
+Note that a form that is closed is often referred to as a **closure**. 
+
+## Lambda Conversion Rules 
+
+* α alpha - a bound parameter may be renamed, e.g. λx.xat becomes λy.yat
+* β beta - replace occurrences of a bound parameter with an applied value, e.g.  (λx.xat)b == bat
+* η eta - a lambda binding may be dropped if there are no occurrences of the bound parameter
+
+Lambda only allows for one argument functions, but we can get around that because a multi argument function may be represented as a composition of one argument functions. This is called currying. Ex.  λx.(λy.xy) == λxy.xy and (λxy.xy)ab == ab
+
+
+## Logic in Lambda
+In the following expression, p and q represent arbitrary boolean values.
+```
+TRUE         λx.(λy.x)
+FALSE       λx.(λy.y)
+AND          pq(λx.(λy.y))             // p and q are boolean expressions
+OR            p(λx.(λy.x))q
+NOT          p(λx.(λy.y))(λx.(λy.x))
+```
+
+## Natural Numbers in Lambda
+Natural numbers are functions in Lambda calculus. The number zero "means" do not perform the function f. The number one "means" invoke the function f once. Each following natural number will compose the function f with the result of the previous application.
+
+In the following expressions, interpret, n, as an arbitrary natural number. Successor is the "plus one" function. The interested reader may attempt to calculate 3 + 1 to see if 4 is the answer. 
+```
+0           λf.(λx.x)
+1           λf.(λx.fx)
+2           λf.(λx.f(fx))
+3           λf.(λx.f(f(fx)))
+successor   λn.(λf.(λx.f(nfx)))
+```