100 天计划第一期,决定读一些经典的技术类书籍。作为 IT 从业者,虽然是科班出身,但是基础知识结构仍然有很多需要夯实。

《计算机的本质:深入剖析程序和计算机》这本书涵盖了计算理论和编程语言设计,阐释了形式语义、自动机理论,以及通过 lambda 演算进行函数式编程等计算问题,可以帮助更好的理解计算机科学和计算原理。

drawing

本文主要是阅读过程中的一些摘录和整理。

语法

传统的计算机程序是长长的字符串。每一种编程语言都有一系列规则,描述在那种语言中什么样的字符串被认为是有效程序。这些规则定义了这种语言的语法。

语法关心的只是程序的表面是什么样的,而不是它的含义。程序有可能语法正确但没有任何实际意义。例如,程序 y = x + 1 本身可能没有任何意义,因为并没有事先说明 x 是什么,而程序 z = true + 1 可能会在运行时候报错,因为它试图在一个布尔型值上加数字。
(当然,这依赖于具体编程语言的其他属性。 )

操作语义

操作语义学(operational semantic)的基础,这种方法为程序在某种机器上的执行定义一些规则,以此来捕捉编程语言的含义。这个机器常常是一种抽象的机器:为了解释这种语言所写的程序如何执行而设计出来的一个想象的、理想化的计算机。为了更好地捕获编程语言的运行时行为,通常需要针对不同种类的编程语言设计不同的抽象机器。

小步语义

假想一台机器,用这台机器直接按照这种语言的语法进行操作一小步一小步地对其进行反复规约,从而对一个程序求值。不管最后得到的结果含义是什么,我们每一步都能让程序更接近最终结果。

这种小步规约类似于对代数式求值的方式。

例如,为了对 (1×2) + (3×4) 求值,我们知道应该:(1) 执行左侧的乘法(1×2 变成了 2) ,这样表达式就规约成了 2 + (3×4);(2) 执行右侧的乘法(3×4 变成了 12) ,这样表达式规约成了 2 + 12;(3) 执行加法(2 + 12 变成了 14) ,最终得到 14。

大步语义

大步语义的思想是,定义如何从一个表达式或者语句直接得到它的结果。这必然需要把程序的执行当成一个递归的而不是迭代的过程:大步语义说的是,为了对一个更大的表达式求值,我们要对所有比它小的子表达式求值,然后把结果结合起来得到最终答案。

大步语义经常会写成更为松散的形式,只会说哪些子计算会执行,而不会指明它们按什么顺序执行。

指称语义

指称语义(denotational semantic)关心从程序本来的语言到其他表示的转换。

指称语义确实是一种比操作语义更抽象的方法,因为它只是用一种语言替换另一种语言,而不是把一种语言转换成真实的行为。

形式化语义

形式化的语义通常都是由数学化的工具完成的。

形式化语义的一个重要应用是为一种编程语言的含义给出一个无歧义的定义,而不是让其依赖于像自然语言规范文档和“由实现规范”这样更加随意的方法。形式化的定义还有其他用途,例如证明某种语言通常情况下的特性,以及特定程序在特定情况下的特性,证明语言中程序之间的等价性,研究如何在不改变程序行为的情况下安全地变换程序而使其效率更高。

例如,既然操作语义与解释器的实现极为接近,那么计算机科学家就可以把一个适当的解释器看成一种语言的操作语义,然后证明它在那种语言的指称语义方面的正确性——这意味着证明了由解释器给出的含义和由指称语义给出的含义之间存在着明显的联系。

指称语义的一个优点是比操作语义抽象层次更高,它忽略了程序如何执行的细节,而只关心如何把它转换成一个不同的表示。例如,如果存在一种指称语义可以把两种语言翻译成某种共通的表示,就使对不同语言写成的两个程序进行比较成为可能。

抽象程度会使指称语义看起来有点兜圈子。如果问题是如何解释一种程序设计语言的含义,那么把一种语言翻译成另一种语言是如何让我们更接近问题答案的呢?一个指称只不过与它的含义一样好;尤其是,如果指称的语言有某种操作性的含义,那么一个指称语义只是让我们更接近于能实际执行一个程序,这个语言的语义本身展示了它是如何执行的,而不是如何翻译成另一种语言的。

形式化的指称语义使用抽象的数学对象(通常是函数)来表示表达式和语句这样的编程语言结构,并且因为数学上的约定会规定如何对函数求值这样的事情,这就有了一种直接在操作意义上思考指称的方式。我们已经使用了不太正式的方式,把指称语义看成是一种语言到另一种语言的编译器,而事实上这是多数编程语言最终得以执行的方式:一个 Java 程序将会由 javac 编译成字节码,字节码将会被 java 的虚拟机即时编译成 x86 的指令,然后一个 CPU 会把每一条 x86 指令解码成类 RISC(精简指令集)的微指令放到一个核上去执行

treetop

treetop 是本书中推荐的一个 ruby 的语法解释器。

尾巴

偷偷的放一下本书的资源吧,点我下载, 侵权删。