Functional Programming (FP) Languages : Lisp, Haskell, Scala, Kotlin, etc.
Inventor of Lambda Calculus : Alonzo Church (1903 – 1995), whose student in Princeton University (1936-1938) was Alan Turing (The Father of Artificial Intelligence).
Lambda Calculus is not : another Differential Calculus !
Note: Calculus has a meaning of manipulating symbolic expressions : either in functions (differentiation, integration) or computations.
Lambda Calculus is almost programming!
I. Syntax of Lambda Calculus:
Notice: it has only one parameter “x”.
- Function definition:
- Identifier reference:
- Function application:
II. Currying 柯里化 : (named after Haskell Curry ) for multiple parameters.
written by “Currying” as :
Syntactic Sugar 语法糖 : a notational shorthand. Eg. “cubic”
cubic = λ x . x * x * x
III. Binding: Every parameter (aka variable) must be declared (syntactically binding).
here, x is bound, but z is FREE (error!)
IV. Two Execution Methods:
- rename variables to avoid conflict
- Eager evaluation strategy : Right to Left (innermost expression first to outermost) or
- Lazy evaluation strategy : Left to Right (outermost expression first to innermost) – don’t compute the value of an expression until you need to – (save memory space and computing time)
- Most FP are Lazy.
- Most Procedural (Imperative) languages (C, Fortran, Basic, …) are Eager.
V. Lambda Calculus fulfilling the 3 conditions for “Turing Complete” Computation :
- Unbounded “Storage” (not necessarily a physical device) – generate arbitrarily complicated values in a variable or many functions without bound.
- Arithmetic – Church numerals (Peano arithmetic using functions): eg z=0, s= z+ 1 => 1 = λ s z . s z => 2 = λ s z . s ( s z ) … => 7= λ s z . s (s(s(s(s(s(s(z )))))))
- Control Flow – TRUE = λ t f . t / FALSE = λ t f . f / BoolAnd = λ x y . x y FALSE / BoolOr = λ x y . x TRUE y / Repetition by Recursion (Y Combinator )
Conclusion: Lambda Calculus = “Computer on paper”
VI. Type – Consistent Model (notation “:“)
eg. λ x : I . x + 3 ( I is Integer Type)
=> The result (x + 3) is also Type I since by inference “+” is of Type I -> I
Reference: “Good Math” by Mark Chu-Carroll https://www.amazon.com/Good-Math-Computation-Pragmatic-Programmers/dp/1937785335/