lambda
這幾天研究了一下 lambda 之後，發現 lambda 根本不只是匿名的函數這麼簡單而已。在很早之前邱奇就很想用數學表達世界上所有的事情。而當中為為了設計一套方法來判斷什麼樣的東西是可以拿來被計算的，lambda 就被獨立出來發展了。
而 lambda 運算其實包含的元素其實很簡單，只有包含兩個東西，就是變數跟函數而已。
先講一下如何表示一個 lambda 表達式 ( lambda term )，接著舉幾個例子就能很快看懂這套數學系統了。
lambda 表達式的規則(以下用 t 來代表 lambda 表達式，變數用 x 來代表）：
- x
- λx. t
- t t
光是自己取名一個變數 x, y , z 就能構成基本的 lambda 函數，不過這裡的變數更精確一點的說應該是符號，只要是自己設計的系統中可以拿來用的符號像是 1, 2, 3, x, y, z, +, - 都能夠拿來使用
接著如果要表示一個可以傳入參數的函數來達成 x + 1 這個動作，
以往的數學符號裡我們會表達成：
f(x) = x + 1
在數學裡面我們要自己為這個函數取名叫做 f ，但是在 lambda 只關心傳入的變數還有函數運算的本體而已，所以上面的例子我們可以改成像下面這樣：
λx. x + 1
我們用 λ 表示接下來是一個可以讓人傳入參數 x 的 lambda 表達式，而參數 x 跟函數的本體則是用 . 去隔開，這樣就構成函數的基本宣告了。
談到現在還有奇怪的地方，那就是講解到現在只有講出怎麼表達一個函數，那我要怎麼樣把數字丟進我的函數去計算呢？
那就是第三條規則啦！
看到 t t 這條規則，其中一個應用就是把右邊的表達式丟到左邊去運算，舉個例子比較好明白：
(函數) (要丟入的參數)
(λx. x + 1)(5)
=> 6 #這行是說明計算的結果為 6 ，箭號並不是表達式的意思
這個表達方式代表我把 5 丟到左邊運算式去計算，但是為了避免 5 被當成左邊 lambda 表達式的本體，所以用括號區隔開來說明。
如果現在我們需要傳入兩個參數給 lambda 函數要怎麼辦呢？其實依然可以透過這個規則去表達。
不過在這之前先猜一下要怎麼去宣告這個函數是包含兩個參數呢？我們可能會猜想成下面這種方法：
λx y. x + y #wrong
或者
λx, y. x + y #wrong
基本上 lambda 函數遵循古老的數學模型，就是函數只有一個參數輸入
當然某些支援 lambda 的程式語言是可以直接表示出有多個參數的 lambda 表達式。
但是為了符合數學的概念
所以我們需要把上面的方法改寫一下，透過第三個規則將他寫成 lambda 包住 lambda 的方式：
λx.λy. x + y
等同於
(λx.(λy. x + y))
這個轉換過程也稱為 currying 。這種表達方式代表我 λx. 後面的函數本體是 λy. x + y ，如果有參數丟進來，我會把函數本體 λy. x + y 所有的 x 給換掉，就剩下 (λy. 傳入的某東西 + y) ，如果再傳入一個參數又會換掉 y 。
所以說如果有數字傳入 lambda 裡面，會把丟進去的參數，從左到右一個一個丟進去，一樣拿 x + y 的例子來解釋：
(函數) (參數 1)(參數 2)
(λx.(λy. x + y)) (4) (8)
=> (λy. 4 + y)(8) # 把第一個參數 4 丟進去把所有的 x 都換成 4
=> 4 + 8 # 把第二個參數 8 丟進去換掉所有的 y
=> 12
我也可以把 lambda 做得複雜一點，把函數當成參數丟進去
(函數) (參數 1) (參數 2)
(λf.λx. f x)(λa. a + 1)(5)
=> (λx.(λa. a + 1) x) (5) # 將 f 代換為第一個參數 (λa. a + 1)
=> (λa. a + 1)(5) # 將 x 代入第二個參數 5
=> 5 + 1 # 將 a 代入參數 5
=> 6
這段說明了丟進去的參數，不只有簡單的數字符號，也能再把另一個 lambda 函數丟進去計算。
光是這三個規則的結合方式就能構組成很多東西，也促進了 functional language 的發展，如 Lisp, Scheme, Pyhton, Haskell
看到這裡已經對於表示 lambda 跟計算 lambda 有了基本的認識了，但是仔細套用這三個規則會發現還有一個規則沒有用上
如果今天左邊的函數是個變數 x，例如下面這樣：
(5)((λx. x + 1)
這樣依然符合規則，不過其意義等到講完邱奇數會比較讓人明白一點。
邱奇數
看了 lambda 的使用方式之後，也能了解 lambda 說明了所有的事物都能用函數來表示。而邱奇更是進一步的把像是基本的自然數、加減乘除這類的東西也用 lambda 來表示。
起初小弟我真的看不太懂邱奇表達自然數的方式，所我先從他表示布林函數的方式來介紹好了。
布林函數有 true 跟 false 兩個值，在數位系統中則可能為 0 跟 1。
這就麻煩了呀，邱奇不想被 0, 1 跟 true, false 先給卡住，他希望不管如何，我先用 lambda 函數表示出來就對了，那些符號之類的絕對不是布林函數的重點，我先把他表示出來，到時候你在告訴我你要用什麼符號來表示就好了。
所以邱奇的布林表示方式像是下面這樣：
true = λx.λy. x
false = λx.λy. y
如果寫成 scheme 跟 python 的話會是這樣：
Scheme:
(define true (lambda (x y) (begin x))) #直接用雙參數的方法表示了
Python:
true = lambda x, y: x
可以看到 true 跟 false 等待人家輸入兩個參數，分別假設為 x 跟 y ，對於 true 跟 false 只不過是兩個相反的值罷了。所以 true 這邊永遠傳回 x 而 false 傳回 y，這樣一來不管 x, y 輸入些什麼東西，永遠不會相同了。
因此如果要達到數位世界的 true false 那我們可以將 lambda 改成這樣：
true = (λx.λy. x)(1 0) => 1
false = (λx.λy. y)(1 0) => 0
這種函數表達的概念在接下來介紹邱奇的自然數（正整數）時很重要，邱奇依然想把一些東西抽掉，光是靠 lambda 就能夠表達自然數的概念了。
這次邱奇抽走等待使用者去定義的東西有兩個，一個是遞增的方法，另一個是從哪個起始值開始起跳，所以下面把遞增的函數先用 f 來表示，而起始數字用 x 表示：
0 := λf.λx. x
1 := λf.λx. f x
2 := λf.λx. f (f x)
3 := λf.λx. f (f (f x))
下面以此類推
0 這個數字就是起始值的意思，所以直接保留 x 就好了
1 就是遞增起始值一次的意思，所以透過 f 去遞增 x 一次，那就是 1 的意義了
2 可以看出來是遞增了一遍，又去呼叫 f 再去遞增一遍，所以可以看到 f (f x) 這樣的形式，自然結果就是 2 囉
如果按照地球上的定義，我們遞增的方法其實就是 x + 1 ，而自然數的起始值就是 0。邱奇這種表示方式可能是為了避免某個地方不是遵循這種規則，或許我們有個世界起始值是 0 但是他的遞增方法是 x - 1 的顛倒世界，那邱奇數依然符合他們的自然數。
所以現在我想把邱奇數代入地球的表示方式，我們可以表示成下面這樣：
丟進去的兩個參數都是(λa. a + 1)(0) 第一個參數代表如何遞增，第二個參數代表起始值為 0
下面大中小括號的用途只是作分隔而已
0 = (λf.λx x)(λa. a + 1)(0)
=> (λx x)(0) #函數本體沒有用到 (λa. a + 1) 所以代換 f 時，並沒有任何東西出現
=> 0
-----------------------------
1 = (λf.λx. f x)(λa. a + 1)(0)
=> [λx.(λa. a + 1) x](0) #先把第一個參數 (λa. a + 1) 丟進去把 f 換掉
=> [(λa. a + 1)(0)] #把第二個參數 0 丟進去換掉 x ，結果產生新的函數囉
=> 0 + 1 #把 0 給丟進去計算
=> 1
-----------------------------
2 = (λf.λx. f (f x)) (λa. a + 1) (0)
=> {λx. (λa. a + 1) [(λa. a + 1) x]} (0)
=> (λa. a + 1) ((λa. a + 1) 0)
=> (λa. a + 1) (0 + 1)
=> (λa. a + 1) (1)
=> 1 + 1
=> 2
透過上面的計算過程應該可以比較明白如何計算出邱奇自然數了。透過不斷的呼叫遞增函數就能算出我們要的自然數了。
不過這裡有個問題，看到 3 := λf.λx. f (f (f x)) 這個樣子，雖然我們可以看懂就是不斷的呼叫遞增函數，但是如果要表達 100 這個自然數，那不是要寫出 100 個 f 去表示要呼叫 100 次遞增函數了嗎？
所以應該還記得上一節講到 (5)((λx. x + 1) 這種奇怪的表達方式吧？這裡就是用來表示，如果未來後面又有個參數丟進來，像是：
[(5)(λx. x + 1)](10)
這種表示方法意思就類似上面的 f (f (f x))，代表他會套入這個函數 5 次。
所以上面的自然數的部份我們可以稍微改寫一下，變成下面這樣：
λn.λf.λx. n f x # n 代表你需要的是第幾個自然數
拿剛剛的自然數 3 下去的算的話，大致的運算會是這樣：
(λn.λf.λx. n f x)(3)(λa. a + 1)(0) # 3 表示我要第幾個自然數，最右邊兩個參數依然跟前面相同
省略前面的代換過程
=> (λa. a + 1)(0)
=> (λa. a + 1)(0+1) # 第一次把參數丟進去 +1
=> (λa. a + 1)(0+1+1) # 第二次把參數丟進去 +1
=> (0+1+1+1) # 第三次把參數丟進去 +1
這個過程不太正式啦，但是比較好理解
當然也可以直接先寫成
f (f (f x))
=> 長太醜我不寫了
到這裡才算真的把 lambda 表達的方式完全講完了，但是邱奇設計的這套 lambda 可以做的事情可沒有那麼少。
他也能拿來表示基礎的四則運算，當然他也抽走了基本的元素，讓他能符合不同世界的要求，下面用加法來舉例
加法如下面這個樣子表示：
λm.λn.λf.λx. m f (n f x)
這個加法的方式可以讓人丟入四個參數，裡面的 f 跟 x 一樣是像前面所講的那樣，一樣是被抽掉的遞增方法 f 跟起始數值 x。所以 m 跟 n 就是用來相加的兩個數字囉。
有沒有看到很熟悉的一個東西 n f x 是不是就是我前面用來表示自然數 n 的方式呢？
所以 n f x 就是先不斷的重複的使用遞增函數 f ，把起始值加到 n 為止。
這時候就會變成 m f n 這個樣子
再去使用 f 遞加 n 加個 m 遍，這就是 m + n 的作法囉。
邱奇的 lambda 包含了這種基礎四則運算，也能夠計算布林的 and, or, not 我想邱奇可能真的很希望用函數表達世界上的一切吧！
當然邱奇的 lambda 演算還有一些沒有提到的東西，像是我一開始提到的判斷函數是否可以被計算、兩函數之間是否相同。
甚至在還沒有電腦的時代，就開始探討如果這些函數的變數有型別的話會如何。因此電腦這塊就開始有一些型別推導之類的東西出現可以讓人研究。