怎麼理解邱奇計數？

01-27

SICP里CONS CAR CDR的實現已經把我嚇尿過一次了。
它居然在習題2.6里說還有一個更讓人醍醐灌頂的東西：church計數。
(define zero (lambda (f) (lambda (x) x))) (define (add-1 n) (lambda (f) (lambda (x) (f ((n f) x)))))
怎麼理解這玩意兒？
------

拓展：和皮亞諾算術、邱奇-圖靈論題等有何聯繫？

在靜態類型函數式語言的背景下，理解了 ADT（algebraic data type）的 Church encoding，回頭看 Church numerals 就豁然開朗了。

{-# LANGUAGE RankNTypes #-}


data Nat = Zero | Succ Nat
newtype NatChurch = NatChurch (forall r . r -&> (r -&> r) -&> r)
zeroChurch :: NatChurch

zeroChurch = NatChurch const
succChurch :: NatChurch -&> NatChurch

succChurch (NatChurch n) = NatChurch (z s -&> s (n z s))
addChurch :: NatChurch -&> NatChurch -&> NatChurch

addChurch (NatChurch n) (NatChurch m) = NatChurch (z s -&> n (m z s) s)
evalChurch :: NatChurch -&> Int

evalChurch (NatChurch n) = n 0 succ
newtype NatScott = NatScott (forall r . r -&> (NatScott -&> r) -&> r)
zeroScott :: NatScott

zeroScott = NatScott const
succScott :: NatScott -&> NatScott

succScott n = NatScott (\_ s -&> s n)
addScott :: NatScott -&> NatScott -&> NatScott

addScott n (NatScott m) = m n (succScott . addScott n)

evalScott :: NatScott -&> Int evalScott (NatScott n) = n 0 (succ . evalScott)

以上定義了一個 inductive Nat。這個 data type 可以用不同的方法做 encoding，也就是用普通的函數來進行編碼。代碼展示了 Church 和 Scott 兩種不同的編碼方式，包括相應的 zero/succ constructor，以及一個加法操作的樣例，最後可以用 eval 轉回普通的 Int，用於檢驗結果是否正確（不妨在 ghci 下試幾個例子）

Church encoding 的實質，就是把 datatype 上的 fold 操作用 CPS 方式表示。Scott encoding 的實質，就是把 datatype 的每種 case 上的模式匹配操作用 CPS 方式表示。

最後，去掉各種 newtype 相關的轉換，用 untyped lambda calculus 把 zero/succ/add 等定義寫出來，對照 wikipedia 上的定義，一切盡在不言中。

quiz：

1. Church/Scott encoding 孰優孰劣？適用範圍分別是？

2. Church encoding 與 Finally tagless style 之間的隱藏關聯？

我也是剛看到這裡，我的理解如下：

首先看對於數的定義：

(define zero (lambda (f) (lambda (x) x))) (define one (lambda (f) (lambda (x) (f x)))) (define two (lambda (f) (lambda (x) (f (f x)))))

這裡我們可以看到所謂的數只是將過程f應用於x的次數。

對於add-1：

(define (add-1 n) (lambda (f) (lambda (x) (f ((n f) x)))))

結果就等於將f再應用於n一次。

上面這些估計不好理解，來點直觀的。

－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－－

下面把f和x形象化。

(define (inc x) (+ 1 x))

下面我就把這個過程作為f，並且把0作為x傳入zero, one和two。

((zero inc) 0) ((one inc) 0) ((two inc) 0)

結果如下：

1 ]=&> ((zero inc) 0) ;Value: 0


1 ]=&> ((one inc) 0)

;Value: 1

1 ]=&> ((two inc) 0) ;Value: 2

發生了什麼呢？以two為例，把inc和0分別作為參數傳遞給two所代表的過程，用代換模型最後可以得到(inc (inc 0))，結果就是２啦。

至於add-1:

(((add-1 one) inc) 0)

結果如下：

1 ]=&> (((add-1 one) inc) 0) ;Value: 2

運用代換模型（省略了一些步驟）：

(inc ((one inc) 0)

(inc (inc 0)) ;在過程f(inc)的基礎上又用了一次f(inc)。

好了，現在會過頭再看看最原始的定義。

ps:有錯誤請在評論區指出，謝謝。

拓展閱讀：Church encoding

邱奇的λ演算理論是一個高度形式化的理論。他定義了一種符號運算規則，叫做λ表達式（依我的理解，這種規則似乎以替換為核心）。姑且把這種符號所代表的元素稱為「函數」，這些函數作用的對象和給出的結果是與它自身同一類型的元素，也就是說，也是函數。

（其實我個人更傾向於將之理解為一種代數結構，把「作用於」這個行為理解為一個二元運算。但這種理解方式似乎不是主流。）

λ表達式是對這些符號的一個抽象運算。具體規則我一兩句話說不清楚。

在λ表達式的規則下，用題中這種方法定義的一族元素（一個用於描述一個函數迭代多少次的函數），恰好具有和用皮亞諾公理定義的「自然數」完全相同的性質，因此我們不妨也稱之為自然數。

這就是邱奇計數和皮亞諾公理的關係了。

至於邱奇圖靈議題，是基於這套理論的另一個結論（稱之為「議題」或許更好些）。邱奇聲稱，任何「可計算」的運算，都可以寫成一個λ表達式。後來這被證明和圖靈機假設是等價的。

也就是說，邱奇圖靈議題可以被認為是對「可計算性」的一個定義：任何一個可以被圖靈機實現的運算一定可以寫成一個λ表達式，反之亦然，我們稱這樣的運算是可計算的。

總之，邱奇的λ演算理論是邱奇計數和邱奇圖靈議題的出發點。它們的關係就是這樣了。

丘奇數和皮亞諾數都是算術公理的形式化表達。

算術公理定義在自然數集上，從定義0開始，定義數的後繼，定義加法、乘法，定義形式歸納原理，加上謂詞演算公理和等詞公理，就可以為算術理論建立形式系統。

它的目的是「從公理出發，證明一切可證明的定理」，試圖建立一個完備的數學體系。比如證明1+1=2，再比如證明費馬小定理，a^p模p得a，再比如證明哥德巴赫猜想。當然，由哥德爾不完備定理知道，不是所有的真命題都可以證明的。

最後說說丘奇圖靈論題。這個回答的是可計算性問題或者說可判定問題。即什麼樣的問題是可以用演算法解決的？丘奇說演算法可計算函數可以表達為遞歸函數，圖靈說圖靈機能解決的問題能表達為遞歸語言。而二者是可以證明為等效的，圖靈可計算函數是遞歸函數而遞歸函數都可以用一台圖靈機表示。

推薦讀一讀《數理邏輯》和《計算理論》相關的書。

就是帶括弧的扳手指數數

扳手指的時候

1 表示1

11 表示 2

111 表示 3

現在Church說了，數數也要用括弧

(1 ()) 表示 1

(1 (1 ())) 表示 2

(1 (1 (1 ()))) 表示 3

以上不完全準確，大意就是這樣

它是通過指定函數參數調用次數的方式來記錄自然數

從 1 開始比較好理解：

用 g(1)(f)(x) = f(x) 來記錄 1

用 g(2)(f)(x) = f(f(x)) = f^2(x) 來記錄 2

用 g(3)(f)(x) = f(f(f(x))) = f^3(x) 來記錄 3

依次類推

倒推可得 g(0)(f)(x) = x

省略兩邊f的參數就是：

用 g(1)(f) = f 來記錄 1

用 g(2)(f) = f^2 來記錄 2

用 g(3)(f) = f^3 來記錄 3

省略其本身的參數 f 來表述就是：

用 g(1) 的結果函數來記錄 1 這個數字

用 g(2) 的結果函數來記錄 2 這個數字

用 g(3) 的結果函數來記錄 3 這個數字

所以說，它的實質就是通過記錄 lambda f = f^n 這樣的函數來記錄自然數的

Programming with Nothing ruby 版本的。。

只用函數 -&> p {x} // 這樣得完成了 FizzBuzz 題目。。