作者noctem (noctem)
看板PLT
標題[心得] Fixed-points, Curry-Howard, etc.
時間Wed Apr 25 16:29:01 2007
Ruby 板在聊 Y combinator. 蠻巧的，昨天發現四月七日也有人在
Haskell mailing list 上面提起 fixed-point.
http://www.mail-archive.com/[email protected]/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
1F：推 godfat:不太懂|||b 證明 false 是什麼意思？ 04/25 22:24
2F：推 buganini:其實我覺得那個(a->a)->a是必需成立的 04/26 06:34
3F：→ buganini:在數學哲學裡面探討真理的部份，我覺得最基本的問題是 04/26 06:35
4F：→ buganini:因果論是正確的 這個命題 如果不正確的話也就不需探究 04/26 06:35
5F：→ buganini:true/false的問題 希望我沒有誤解你的意思 04/26 06:36
6F：推 buganini:這似乎也跟The Church-Turing thesis有點關係 04/26 06:40
7F：→ buganini:(不是很清楚這些東西，但又好像摸到一點邊，這些真有趣:) 04/26 06:40
8F：→ buganini:不過想到這些就覺得有點淡淡的憂傷 04/26 06:41
9F：→ buganini:The Church-Turing thesis說是被普遍假定為真 04/26 06:42
10F：→ buganini:我就想，其實每個公設還不都是被假定為真 04/26 06:42
11F：→ buganini:我所相信的一切最後也是based on普遍認同.....~"~ 04/26 06:42
12F：→ noctem:buganini 可以多解說一下嗎？好像很有趣 04/26 09:07
13F：推 buganini:蛤? 我在等你多解說耶.... 04/26 09:09
14F：→ buganini:之前一開始是在想"科學"本身的可證偽性... 04/26 09:10
15F：→ buganini:結果就慘了...無窮遞迴下去...那陣子頭昏昏的 04/26 09:12
16F：→ buganini:後來看到Kurt Godel不完備定理覺得真是深得我心 04/26 09:13
17F：→ buganini:我們在用的邏輯應該可以說是based on因果 04/26 09:13
18F：→ buganini:其他任何東西也都會based on something... 04/26 09:14
19F：→ buganini:就是那些所謂公理的東西無所依據... 04/26 09:15
20F：→ buganini:雖然是有人說依據真實世界,不過真實世界又因什麼而真實? 04/26 09:15
21F：→ buganini:於是就變成駭客任務了.... 04/26 09:16
22F：→ buganini:wikipedia裡面有個條目就叫真理..我是從lambda calculus 04/26 09:16
23F：→ buganini:一路連到數學哲學，最後到真理...真理裡面有講一些理論 04/26 09:18
24F：→ buganini:其中有些我覺得像是宗教式的嘴砲,不過我也無從反駁.... 04/26 09:19
25F：→ buganini:融貫,符合,共識這些我是覺得其實都一樣... 04/26 09:19
26F：→ buganini:融貫論+真實世界的真實=符合論 04/26 09:20
27F：→ buganini:真實世界的真實應該算是共識(其實也不一定,也許有人真的 04/26 09:21
28F：→ buganini:看的到阿飄,但我看不到) 總之最後都是共識.. 04/26 09:21
29F：→ buganini:就是普遍認同...因為對錯都是人(們)在判定... 04/26 09:22
30F：→ buganini:剛剛在想，因果可不可以based on一個不符合因果的東西 04/26 09:23
31F：→ buganini:就是說non-deterministic的規則能不能建立出 04/26 09:24
32F：→ buganini:deterministic的結果.....頭又昏了... 04/26 09:24
33F：→ buganini:這不知道會不會弄成Russell paradox 04/26 09:25
34F：→ buganini:以上好像都應該是base on sth....真的昏了啦~"~ 04/26 09:26
35F：推 buganini:慘慘慘...其實是based on沒錯...囧.... 04/26 09:33
36F：推 buganini:令我我私底下其實覺得一切都是deterministic的 04/26 09:40
37F：推 buganini:這樣與 同意Church-Turing thesis 等價 嗎?... 04/26 09:42
38F：推 buganini:把共識的想法套用在社會的東西看,也很有趣,譬如法律 04/26 09:48
39F：→ buganini:法律應該是恐怖平衡(?)之後大家形成的共識訂出的規則 04/26 09:50
40F：→ buganini:其實沒有也沒關係，但為了避免小團體作怪，所以還是要有 04/26 09:50
41F：→ buganini:如果單就這樣而言，法律不應限定犯行 04/26 09:51
42F：→ buganini:只要限定刑罰和行刑人，剩下的公投... 04/26 09:52
43F：→ buganini:不過這樣又要考慮怎樣才能提案公投...不然有人告另一個人 04/26 09:52
44F：→ buganini:踩死蟑螂之類的.... 04/26 09:53
45F：→ buganini:而且在人說眾多的社會公投也是很麻煩...所以還是要有法律 04/26 09:54
46F：→ buganini:對不起我瞎扯了..總之法律要能反映民意(共識),民意範圍.. 04/26 09:54
47F：→ buganini:應該說每個人的意見所佔份量....不可考... 04/26 09:56