程序设计语言理论

1、程序设计语言理论程序设计语言理论计算机科学与技术学院计算机科学与技术学院陈意云，陈意云，3607043http:/ 程程 简简 介介计算机科学的理论体系计算机科学的理论体系1、模型理论、模型理论 关心的问题关心的问题 给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M解决解决 如何比较模型的表达能力如何比较模型的表达能力 经典计算经典计算 确定的图灵机，可计算性理论属于模型理论确定的图灵机，可计算性理论属于模型理论 新型计算新型计算 本质特点是交互本质特点是交互( 并发、分布、网络、网格、云并发、分布、网络、网格、云 ) 计算和交互的统一模型理论尚未出现计算和交互的统一模型理论尚未出

2、现课课 程程 简简 介介计算机科学的理论体系计算机科学的理论体系2、程序理论、程序理论 关心的问题关心的问题 给定模型给定模型M，如何用模型，如何用模型M解决问题解决问题 包括的领域包括的领域 程序设计范型、程序设计语言、程序设计、形式程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等语义、类型论、程序验证、程序分析等课课 程程 简简 介介计算机科学的理论体系计算机科学的理论体系3、计算理论、计算理论 关心的问题关心的问题 给定模型给定模型M和一类问题，解决该类问题需要多少和一类问题，解决该类问题需要多少资源资源 包括的领域包括的领域 计算复杂性理论计算复杂性理论课课

3、 程程 简简 介介围绕程序设计语言的研究（课程涉及内容用围绕程序设计语言的研究（课程涉及内容用绿色绿色表示）表示） 语法：形式语言和自动机理论，语法分析的实现语法：形式语言和自动机理论，语法分析的实现技术技术 语义：语义：公理语义、操作语义、指称语义公理语义、操作语义、指称语义 形式描述技术还有：形式描述技术还有：代数规范代数规范、范畴论范畴论、属性、属性文法文法 程序设计的范型程序设计的范型：命令式语言、函数式语言命令式语言、函数式语言、逻、逻辑程序设计语言、辑程序设计语言、面向对象程序设计语言面向对象程序设计语言、并行、并行程序设计语言程序设计语言课课 程程 简简 介介围绕程序设计语言的研

4、究（课程涉及内容用围绕程序设计语言的研究（课程涉及内容用绿色绿色表示）表示） 类型论与类型系统：多态类型、子类型、存在类类型论与类型系统：多态类型、子类型、存在类型型 程序验证：程序验证：程序正确性证明程序正确性证明 程序分析技术：数据流分析、控制流分析、模型程序分析技术：数据流分析、控制流分析、模型检查、抽象解释检查、抽象解释 程序的自动生成技术：程序变换程序的自动生成技术：程序变换课课 程程 简简 介介学习的意义学习的意义 掌握与程序设计语言有关的理论，为从事有关的掌握与程序设计语言有关的理论，为从事有关的研究起一个奠基的作用研究起一个奠基的作用应用：应用： 程序设计语言的设计和实现程序设

5、计语言的设计和实现 程序的自动生成程序的自动生成 程序分析与程序验证程序分析与程序验证 提高软件的可信程度提高软件的可信程度 协议的形式描述和验证协议的形式描述和验证课课 程程 简简 介介教材和参考书教材和参考书 陈意云、张昱，程序设计语言理论（第二版），陈意云、张昱，程序设计语言理论（第二版），高等教育出版社，高等教育出版社，2010.2 教学资源网页：教学资源网页：http:/ 马世龙、眭跃飞等译，类型和程序设计语言，电马世龙、眭跃飞等译，类型和程序设计语言，电子工业出版社，子工业出版社，2005.5 许满武译，程序设计语言理论基础，电子工业出许满武译，程序设计语言理论基础，电子工业出版社

6、，版社，2006.11 陈意云、张昱，编译原理（第二版），高等教育陈意云、张昱，编译原理（第二版），高等教育出版社，出版社，2008.6课课 程程 简简 介介教材和参考书教材和参考书 John C. Mitchell, Foundations For Programming Languages, MIT Press, 1996. Banjamin C. Pierce, Types and Programming Laungages, MIT Press, 2002. Robert Harper, Practical Foundations for Programming Languages,

7、working draft, 2009. John C. Reynolds, Theories of Programming Languages , Cambridge University Press, 1998. Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction , MIT Press, 1993. 课课 程程 简简 介介课程要求课程要求 讲课进展较快，平时不复习不加深理解，后面将讲课进展较快，平时不复习不加深理解，后面将听不懂听不懂 作业较多，要求独立完成作业较多，要求独立完成 没有

8、上机实验没有上机实验 考试开卷考试开卷 成绩：考试成绩成绩：考试成绩占占70%，作业占，作业占30% 第第1章章 引引 言言 介绍一个非常简单的、以自然数和布尔值作介绍一个非常简单的、以自然数和布尔值作为基本类型的、基于类型化为基本类型的、基于类型化 演算的语言演算的语言 介绍该语言的语法、公理语义和操作语义介绍该语言的语法、公理语义和操作语义 主要议题如下：主要议题如下： 表示法和表示法和 演算系统概述演算系统概述 类型和类型系统的扼要讨论类型和类型系统的扼要讨论 基于表达式的归纳、基于证明的归纳和良基归纳基于表达式的归纳、基于证明的归纳和良基归纳1.1 基基 本本 概概 念念1.1.1 模

9、型语言模型语言 对程序设计语言进行数学分析对程序设计语言进行数学分析 从设计模型语言开始从设计模型语言开始 突出感兴趣的程序构造，忽略无关的细节突出感兴趣的程序构造，忽略无关的细节 语言的形式化分为两部分语言的形式化分为两部分 能抓住语言本质机制的非常小的核心：能抓住语言本质机制的非常小的核心： 演算演算 导出部分：它们可以翻译成核心的导出部分：它们可以翻译成核心的 演算演算 用类型化用类型化 演算的框架来研究程序设计语言的演算的框架来研究程序设计语言的各种概念各种概念1.1 基基 本本 概概 念念1.1.2 表示法表示法 表示法的主要特征表示法的主要特征 抽象：抽象：用于定义函数用于定义函数

10、 应用：应用：将所定义的函数作用于变元将所定义的函数作用于变元 抽象的例子抽象的例子 （自然数类型上的几个例子自然数类型上的几个例子） 恒等函数：恒等函数： x : nat.x / 命令式表示命令式表示Id(x : nat) = x 后继函数：后继函数： x : nat.x 1 / 函数式无需给函数命名函数式无需给函数命名 常函数：常函数： x : nat.10 x : nat. .x true 不是良形的表达式不是良形的表达式 表示法写出的表达式叫做表示法写出的表达式叫做 表达式表达式或或 项项1.1 基基 本本 概概 念念 项项 x: . .M 和谓词演算公式和谓词演算公式 x :A. .

11、 的比较的比较 是一个约束算子是一个约束算子 x是一个占位符是一个占位符，约束变元，可，约束变元，可以重新命名以重新命名 约束约束变元变元而不改变表达式的含义而不改变表达式的含义 在在 x: . .x + y中，中，x的出现是的出现是约束的，约束的， y的出现是的出现是自由的自由的 不含自由变元的表达式称为闭表达式不含自由变元的表达式称为闭表达式 应用：应用：用项的并置来表示函数应用，例：用项的并置来表示函数应用，例： ( x : nat. .x) 5 ( x : nat. .x) 5 5 / 应用后面介绍的应用后面介绍的 公理公理1.1 基基 本本 概概 念念 一个简单的例子一个简单的例子

12、( x : nat. ( y : nat. z : nat. ( x + y ) + z ) 3 ) 4 5= ( x : nat. z : nat. ( x + 3 ) + z ) 4 5= ( z : nat. ( 4 + 3 ) + z ) 5= ( 4 + 3 ) + 5= 121.1 基基 本本 概概 念念 表示法中有两个约定表示法中有两个约定 函数应用是左结合的：函数应用是左结合的： MNP 应看成应看成 (MN)P 每个每个 的约束范围尽可能地大的约束范围尽可能地大：一直到表达式的结束，或一直到表达式的结束，或碰到不能配对的右括号为止碰到不能配对的右括号为止 例例 x: . .M

13、N解释为解释为 x: . .(MN)，而不是而不是( x: . .M)N x: . . y: . .MN是是 x: . .( y: . .(MN)的简写的简写 ( x: . .( y: . .( z: . .M)N)P)Q可以简写为可以简写为( x: . . y: . . z: . .M)NPQ 1.2 等式、归约和语义等式、归约和语义 表示法是表示法是 演算演算的一部分，的一部分， 演算是关于演算是关于 表表达式的一个推理系统达式的一个推理系统 除了语法外，该形式系统有三个主要部分除了语法外，该形式系统有三个主要部分 公理语义：公理语义：推导表达式相等的一个形式系统推导表达式相等的一个形式系

14、统 操作语义：操作语义：基于单方向的等式推理基于单方向的等式推理（归约、符号（归约、符号计算）计算）上述两者都称为证明系统上述两者都称为证明系统 指称语义：形式系统的模型指称语义：形式系统的模型1.2 等式、归约和语义等式、归约和语义1.2.1 公理语义公理语义一个等式公理系统一个等式公理系统 约束变元改名公理约束变元改名公理（ 公理公理） x: . .M y: . . y x M，M中无自由出现的中无自由出现的y其中其中 N x M表示表示M中的中的x用表达式用表达式N代换的结果代换的结果 例如例如 x: .x y: .y 函数应用公理函数应用公理（ 公理公理） ( x: . .M)N N/

15、xM 例如例如 ( x:nat.x+4) 4 4/x(x+4) 4 + 41.2 等式、归约和语义等式、归约和语义 自反公理、对称性规则、传递性规则自反公理、对称性规则、传递性规则 同余规则同余规则 相等的函数应用于相等的变元产生相等的结果相等的函数应用于相等的变元产生相等的结果 等式证明规则允许推导任何一组等式前提的等式证明规则允许推导任何一组等式前提的逻辑推论逻辑推论M1 = M2 N1 = N2 M1 N1 = M2 N21.2 等式、归约和语义等式、归约和语义1.2.2 操作语义操作语义语言的操作语义可用不同的方式给出语言的操作语义可用不同的方式给出 定义一个抽象机定义一个抽象机, ,

16、通过一系列的机器状态变换通过一系列的机器状态变换来计算程序来计算程序 演绎出最终结果的证明系统演绎出最终结果的证明系统 前面所列的等式公理的单向形式给出了归约规则前面所列的等式公理的单向形式给出了归约规则 最核心的归约规则是最核心的归约规则是( )的单向形式的单向形式( x: .M)N N/xM 通常没有通常没有 归约规则：归约规则： x: .M y: . y x M1.2 等式、归约和语义等式、归约和语义1.2.3 指称语义指称语义 确定语言构造（程序、语句、表达式等）到确定语言构造（程序、语句、表达式等）到指称物（各种集合）的语义映射，满足：指称物（各种集合）的语义映射，满足： 各种语言构

17、造的实例都有对应的指称物各种语言构造的实例都有对应的指称物 复合构造的指称只依赖于它的子构造的指称复合构造的指称只依赖于它的子构造的指称 类型化类型化 演算的指称语义演算的指称语义 每个类型表达式对应到一个集合每个类型表达式对应到一个集合 类型类型 的项解释为其值集上的一个元素的项解释为其值集上的一个元素 类型类型 的值集是函数集合，项的值集是函数集合，项 x: .M解释为解释为一个数学函数一个数学函数1.3 类型和类型系统类型和类型系统 类型论类型论 为避免集合论悖论而建立起来的数学理论为避免集合论悖论而建立起来的数学理论 主要研究集合的分层、分类方法主要研究集合的分层、分类方法 在程序设计

18、语言理论中，类型论是指类型系统的在程序设计语言理论中，类型论是指类型系统的设计、分析和研究设计、分析和研究 类型提供了所有可能值的一种划分类型提供了所有可能值的一种划分 一个类型是一群有某些公共性质的值一个类型是一群有某些公共性质的值 对于不同的类型系统，类型的多少和值所属对于不同的类型系统，类型的多少和值所属的类型可能不同的类型可能不同1.3 类型和类型系统类型和类型系统1.3.1 类型和类型系统类型和类型系统 类型语言类型语言：变量都被给定类型：变量都被给定类型 未未类类型化的型化的语语言言：不限制变量值的范围：不限制变量值的范围 类型系统类型系统 语言的一个组成部分语言的一个组成部分 由

19、一组定型规则构成由一组定型规则构成 类型系统的研究有两个分支类型系统的研究有两个分支 类型系统在程序设计语言中的应用类型系统在程序设计语言中的应用 “纯类型化纯类型化 演算演算”和各种逻辑之间的对应关系和各种逻辑之间的对应关系1.3 类型和类型系统类型和类型系统设计类型系统的目的设计类型系统的目的 用来证明程序不会出现不良行为用来证明程序不会出现不良行为 类型可靠的语言（安全语言）类型可靠的语言（安全语言） 所有程序运行时都没有不良行为出现所有程序运行时都没有不良行为出现 类型系统的研究也需要形式化的方法类型系统的研究也需要形式化的方法 许多语言定义被发现不是类型可靠的，甚至经过许多语言定义被

20、发现不是类型可靠的，甚至经过类型检查后接受的程序也会崩溃类型检查后接受的程序也会崩溃 显式类型化的语言：显式类型化的语言：类型是语法的一部分类型是语法的一部分 隐式类型化的语言隐式类型化的语言1.3 类型和类型系统类型和类型系统1.3.2 类型语言的优点类型语言的优点 开发时的实惠开发时的实惠 可以较早发现错误可以较早发现错误 类型信息具有文档作用（比程序注解精确，比形类型信息具有文档作用（比程序注解精确，比形式规范容易理解）式规范容易理解） 编译时的实惠编译时的实惠 程序模块可以相互独立地编译程序模块可以相互独立地编译 运行时的实惠运行时的实惠 更有效的空间安排和访问方式，提高了目标代码更有

21、效的空间安排和访问方式，提高了目标代码的运行效率的运行效率1.3 类型和类型系统类型和类型系统类型系统的其他应用类型系统的其他应用 许多程序分析工具使用类型检查或类型推断许多程序分析工具使用类型检查或类型推断算法算法 类型系统用来表示逻辑命题和证明类型系统用来表示逻辑命题和证明1.4 归归 纳纳 法法本节介绍本书常用的归纳法本节介绍本书常用的归纳法 自然数归纳法（有两种形式，不专门介绍）自然数归纳法（有两种形式，不专门介绍） 结构归纳（介绍表达式上的归纳，有两种形结构归纳（介绍表达式上的归纳，有两种形式）式） 证明上的归纳证明上的归纳 良基归纳法（重点介绍）良基归纳法（重点介绍）1.4 归归

22、纳纳 法法1.4.1 表达式上的归纳表达式上的归纳 表达式文法表达式文法 e := 0 | 1 | v | e + e | e e 每个表达式都有各自的语法树每个表达式都有各自的语法树 如果如果P是表达式的性质，是表达式的性质，Q是是自然数的性质自然数的性质 Q(n) 语言语言树树t. .如果如果height(t) = n 并且并且t是是e的的语法树，那么语法树，那么P(e)为真为真 首先必须为高度是首先必须为高度是0的语法树直接证明的语法树直接证明P 然后，对于语法树高度至少为然后，对于语法树高度至少为1的表达式的表达式e，假定，假定对于语法树高度较小的表达式，对于语法树高度较小的表达式，P

23、都为真，证明都为真，证明P(e)为真为真1.4 归归 纳纳 法法 结构归纳结构归纳（形式（形式1） 对每个原子表达式对每个原子表达式e，证明证明P(e) 对直接子表达式为对直接子表达式为e1, ek的任何复合表达式的任何复合表达式e，证明，如果证明，如果P(ei)（i=1, k）都为真，那么都为真，那么P(e) 也为真也为真 结构归纳结构归纳（形式（形式2） 证明：对任何表达式证明：对任何表达式e，如果如果P(e )对对e的任何子表的任何子表达式达式e 都成立，那么都成立，那么P(e)也成立也成立 形式形式2的归纳假设包含了所有的子表达式，并的归纳假设包含了所有的子表达式，并非只是直接子表达式

24、非只是直接子表达式1.4 归归 纳纳 法法1.4.2 证明上的归纳证明上的归纳 证明系统证明系统由公理和推理规则组成由公理和推理规则组成 证明是一个公式序列，该序列中的每个公式证明是一个公式序列，该序列中的每个公式都是公理或者是由前面的公式通过一个推理都是公理或者是由前面的公式通过一个推理规则得到的结论规则得到的结论 基于证明的长度，用自然数归纳法来讨论证基于证明的长度，用自然数归纳法来讨论证明的性质明的性质 另一种观点把证明看成是某种形式的树另一种观点把证明看成是某种形式的树1.4 归归 纳纳 法法 证明上的结构归纳证明上的结构归纳 对该证明系统中的每个公理，证明对该证明系统中的每个公理，证

25、明P成立成立 假定对证明假定对证明 1, , k，P成立，证明成立，证明P( )也为真也为真 是这样的证明，它结束于用一个推理规则，并是这样的证明，它结束于用一个推理规则，并且是从证明且是从证明 1, , k延伸出来的一个证明延伸出来的一个证明BAn- - -A1证明树示意图证明树示意图1.4 归归 纳纳 法法1.4.3 良基归纳良基归纳 集合集合A的二元关系被称为是良基的的二元关系被称为是良基的 ：若：若A上上不存在无穷递减序列不存在无穷递减序列a0 a1 a2 例：在自然数上，如果例：在自然数上，如果j i +1，则则i j。这个。这个关系是良基关系关系是良基关系 良基关系的一些特点良基关

26、系的一些特点 良基关系不一定有传递性良基关系不一定有传递性 良基关系都是非自反的，即对任何良基关系都是非自反的，即对任何a A，a a不不成立；否则会出现无穷递减序列成立；否则会出现无穷递减序列a a a 1.4 归归 纳纳 法法 引理引理1.1 若若 是集合是集合A上的二元关系，上的二元关系， 是良基是良基的，的，当且仅当当且仅当A的每个非空子集都有极小元的每个非空子集都有极小元 证明证明 假定假定 是良基的，是良基的，证明非空子集证明非空子集B(B A)有极小元有极小元 用反证法。如果用反证法。如果B无极小元，那么对每个无极小元，那么对每个a B，可以找到某个可以找到某个aB使得使得a a

27、。则可以从任意的则可以从任意的a0 B开始，构造一个无穷递减序列开始，构造一个无穷递减序列a0 a1 a2 假定每个子集都有极小元假定每个子集都有极小元 则不可能存在则不可能存在a0 a1 a2 ，因该序列给出了因该序列给出了无极小元的集合无极小元的集合a0, a1, a2, 。故。故 是良基的是良基的1.4 归归 纳纳 法法 命题命题1.2（良基归纳）（良基归纳）令令 是集合是集合A上的良基关系，上的良基关系，令令P是是A上某个性质，上某个性质，若每当所有的若每当所有的P(b) (b a)为真，则为真，则P(a)为真，即为真，即 a.( b.(b a P(b) P(a)那么，对所有的那么，对所有的a A，P(a)为真为真1.4 归归 纳纳 法法 命题命题1.2（良基归纳）（良基归纳）若若 a.( b.(b a P(b) P(a)，则，则 a.P(a) 证明证明 若存在某个若存在某个x A使得使得 P(x)成立，则下面集合非空成立，则下面集合非空B a A | P(a) 由引理由引理1.1，B一定有极小元一定有极小元a B 但是，对所有的但是，对所有的b a，P(b)一定成立（否则一定成立（否则a不是