[心得] Fixed-points, Curry-Howard, etc.

[noctem (noctem)]

Ruby 板在聊 Y combinator. 蠻巧的，昨天發現四月七日也有人在
Haskell mailing list 上面提起 fixed-point.

  http://www.mail-archive.com/[e-mail]/msg20045.html

在 untyped lambda calculus 裡頭，我們可以這樣定義 Y combinator,
fixed-point combinator 的一例:

  Y = \f -> (\x -> f (x x)) (\x -> f (x x))

但是這個式子在 simply typed 或是 polymorphic typed lambda
calculus 都是無法給 type 的。

比如說，如果我們用 Haskell, 想要讓上面的式子 type check
過，必須要改寫一下，並且會用到這樣的一個 recursive type:

  data C a = C (C a -> a)

有了它之後，我們可以稍微改寫 Y。 Y 的 type 會成為 (a -> a) -> a.

根據 Curry/Howard isomorphism, type 就是 proposition.
如果把 -> 讀做邏輯上的 implication, 那麼 (a -> a) -> a 的
意思就是
  對任何 a, 如果 a -> a, 那麼 a 就是正確的
但這個陳述直覺上就不太對。也難怪 Y 沒有 type, 因為 (a -> a) -> a
這個事情是證不出來的。

如果我們在一個語言裡面硬是加了一個 fixed-point operator
（也就是允許使用遞迴），這等於是在語言中讓 (a -> a) -> a
成為一個公設。不過，一個邏輯系統裡面如果有這個公設，任何東西
都證得出來了。甚至連 false 都證得出來。
比如說， (\a -> a) 的 type 可以是 false -> false,
那麼 Y (\a -> a) 的 type 就是 false.
Y (\a -> a) 就是 false 的一個證明。

另一個觀點的讀解是，只要我們允許遞迴，我們就允許了 programmer
寫出不會中斷的程式。（確實 Y (\a -> a) 是一個不會中斷的程式）

同時，data C a = C (C a -> a) 這個東西把 Haskell 的語法拿掉
之後，意思就是在宣告 C a 和 C a -> a 這兩個 type 是一樣的。
也就是說

   C a = (((.. -> a) -> a) -> a) -> a

這個 type （或 proposition）被用在 Curry's paradox 裡面。
同樣的，如果 C a 成立，那麼任何東西都成立。

程式語言的研究剛開始時，Christopher Strachey 當時提出了想用
數學方式給程式語言 semantics 的計畫。 Dana Scott 本來想把這
個現象當作一個例子，說服 Strachey：untyped lambda calculus
根本是沒有數學意義的。不過他接下來繼續做呀做的，就發明了
Scott domain, 後來變成 domain theory 的基礎...

--
※ 發信站: 批踢踢實業坊(ptt.cc) 
◆ From: 140.109.20.217
推 godfat:不太懂|||b 證明 false 是什麼意思？
推 buganini:其實我覺得那個(a->a)->a是必需成立的
→ buganini:在數學哲學裡面探討真理的部份，我覺得最基本的問題是
→ buganini:因果論是正確的 這個命題 如果不正確的話也就不需探究
→ buganini:true/false的問題   希望我沒有誤解你的意思
推 buganini:這似乎也跟The Church-Turing thesis有點關係
→ buganini:(不是很清楚這些東西，但又好像摸到一點邊，這些真有趣:)
→ buganini:不過想到這些就覺得有點淡淡的憂傷
→ buganini:The Church-Turing thesis說是被普遍假定為真
→ buganini:我就想，其實每個公設還不都是被假定為真
→ buganini:我所相信的一切最後也是based on普遍認同.....~"~
→ noctem:buganini 可以多解說一下嗎？好像很有趣
推 buganini:蛤? 我在等你多解說耶....
→ buganini:之前一開始是在想"科學"本身的可證偽性...
→ buganini:結果就慘了...無窮遞迴下去...那陣子頭昏昏的
→ buganini:後來看到Kurt Godel不完備定理覺得真是深得我心
→ buganini:我們在用的邏輯應該可以說是based on因果
→ buganini:其他任何東西也都會based on something...
→ buganini:就是那些所謂公理的東西無所依據...
→ buganini:雖然是有人說依據真實世界,不過真實世界又因什麼而真實?
→ buganini:於是就變成駭客任務了....
→ buganini:wikipedia裡面有個條目就叫真理..我是從lambda calculus
→ buganini:一路連到數學哲學，最後到真理...真理裡面有講一些理論
→ buganini:其中有些我覺得像是宗教式的嘴砲,不過我也無從反駁....
→ buganini:融貫,符合,共識這些我是覺得其實都一樣...
→ buganini:融貫論+真實世界的真實=符合論
→ buganini:真實世界的真實應該算是共識(其實也不一定,也許有人真的
→ buganini:看的到阿飄,但我看不到) 總之最後都是共識..
→ buganini:就是普遍認同...因為對錯都是人(們)在判定...
→ buganini:剛剛在想，因果可不可以based on一個不符合因果的東西
→ buganini:就是說non-deterministic的規則能不能建立出
→ buganini:deterministic的結果.....頭又昏了...
→ buganini:這不知道會不會弄成Russell paradox
→ buganini:以上好像都應該是base on sth....真的昏了啦~"~
推 buganini:慘慘慘...其實是based on沒錯...囧....
推 buganini:令我我私底下其實覺得一切都是deterministic的
推 buganini:這樣與 同意Church-Turing thesis 等價 嗎?...
推 buganini:把共識的想法套用在社會的東西看,也很有趣,譬如法律
→ buganini:法律應該是恐怖平衡(?)之後大家形成的共識訂出的規則
→ buganini:其實沒有也沒關係，但為了避免小團體作怪，所以還是要有
→ buganini:如果單就這樣而言，法律不應限定犯行
→ buganini:只要限定刑罰和行刑人，剩下的公投...
→ buganini:不過這樣又要考慮怎樣才能提案公投...不然有人告另一個人
→ buganini:踩死蟑螂之類的....
→ buganini:而且在人說眾多的社會公投也是很麻煩...所以還是要有法律
→ buganini:對不起我瞎扯了..總之法律要能反映民意(共識),民意範圍..
→ buganini:應該說每個人的意見所佔份量....不可考...