《程序设计语言理论》PPT课件

程序设计语言理论,课程简介,计算机科学的理论体系1、模型理论关心的问题给定模型M，哪些问题可以由模型M解决如何比较模型的表达能力经典计算确定的图灵机，可计算性理论属于模型理论新型计算本质特点是交互(并发、分布、网络、网格、云)计算和交互的统一模型理论尚未出现,课程简介,计算机科学的理论体系2、程序理论关心的问题给定模型M，如何用模型M解决问题包括的领域程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等,课程简介,计算机科学的理论体系3、计算理论关心的问题给定模型M和一类问题，解决该类问题需要多少资源包括的领域计算复杂性理论,课程简介,围绕程序设计语言的研究（课程涉及内容用绿色表示）语法：形式语言和自动机理论，语法分析的实现技术语义：公理语义、操作语义、指称语义形式描述技术还有：代数规范、范畴论、属性文法程序设计的范型：命令式语言、函数式语言、逻辑程序设计语言、面向对象程序设计语言、并行程序设计语言,课程简介,围绕程序设计语言的研究（课程涉及内容用绿色表示）类型论与类型系统：多态类型、子类型、存在类型程序验证：程序正确性证明程序分析技术：数据流分析、控制流分析、模型检查、抽象解释程序的自动生成技术：程序变换,课程简介,学习的意义掌握与程序设计语言有关的理论，为从事有关的研究起一个奠基的作用应用：程序设计语言的设计和实现程序的自动生成程序分析与程序验证提高软件的可信程度协议的形式描述和验证,课程简介,教材和参考书陈意云、张昱，程序设计语言理论（第二版），高等教育出版社，2010.2教学资源网页：,课程简介,教材和参考书JohnC.Mitchell,FoundationsForProgrammingLanguages,MITPress,1996.BanjaminC.Pierce,TypesandProgrammingLaungages,MITPress,2002.RobertHarper,PracticalFoundationsforProgrammingLanguages,workingdraft,2009.JohnC.Reynolds,TheoriesofProgrammingLanguages,CambridgeUniversityPress,1998.GlynnWinskel,TheFormalSemanticsofProgrammingLanguages:AnIntroduction,MITPress,1993.,课程简介,课程要求讲课进展较快，平时不复习不加深理解，后面将听不懂作业较多，要求独立完成没有上机实验考试开卷成绩：考试成绩占70%，作业占30%,第1章引言,介绍一个非常简单的、以自然数和布尔值作为基本类型的、基于类型化演算的语言介绍该语言的语法、公理语义和操作语义主要议题如下：表示法和演算系统概述类型和类型系统的扼要讨论基于表达式的归纳、基于证明的归纳和良基归纳,1.1基本概念,1.1.1模型语言对程序设计语言进行数学分析从设计模型语言开始突出感兴趣的程序构造，忽略无关的细节语言的形式化分为两部分能抓住语言本质机制的非常小的核心：演算导出部分：它们可以翻译成核心的演算用类型化演算的框架来研究程序设计语言的各种概念,1.1基本概念,1.1.2表示法表示法的主要特征抽象：用于定义函数应用：将所定义的函数作用于变元抽象的例子（自然数类型上的几个例子）恒等函数：x:nat.x/命令式表示Id(x:nat)=x后继函数：x:nat.x1/函数式无需给函数命名常函数：x:nat.10x:nat.xtrue不是良形的表达式表示法写出的表达式叫做表达式或项,1.1基本概念,项x:.M和谓词演算公式x:A.的比较是一个约束算子x是一个占位符，约束变元，可以重新命名约束变元而不改变表达式的含义在x:.x+y中，x的出现是约束的，y的出现是自由的不含自由变元的表达式称为闭表达式应用：用项的并置来表示函数应用，例：(x:nat.x)5(x:nat.x)55/应用后面介绍的公理,1.1基本概念,一个简单的例子(x:nat.(y:nat.z:nat.(x+y)+z)3)45=(x:nat.z:nat.(x+3)+z)45=(z:nat.(4+3)+z)5=(4+3)+5=12,1.1基本概念,表示法中有两个约定函数应用是左结合的：MNP应看成(MN)P每个的约束范围尽可能地大：一直到表达式的结束，或碰到不能配对的右括号为止例x:.MN解释为x:.(MN)，而不是(x:.M)Nx:.y:.MN是x:.(y:.(MN)的简写(x:.(y:.(z:.M)N)P)Q可以简写为(x:.y:.z:.M)NPQ,1.2等式、归约和语义,表示法是演算的一部分，演算是关于表达式的一个推理系统除了语法外，该形式系统有三个主要部分公理语义：推导表达式相等的一个形式系统操作语义：基于单方向的等式推理（归约、符号计算）上述两者都称为证明系统指称语义：形式系统的模型,1.2等式、归约和语义,1.2.1公理语义一个等式公理系统约束变元改名公理（公理）x:.My:.yxM，M中无自由出现的y其中NxM表示M中的x用表达式N代换的结果例如x:.xy:.y函数应用公理（公理）(x:.M)NN/xM例如(x:nat.x+4)44/x(x+4)4+4,1.2等式、归约和语义,自反公理、对称性规则、传递性规则同余规则相等的函数应用于相等的变元产生相等的结果等式证明规则允许推导任何一组等式前提的逻辑推论,1.2等式、归约和语义,1.2.2操作语义语言的操作语义可用不同的方式给出定义一个抽象机,通过一系列的机器状态变换来计算程序演绎出最终结果的证明系统前面所列的等式公理的单向形式给出了归约规则最核心的归约规则是()的单向形式(x:.M)NN/xM通常没有归约规则：x:.My:.yxM,1.2等式、归约和语义,1.2.3指称语义确定语言构造（程序、语句、表达式等）到指称物（各种集合）的语义映射，满足：各种语言构造的实例都有对应的指称物复合构造的指称只依赖于它的子构造的指称类型化演算的指称语义每个类型表达式对应到一个集合类型的项解释为其值集上的一个元素类型的值集是函数集合，项x:.M解释为一个数学函数,1.3类型和类型系统,类型论为避免集合论悖论而建立起来的数学理论主要研究集合的分层、分类方法在程序设计语言理论中，类型论是指类型系统的设计、分析和研究类型提供了所有可能值的一种划分一个类型是一群有某些公共性质的值对于不同的类型系统，类型的多少和值所属的类型可能不同,1.3类型和类型系统,1.3.1类型和类型系统类型语言：变量都被给定类型未类型化的语言：不限制变量值的范围类型系统语言的一个组成部分由一组定型规则构成类型系统的研究有两个分支类型系统在程序设计语言中的应用“纯类型化演算”和各种逻辑之间的对应关系,1.3类型和类型系统,设计类型系统的目的用来证明程序不会出现不良行为类型可靠的语言（安全语言）所有程序运行时都没有不良行为出现类型系统的研究也需要形式化的方法许多语言定义被发现不是类型可靠的，甚至经过类型检查后接受的程序也会崩溃显式类型化的语言：类型是语法的一部分隐式类型化的语言,1.3类型和类型系统,1.3.2类型语言的优点开发时的实惠可以较早发现错误类型信息具有文档作用（比程序注解精确，比形式规范容易理解）编译时的实惠程序模块可以相互独立地编译运行时的实惠更有效的空间安排和访问方式，提高了目标代码的运行效率,1.3类型和类型系统,类型系统的其他应用许多程序分析工具使用类型检查或类型推断算法类型系统用来表示逻辑命题和证明,1.4归纳法,本节介绍本书常用的归纳法自然数归纳法（有两种形式，不专门介绍）结构归纳（介绍表达式上的归纳，有两种形式）证明上的归纳良基归纳法（重点介绍）,1.4归纳法,1.4.1表达式上的归纳表达式文法e:=0|1|v|e+e|ee每个表达式都有各自的语法树如果P是表达式的性质，Q是自然数的性质Q(n)语言树t.如果height(t)=n并且t是e的语法树，那么P(e)为真首先必须为高度是0的语法树直接证明P然后，对于语法树高度至少为1的表达式e，假定对于语法树高度较小的表达式，P都为真，证明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的归纳假设包含了所有的子表达式，并非只是直接子表达式,1.4归纳法,1.4.2证明上的归纳证明系统由公理和推理规则组成证明是一个公式序列，该序列中的每个公式都是公理或者是由前面的公式通过一个推理规则得到的结论基于证明的长度，用自然数归纳法来讨论证明的性质另一种观点把证明看成是某种形式的树,1.4归纳法,证明上的结构归纳对该证明系统中的每个公理，证明P成立假定对证明1,k，P成立，证明P()也为真是这样的证明，它结束于用一个推理规则，并且是从证明1,k延伸出来的一个证明,1.4归纳法,1.4.3良基归纳集合A的二元关系被称为是良基的：若A上不存在无穷递减序列a0a1a2例：在自然数上，如果ji+1，则ij。这个关系是良基关系良基关系的一些特点良基关系不一定有传递性良基关系都是非自反的，即对任何aA，aa不成立；否则会出现无穷递减序列aaa,1.4归纳法,引理1.1若是集合A上的二元关系，是良基的，当且仅当A的每个非空子集都有极小元证明假定是良基的，证明非空子集B(BA)有极小元用反证法。如果B无极小元，那么对每个aB，可以找到某个aB使得aa。则可以从任意的a0B开始，构造一个无穷递减序列a0a1a2假定每个子集都有极小元则不可能存在a0a1a2，因该序列给出了无极小元的集合a0,a1,a2,。故是良基的,1.4归纳法,命题1.2（良基归纳）令是集合A上的良基关系，令P是A上某个性质，若每当所有的P(b)(ba)为真，则P(a)为真，即a.(b.(baP(b)P(a)那么，对所有的aA，P(a)为真,1.4归纳法,命题1.2（良基归纳）若a.(b.(baP(b)P(a)，则a.P(a)证明若存在某个xA使得P(x)成立，则下面集合非空BaA|P(a)由引理1.1，B一定有极小元aB但是，对所有的ba，P(b)一定成立（否则a不是B的极小元）这就和假定b.(baP(b)P(a)矛盾,1.4归纳法,良基归纳法的使用如何理解：若每当所有的P(b)(ba)为真，则P(a)为真，即：(b.(baP(b)P(a)对某些a，不存在b，使得ba，则b.(baP(b)P(a)等价于P(a)（因为b:.P(b)为真，其中表示空集）对另一些a，存在b，使得ba，则b.(baP(b)P(a)的证明是基于b.(baP(b)为真来推导P