编程的模型

当年，丘奇用数学方法定义可计算性时，哥德尔觉得不够直观。

等到图灵用图灵机定义可计算性时，哥德尔觉得这个模型比较直观。

国内计算机方面的教材大多基于图灵机理论，很少基于其它计算模型，包括λ演算。

可能是大多数人对机械系统的接受程度远高于数学系统，所以基于图灵机的计算模型比较容易接受。

图灵证明了图灵机的计算能力与丘奇的lambda演算是等价的。

此外，还有许许多多的计算模型，它们都等价：

* 图灵机

* λ演算

* 一阶逻辑

* 时序逻辑MPTL

* 动态逻辑

* petri网

* 进程代数

* 递归可枚举语言

这些计算模型都是相互关联有所侧重的，比如说

* 图灵机能接受的语言是递归可枚举语言，

* 一阶逻辑的归约是λ演算，

*一阶逻辑的扩充是时序逻辑、动态逻辑，

* 进程代数关心迁移而图灵机关心状态。

这些计算模型能力都等价，它们从不同的视角去看待计算这件事情，面对着不同的问题，采用不同的计算模型效果是不一样的。

这说明“计算”是一个高维存在，这些计算模型不过是“可计算”的不同剪影。

在有些问题里面，用图灵机就表达不清楚，但是用递归可枚举语言就能很好地解释。

图灵机需要知道系统内部状态，而进程代数只需要关心交互过程。

动态逻辑和petri网能给出计算的全局状态，而时序逻辑、图灵机、进程代数则“只见树木不见森林”。