只要是 strong normalizing，不管是否 typed or untyped 都可以避免停机。也就是说，如果我把 Lisp 的定义修改一下，全改成 total function，另外只允许能证明 terminate 的递归调用，整个系统就是 strong normalizing 的，没什么了不起的。
读 “请注意” 那一段
沒有 Flash, Could someone help copy that to here
这个Y组合子其实还是用了trick
newtype Mu a = Roll { unroll :: Mu a -> a }
注意：这里的Mu是具名的，它引用自身了，这是因为Haskell支持递归类型，而STLC不支持。
不仅STLC不支持，Haskell对应的typed LC是STLC的扩展System F（不看rank-N types的话），System F也不支持recursive bindings所以写不出不动点组合子。但是Haskell本身是有不动点组合子的，原因的确就是Haskell支持任意递归。这也是从实用的角度出发才加上去的，对于一门不是针对定理证明的语言来说turing completeness还是很重要的
Martin-Löf，System F 的 inconsistent extension。
我现在比较困惑的是，函数式编程范式固然是很好的，比如golang和rust里都加入了这个范式，js写这种范式也很简便。但当发现很多人研究type lambda之类的，我又迷茫了。我们的目的不是开发吗？搞太多技巧，对生产性有什么提高吗？
另外，我虽然也经常在golang，rust，js中写lambda，在Ruby中写block。但并不清楚untyped与typed的区别。有人科普一下吗？
他们是数学家，不是工程师
2 个赞
如果想知道为什么会有LC的话，可以去看希尔伯特的23个问题。当初只是为了设计出一个完备，一致的公理化系统而已。跟计算机没太大的关系。
计算机也有搞逻辑的