[bssd]计算机科学的自然律# Programming - 葵花宝典
g*t
1 楼
functional programming逐步变成非显学。人少的时候我来趁机发个言。
计算机科学第一重要的自然律，我觉得是universal Turing machine
或者church－turing thesis的构造性证明。
它绝对不是显然的。一个系统内部可以有自己的严格表示。这绝对不是显然的。
觉得是显然的，可以猜一下多久量子计算机会有universal machine
三大计算系统，Godel，Church，Turing的等价性，是Turing证明的。
Church率先发表，但是证明中间有gap。正确的证明需要通过Turing 的工具。
Godel没有指出Church证明中的数学正确性问题（我怀疑他知道）。
Godel毫不含糊的说，Turing统一的定义了可计算性。（指的是概念的建模方面）
从实践的角度，图灵1936年的一个单独论文提出，给一个函数f（n），
要定义f（n－1）的一些属性，有一个办法可以用函数调用方便的做到。
这就是loop用lambda calculus／function call实现的一般技术。
或者goto用函数调用来实现的起源。
这是我看到的第一个用fixed point contaminator加上高一级
函数调用解决这问题的文章。这绝对不是显然的。
lambda系统和图灵机的goto系统的等价性，以及构造性的证明。这是被发现的自然律。
如果你没有这个数理逻辑的基础，只能永远被各种眼花缭乱的后世函数call back
和goto的数学转换弄昏头。
时至今日的continuation pass style，cooroutine 。。。各种技术都起源于图灵这个
trick。
影响力最大的可能是lisp／scheme那批人实现结构化编程模式的for，while，等结构的
转换
的一些文章。
从这个角度来看，王垠说天下文章一大抄也没什么错。都是同一个方法?
（这情况还和牛顿定律还不一样。你不能说牛顿以后无力学，因为牛顿没有发明
偏微分方程。三维空间的曲线无法把三维空间分成两部分。二维空间可以。
所以常微分方程是完全不同的。简单说，在计算中，偏微分方程的有限差分法可以
按多个不同路径走running index。常微分方程就一条路走到你要求解的T。）
(我觉得rust很有意思。
现今这个linear logic还没有大规模的热起来。
continuation passing style，coroutine，fixed point combinator。。。
这类的代数技巧或者符号操作技术，在新的上下文里面，想来今后要热一波。
如果我是教授，肯定会指派个学生看看把图灵的文章嫁接过来这类structal logic
是什么效果。
)
计算机科学第一重要的自然律，我觉得是universal Turing machine
或者church－turing thesis的构造性证明。
它绝对不是显然的。一个系统内部可以有自己的严格表示。这绝对不是显然的。
觉得是显然的，可以猜一下多久量子计算机会有universal machine
三大计算系统，Godel，Church，Turing的等价性，是Turing证明的。
Church率先发表，但是证明中间有gap。正确的证明需要通过Turing 的工具。
Godel没有指出Church证明中的数学正确性问题（我怀疑他知道）。
Godel毫不含糊的说，Turing统一的定义了可计算性。（指的是概念的建模方面）
从实践的角度，图灵1936年的一个单独论文提出，给一个函数f（n），
要定义f（n－1）的一些属性，有一个办法可以用函数调用方便的做到。
这就是loop用lambda calculus／function call实现的一般技术。
或者goto用函数调用来实现的起源。
这是我看到的第一个用fixed point contaminator加上高一级
函数调用解决这问题的文章。这绝对不是显然的。
lambda系统和图灵机的goto系统的等价性，以及构造性的证明。这是被发现的自然律。
如果你没有这个数理逻辑的基础，只能永远被各种眼花缭乱的后世函数call back
和goto的数学转换弄昏头。
时至今日的continuation pass style，cooroutine 。。。各种技术都起源于图灵这个
trick。
影响力最大的可能是lisp／scheme那批人实现结构化编程模式的for，while，等结构的
转换
的一些文章。
从这个角度来看，王垠说天下文章一大抄也没什么错。都是同一个方法?
（这情况还和牛顿定律还不一样。你不能说牛顿以后无力学，因为牛顿没有发明
偏微分方程。三维空间的曲线无法把三维空间分成两部分。二维空间可以。
所以常微分方程是完全不同的。简单说，在计算中，偏微分方程的有限差分法可以
按多个不同路径走running index。常微分方程就一条路走到你要求解的T。）
(我觉得rust很有意思。
现今这个linear logic还没有大规模的热起来。
continuation passing style，coroutine，fixed point combinator。。。
这类的代数技巧或者符号操作技术，在新的上下文里面，想来今后要热一波。
如果我是教授，肯定会指派个学生看看把图灵的文章嫁接过来这类structal logic
是什么效果。
)
