程序设计语言理论

《程序设计语言理论》由会员分享，可在线阅读，更多相关《程序设计语言理论（39页珍藏版）》请在金锄头文库上搜索。

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

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

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

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

5、信程度协议的形式描述和验证协议的形式描述和验证课课 程程 简简 介介教材和参考书教材和参考书陈陈意意云云、张张昱昱，程程序序设设计计语语言言理理论论（第第二二版版），高等教育出版社，高等教育出版社，2010.2教学资源网页：教学资源网页：http:/ 程程 简简 介介教材和参考书教材和参考书John C. Mitchell, Foundations For Programming Languages, MIT Press, 1996.Banjamin C. Pierce, Types and Programming Laungages, MIT Press, 2002. Robert Harp

6、er, 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. 课课 程程 简简 介介课程要求课程要求讲讲课课进进展展较较快快，平平时时不不复复习

7、习不不加加深深理理解解，后后面面将将听不懂听不懂作业较多，要求独立完成作业较多，要求独立完成没有上机实验没有上机实验考试开卷考试开卷成绩：考试成绩成绩：考试成绩占占70%，作业占，作业占30% 第第1章章 引引 言言介绍一个非常简单的、以自然数和布尔值作介绍一个非常简单的、以自然数和布尔值作为基本类型的、基于类型化为基本类型的、基于类型化 演算的语言演算的语言介绍该语言的语法、公理语义和操作语义介绍该语言的语法、公理语义和操作语义主要议题如下：主要议题如下： 表示法和表示法和 演算系统概述演算系统概述类型和类型系统的扼要讨论类型和类型系统的扼要讨论基于表达式的归纳、基于证明的归纳和良基归纳基于

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

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

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

11、 基基 本本 概概 念念一个简单的例子一个简单的例子 ( 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每个每个 的约束范围尽可能地大的约束范围尽可能地大：一直到表达式的结束，或一直到表达式的结束，或碰到不能配对的右括号

12、为止碰到不能配对的右括号为止例例 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 1.2 等式、归约和语义等式、归约和语义 表示法是表示法是 演算演算的一部分，的一部分， 演算是关于演算是关于 表表达式的一个推理系统达式的一个推理系统除了语法外，该形式系统有三个主要部分除了语法外，该形式系统有三个主要部分公理语义：公理语义：推导表达式相

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

14、理）( x: . .M)N N/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 操作语义操作语义语言的操作语义可用不同的方式给出语言的操作语义可用不同的方式给出定义一个抽象机

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

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

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

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

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

20、类型系统类型和类型系统类型系统的其他应用类型系统的其他应用许多程序分析工具使用类型检查或类型推断许多程序分析工具使用类型检查或类型推断算法算法类型系统用来表示逻辑命题和证明类型系统用来表示逻辑命题和证明1.4 归归 纳纳 法法本节介绍本书常用的归纳法本节介绍本书常用的归纳法自然数归纳法（有两种形式，不专门介绍）自然数归纳法（有两种形式，不专门介绍）结构归纳（介绍表达式上的归纳，有两种形结构归纳（介绍表达式上的归纳，有两种形式）式）证明上的归纳证明上的归纳良基归纳法（重点介绍）良基归纳法（重点介绍）1.4 归归 纳纳 法法1.4.1 表达式上的归纳表达式上的归纳表达式文法表达式文法 e := 0

21、 | 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)为真为真1.4 归归 纳纳 法法结构归纳结构归纳（形式（形式1）

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

23、则组成由公理和推理规则组成证明是一个公式序列，该序列中的每个公式证明是一个公式序列，该序列中的每个公式都是公理或者是由前面的公式通过一个推理都是公理或者是由前面的公式通过一个推理规则得到的结论规则得到的结论基于证明的长度，用自然数归纳法来讨论证基于证明的长度，用自然数归纳法来讨论证明的性质明的性质另一种观点把证明看成是某种形式的树另一种观点把证明看成是某种形式的树1.4 归归 纳纳 法法证明上的结构归纳证明上的结构归纳对该证明系统中的每个公理，证明对该证明系统中的每个公理，证明P成立成立假定对证明假定对证明 1, , k，P成立，证明成立，证明P( )也为真也为真 是这样的证明，它结束于用一个

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

25、a不成立；否则会出现无穷递减序列不成立；否则会出现无穷递减序列a a a 1.4 归归 纳纳 法法引理引理1.1 若若是集合是集合A上的二元关系，上的二元关系，是良基是良基的，的，当且仅当当且仅当A的每个非空子集都有极小元的每个非空子集都有极小元证明证明假定假定是良基的，是良基的，证明非空子集证明非空子集B(B A)有极小元有极小元 用反证法。如果用反证法。如果B无极小元，那么对每个无极小元，那么对每个a B，可以找到某个可以找到某个aB使得使得a a。则可以从任意则可以从任意的的a0 B开始，构造一个无穷递减序列开始，构造一个无穷递减序列a0 a1 a2 假定每个子集都有极小元假定每个子集都

26、有极小元 则则不不可可能能存存在在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

27、.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)矛盾矛盾1.4 归归 纳纳 法法良基归纳法的使用良基归纳法的使用如何理解：若每当所有的如何理解：若每当所有的P(b) (b a)为真，则为真，则P(a)为真，即：为真，即： ( b.(b a P(b) P(a)对某些对某些a，不存在，不存在b，使得，使得b a，则

28、，则 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)为为真真1.4 归归 纳纳 法法表表1.1 常用归纳形式的良基关系常用归纳形式的良基关系归纳形式归纳形式良基关系良基关系自然数归纳自然数归纳(1) m n，如果如果m +1 n自然数归纳自然数归纳(2) m n，如果如果m n结构归纳结构归纳(1)e e ，如如果果e是是e 的的直直接接子子表表

29、达达式式结构归纳结构归纳(2)e e ，如果如果e是是e 的子表达式的子表达式基基于于证证明明的的归归纳纳 ，如如果果 是是证证明明 的的最最后后一一步步推导规则的某个前提的证明推导规则的某个前提的证明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习习 题题1.2，1.5，1.6