计算机由来与原理？

现代逻辑肇始于莱布尼茨，在布尔和弗雷格处发生了分流，形成了所谓的逻辑的代数传统和逻辑的语言传统，然而，无论是代数传统亦或者是语言传统都离莱布尼茨的逻辑学纲领（即：“作为科学、数学和哲学”的基础）相去甚远。在图灵机理论中，图灵核心阐述了“自动机”和“指令表语言”这两个概念，这两者很好地契合了莱布尼茨关于 “理性演算”和“普遍语言”的构想，可以说，图灵机理论最为接近莱布尼茨的逻辑学纲领，也跳出代数传统和语言传统，另辟蹊径，形成了一种新的“作为计算的逻辑”传统（也可以称为“计算传统”）。“作为计算的逻辑”实质上是一种“主体转向”，“以往的逻辑”是当仁不让地以人类为主体，研究的对象是人的思维、自然语言种种，“作为计算的逻辑”则是将计算机作为信息处理的主体，研究的是计算机的处理方式以及人与计算机的互动关系。

关键词：逻辑学；莱布尼茨纲领；图灵机；作为计算的逻辑



引言
如果谈及逻辑与计算的关系，大多数人都会认 同逻辑与计算彼此紧密关联，例如，美国计算机科学家马纳（Manna）就曾经提出过“逻辑即计算机科学的演算”的观点，此外，甚至还有人认为“计 算本质上就是逻辑”，例如，我国著名数理逻辑学家莫绍揆指出：“事实上，它们［程序设计］或者就是数理逻辑，或者是用计算机语言书写的数理逻辑，或者是数理逻辑在计算机上的应用” 。从某种意义上来说，逻辑之于计算的重要性怎么强调都不过分，这些主张可以通过如下论据来为之辩护：

1．从计算机的发展历史来看，计算科学起源于逻辑学

追溯现代计算机科学的起源，应该说，它与逻辑有着密不可分的关系。众所周知，自从罗素与怀特海共同撰写《数学原理》之后，兴起对数理逻辑的研究，人们甚至期望以逻辑为基础，构建整个数学，乃至科学大厦。在这种逻辑主义的驱使下，不可避免地需要对“能行可计算”概念进行形式化。在“能行可计算”概念的探索中，丘奇、哥德尔和图灵几乎在同一时间给出完全不同且又相互等价的定义。丘奇发明了Lambda演算，用来刻画“能行可计算”。哥德尔提出“一般递归函数”作为对“能行可计算”的定义。图灵则通过对一种装置的描述，定义”能行可计算”的概念，这种装置被后人称作“图灵机”，这正是现代计算机的理论 模型，标识现代计算机科学的诞生。

2．逻辑成为计算机软硬件系统的理论基础

布尔逻辑成为集成电路设计的一个核心理论，正如赫尔曼·戈德斯坦所说： “正是通过它［布尔逻辑］，使得电路设计从一门艺术变成一门科学”。同时，也正是由于布尔逻辑的思想融汇在开关电路的设计中，才会在集成电路领域形成著名的摩尔定律，才使得集成电路和技术的创新发展得以实现。一阶逻辑、逻辑类型论和Lambda演算与编程语言的深度交叉，形成了程序设计理论的核心。形式语法、类型系统和形式语义成为一门程序设计语言的基础。逻辑的证明论模型论思 想与计算机软硬件系统的互动，构成了计算机系统 正确性验证理论。人类基于霍尔逻辑、分离逻辑、Isabelle、Coq