PTT數位生活區 / PLT (程式語言與理論)

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

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