Lambda Calculus is a set of rules for manipulating symbols. They can be
given meanings that map well to computation.
Lambda Calculus Term Grammar
term ::= variable
term ::= ( term )
term ::= λ variable . term
term ::= term term
Rules
Alpha Reduction: (renaming variables)
λ y . M →α λ v . M [y |→ v]) where v does not occur in M.We can change the name of a lambda variable by replacing all occurances of the variable in the body term with a new name that does not appear in the body term.
Beta Reduction: (substitution)
(λ x . M) N →β M [ x |→ N ]All computation can be modeled using Beta Reduction! Examples
1.
( λ x . x ) (λ y . y) →β
2.
S ≡ λ wyx . y(wyx)
Z ≡ λ sz . z
SZ ≡ (λ wyx . y(wyx)) (λ sz . z)
→β
3.
(λ xy . (xy))y
→β
4.
(λ x . (λ y . (x(λ x . xy))))y
→β
5.
(λ f . ((λ x . f (xx)) (λ x . f (xx))))(λ z . z)
→β
(Note: you may need some more space to finish this one.)
Alan Turing's advice on finishing a PhD thesis (from a letter to his mother, 7 May 1938)
My Ph. D. thesis has been delayed a good deal more than I expected. Church made a number of suggestions which resulted in the thesis being expanded to an appalling length. I hope the length of it won't make it difficult to get it published. I lost some time too when getting it typed by a professional typist here. I took it to a firm which was very well spoken of, but they put a very incompetent girl onto it. She would copy things down wrong on every page from the original, which was almost entirely in type. I made long lists of corrections to be done and even then it would not be right. ... I had an offer of a job here as von Neumann's assistant at $1,500 a year but decided not to take it.
Simulating computing with Lambda Calculation
T ≡
F ≡
if F T F
→β
0 ≡
1 ≡ succ 0 ≡
2 ≡
first ≡
rest ≡
null ≡ λ p . T
null? ≡
λ x . (x λ y .
λ z . F)