第3章 简单类型化演算 函数式程序设计语言PCF由三部分组成 第2章对代数数据类型进行了透彻的研究 本章研究简单类型化演算

Presentation on theme: "第3章 简单类型化演算 函数式程序设计语言PCF由三部分组成 第2章对代数数据类型进行了透彻的研究 本章研究简单类型化演算"— Presentation transcript:

1 第3章 简单类型化演算 函数式程序设计语言PCF由三部分组成 第2章对代数数据类型进行了透彻的研究 本章研究简单类型化演算
第3章 简单类型化演算 函数式程序设计语言PCF由三部分组成 代数数据类型：自然数类型和布尔类型等 带函数和积等类型的纯类型化演算 不动点算子 第2章对代数数据类型进行了透彻的研究 本章研究简单类型化演算 第4章研究不动点算子

2 3.1 引 言 本章的系统是以后各章研究的所有其它演算的核心 抽象可用来定义新的函数，而代数数据类型只涉及到所声明的一阶函数的应用
3.1 引 言 本章的系统是以后各章研究的所有其它演算的核心 抽象可用来定义新的函数，而代数数据类型只涉及到所声明的一阶函数的应用 在类型化演算的指称语义中需要考虑函数类型的解释

3 3.1 引 言 演算的历史 Church在20世纪30年代研究的定义可计算函数的一种形式体系
3.1 引 言 演算的历史 Church在20世纪30年代研究的定义可计算函数的一种形式体系 Kleene在1936年证明，可定义的所有自然数函数正好是所有的递归函数 Turing在1937年证明，可定义的数值函数正好是Turing机可计算的函数 演算一直影响着程序设计语言的研究

4 3.1 引 言 演算和程序设计语言 20世纪50年代，无类型演算明显影响了Lisp语言的研究
3.1 引 言 演算和程序设计语言 20世纪50年代，无类型演算明显影响了Lisp语言的研究 20世纪60年代认识到，程序设计语言的语义可以通过使用拓展的演算给出 现代的观点认为，类型化演算引导对程序设计语言进行更加涉及本质的分析 让类型化演算的类型对应到程序设计语言中的类型，就可以忠实地为类型化程序设计语言的能力和局限性建模

5 3.1 引 言 本章的主要内容 提出使用定型公理和推理规则的上下文有关语法 讨论类型化演算的等式证明系统(公理语义)和归约系统（操作语义）
3.1 引 言 本章的主要内容 提出使用定型公理和推理规则的上下文有关语法 讨论类型化演算的等式证明系统(公理语义)和归约系统（操作语义） 讨论类型化演算的通用模型（指称语义）及可靠性和完备性定理 介绍PCF语言（递归函数留待下一章）及其公理语义和操作语义

6 3.2 类型和项 3.2.1 类型的语法 简单类型化演算的类型表达式文法 用、和来命名所讨论的演算
3.2 类型和项 3.2.1 类型的语法 简单类型化演算的类型表达式文法  ::= b | null | unit |   |   |   b：类型常量 null：初始类型 unit：终结类型 和、积与函数类型 类型表达式中不含类型变量 用、和来命名所讨论的演算

7 3.2 类型和项 3.2.2 上下文有关语法 不存在上下文无关文法，它正好产生良类型的项 用一种基于逻辑的形式系统来定义类型语言
3.2 类型和项 3.2.2 上下文有关语法 不存在上下文无关文法，它正好产生良类型的项 用一种基于逻辑的形式系统来定义类型语言 用公理和推理规则来同时定义表达式及其类型 定型公理 c : 推理规则 定型断言   M : , 其中  {x1 :1 , …, xk:k } M1:1 … Mk:k N : 1  M1:1 … k  Mk:k   N : 7

8 3.2 类型和项 3.2.3 项的语法 一个基调  B, C包含
3.2 类型和项 项的语法 一个基调  B, C包含 一个集合B，其元素叫做基本类型或类型常量 形式为c的项常量集合C，其中是B上的类型表达式 多类代数的基调  S, F 的基调很容易变换成基调  B, C 令B就等于S 若F有f : s1  …  sk  s，则在C中包含项常量 f : s1  …  sk  s 8

9 3.2 类型和项 项的语法及类型按如下方式描述 定型公理 首先用BNF定义类型表达式的语法（3.2.1节）
3.2 类型和项 项的语法及类型按如下方式描述 首先用BNF定义类型表达式的语法（3.2.1节） 然后用定型公理和定型规则同时定义上的项和它们的类型（良形的项就是良类型的项） 良形（well-formed）和良类型（well-typed） 良形的项x + 3在x是整型时才是良类型的 定型公理   c   (cst) x    x   (var) 9

10 3.2 类型和项 定型规则   M : , x :  M : , x :  M :
3.2 类型和项 定型规则 (add var) ( Intro) ( Elim) 定型断言的证明叫做定型推导   M : , x :  M : , x :  M :   ( x : . M) :     M :    N :   MN : 10

11 3.2 类型和项 例 y:  (x:.x)y: 是一个需要用到所有这些定型规则的项 从定型公理x:  x:开始
3.2 类型和项 例 y:  (x:.x)y: 是一个需要用到所有这些定型规则的项 从定型公理x:  x:开始 根据( Intro) 规则，得到  x:. x :    再由（add var），得到y:   x:. x :    由公理y:  y: 最后，由( Elim)规则可知 y:  (x:. x)y:是良类型的 11

12 3.2 类型和项 引理3.1 引理3.2 引理3.3 如果M:，那么M中的每个自由变量都出现在中
3.2 类型和项 引理3.1 如果M:，那么M中的每个自由变量都出现在中 引理3.2 如果M:，且包含M中所有的自由变量，那么M: 引理3.3 如果M:，并且y不出现在中，那么[y/x]  [y/x]M: 12

13 3.2 类型和项 引理3.4 如果1,x:  M:和2N:都是项，且12是良形的类型指派，那么代换实例12  [N/x]M:是良形项 证明 基于对定型断言1，x:  M: 的证明的归纳 13

14 3.2 类型和项 3.2.4 有积与和及相关类型的项 1、笛卡儿积（把扩展到, ） ( Intro) ( Elim)1
3.2 类型和项 3.2.4 有积与和及相关类型的项 1、笛卡儿积（把扩展到, ） ( Intro) ( Elim)1 ( Elim)2   M :    N :    M, N :      M :      Proj1,  M:    M :      Proj2,  M:  14

15 3.2 类型和项 积的另一种表示 对所有的类型和，存在项常量 Pair,  :     ( )
3.2 类型和项 积的另一种表示 对所有的类型和，存在项常量 Pair,  :     ( ) Proj1,  : ( )   Proj2,  : ( )   M, N,  看成Pair,  M N的语法美化 两种表示的主要区别 第二种表示：Pair、Proj1和Proj2都是项 第一种表示：x:.y:.Pair x y、x: .Proj1x和x: .Proj2x 才是良形的项 15

16   M :  +    N :    P : 
3.2 类型和项 2、和 (+ Intro)1 (+ Intro)2 (+ Elim)   M :    Inleft,  M :  +    M :    Inright,  M:  +    M :  +    N :    P :    Case, ,  M N P :  16

17 3.2 类型和项 初始类型和终结类型 与终结类型unit有关的唯一的项  : unit (unit Intro) 终结类型也叫做单位类型
3.2 类型和项 初始类型和终结类型 与终结类型unit有关的唯一的项  : unit (unit Intro) 终结类型也叫做单位类型 C语言的void类型就是单位类型，因为该类型的 表达式没有能够引起兴趣的值（而不是没有值） 与初始类型null有关的项形式 Zero : null   (null Elim) 若null类型有元素， 函数Zero给出使用方式 17

18 3.2 类型和项 有了单位类型与和类型后，bool类型可省略 bool类型可以定义成 bool  unit + unit
3.2 类型和项 有了单位类型与和类型后，bool类型可省略 bool类型可以定义成 bool  unit + unit true和false可以定义成 true  Inleft  false  Inright  if … then … else可以定义成 if M then N else P  Caseunit, unit,  M (K, unit N) (K, unit P) 其中K, unit  x:.y:unit.x 18

19 3.2 类型和项 多元函数和高阶函数之间的关系 Curry,  f :  .x:.y:.f x, y
3.2 类型和项 多元函数和高阶函数之间的关系 Curry,  f :  .x:.y:.f x, y add  p:nat  nat.(Proj1 p) + (Proj2 p) Curry(add)  (f:nat  nat  nat.x:nat.y:nat.f x, y) add = x:nat.y:nat.add x, y  x:nat.y:nat.(p:nat  nat. (Proj1 p) + (Proj2 p)) x, y = x:nat.y:nat.Proj1x, y + Proj2 x, y = x:nat.y:nat.x + y 19

20 3.2 类型和项 3.2.5 定型算法 基调上预备项 给定, M, ，   M:是否为可证明的定型断言
3.2 类型和项 3.2.5 定型算法 给定, M, ，   M:是否为可证明的定型断言 给定，M，判定是否存在一个，使得   M:可证 基调上预备项 M ::= c | x | MM | x:.M 该文法可以从定型公理和推理规则得到 类型检查的输入是符合该文法的预备项 20

21 3.2 类型和项 类型检查算法 TC(, c) =  若 c:  是该基调的一个常量 fail 否则
3.2 类型和项 类型检查算法 TC(, c) =  若 c:  是该基调的一个常量 fail 否则 TC(, x) =  若 x:   否则 fail TC(, MN) =  若TC(, M) =    且 TC(, N) =  TC(, x:.M) =    若TC((x:.M , x:), M) =  21

22 3.2 类型和项 命题3.5 算法TC(, M)终止且得到类型，当且仅当定型断言  M:是可推导的
3.2 类型和项 命题3.5 算法TC(, M)终止且得到类型，当且仅当定型断言  M:是可推导的 若对于和M，不存在可推导的定型断言，则算法停机，报告失败 22

23 3.3 证明系统 3.3.1 等式和理论 等式 泛代数：M  N []，只有平凡的永真等式
3.3 证明系统 3.3.1 等式和理论 等式 泛代数：M  N []，只有平凡的永真等式 类型化演算：  M  N  ，有非平凡的永真等式，和代数不同的是，等式包含类型，它用于等式证明系统 代数系统中和类型有关的规则（作为副条件） P , Q Termss(, ) M = N , x : s P = Q  P/xM = Q/xN  23

24 3.3 证明系统 3.3.1 等式和理论 等式 泛代数：M  N []，只有平凡的永真等式
3.3 证明系统 3.3.1 等式和理论 等式 泛代数：M  N []，只有平凡的永真等式 类型化演算：  M  N  ，有非平凡的永真等式，和代数不同的是，等式包含类型，它用于等式证明系统 等式的另一种表示方式是 x1:1… xk:k.M  N 若某个类型为空，则该等式无意义地成立 24

25 3.3 证明系统 公理和推理规则 (add var)   M = N :    M = M : (ref)
3.3 证明系统 公理和推理规则 (add var)   M = M : (ref) (sym) (trans)   M = N :  , x :   M = N :    M = N :    N = M :    M = N :    N = P :    M = P :  25

26 3.3 证明系统 公理和推理规则 () , x:  M = N :  ()
3.3 证明系统 公理和推理规则 () ()   x.M = y.[y/x]M : , 其中y FV(M) ()   (x.M)N =[N/x]M : ()   x.(Mx) =M : , 其中x FV(M) () , x:  M = N :    x:.M = x:.N :      M1 = M2 :      N1 = N2 :    M1 N1 = M2 N2 :  26

27 3.3 证明系统 引理3.6 如果  M = N :并且包含M和N中所有的自由变量，那么  M = N: 
3.3 证明系统 引理3.6 如果  M = N :并且包含M和N中所有的自由变量，那么  M = N:  基调的类型化理论 项之间的包含上述公理的一组良类型的等式，并且封闭于上述推理规则 E   M = N: 表示：等式  M = N:是从公理和E的等式可证 E的理论Th(E)是指：从公理和E的等式可证的等式集合 27

28 3.3 证明系统 代数和简单类型化演算之间的联系 在类型化上可以增加代数公理，任何代数等式可以看成等式
3.3 证明系统 代数和简单类型化演算之间的联系 在类型化上可以增加代数公理，任何代数等式可以看成等式 任何一个代数证明可以在中执行 代数证明规则(subst)不在中，但可以证明它是的导出规则 P, Q Termss(, ) M = N , x : s P =Q  P/xM = Q/xN  28

29 3.3 证明系统 命题3.8 命题3.9（守恒性） 令E 是代数基调上代数项之间的一组等式，令E
3.3 证明系统 命题3.8 令E 是代数基调上代数项之间的一组等式，令E 是单个这样的等式。若在代数证明系统中有EE， 则把E的等式和E都看成是基调上项之间的等 式，在证明系统中也有E  E 命题3.9（守恒性） 令E是代数基调上代数项之间的等式集合，并令E 是单个这样的等式。当把E的等式和E都看成是基 调上项之间的等式时，若在证明系统中有 E  E，则在该代数证明系统中也有E  E 29

30 3.3 证明系统 命题3.10 存在有类型化演算理论E及没有x自由出现的项M和N，使得 E  , x:  M = N : 
3.3 证明系统 命题3.10 存在有类型化演算理论E及没有x自由出现的项M和N，使得 E  , x:  M = N :  但是E    M = N : 表明等式中变量情况会影响可证明性 30

31 3.3 证明系统 积类型 和类型   Proj1M, N = M :  (proj1)
3.3 证明系统 积类型   Proj1M, N = M :  (proj1)   Proj2M, N = N : (proj2)   Proj1M, Proj2M = M : (sp) 和类型   Case, , (Inleft, M) N P = N M :  (case)1   Case, , (Inright, M) N P = P M : (case)2   Case, ,  M (N  Inleft, ) (N  Inright, ) = N M : + (case)3 仅N:( +)  ( +)时，(case)3的项才是良形的 31

32 3.3 证明系统 终结类型 初始类型   M =  : unit 对每个类型，存在唯一的函数One :   unit
3.3 证明系统 终结类型   M =  : unit 对每个类型，存在唯一的函数One :   unit 可以把One写成x:. 初始类型   M  Zero : null  对任何类型，存在唯一的函数Zero : null  32

33 3.3 证明系统 简单类型化演算版本之间的联系  在上守恒 逻辑系统或语言L2在L1上守恒，如果 L2包含L1，并且
3.3 证明系统 简单类型化演算版本之间的联系 逻辑系统或语言L2在L1上守恒，如果 L2包含L1，并且 对L1的任意一组公式F和任意一个公式F，若在L2的证明系统中有 F  F，则在L1的证明系统中也有F  F  在上守恒 33

34 3.3 证明系统 3.3.2 归约规则 归约规则 引理3.11 合流性和强范式化 预备项上的规则并不合流
3.3 证明系统 3.3.2 归约规则 归约规则 (x:.M)N  NxM ()red x:.Mx  M， xFV(M) ()red 引理3.11 如果  M :并且M  N，那么  N : 合流性和强范式化 预备项上的规则并不合流 x :.(y :.y)x的范式有两个：x :.x和y :.y 34

35 3.3 证明系统 在类型化项上的可变换关系 推论3.12   M N 当且仅当存在项M0, …, Mk 且
3.3 证明系统 在类型化项上的可变换关系   M N 当且仅当存在项M0, …, Mk 且   Mi （0 i  k），使得 M  M0  M1  …  Mk  N 就纯, 归约来说，对每个i，所做假设Mi不是必要的 推论3.12 等式  M  N 从的公理可以证明，当且仅当  M  N ，当且仅当存在某个项P，使得M  P并且N  P 35

36 3.3 证明系统 小结 带积、和、unit及null类型的类型化演算的归约公理都可以由从左向右定向相应的等式公理得到
3.3 证明系统 小结 带积、和、unit及null类型的类型化演算的归约公理都可以由从左向右定向相应的等式公理得到 对简单类型化演算的所有版本，强范式化都成立，但是合流性却难以捉摸 36

37 3.3 证明系统 3.3.3 有其它规则的归约 每个代数基调都可以看成一个基调 一些结论 代数项集可以看成是项的一个子集，并且
3.3 证明系统 3.3.3 有其它规则的归约 每个代数基调都可以看成一个基调 代数项集可以看成是项的一个子集，并且 代数重写规则可以应用到项 一些结论 若代数基调的代数重写系统R合流并终止，那么对上的项，R，归约合流并终止 若R合流并左线性，那么对上项，R，，fix归约是合流的 37

38 3.4 通用模型、可靠性和完备性 模型概述 对于一个逻辑系统来说，模型提供一种机制，它给出每个良形表达式的数学含义，以确定该逻辑中的任何公式是否为真 对于使用变量的逻辑系统，通常把给变量指派值（称为环境）从模型的一般概念中分离 代数规范的模型是代数（类似的还有一阶逻辑） 把类别解释为集合 把函数符号解释为函数 为代数项中变量指派值后，就可计算项的解释 38

39 3.4 通用模型、可靠性和完备性 3.4.1 通用模型和项的含义 类型化演算的模型类似于一个代数 每个类型需要一个值集
每个常量符号解释到对应值集中的特定元素 还必须使应用表达式和抽象表达式有意义 假定A是类型的值集，则要求A为从A到A的一个函数集合 每个可定义的函数必须处于适当的值集中 39

40 3.4 通用模型、可靠性和完备性 3.4.1 通用模型和项的含义 类型化演算的模型论比代数规范的模型论要复杂得多
上述简单扩展不能适应有不动点算子的情况（好在本章暂不关心） 本章将采用比上述简单扩展的适应性更广一点的“通用模型”，它由三部分组成： （1）类型化的应用结构 （2）作为模型的外延性条件 （3）作为模型的环境条件 40

41 3.4 通用模型、可靠性和完备性 3.4.2 应用结构、外延性和框架 基调上的类型化应用结构A：
{A}, {App, }, Const 对其中每对和，假定满足下列条件： A是一个集合 App, 是映射App, : A   A  A Const是从的项常量到所有A并集的成员的映射,使得若c:，则Const(c) A 引入App,  映射的目的是给A 以宽松的解释 41

42 3.4 通用模型、可靠性和完备性 满足下列条件的应用结构是外延的 可以用直接具有外延性的模型定义来代替应用结构
对任意的f, gA，若对所有的dA，都有 App f d = App g d，则f = g 函数外延性：若对任意x有f(x)=g(x) ，则f和g相等 可以用直接具有外延性的模型定义来代替应用结构 类型框架是一个应用结构 {A}, {App, }, Const 满足A   (A) 且App,  f d = f (d) 类型框架可简写成{A}, Const，甚至{A} A 42

43 3.4 通用模型、可靠性和完备性 例 一组基类型上完备的集合论函数层级（full set-theoretic function hierarchy） A = {A}, Const，其中A 包含从A 到A的所有集合论函数 引理3.13 一个应用结构A是外延的当且仅当存在同构的类型框架B A 43

44 3.4 通用模型、可靠性和完备性 3.4.3 环境条件 环境  下的良型项  M:的含义AM 
环境条件 环境  下的良型项  M:的含义AM  由对定型推导子句进行归纳来定义 A  c: = Const(c) Ax:  x: = (x) A, x:  M: = A  M: A  MN: = App,  A  M:  A   N: A  x:.M:  = 唯一的fA ，使得dA.App f d = A, x:  M: [x  d] 若定义了全函数A，则说A满足环境条件 44

45 3.4 通用模型、可靠性和完备性 通用模型 满足外延性和环境两条件的类型化应用结构 外延性条件等价于 一个函数类型的解释必须是某个函数集合
环境条件保证 有足够多的元素，使得每个可定义的函数都在这个模型中 若无环境条件，使得dA.App f d = A, x:  M: [x  d] 的 f A  可能不存在 外延性保证，若存在则唯一 45

46 3.4 通用模型、可靠性和完备性 3.4.4 类型可靠性和等式可靠性 两个证明系统：分别证明定型断言和等式 引理3.17（类型可靠性）
令A是基调的任意通用模型，M:是可证明的定型断言，并且  是A的一个环境，那么 A  M :   A 良类型的项不包含类型错误 46

47 3.4 通用模型、可靠性和完备性 等式可靠性 引理3.20（代换引理） 可满足性
令, x:  M : 和   N : 都是项，  ，且d =  N:，则   [Nx]M :   = , x:  M : [x d] 可满足性 若 A  M : = A  N :，就说通用模型A和环境   满足等式  M = N :，写成 A,     M = N : 47

48 3.4 通用模型、可靠性和完备性 定理3.21（可靠性） 对任何类型化的等式集合E，若 E    M = N :，
写成 E    M = N : 48

49 3.4 通用模型、可靠性和完备性 3.4.5 没有空类型的通用模型的完备性 多类代数中有两个完备性定理 演算 一般情况下的演绎完备性
空类别被略去时的最小模型完备性 演算 没有空类型时的最小模型完备性（本小节） 不扩展证明系统的话，通用模型没有演绎完备性（下一小节，课堂不介绍） 考虑更一般的范畴模型的话，对给定的证明系统,有直截了当的最小模型完备性 49

50 3.4 通用模型、可靠性和完备性 非空类型的推理规则 定理3.22 x在M和N中没有自由出现 (nonempty)
令E是封闭于(nonempty)规则的任意理论。 那么，存在一个通用模型A，它没有任何A = ， 并且它正好满足E的等式 , x:  M =N:   M = N :  50

51 3.5 可计算函数编程语言 3.5.1 概述 讨论代数数据类型和简单类型化演算在程序设计语言设计中的应用
3.5 可计算函数编程语言 3.5.1 概述 讨论代数数据类型和简单类型化演算在程序设计语言设计中的应用 提出用于对可计算函数进行编程的函数式程序设计语言PCF 有关递归函数的部分推迟到第4章给出 PCF的设计目的是便于本章和以后章节的分析和讨论 本节还总结该语言的公理语义和操作语义 51

52 3.5 可计算函数编程语言 3.5.2 PCF的语法 1、布尔类型和自然数类型 布尔类型常量：true，false 布尔类型条件表达式：
3.5 可计算函数编程语言 PCF的语法 1、布尔类型和自然数类型 布尔类型常量：true，false 布尔类型条件表达式： if bool_exp then bool_exp else bool_exp 自然数类型常量0, 1, 2, 3, …（数码 ） 自然数类型条件表达式 if bool_exp then nat_exp else nat_exp 自然数相等测试： Eq? 如： Eq? 5 0  false 并未列出基本类型的表达式的所有可能形式 52

53 3.5 可计算函数编程语言 2、其他类型 3、条件表达式可定义在任意类型上 函数类型与积类型 和简单类型化演算中的一样
3.5 可计算函数编程语言 2、其他类型 函数类型与积类型 和简单类型化演算中的一样 不加入和类型、unit类型和null类型 3、条件表达式可定义在任意类型上 文法表示 _exp::=… | if bool_exp then _exp else _exp 例： nat_exp ::= if bool_exp then nat_exp else nat_exp 53

54 3.5 可计算函数编程语言 3.5.3 声明和语法美化 在PCF语言中引入let声明，相当于命令式语言的局部声明
3.5 可计算函数编程语言 3.5.3 声明和语法美化 在PCF语言中引入let声明，相当于命令式语言的局部声明 let x :  = M in N 表达的意思是，在声明体N中，x被约束到M 可以用PCF语言已有部分来严格定义 let x :  = M in N  (x : .N)M 因此，把let看成一种缩写，或称为语法美化，而不把let声明直接加入PCF 这样，无须规定任何有关let的等式公理和归约规则 54

55 3.5 可计算函数编程语言 例1：命令式语言的局部声明可用let形式表示 对应的表达式
3.5 可计算函数编程语言 例1：命令式语言的局部声明可用let形式表示 begin function f (x : nat) : nat; return x; end; body end 对应的表达式 let f : nat  nat = x : nat.x in body (f : nat  nat . body) (x : nat.x) 55

56 3.5 可计算函数编程语言 例2：let可以嵌套（做两步消去两个let）
3.5 可计算函数编程语言 例2：let可以嵌套（做两步消去两个let） let compose : (nat  nat)  (nat  nat)  nat  nat = f : nat  nat.g : nat  nat.x : nat.f(gx) in let h : nat  nat = x : nat.x + x in compose h h 5 (h : nat  nat. compose h h 5) x : nat.x + x) (compose : (nat  nat)  (nat  nat)  nat  nat. f : nat  nat.g : nat  nat.x : nat.f(gx) 56

57 3.5 可计算函数编程语言 例2：完成化简演算 (compose : (nat  nat)  (nat  nat)  nat  nat. (h : nat  nat. compose h h 5) x : nat.x + x) f : nat  nat.g : nat  nat.x : nat.f(gx)  (h : nat  nat.(f : nat  nat.g : nat  nat. x: nat.f (gx))h h 5) (x : nat.x + x)  (f : nat  nat.g : nat  nat.x : nat.f(gx)) (x : nat.x + x) (x : nat.x + x) 5  (x : nat.x + x) ((x : nat.x + x) 5)  ((x : nat.x + x) 5) + ((x : nat.x + x) 5)  (5 + 5) + (5 + 5)  20 57

58 3.5 可计算函数编程语言 另一种语法美化 let f (x : ) : = M in N
3.5 可计算函数编程语言 另一种语法美化 let f (x : ) : = M in N let f :  = x :.M in N ( f : .N) (x :.M) 58

59 3.5 可计算函数编程语言 3.5.4 程序和结果 PCF语言有两个语法范畴：类型和项 可观测类型：自然数类型和布尔类型
3.5 可计算函数编程语言 3.5.4 程序和结果 PCF语言有两个语法范畴：类型和项 可观测类型：自然数类型和布尔类型 像nat  nat这样的函数类型不是可观测的类型 程序：良形的、可观测类型的闭项 注意：PCF语言无输入和输出 结果：执行程序的可观测的效果，应该是可观测类型的闭范式 语义：程序集合和结果集合之间的一种关系 59

60 3.5 可计算函数编程语言 3.5.5 公理语义 公理语义是一个证明系统 性质的表示 等式公理语义 两个程序在公理语义中等价
3.5 可计算函数编程语言 3.5.5 公理语义 公理语义是一个证明系统 可以推导程序及其组成部分的性质 性质的表示 等式、给定输入下的输出断言、或其它形式 等式公理语义 性质仅用等式表示 两个程序在公理语义中等价 为它们推导出的断言正好完全相同 60

61 3.5 可计算函数编程语言 公理 自反 基本类型nat和bool (cond) if true then M else N = M
3.5 可计算函数编程语言 公理 自反 (ref) M = M 基本类型nat和bool (add) = 0, = 1, … , = 8, … (Eq?) Eq? n n = true, Eq? n m = false （n和m是不同的数码） (cond) if true then M else N = M if false then M else N = N 61

62 3.5 可计算函数编程语言 二元组 重新命名约束变量 函数 (proj) Proj1 M, N = M Proj2 M, N = N
3.5 可计算函数编程语言 二元组 (proj) Proj1 M, N = M Proj2 M, N = N (sp)  Proj1 P, Proj2 P  = P 重新命名约束变量 ( ) x:.M = y:.yxM （y在M中不是自由的） 函数 ( ) (x : .M)N = N/xM ( ) x : .Mx = M （x在M中不是自由的） 62

63 if M1 then N1 else P1 = if M2 then N2 else P2
3.5 可计算函数编程语言 推理规则 等价 (sym),(trans) 同余 nat和bool M = N N = M M = N N = P M = P M = N P = Q M+P = N+Q M = N P = Q EQ? MP = EQ? NQ M1 = M2 N1 = N2 P1 = P2 if M1 then N1 else P1 = if M2 then N2 else P2 63

64 3.5 可计算函数编程语言 同余 序对 函数 M = N Proji M = Proji N M = N P = Q
3.5 可计算函数编程语言 同余 序对 函数 M = N Proji M = Proji N M = N P = Q M, P  =  N, Q  M = N x:. M = x:. N M = N P = Q M P = N Q 64

65 3.5 可计算函数编程语言 部分同余规则多余 例：+的同余规则多余 抽象和应用必须有 若M=N 和P=Q，则由自反公理，有等式
3.5 可计算函数编程语言 部分同余规则多余 抽象和应用必须有 例：+的同余规则多余 若M=N 和P=Q，则由自反公理，有等式 x : nat.y : nat.x  y = x : nat.y : nat.x  y 由应用的同余规则可得 (x:nat.y:nat.x  y)M = (x:nat.y:nat.x  y)N 由公理和传递性可得 y : nat.M  y = y : nat.N  y 再次使用同余规则、公理和传递性可得 M  P = N  Q 65

66 3.5 可计算函数编程语言 PCF语言公理语义的特点 PCF语言对类型并不需要证明系统 强到足以确定程序的含义
3.5 可计算函数编程语言 PCF语言公理语义的特点 强到足以确定程序的含义 证明不了加法可交换，也证明不了递归函数之间的许多有意义的等价 这些性质需要用归纳法来证明 PCF语言对类型并不需要证明系统 因为两个类型相同当且仅当它们在语法上相同 66

67 3.5 可计算函数编程语言 3.5.6 操作语义 基本特点 类型nat和bool 把等式规则定向为重写规则，以强调归约方向
3.5 可计算函数编程语言 3.5.6 操作语义 基本特点 把等式规则定向为重写规则，以强调归约方向 eval (M) = N当且仅当M  N 类型nat和bool (add)  0, 0 +1  1, … , 3 +5  8, … (Eq?) Eq? n n  true, Eq? n m  false (n和m是不同的数码) (cond ) if true then M else N  M if false then M else N  N 67

68 3.5 可计算函数编程语言 序对 重新命名约束变量 函数 (proj) Proj1 M, N  M Proj2 M, N  N
3.5 可计算函数编程语言 序对 (proj) Proj1 M, N  M Proj2 M, N  N 重新命名约束变量 ( ) x:.M = y:.yxM (y在M中不是自由的) 用本规则进行约束变元改名，而不是化简 函数 ( ) (x:.M)N  N/xM 68

69 3.5 可计算函数编程语言 该操作语义的特点 定理3.23 抽象：没有指定计算步骤 3.6节用几种归约策略把它具体化
3.5 可计算函数编程语言 该操作语义的特点 抽象：没有指定计算步骤 3.6节用几种归约策略把它具体化 保留了重新命名约束变量的等式公理的形式 因而不是一个终止的重写系统 对于序对的满射配对公理(sp)和函数的外延公理()，没有相应的归约规则 因为对于归约程序来说，这些规则多余 定理3.23 PCF归约是合流的 69

70 3.5 可计算函数编程语言 定理3.24 PCF语言是安全的 安全语言：具有保持性和前进性的语言 保持性
3.5 可计算函数编程语言 定理3.24 PCF语言是安全的 安全语言：具有保持性和前进性的语言 保持性 若  M:且M  M'，那么  M': 前进性 若  M :且是可观察类型，则M是闭范式，或者存在程序M'，使得M  M' 前进性并不保证得到闭范式，但保证在未归约到闭范式时，还能继续归约 70

71 3.5 可计算函数编程语言 3.5.7 由各种形式的语义定义的等价关系 各种语义上的等价关系 公理等价：M = N 可证
3.5 可计算函数编程语言 3.5.7 由各种形式的语义定义的等价关系 各种语义上的等价关系 公理等价：M = N 可证 用M =ax N表示 指称等价：M和N对自由变量的任何取值都有相同的指称 用M =den N表示 操作等价：eval(M ) ≃ eval (N )（程序M和N求值的结果一样，或者都没有定义） 用M =op N表示 71

72 3.5 可计算函数编程语言 操作等价M =op N的推广 上下文C[ ]是一个项，但其中有一个洞 例：
3.5 可计算函数编程语言 操作等价M =op N的推广 上下文C[ ]是一个项，但其中有一个洞 例： 若C0[ ]  x : nat.x + [ ] 则 C0[x]是x : nat.x + x 操作等价可以从程序推广到一般项 如果对任意使得C[M]和C[N]都是程序的上下文C[]，都有eval (C[ M ] ) ≃ eval (C[ N ] )，则项M和N操作等价 72

73 3.5 可计算函数编程语言 等式证明系统的可靠性 如果在公理语义中能证明M和N相等，那么在指称语义中，M和N应该有同样的含义
3.5 可计算函数编程语言 等式证明系统的可靠性 如果在公理语义中能证明M和N相等，那么在指称语义中，M和N应该有同样的含义 即 =ax  =den 这是判断公理系统正确性的基本标准 对PCF语言而言，公理语义对指称语义是可靠的 73

74 3.5 可计算函数编程语言 操作语义的计算适当性 若M是个程序，且M和作为结果的N有同样的指称，则在操作语义中，执行程序M的结果是N
3.5 可计算函数编程语言 操作语义的计算适当性 若M是个程序，且M和作为结果的N有同样的指称，则在操作语义中，执行程序M的结果是N 计算适当性表明已有足够的归约规则去确定任何程序的值 对PCF语言而言，操作语义有计算的适当性 74

75 3.5 可计算函数编程语言 PCF等价性小结 对任意程序
3.5 可计算函数编程语言 PCF等价性小结 对任意程序 (programs M )(results N ) M =ax N iff M =denN iff M =op N 对任意项 =ax  =den  =op 操作等价是三者中最粗糙的一个，和指称等价或可证明的等价相比，可能有更多的项操作等价 若=op  =ax，可能会出现不一致的证明系统 75

76 3.5 可计算函数编程语言 3.5.8 记录和n元组 记录类型 优点 记录是多个成分的聚集，每个成分有不同的标记
3.5 可计算函数编程语言 3.5.8 记录和n元组 记录类型 记录是多个成分的聚集，每个成分有不同的标记 类型写成l1 : 1, …, l k : k 记录写成l1 = M1, …, l k = Mk 记录r中的成分li的选择可用加点的记号r.li来表示 等式公理 l1 = M1, …, l k = Mk .li = Mi 优点 成分次序无关紧要，选择助记忆的名字作为标记 76

77 3.5 可计算函数编程语言 引入n元积记号 n元积 1  …  n  1  (2  … (n-1  n) … )
3.5 可计算函数编程语言 引入n元积记号 n元积 1  …  n  1  (2  … (n-1  n) … ) n元组 M1, …, Mn  M1, M2, … Mn-1, Mn …   很容易检查 若Mi : i，则M1, … , Mn : 1  …  n 取n元组的成分  x:1  …  n .Proj1( x) (i < n)  x:1  …  n .( x) 1  …  n Proji i - 1 Proj2 1  …  n Projn n - 1 Proj2 77

78 3.5 可计算函数编程语言 记录翻译成PCF表达式
3.5 可计算函数编程语言 记录翻译成PCF表达式 l1 : 1, …, l k : k   1  …  k l1 = M1, …, l k = Mk   M1, …, M k M.li  M 例：let r :A:int, B:bool = A = 5, B = false in if r.B then r.A else r.A + 1 去掉语法美化，得到： let r :int  bool = 5, false in if Proj2 r then Proj1 r else (Proj1 r) +1 1  …  n Proji 78

79 3.6 各种归约策略 3.6.1 归约策略 归约策略F 部分计算函数evalF : PCF  PCF
3.6 各种归约策略 3.6.1 归约策略 归约策略F 项到项的部分函数F，如果F(M) = N，那么MN 部分计算函数evalF : PCF  PCF M, F(M) 未定义 evalF (M) = N, F(M) = M且evalF(M) = N evalF在数学上等价于遵循策略F逐步进行归约，直到该策略不能再遵循为止 79

80 3.6 各种归约策略 一步归约策略 只要有可能便进行一步归约的策略 程序M的计算eval(M)是M的范式或者eval(M)没有定义
3.6 各种归约策略 一步归约策略 只要有可能便进行一步归约的策略 程序M的计算eval(M)是M的范式或者eval(M)没有定义 基于项本身的形式来选择一步归约 先“优化”函数x : .M 最左归约（惰性归约） 急切归约 (x : .M)N (x : .M)N (x : .M)N [N/x]M 80

81 3.6 各种归约策略 3.6.2 最左归约和惰性归约 最左归约：对项中尽可能左边的符号进行归约 例 遵循的是结构化操作语义的风格
3.6 各种归约策略 3.6.2 最左归约和惰性归约 最左归约：对项中尽可能左边的符号进行归约 遵循的是结构化操作语义的风格 每条规则正好作用到一种形式的项 考察项的结构就知道该用哪条规则 例 (x : nat.y : nat.x + y) ( (z : nat.z) 20) left y : nat.( (z : nat.z) 20) + y left y : nat.20 + y 81

82 3.6 各种归约策略 例 ((x : nat.y : nat.x + y) 9) 7 + (x : nat.x) 5
3.6 各种归约策略 例 ((x : nat.y : nat.x + y) 9) 7 + (x : nat.x) 5 left (y : nat.9+ y) 7 + (x : nat.x) 5 left (9 + 7) + (x : nat.x) 5 left 16 + (x : nat.x) 5 left left 21 82

83 3.6 各种归约策略 PCF的最左归约 公理 M  N是归约公理 M  N 子项规则 M left N nat和bool N是范式
3.6 各种归约策略 PCF的最左归约 公理 M  N是归约公理 子项规则 nat和bool N是范式 M  N M left N M left M M + N left M + N M left M N + M left N + M 83

84 3.6 各种归约策略 M left M Eq? M N left Eq? M N N是范式 M left M
3.6 各种归约策略 N是范式 M left M Eq? M N left Eq? M N M left M Eq? N M left Eq? N M 84

85 3.6 各种归约策略 M left M if M then N else P left if M then N else P
3.6 各种归约策略 M是范式 M,N是范式 M left M if M then N else P left if M then N else P N left N if M then N else P left if M then N else P P left P if M then N else P left if M then N else P 85

86 3.6 各种归约策略 序对 M left M M, N left M, N M是范式 N left N
3.6 各种归约策略 序对 M是范式 M left M M, N left M, N N left N M, N left M, N M left M Proji M left Proji M 86

87 3.6 各种归约策略 x : . M left x : . M 函数 M left M M N left M N
3.6 各种归约策略 函数 M是范式 M left M M N left M N N left N M N left M N M left M x : . M left x : . M 87

88 3.6 各种归约策略 命题3.25 命题3.26 令M是任意类型的PCF项，则对任何范式N，M left N当且仅当M  N
3.6 各种归约策略 命题3.25 令M是任意类型的PCF项，则对任何范式N，M left N当且仅当M  N 命题3.26 令M是任意类型的PCF项，则evelleft(M)=N当且仅当M  N并且N是范式 若仅要求这两个命题对PCF程序成立，则可以采用惰性归约 在实际实现中惰性归约比最左归约用得更普遍 88

89 3.6 各种归约策略 PCF的惰性归约 nat和bool n是数码 公理 M  N是归约公理 M  N 子项规则 M lazy N
3.6 各种归约策略 PCF的惰性归约 公理 M  N是归约公理 子项规则 nat和bool n是数码 M  N M lazy N M  lazy M M + N  lazy M + N M  lazy M n + M  lazy n + M 89

90 3.6 各种归约策略 M lazy M Eq? M N lazy Eq? M N n是数码 M lazy M
3.6 各种归约策略 n是数码 M lazy M Eq? M N lazy Eq? M N M lazy M Eq? n M lazy Eq? n M 90

91 3.6 各种归约策略 M lazy M if M then N else P lazy if M then N else P
3.6 各种归约策略 下面两条规则不再需要 M是范式 M, N是范式 M lazy M if M then N else P lazy if M then N else P N left N if M then N else P left if M then N else P P left P if M then N else P left if M then N else P 91

92 3.6 各种归约策略 二元组 前两条规则不再需要 M是范式 M left M M, N left M, N
3.6 各种归约策略 二元组 前两条规则不再需要 M是范式 M left M M, N left M, N N left N M, N left M, N M lazy M Proji M lazy Proji M 92

93 3.6 各种归约策略 x : . M left x : . M 函数 M lazy M M N lazy M N
3.6 各种归约策略 函数 下面两条规则不再需要 M是范式 M lazy M M N lazy M N N left N M N left M N M left M x : . M left x : . M 93

94 3.6 各种归约策略 命题3.27 推论3.28 比较 若M 是PCF闭项，但它不是x:.M1或M1, M2
3.6 各种归约策略 命题3.27 若M 是PCF闭项，但它不是x:.M1或M1, M2 的形式，则对任何项N，M lazy N当且仅当M left N 推论3.28 如果P是PCF程序，R是结果，那么P lazy R当且仅当P left R 比较 和最左归约相比，因惰性归约的规则集小一些，因此有可能得到一个效率相对较高的实现 94

95 3.6 各种归约策略 3.6.3 并行归约 并行归约的特点 对PCF来说，当能独立地归约两个子表达式中的 任意一个时，就应该可以同时归约它们
3.6 各种归约策略 3.6.3 并行归约 对PCF来说，当能独立地归约两个子表达式中的 任意一个时，就应该可以同时归约它们 并行归约的特点 在PCF中，M  N当且仅当M  N 并行归约可以较快到达范式 M  N M  N M1  N1, …, Mk  Nk C[M1, …, Mk]  C[N1, …, Nk] 95

96 3.6 各种归约策略 3.6.3 急切归约 最左归约和急切归约 最左归约和PCF的公理语义一致，并且允许不确定地或并行地实现
3.6 各种归约策略 3.6.3 急切归约 最左归约和急切归约 最左归约和PCF的公理语义一致，并且允许不确定地或并行地实现 更常用的次序是急切归约，它和PCF的公理语义不一致 下面的表达式在最左归约下终止，但在急切归约下不终止 let f(x : nat) : nat = 5 in letrec g(x : nat) : nat = g(x + x) in f(g 3) 96

97 3.6 各种归约策略 值 急切归约与其它归约策略的主要区别 指不能再进行急切归约的项，即已完全计算的项
3.6 各种归约策略 值 指不能再进行急切归约的项，即已完全计算的项 常量、变量和抽象都是值，值的序对也是值 序对中至少有一元不是值，以及函数应用都不能称为值 急切归约与其它归约策略的主要区别 只有当函数变元是值时才能使用 归约，只有当序对的两个元素都是值时才能使用Proji归约 97

98 3.6 各种归约策略 PCF的急切归约 值 若V是常量、变量、抽象或值的二元组，则V是一个值 公理
3.6 各种归约策略 PCF的急切归约 值 若V是常量、变量、抽象或值的二元组，则V是一个值 公理 (x : .M)V eager VxM V是值 Proji(V1,V2) eager Vi V1, V2是值 0 + 0 eager 0, eager 1, …, eager 8,… Eq? n n eager true, Eq? n m eager false 98

99 3.6 各种归约策略 if true then M else N eager M
3.6 各种归约策略 if true then M else N eager M if false then M else N eager N x : .M = y : .yxM，y在M中不是自由的 子项规则 nat n是数码 M eager M M + N eager M + N M eager M n + M eager n + M 99

100 if M then N else P eager if M then N else P
3.6 各种归约策略 bool n是数码 M eager M Eq? M N eager Eq? M N M left M Eq? n M left Eq? n M M eager M if M then N else P eager if M then N else P 100

101 3.6 各种归约策略 序对 M eager M M, N eager M, N V是值 N eager N
3.6 各种归约策略 序对 V是值 M eager M M, N eager M, N N eager N V, N eager V, N M eager M Proji M eager Proji M 101

102 3.6 各种归约策略 x : . M left x : . M 函数 M eager M M N eager M N
3.6 各种归约策略 函数 V是值 下面一条规则不再需要 M eager M M N eager M N N eager N V N eager V N M left M x : . M left x : . M 102

103 3.6 各种归约策略 在实际中用急切计算而不用最左计算的原因
3.6 各种归约策略 在实际中用急切计算而不用最左计算的原因 最左归约的实现通常是低效的。当像fx这样的变元传给函数g时（g(fx)），必须传递f 的代码的指针并记住适当的词法环境 最左归约和赋值的组合令人混淆，副作用的出现使得最左计算与不确定计算和并行计算不一致 103

104 习 题 第一次：3.3(a)，3.6(b)， 3.9(a) 第二次：3.12，3.14(a)，3.21
习 题 第一次：3.3(a)，3.6(b)， 3.9(a) 第二次：3.12，3.14(a)，3.21 第三次：3.22，3.23，3.24，3.27(a)(b)，3.28 104