Lambda Calculus – The Math Behind Functional Programming

Functional Programming (FP) Languages : Lisp, Haskell, Scala, Kotlin, etc.

Other non-FP influenced by Lambda Calculus: Python, Ruby, Javascript, Java 8, C++

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: \boxed {\lambda \text { param . body }}

eg. \lambda \: x \: . \: x + 1

Notice: it has only one parameter “x”.

  1. Function definition: \lambda
  2. Identifier reference: x
  3. Function application: x + 1

II. Currying 柯里化 : (named after Haskell Curry ) for multiple parameters.

eg. \lambda \: x \: . \: (\lambda \: y \: . \: x + y)

written by “Currying” as : \boxed { \lambda \: x \: y \: . \: x + y}

Syntactic Sugar 语法糖 : a notational shorthand. Eg. “cubic”
cubic = λ x . x * x * x

III. Binding: Every parameter (aka variable) must be declared (syntactically binding).

eg. \lambda \: x \: . \: z x

here, x is bound, but z is FREE (error!)

IV. Two Execution Methods:

1. \alpha \text{ conversion }

  • rename variables to avoid conflict

2. \beta \text{ reduction} \text { - Apply a function}

  • 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 :

  • UnboundedStorage” (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/

Advertisements

直观 数学 Intuition in Abstract Math

Can Abstract Math be intuitive, ie understood with concrete examples from daily life objects and phenomena ?

Yes! and Abstract Math should be taught by intuitive way!

1. 直观 线性空间 : Intuition in Linear Space

(Part I & II) 矩阵 (Matrix), 线性变换 (Linear Transformation)

http://m.blog.csdn.net/myan/article/details/647511

(Part III)

http://m.blog.csdn.net/myan/article/details/1865397

Animation: English (Chinese subtitles)

http://m.bilibili.com/video/av6731067.html

2. 直观 群论 (Intuition in Group Theory)

https://www.zhihu.com/question/23091609

https://www.zhihu.com/question/23091609/answer/127659716

Univalent Foundation – Computer Proof of All Maths

The scary complex field of Math worried the mathematicians who would prove a theorem relying on the previous theorems assumed proven correct by other mathematicians.

A sad example was Zhang YiTang (1955 – ) who prepared his PhD Thesis based on a previous “flawed” Theorem proved by none other than his PhD Advisor Prof Mok in Purdue University. Unfortunately his Thesis was found wrong, and the tragic happened to Zhang as he had revealed the mistake of his PhD advisor who insisted his (Mok’s) Theorem was correct. As a result Zhang failed the 7-year PhD course without any teaching job recommendation letter from his angry advisor. He ended with a Subway Sandwich Kitchen job offered by his Chinese friend, sleeping in another Chinese music conductor’s house on a sofa. It was there he spent another 7 years thinking on Math, finally an Eureka breakthrough one 2013 morning in the backyard wild forest – the proof of the famous “70 million Prime Gap Conjecture”!

Univalent Foundation was born out of the same requirement by the (late) mathematician Vladimir Voevodsky (1966 – 2017) [#] – Use computer to prove Mathematics !

https://www.quantamagazine.org/univalent-foundations-redefines-mathematics-20150519/

Note : [#] Vladimir Voevodsky

Category Theory – Purest of pure mathematical disciplines may also be a cornerstone of applied solutions in computational science

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.

https://www.linkedin.com/pulse/category-theory-classic-dichotomy-purest-pure-may-also-khan-ksg/

Zhihu 知乎: 环Ring, 域Field, (半Semi-)群Group, 幺半群 MonoId

数学中代数的有两个名词:环,半群,请问环为什么叫做环,它和汉字里的环(字典中的意思)有什么相同之处;同样,半群为什么叫做半群,这个”半“字是怎么解释呢?

[葛利流,数学科技]

(I) 环和域
环 (Ring) 是德文, 这名词是David Hilbert发明的。
“环”最好的例子: 整数(Integer) 记作 Z (德文Zahl) 是个环。 他研究 Clock Arithmetic 时钟 是个 Modular Arithmetic (Mod 12)运算, 比如 15 = 3 mod 12

钟表上的整数 Z 数字 排成 一个钟的环状, 故称 此数是 “Zahl Ring” 整数 “环”。

Hilbert 的得意女弟子 Emile Noether 把 环论 发扬光大, 创造 “Noether Ring”。

如果 把 “12” 变成 任一素数 p , “环”就升级成”域” (Field) – 除了有环的( + – *) 运算, 还可以 (÷)。

Hilbert 发现 “环”有个重要性质是含有 “理想” (Ideal) – 理想 * 任何”外面”的东西 还回来”里面”。
例子: Z Ring 里有 “0”, 2Z, nZ…
0 * 任何Z数 => 回来 “0家族里面”
偶数 2 * 任何Z数 => 回来” 偶数 (2Z)家族里面”

大名鼎鼎的中国古代算术”韩信点兵”就是 含有 “环 和理想”的理论。

(II) 群 Group / 半群 Semi-Group / 幺半群MonoId
Group 群 有4个性质 C.A.N.I.
C: Close 封闭性
A: Associative 连续性
N: Neutral (or Identity = Id) 幺元
I: Inverse 逆元

Semi-Group 半群 只有2个性质: C.A.

Monoid 么半群 : C.A. + N (= Id) => Mono + Id

https://www.zhihu.com/question/20564445/answer/233486338