1. BCCC (Bi-Cartesian Closed Category): PRODUCT (tuple) , SUM (either) , EXPONENTIAL (function)
2. UNIT, ZERO, Absurd
The mathematicians proved there are ONLY 7 solutions.
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”.
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:
V. Lambda Calculus fulfilling the 3 conditions for “Turing Complete” Computation :
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/
There exists in almost all Universities a clear division between pure and applied mathematics. A friendly (and sometimes not so friendly) rivalry exists between both sides of the divide, with separate conferences, separate journals and in many cases even a whole separate language. Category Theory was seen as such an abstract area of research that even pure mathematicians started to refer to it as “abstract nonsense“, and until the mid 1980’s almost all category theorists occupied a place hidden somewhere up above the ‘cloud level’ in the highest reaches of the peaks that defined “pure” maths.
By the mid 1990’s and then by the turn of the millenium, a whole world of computer programmers were learning basic category theory as part of their induction into functional programming. The best known product of these efforts is the Haskell language, but even in the past 7 or 8 yrs, workshops on category theory for computer programmers of all types have flourished and proliferated. It is almost as if there are two separate communities masquerading as one – mathematical category theory and computer programming category theory – and never the twain would meet. Or so it seemed, until now.