编程语言理论（综述）

贡献者： 待更新

　　 本文根据 CC-BY-SA 协议转载翻译自维基百科相关文章。

　　 编程语言理论（PLT）是计算机科学的一个分支，研究编程语言这一形式语言的设计、实现、分析、特征描述和分类。编程语言理论与数学、软件工程和语言学等领域密切相关。该领域有许多学术会议和期刊。

1. 历史

　　 在某些方面，编程语言理论的历史甚至早于编程语言本身的发展。λ 演算（lambda calculus）由阿隆佐·丘奇（Alonzo Church）和斯蒂芬·科尔·克莱尼（Stephen Cole Kleene）在 1930 年代提出，被一些人认为是世界上第一个编程语言，尽管它的初衷是用来建模计算，而不是作为程序员向计算机系统描述算法的工具。许多现代的函数式编程语言被描述为在 λ 演算之上提供了一个 “薄薄的表面层”，[2] 并且许多语言可以通过 λ 演算来简单地描述。

　　 第一个发明的编程语言是 Plankalkül，它由康拉德·祖泽（Konrad Zuse）在 1940 年代设计，但直到 1972 年才为公众所知（并且直到 1998 年才实现）。第一个广为人知且成功的高级编程语言是 FORTRAN（表示 “公式翻译”），由 IBM 研究团队在 1954 至 1957 年间开发，约翰·巴克斯（John Backus）领导。FORTRAN 的成功促成了一个科学家委员会的形成，旨在开发一种 “通用” 计算机语言；他们的努力结果是 ALGOL 58。与此同时，麻省理工学院的约翰·麦卡锡（John McCarthy）开发了 Lisp，它是首个源自学术界且成功的编程语言。随着这些初步努力的成功，编程语言在 1960 年代及以后成为了一个活跃的研究主题。

时间轴

　　 自那时以来，编程语言理论历史中的一些关键事件：

　　 1950 年代

• 诺姆·乔姆斯基（Noam Chomsky）在语言学领域提出了乔姆斯基层次结构，这一发现直接影响了编程语言理论和计算机科学的其他分支。

　　 1960 年代

• 1962 年，Ole-Johan Dahl 和 Kristen Nygaard 开发了 Simula 语言，它被广泛认为是第一个面向对象编程语言的例子；Simula 还引入了协程（coroutine）的概念。
• 1964 年，彼得·兰丁（Peter Landin）首次意识到教堂的 λ 演算可以用于建模编程语言。他提出了 SECD 机器，它 “解释”λ表达式。
• 1965 年，兰丁引入了 J 操作符，本质上是一种延续（continuation）形式。
• 1966 年，兰丁在他的文章《The Next 700 Programming Languages》中提出了 ISWIM，它是一种抽象的计算机编程语言，对设计导致 Haskell 编程语言的语言产生了影响。
• 1966 年，科拉多·博姆（Corrado Böhm）提出了编程语言 CUCH（Curry-Church）。[3]
• 1967 年，克里斯托弗·斯特雷奇（Christopher Strachey）发布了具有影响力的讲义《Fundamental Concepts in Programming Languages》，引入了术语 R 值、L 值、参数多态性和临时多态性。
• 1969 年，J·罗杰·辛德利（J. Roger Hindley）发布了《The Principal Type-Scheme of an Object in Combinatory Logic》，后续推广为辛德利-米尔纳类型推导算法。
• 1969 年，托尼·霍尔（Tony Hoare）提出了霍尔逻辑（Hoare logic），一种公理化语义形式。
• 1969 年，威廉·阿尔文·霍华德（William Alvin Howard）观察到 “高级” 证明系统，称为自然推理（natural deduction），可以直接在其直觉主义版本中解释为 λ 演算的类型变体。这被称为库里-霍华德对应（Curry–Howard correspondence）。

　　 1970 年代

• 1970 年，达纳·斯科特（Dana Scott）首次发布了他关于指示语义学（denotational semantics）的工作。
• 1972 年，逻辑编程和 Prolog 的开发使得计算机程序可以用数学逻辑表示。 由艾伦·凯（Alan Kay）领导的一组科学家在施乐 PARC 开发了 Smalltalk，这是一种面向对象的语言，因其创新的开发环境而广为人知。
• 1974 年，约翰·C·雷诺兹（John C. Reynolds）发现了系统 F，它早在 1971 年就已被数学逻辑学家让-伊夫·吉拉尔（Jean-Yves Girard）发现。
• 1975 年起，杰拉尔德·杰伊·萨斯曼（Gerald Jay Sussman）和盖伊·斯蒂尔（Guy Steele）开发了 Scheme 编程语言，这是一种 Lisp 方言，融入了词法作用域、统一命名空间以及来自演员模型的元素，包括一类优先的延续（first-class continuations）。
• 在 1977 年的图灵奖讲座上，巴克斯（Backus）批评了工业语言的现状，并提出了一类新的编程语言，现在被称为函数级编程语言。
• 1977 年，戈登·普洛特金（Gordon Plotkin）提出了《编程可计算函数》（Programming Computable Functions），一种抽象类型的函数式语言。
• 1978 年，罗宾·米尔纳（Robin Milner）为 ML 引入了辛德利-米尔纳类型推导算法。类型理论作为一种学科应用于编程语言，这一应用在多年里带来了类型理论的巨大进展。

1980 年代

• 1981 年，戈登·普洛特金发布了关于结构化操作语义学（structured operational semantics）的论文。
• 1988 年，吉尔·卡恩（Gilles Kahn）发布了关于自然语义学的论文。
• 出现了过程演算（process calculi），如罗宾·米尔纳（Robin Milner）的《通讯系统演算》（Calculus of Communicating Systems）和 C·A·R·霍尔（C. A. R. Hoare）的《通讯顺序过程模型》（Communicating Sequential Processes），以及其他类似的并发模型，如卡尔·休伊特（Carl Hewitt）的演员模型（actor model）。
• 1985 年，《Miranda》的发布激发了学术界对懒惰求值的纯函数式编程语言的兴趣。一个委员会成立以定义开放标准，最终导致 1990 年发布 Haskell 1.0 标准。
• 伯特兰·梅耶（Bertrand Meyer）创建了契约设计法（Design by Contract），并将其纳入了 Eiffel 编程语言中。

1990 年代

• 格雷戈尔·基察尔斯（Gregor Kiczales）、吉姆·德里维埃尔（Jim Des Rivieres）和丹尼尔·G·博布罗（Daniel G. Bobrow）出版了《元对象协议的艺术》（The Art of the Metaobject Protocol）。
• 尤金·莫吉（Eugenio Moggi）和菲利普·沃德勒（Philip Wadler）引入了单子（monads）用于结构化函数式编程语言中的程序。

2. 子学科与相关领域

　　 编程语言理论（PLT）涉及多个学科，这些学科或属于编程语言理论的范畴，或对其产生深远影响；其中许多领域存在显著的交叉。此外，PLT 还借用了数学的其他分支，包括可计算性理论、范畴理论和集合论。

形式语义学

　　 形式语义学是计算机程序和编程语言行为的形式规范。描述计算机程序 “语义” 或 “意义” 的三种常见方法是指示语义学（denotational semantics）、操作语义学（operational semantics）和公理化语义学（axiomatic semantics）。

类型理论

　　 类型理论是研究类型系统的学科；类型系统是 “通过根据程序短语所计算的值类型对短语进行分类，以证明某些程序行为缺失的可处理语法方法”。许多编程语言的特征由其类型系统的特点决定。

程序分析与转换

　　 程序分析是检查程序并确定关键特征（如是否缺少某些类型的程序错误）的通用问题。程序转换是将一个形式（语言）的程序转换为另一种形式的过程。

编程语言的比较分析

　　 编程语言的比较分析旨在根据其特征将编程语言分类；编程语言的广泛分类通常称为编程范式。

泛型编程与元编程

　　 元编程是生成高阶程序的过程，这些程序在执行时会生成程序（可能是另一种语言，或原始语言的一个子集）作为结果。

领域特定语言

　　 领域特定语言是为了高效解决特定领域问题而构建的语言。

编译器构造

　　 编译器理论是编写编译器（或更一般的翻译器）的理论；编译器是将用一种语言编写的程序转换为另一种形式的程序。编译器的动作通常分为语法分析（扫描与解析）、语义分析（确定程序应该做什么）、优化（根据某种度量提高程序性能；通常是执行速度）和代码生成（生成并输出等效程序，通常是 CPU 指令集的目标语言）。

运行时系统

　　 运行时系统指的是开发编程语言运行环境及其组件的过程，包括虚拟机、垃圾回收和外部函数接口等。

3. 期刊、出版物与会议

　　 会议是展示编程语言研究的主要平台。最著名的会议包括编程语言原理研讨会（POPL）、编程语言设计与实现会议（PLDI）、国际函数式编程会议（ICFP）、国际面向对象编程、系统、语言与应用会议（OOPSLA）和国际编程语言与操作系统架构支持会议（ASPLOS）。

　　 一些重要的发布 PLT 研究的期刊包括 ACM《编程语言与系统交易》（TOPLAS）、《函数式编程期刊》（JFP）、《函数式与逻辑编程期刊》和《高阶与符号计算》。

4. 另见

• SIGPLAN
• 高级编程语言

5. 参考文献

1. Abelson, Harold (1996). 《计算机程序的结构与解释》. Gerald Jay Sussman, Julie Sussman (第二版). 剑桥，马萨诸塞州：麻省理工学院出版社。ISBN 0-262-01153-0。OCLC 34576857。
2. “计算模型”。wiki.c2.com。2014 年 12 月 3 日。原文存档于 2020 年 11 月 30 日。
3. C. Böhm 和 W. Gross (1996)。《CUCH 介绍》。见 E. R. Caianiello（编辑），《自动机理论》，第 35-64 页。
4. Benjamin C. Pierce. 2002. 《类型与编程语言》。麻省理工学院出版社，剑桥，马萨诸塞州，美国。

6. 进一步阅读

• Abadi, Martín 和 Cardelli, Luca. 《对象的理论》。Springer-Verlag。
• Michael J. C. Gordon. 《编程语言理论及其实现》。Prentice Hall。
• Gunter, Carl 和 Mitchell, John C.（编辑）。《面向对象编程语言的理论方面：类型、语义与语言设计》。MIT 出版社。
• Harper, Robert. 《编程语言的实用基础》。草稿版本。
• Knuth, Donald E.（2003）。《计算机语言精选论文》。加利福尼亚州斯坦福：语言与信息研究中心。
• Mitchell, John C. 《编程语言的基础》。
• Mitchell, John C. 《编程语言理论导论》。
• O'Hearn, Peter W. 和 Tennent, Robert D.（1997）。《类似 Algol 的语言》。理论计算机科学进展。Birkhauser 出版社，波士顿。
• Pierce, Benjamin C.（2002）。《类型与编程语言》。MIT 出版社。
• Pierce, Benjamin C. 《类型与编程语言的高级主题》。
• Pierce, Benjamin C. 等（2010）。《软件基础》。

7. 外部链接

• Lambda the Ultimate，一个供专业讨论和编程语言理论文献存储的社区博客。
• 《编程语言中的伟大作品》。由 Benjamin C. Pierce（宾夕法尼亚大学）收集。
• 《编程语言和逻辑中的经典论文》。由 Karl Crary（卡内基梅隆大学）收集。
• 《编程语言研究》。由 Mark Leone 编排的目录。
• Dana S. Scott 为 ACM 图灵百年庆典所写的《λ-计算：过去与现在》。
• 《编程语言中的重大挑战》。2009 年 POPL 会议上的小组讨论。