Sorensen and Urzyczyn的CH同构讲义...
- 有个梨GPT
- 2024-11-22 15:50:19
Sorensen and Urzyczyn的CH同构讲义（Lectures on the Curry Howard Isomorphism）里看到的令我震惊的内容。
和λ calculus与simple type结合后产生natural deduction证明与λ term同构类似；给combinator戳上type后：
combinatory logic term是Hilbert-style证明；所以我前面一贴看到的ski组合子戳上类型是三条公理是有原因的。
这是非常令人激动的时刻。它揭示了λ calculus即使在term rewriting的意义上也不是抽象计算模型的唯一实现。说明了「停机」概念的本质，是超越了具体的形式化方式的。
Wolfram搞的那个被 @九瓜 鉴定为民科的问题，那个问题如果rephrase一下，不是针对S组合子，而是问是否存在通用的一条规则实现通用计算，其实λ就算。因为abstraction是构造规则，不是reduction规则。使用时的reduction规则就一条，即beta reduction。但是呢，这条规则只是写在纸上时简单，因为λ的substitution rule是implicit的。
这个rule在两个地方要用到，一个是α-conversion，可以用substitution定义。另一个就是β-reduction，也要用。而这个substitution rule并不简洁，要pattern matching好多情况，根据变量的free/bound情况，以及有可能需要先做α-conversion。
所以λ在很大意义上就像「与非门」一样，它虽然砍剩了一条规则貌似简单到极致，在实践上却并非如此。而combinator的sk组合：
1 没有bound variable，就像人类在纸上演算时一样，哪有bound variable这个东西。
2 sk组合子具有λ的「好」特性，包括church rosser定理带来的normalization，这贴开篇的内容显示了CH同构也在。
3 组合子的硬件实现似乎是比λ简单很多的；Wolfram的书上有写有人干这个事情；@田春冰河 伞哥最近开始沉迷FPGA了，不妨考虑一下组合子计算机，
++++
另外图中所述有不确切的地方。作者说Schonfinkel和Curry为了解决λ calculus的free variable/bound variable问题，发明了combinator。这是不对的。1920年12月7日，Schonfinkel第一次在哥廷根的学术周会上向大家介绍combinator。这是Schonfinkel一生中发表的两篇论文之一，另一篇是和Bernays合作的关于decidability的论文与combinator无关。
这篇论文里的五个组合子是人类历史上第一个「通用计算模型」，也是五个等价的通用计算模型之一。这五个模型是：
Schonfinkel的combinator
Turing的turing machine
Church的λ calculus
Post的String rewriting
Kleene的Recursion theory
String rewritting我只知道名字，不知道具体含义，但我猜想这是 @Puzzler_红叶 崇拜Post的原因
和λ calculus与simple type结合后产生natural deduction证明与λ term同构类似；给combinator戳上type后：
combinatory logic term是Hilbert-style证明；所以我前面一贴看到的ski组合子戳上类型是三条公理是有原因的。
这是非常令人激动的时刻。它揭示了λ calculus即使在term rewriting的意义上也不是抽象计算模型的唯一实现。说明了「停机」概念的本质，是超越了具体的形式化方式的。
Wolfram搞的那个被 @九瓜 鉴定为民科的问题，那个问题如果rephrase一下，不是针对S组合子，而是问是否存在通用的一条规则实现通用计算，其实λ就算。因为abstraction是构造规则，不是reduction规则。使用时的reduction规则就一条，即beta reduction。但是呢，这条规则只是写在纸上时简单，因为λ的substitution rule是implicit的。
这个rule在两个地方要用到，一个是α-conversion，可以用substitution定义。另一个就是β-reduction，也要用。而这个substitution rule并不简洁，要pattern matching好多情况，根据变量的free/bound情况，以及有可能需要先做α-conversion。
所以λ在很大意义上就像「与非门」一样，它虽然砍剩了一条规则貌似简单到极致，在实践上却并非如此。而combinator的sk组合：
1 没有bound variable，就像人类在纸上演算时一样，哪有bound variable这个东西。
2 sk组合子具有λ的「好」特性，包括church rosser定理带来的normalization，这贴开篇的内容显示了CH同构也在。
3 组合子的硬件实现似乎是比λ简单很多的；Wolfram的书上有写有人干这个事情；@田春冰河 伞哥最近开始沉迷FPGA了，不妨考虑一下组合子计算机，
++++
另外图中所述有不确切的地方。作者说Schonfinkel和Curry为了解决λ calculus的free variable/bound variable问题，发明了combinator。这是不对的。1920年12月7日，Schonfinkel第一次在哥廷根的学术周会上向大家介绍combinator。这是Schonfinkel一生中发表的两篇论文之一，另一篇是和Bernays合作的关于decidability的论文与combinator无关。
这篇论文里的五个组合子是人类历史上第一个「通用计算模型」，也是五个等价的通用计算模型之一。这五个模型是：
Schonfinkel的combinator
Turing的turing machine
Church的λ calculus
Post的String rewriting
Kleene的Recursion theory
String rewritting我只知道名字，不知道具体含义，但我猜想这是 @Puzzler_红叶 崇拜Post的原因
