Lambda Calculus
Table of Contents
- Equivalent to procedural computing used in turing machine. They can be translated to each other.
- Turing machine and lambda calculus represents the two opposite side within the deciplines of computer science. Which is bottom-up approach and top-down approach.
- It was devised by Alonzo Church
1. Rules
1.1. Construction
- Of Lambda Terms
- \(x\): A variables is a sequence of symbols representing a parameter.
- \((\lambda x.M)\): A lambda abstraction is a function definition that takes the bound variable \(x\) and returns \(M\).
- \((M\ N)\): An application that applies \(M\) to an argument \(N\).
1.2. Reduction
- Operations
- \((\lambda x.M[x])\to (\lambda y. M[y])\): α-conversion
- \(((\lambda x.M)\ N)\to (M[x:=N])\): β-reduction
- The result of reduction is called β-normal form.
2. Notation
- \((\lambda x.\lambda y.x + y + 1)\ 2\ 3 = 6\)
- It can be abbreviated: \(\lambda a.\lambda b.\lambda c.b = \lambda abc.b\)
3. Combinatory Logic
- The expressions in combinatory logic can be directly translated into the language of lambda calculus.
- Study of first class, higher order functions with no free variables. Study of combinators.
3.1. Combinators
- Every Program can be written in terms of S and K, Moreover, in terms of ι.
3.1.1. Definition
- Functions with no free variables.
3.1.1.1. I
- Ix = x
- λx.x
3.1.1.2. K
- Kxy = x
- λx.λy.x
3.1.1.3. N
- N := KI
- Nxy = y
- (λx.λy.x)(λz.z) = λy.λz.z
3.1.1.4. B
- Bfgx = f(gx)
3.1.1.5. C
- Cfgx = fxg
3.1.1.6. S
- Sfgx = fx(gx)
3.1.1.7. W
- Wxy = xyy
3.1.1.8. S' or Φ
- Starling' or Phoenix
- Φfghx = f(gx)(hx)
- Φ := B(BS)B
3.1.1.9. D
- Dfgxy = fx(gy)
3.1.1.10. T
- Txf = fx
- T := CI
3.1.1.11. M
- Mf = ff
- M := SII
3.1.1.12. V
- Vxyz = zxy
- V := BCT
3.1.1.13. Y
- Yf = f(Yf)
- This enables recursion.
- Y := BM(CBM)
- By Haskell Curry
- Θ := M(B(SI)M)
- By Alan Turing
- Essentials: Functional Programming's Y Combinator - Computerphile - YouTube
- λf.(λx.f(xx))(λx.f(xx))
- This is general recursion
- Self-application, the very idea of Haskell Curry
- λf.(λx.f(xx))(λx.f(xx))
3.1.1.14. Ω
- Ω = Ω
- Ω := MM
3.1.2. Extensionally Equal
- They are the same in effect.
Combinators are evaluated lazily, which means the expressions in parenthesis stay as is until it is the leading combinator and the evaluation happens from the leading one.
3.2. History
- It was developed in search of the foundation of mathematics.
- Schönfinkel
- Curry
- Church
- Turing
3.3. Church Encoding
3.3.1. Boolean
- T - True : K
- F - False : KI = CK
- NOT : C
- or NOT := C(T False) True
- AND : p => q => pqp
- OR: p => q => ppq
- BEQ: p => q => p(q)(NOT q)
3.3.2. Natural Numbers
- Pair x y := Vxy
- Pair x y True = x, Pair x y False = y
- 0 = f => a => a
- 0: I
- 1 = f => a => fa
- SUCC = n => f => a => f(nfa)
- or SUCC := Pair False
- n = SUCC n-1
- ISZERO = n => n (K False) True
- or IsZero := T True
- MULT = B
4. Currying
4.1. Definition
- The natural bijection between: \[ \operatorname{curry}\colon Z^{X\times Y} \to (Z^Y)^X. \]