程序设计语言理论 计算机科学与技术学院 陈意云，

Presentation on theme: "程序设计语言理论 计算机科学与技术学院 陈意云，"— Presentation transcript:

1 程序设计语言理论 计算机科学与技术学院 陈意云，3607043 http://staff.ustc.edu.cn/~yiyun

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

3 课 程 简 介 计算机科学的理论体系 2、程序理论  关心的问题 给定模型M，如何用模型M解决问题  包括的领域
程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等 3

4 课 程 简 介 计算机科学的理论体系 3、计算理论  关心的问题 给定模型M和一类问题，解决该类问题需要多少资源  包括的领域
计算复杂性理论 4

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

6 课 程 简 介 围绕程序设计语言的研究（课程涉及内容用 绿色表示） 类型论与类型系统：多态类型、子类型、存在类型 程序验证：程序正确性证明
程序分析技术：数据流分析、控制流分析、模型检查、抽象解释 程序的自动生成技术：程序变换

7 课 程 简 介 学习的意义 掌握与程序设计语言有关的理论，为从事有关的研究起一个奠基的作用 应用： 程序设计语言的设计和实现 程序的自动生成
程序分析与程序验证 提高软件的可信程度 协议的形式描述和验证

8 课 程 简 介 教材和参考书 陈意云、张昱，程序设计语言理论（第二版），高等教育出版社，2010.2
教学资源网页： 马世龙、眭跃飞等译，类型和程序设计语言，电子工业出版社，2005.5 许满武译，程序设计语言理论基础，电子工业出版社， 陈意云、张昱，编译原理（第二版），高等教育出版社，2008.6

9 课 程 简 介 教材和参考书 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, 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.

10 课 程 简 介 课程要求 讲课进展较快，平时不复习不加深理解，后面将听不懂 作业较多，要求独立完成 没有上机实验 考试开卷
成绩：考试成绩占70%，作业占30%

11 第1章 引 言 介绍一个非常简单的、以自然数和布尔值作为基本类型的、基于类型化演算的语言 介绍该语言的语法、公理语义和操作语义
第1章 引 言 介绍一个非常简单的、以自然数和布尔值作为基本类型的、基于类型化演算的语言 介绍该语言的语法、公理语义和操作语义 主要议题如下： 表示法和演算系统概述 类型和类型系统的扼要讨论 基于表达式的归纳、基于证明的归纳和良基归纳

12 1.1 基 本 概 念 1.1.1 模型语言 对程序设计语言进行数学分析 语言的形式化分为两部分
1.1 基 本 概 念 1.1.1 模型语言 对程序设计语言进行数学分析 从设计模型语言开始 突出感兴趣的程序构造，忽略无关的细节 语言的形式化分为两部分 能抓住语言本质机制的非常小的核心：演算 导出部分：它们可以翻译成核心的演算 用类型化演算的框架来研究程序设计语言的各种概念

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

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

15 1.1 基 本 概 念 一个简单的例子 ( x : nat. ( y : nat. z : nat. ( x + y ) + z ) 3 ) 4 5 = ( x : nat. z : nat. ( x + 3 ) + z ) 4 5 = ( z : nat. ( ) + z ) 5 = ( ) + 5 = 12

16 1.1 基 本 概 念 表示法中有两个约定 例 函数应用是左结合的： MNP 应看成 (MN)P 每个的约束范围尽可能地大：
1.1 基 本 概 念 表示法中有两个约定 函数应用是左结合的： MNP 应看成 (MN)P 每个的约束范围尽可能地大： 一直到表达式的结束，或 碰到不能配对的右括号为止 例 x:.MN解释为x:.(MN)，而不是(x:.M)N x:.y:.MN是x:.(y:.(MN))的简写 (((x:.(y:.(z:.M)))N)P)Q可以简写为 (x:.y:.z:.M)NPQ

17 1.2 等式、归约和语义 表示法是演算的一部分，演算是关于表达式的一个推理系统 除了语法外，该形式系统有三个主要部分
公理语义：推导表达式相等的一个形式系统 操作语义：基于单方向的等式推理（归约、符号计算） 上述两者都称为证明系统 指称语义：形式系统的模型

18 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/x]M 例如 (x:nat.x+4) 4  [4/x](x+4)  4 + 4

19 1.2 等式、归约和语义 自反公理、对称性规则、传递性规则 同余规则 等式证明规则允许推导任何一组等式前提的逻辑推论
相等的函数应用于相等的变元产生相等的结果 等式证明规则允许推导任何一组等式前提的逻辑推论 M1 = M2 N1 = N2 M1 N1 = M2 N2

20 1.2 等式、归约和语义 1.2.2 操作语义 语言的操作语义可用不同的方式给出 定义一个抽象机,通过一系列的机器状态变换来计算程序
演绎出最终结果的证明系统 前面所列的等式公理的单向形式给出了归约规则 最核心的归约规则是()的单向形式 (x:.M)N  [N/x]M 通常没有 归约规则：x:.M  y:.yxM

21 1.2 等式、归约和语义 1.2.3 指称语义 确定语言构造（程序、语句、表达式等）到指称物（各种集合）的语义映射，满足：
指称语义 确定语言构造（程序、语句、表达式等）到指称物（各种集合）的语义映射，满足： 各种语言构造的实例都有对应的指称物 复合构造的指称只依赖于它的子构造的指称 类型化演算的指称语义 每个类型表达式对应到一个集合 类型 的项解释为其值集上的一个元素 类型   的值集是函数集合，项x:.M解释为一个数学函数

22 1.3 类型和类型系统 类型论 类型提供了所有可能值的一种划分 对于不同的类型系统，类型的多少和值所属的类型可能不同
为避免集合论悖论而建立起来的数学理论 主要研究集合的分层、分类方法 在程序设计语言理论中，类型论是指类型系统的设计、分析和研究 类型提供了所有可能值的一种划分 一个类型是一群有某些公共性质的值 对于不同的类型系统，类型的多少和值所属的类型可能不同

23 1.3 类型和类型系统 1.3.1 类型和类型系统 类型语言：变量都被给定类型 未类型化的语言：不限制变量值的范围 类型系统
语言的一个组成部分 由一组定型规则构成 类型系统的研究有两个分支 类型系统在程序设计语言中的应用 “纯类型化演算”和各种逻辑之间的对应关系

24 1.3 类型和类型系统 设计类型系统的目的 用来证明程序不会出现不良行为 类型可靠的语言（安全语言） 显式类型化的语言：类型是语法的一部分
所有程序运行时都没有不良行为出现 类型系统的研究也需要形式化的方法 许多语言定义被发现不是类型可靠的，甚至经过类型检查后接受的程序也会崩溃 显式类型化的语言：类型是语法的一部分 隐式类型化的语言

25 1.3 类型和类型系统 1.3.2 类型语言的优点 开发时的实惠 编译时的实惠 运行时的实惠 可以较早发现错误
类型信息具有文档作用（比程序注解精确，比形式规范容易理解） 编译时的实惠 程序模块可以相互独立地编译 运行时的实惠 更有效的空间安排和访问方式，提高了目标代码的运行效率

26 1.3 类型和类型系统 类型系统的其他应用 许多程序分析工具使用类型检查或类型推断算法 类型系统用来表示逻辑命题和证明

27 1.4 归 纳 法 本节介绍本书常用的归纳法 自然数归纳法（有两种形式，不专门介绍） 结构归纳（介绍表达式上的归纳，有两种形式）
1.4 归 纳 法 本节介绍本书常用的归纳法 自然数归纳法（有两种形式，不专门介绍） 结构归纳（介绍表达式上的归纳，有两种形式） 证明上的归纳 良基归纳法（重点介绍）

28 1.4 归 纳 法 1.4.1 表达式上的归纳 表达式文法 e ::= 0 | 1 | v | e + e | e  e
1.4 归 纳 法 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都为真，证明P(e)为真

29 1.4 归 纳 法 结构归纳（形式1） 结构归纳（形式2） 形式2的归纳假设包含了所有的子表达式，并非只是直接子表达式
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的归纳假设包含了所有的子表达式，并非只是直接子表达式

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

31 1.4 归 纳 法 A1 An - - - 证明上的结构归纳 证明树示意图 B 对该证明系统中的每个公理，证明P成立
1.4 归 纳 法 证明上的结构归纳 对该证明系统中的每个公理，证明P成立 假定对证明1, …, k，P成立，证明P()也为真 是这样的证明，它结束于用一个推理规则，并且是从证明1, …, k延伸出来的一个证明 B An - - - A1 证明树示意图

32 1.4 归 纳 法 1.4.3 良基归纳 集合A的二元关系被称为是良基的：若A上不存在无穷递减序列a0  a1  a2  …
1.4 归 纳 法 1.4.3 良基归纳 集合A的二元关系被称为是良基的：若A上不存在无穷递减序列a0  a1  a2  … 例：在自然数上，如果j  i +1，则i  j。这个关系是良基关系 良基关系的一些特点 良基关系不一定有传递性 良基关系都是非自反的，即对任何aA，a  a不成立；否则会出现无穷递减序列a  a  a  …

33 1.4 归 纳 法 引理1.1 若是集合A上的二元关系，是良基的，当且仅当A的每个非空子集都有极小元 证明
1.4 归 纳 法 引理1.1 若是集合A上的二元关系，是良基的，当且仅当A的每个非空子集都有极小元 证明 假定是良基的，证明非空子集B(BA)有极小元 用反证法。如果B无极小元，那么对每个aB，可以找到某个aB使得aa。则可以从任意的a0B开始，构造一个无穷递减序列a0  a1  a2  … 假定每个子集都有极小元 则不可能存在a0  a1  a2  …，因该序列给出了无极小元的集合{a0, a1, a2, …}。故是良基的

34 1.4 归 纳 法 命题1.2（良基归纳） 令是集合A上的良基关系， 令P是A上某个性质，
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)为真

35 1.4 归 纳 法 命题1.2（良基归纳） 证明 若a.(b.(b  a  P(b))  P(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不是B的极小元） 这就和假定b.(b  a  P(b))  P(a)矛盾

36 1.4 归 纳 法 良基归纳法的使用 如何理解：若每当所有的P(b) (b  a)为真，则P(a)为真，即： (b.(b  a  P(b))  P(a)) 对某些a，不存在b，使得b  a，则 b.(b  a  P(b))  P(a) 等价于 P(a) （因为b: . P(b)为真，其中表示空集） 对另一些a，存在b，使得b  a，则 b.(b  a  P(b))  P(a) 的证明是基于b.(b  a  P(b)) 为真来推导P(a)为 真

37 1.4 归 纳 法 表1.1 常用归纳形式的良基关系 归纳形式 良基关系 自然数归纳(1) m  n，如果m +1  n
1.4 归 纳 法 表1.1 常用归纳形式的良基关系 归纳形式 良基关系 自然数归纳(1) m  n，如果m +1  n 自然数归纳(2) m  n，如果m  n 结构归纳(1) e  e，如果e是e的直接子表达式 结构归纳(2) e  e，如果e是e的子表达式 基于证明的归纳   ，如果是证明的最后一步推导规则的某个前提的证明

38 1.4 归 纳 法 自然数归纳（形式1） 自然数归纳（形式2） 词典序（以自然数序列为例 ）
1.4 归 纳 法 自然数归纳（形式1） 为证明对所有n，P(n)为真，只需证明P(0)以及证明对任何m，如果P(m)为真则P(m+1)必定为真 自然数归纳（形式2） 为证明对所有n，P(n)为真，只需证明对任何m，如果所有的P(i) (i  m)为真则P(m)必定为真 词典序（以自然数序列为例 ） n1, n2, …, nk  m1, m2, …, ml iff k < l 或者k  l并且存在一个 i  k，使得对所有的 j < i有 nj  mj 并且ni < mi

39 习 题 1.2，1.5，1.6