同學們啊，Covid20已經到達扭腰。是紐約州長鳩毛說他憑直覺知道的。雖然吧。先暫時將越髒越臭越有人愛搞的穿補和女人的屄忘記一下。假設明天有一個飛碟落在你的窗台上，從裡邊走出幾個拇指大小的外星人。或者黑白無常，牛頭馬面帶着鎖鏈來找你。你怎樣與牠們交談？用什麼語言？

摘抄自《維基百科》“λ演算”

λ演算（英語：lambda calculus，λ calculus）是一套從數學邏輯中發展，以變量綁定和替換的規則，來研究函數如何抽象化定義、函數如何被應用以及遞歸的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。

在最簡單的lambda演算中，只使用以下的規則來建構lambda項：
語法       名稱      描述
============================================================
a             變量        表示參數或數學/邏輯值的字符或字符串。
(λx.M)    抽象化    函數定義（M是一個lambda項）。變量x在表達式中已被綁定。
(M N)     應用        將函數應用於參數。M和N是lambda項。

在λ演算中，每個表達式都代表一個函數，這個函數有一個參數，並且會返回一個值。不論是參數和返回值，也都是一個單參的函數。可以這麼說，λ演算中只有一種“類型”，那就是這種單參函數。函數是通過λ表達式匿名地定義的，這個表達式說明了此函數將對其參數進行什麼操作。

lambda演算的語法將一些表達式定義為有效的lambda演算式，而某一些表達式無效。

有效的lambda演算式稱為“lambda項”。

以下三個規則給出了語法上有效的lambda項，如何建構的歸納定義：

1)變量x本身就是一個有效的lambda項；
2)如果t是一個lambda項，而x是一個變量，則(λx.t)是一個lambda項（稱為lambda抽象）；
3)如果t和s是lambda項，那麼(ts)是一個lambda項（稱為應用）。

其它的都不是lambda項。

在lambda演算中，函數被認為是第一類對象，因此函數可以當作輸入，或作為其它函數的輸出返回。

形式化定義

形式化地，我們從一個標識符（identifier）的可數無窮集合開始，比如{a,b,c,...,x,y,z,x1,x2,...}，則所有的lambda表達式可以通過下述以BNF範式表達的上下文無關文法描述：

1. <表達式> ::= <標識符>
2. <表達式> ::= (λ<標識符>.<表達式>)
3. <表達式> ::= (<表達式> <表達式>)

頭兩條規則用來生成函數，而第三條描述了函數是如何作用在參數上的。

（下面的部分我還沒讀懂，呵呵。想妝屄嚇唬我一下的清華北大牛叉人物可要抓緊時間。晚了就錯過機會了。）

lambda演算中的算術在lambda演算中有許多方式都可以定義自然數，但最常見的還是邱奇數，下面是它們的定義：

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

以此類推。

邏輯與謂詞

習慣上，下述兩個定義（稱為邱奇布爾值）被用作TRUE和FALSE這樣的布爾值：

TRUE := λx.λy.x
FALSE := λx.λy.y
(注意FALSE等價於前面定義邱奇數零)

通過這兩個λ-項，我們可以定義一些邏輯運算：
AND := λp q.p q FALSE
OR := λp q.p TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y.p x y

“謂詞”是指返回布爾值的函數。最基本的一個謂詞是ISZERO，當且僅當其參數為零時返回真，否則返回假：

ISZERO := λn.n (λx.FALSE) TRUE

運用謂詞與上述TRUE和FALSE的定義，使得"if-then-else"這類語句很容易用lambda演算寫出。