作者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