从数理逻辑进入计算机科学
达纳·斯科特(Dana Scott)是将逻辑学方法引入计算机科学的研究者。他于1954年获得加利福尼亚大学伯克利分校学士学位,1958年获得普林斯顿大学博士学位;此后曾在斯坦福、普林斯顿和牛津等大学任职,1981年进入卡内基梅隆大学,2003年成为荣休教授。1976年,他与迈克尔·拉宾共同获得图灵奖。
斯科特的研究并不限于编程语言。模型论、集合论、模态逻辑、直觉主义逻辑和范畴逻辑,都属于他的工作范围。自动机研究关注有限装置能识别什么,程序语义研究则追问一个程序究竟表示什么;二者都借助精确的数学对象,把关于计算的直觉变成可以论证的问题。
与拉宾共同研究有限自动机
拉宾和斯科特1959年发表《有限自动机及其判定问题》,系统研究有限状态装置和它们接受的符号串集合。论文的重要内容是非确定性模型:同一状态读入一个符号后,可以有多个允许的后继状态。只要存在一条最终到达接受状态的路径,输入便被接受;这不是按概率随机选路的定义。
二人证明,这种非确定性并不扩大有限自动机能够识别的语言范围。把一组可能状态作为确定性自动机的一个状态,就能同时追踪各条分支。新机器可能需要更多状态,却接受同一个语言。这里的贡献属于两位作者的共同工作,也不能从有限自动机的结论推断所有计算模型中的非确定性都没有代价。
参考:[3]
为程序规定数学含义
斯科特与克里斯托弗·斯特雷奇1971年的技术报告,把程序语言的形式语义建立在数学对象与映射之上。程序的含义不必等同于某台机器逐步执行的记录:表达式可对应值,命令可对应状态之间的变换,再按语言的组合结构解释整个程序。不同语法形式因此可能具有相同的指称。
这一合作将逻辑和数学结构与语言设计问题连接起来。它既区别于只描述语法是否合规,也不要求把某一种编译器的实现细节当成语言本身。指称语义由此提供了一条讨论程序等价和推理规则的道路,但不是宣称所有语言只能拥有这一种数学解释。
参考:[4]
语义域怎样容纳递归
递归定义把正在定义的计算再次用在自身内部,不能仅靠展开一次便获得完整含义。斯科特研究的语义域为计算结果安排信息量上的偏序:尚未确定的结果位于较低位置,更完整的近似位于较高位置。对部分函数而言,这可以表现为函数在更多输入上有了定义。
在合适的有序结构和连续性条件下,递归方程可由逐步增加信息的近似来解释,其含义取为最小不动点。最小意味着不额外加入递归规则没有确定的信息,并不意味着程序运行最快。这些方法为递归、非终止及高阶计算提供了数学工具;后来的语义域教材和应用又扩展了这条研究路线,应与斯科特的具体论文及共同成果分别看待。