100 天阅读计划,深入剖析程序和计算机 - 抽象解释 & 静态语义

编程就是用语法与机器交流思想。在写程序的时候,我们知道在程序执行的时候我们想要机器做什么,而了解编程语言的语义让我们相信机器将理解程序每个细节的含义。

但复杂的计算机程序远非单个语句和表达式的累加那么简单。一旦把许多小零件组合到一起构成更大的整体,能检查整个程序是否实际做了我们想要它做的事会很有用。例如,我们可能想要知道它总是返回确定的结果,或者运行这个程序能对文件系统或者网络有既定的副作用,或者只是不含有明显的一遇见非期望输入就会导致崩溃的 bug。

阅读全文〉

100 天阅读计划,深入剖析程序和计算机 - 不可能的程序

我们已经探索了不同的计算机和编程语言模型,其中包括几种抽象机器。这些机器中有一些更强大,特别是有两种机器有相当明显的限制:有限自动机无法解决涉及无限制计数的问题,例如判定一个括号组成的字符串是否平衡;下推自动机无法处理任何信息需要在多处重用的问题,例如判定一个字符串是否含有同样数目的字符 a、b 和 c。

我们已经看到的最先进的机器——图灵机,似乎拥有我们需要的一切:拥有无限制的存储,这个存储能以任何顺序、在任意的循环中、在任意的条件语句以及子例程中访问。

我们也看到了极小编程语言 lambda 演算,被证明也出奇得强大:稍加精心设计,它就允许我们把简单的值和复杂的数据结构都表示成纯代码,还能实现操纵这些表示的运算。我们看到了许多简单的系统,就像 lambda 演算一样,它们也与图灵机有着同样的通用能力。

我们还能将系统不断增强的过程推进多少?或许并不是不确定的:我们通过增加特性让图灵机做更强大的尝试,但没有取得任何进展,这表明计算能力可能存在着一种硬性的限制。那么计算机和编程语言的基本能力是什么呢?有什么它们做不到的事情吗?存在不可能的程序吗?

阅读全文〉

100 天阅读计划,深入剖析程序和计算机 - 计算的通用性

通用图灵机的存在是极其有意义的。尽管任何一台个体的图灵机都有一个硬编码的规则手册,但是通用图灵机证明了设计这样一个装置的可能性,这个装置可以通过从纸带读取指令来完成任何任务。这些指令实际上是控制机器硬件运行的软件,就像控制我们每天都在使用的通用可编程计算机的软件一样1。有限和下推自动机有点过于简单,不能支持这种全面的可编程性,但是图灵机具有解决这个问题的足够的复杂性。

阅读全文〉

随笔吧

今天是平时混得比较好的同事小 A 离职的日子,突然想发点感想。
从大学毕业到现在,三年有余,时常反思,唯恐虚度光阴,但每每想对别人说起,却发现寂寞的很。但我相信,一定有很多人有类似的感悟。

阅读全文〉

100 天阅读计划,深入剖析程序和计算机 - lambda 演算

我们将研究一种叫作无类型 lambda 演算(untyped lambda calculus)的极小编程语言。首先,我们将用尽可能少的语言特性写(用 Ruby)一些接近 lambda 演算的程序。

这将仍然仅仅是在用 Ruby 编程,但施加虚构的约束之后,我们便能很轻松地探索一个受限的语义,而不需要学习一门新语言。然后,我们了解到这些非常有限的特性集合能做什么以后,就将利用这些特性把它们实现为一种语言(使用它自己的解析器、抽象语法和操作语义)—— 使用我们在之前章节中学到的技术。

阅读全文〉

100 天阅读计划,深入剖析程序和计算机 - 图灵机

有限自动机和下推自动机——都有很严格的限制,这些限制影响了它们作为现实计算模型的使用。我们的小型系统还要多强大,才能摆脱这些限制并完成正常计算机的所有工作呢?它还要多复杂才能对 RAM 或硬盘的行为以及合适的输出机制建模呢?怎么才能设计一台能实际运行程序而不总是执行某个硬编码任务的机器呢?

阅读全文〉

100 天阅读计划,深入剖析程序和计算机 - 增加计算能力

之前部分探讨了有限自动机,这是一种假想的机器,它去掉了真实计算机的复杂性并把其规约成了最简单的形式。我们详细考察了这些机器的行为并了解了它们的用处,而且还发现,非确定性有限自动机虽然有一些奇特的执行方法,但计算能力并不比确定性有限自动机强。那如何增加计算能力呢?

阅读全文〉