程序设计语言理论课件

程序设计语言理论

第1章引言

本章介绍一个非常简单的，以自然数和布尔值作为基本类型的，基于类型化

演算的语言，介绍该语言的语法、操作语义和它在程序设计中的能力主要议题如下：

表示法和

演算系统概述类型和类型系统的扼要讨论基于表达式的归纳、基于证明的归纳和良基归纳1.1基本概念1.1.1模型语言对程序设计语言进行数学分析通常是从设计模型语言开始 突出感兴趣的程序构造，忽略一些无关的细节程序设计语言形式化为两部分能抓住该语言本质机制的一个非常小的核心演算：

演算理解导出部分：通过把它们翻译成核心演算用类型化

演算的框架来研究程序设计语言的各种概念1.1基本概念1.1.2

表示法

表示法的主要特征

抽象：用于定义函数

应用：使用定义的函数例（自然数类型上的几个例子）恒等函数：x:nat.x (Id(x:nat)=x)后继函数：

x:nat.x

1常函数：

x:nat.10

x:nat.x

true不是合式表达式

表示法写出的表达式叫做

表达式或

项1.1基本概念

项

x:

.M和谓词演算公式

x:A.

是一个约束算子x是一个占位符，约束变元，可以重新命名约束变元而不改变表达式的含义在x:

.x

+

y中，x的出现是约束的，y的出现是自由的不含自由变元的表达式称为闭表达式用项的并置来表示函数应用(

x:nat.x)5(

x:nat.x)5

51.1基本概念一个例子(x.(y.z.(x+y)+z)3)45=(x.z.(x+3)+z)45=(z.(4+3)+z)5=(4+3)+5=121.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

1.2等式、归约和语义

表示法是演算的一部分，

演算是关于

表达式的一个推理系统除了语法外，这个形式系统有三个主要部分公理语义：推导表达式之间等式的一个形式系统操作语义：基于一个方向的等式推理（归约、符号计算） 两者都称为证明系统指称语义：形式系统的模型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

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

M1=M2,N1=N2M1N1=M2N21.2等式、归约和语义1.2.2

操作语义语言的操作语义可用不同的方式给出定义一个抽象机,通过一系列的机器状态变换来计算程序演绎出最终结果的证明系统前面所列的等式公理的单向形式给出了归约规则最核心的归约规则是(

)的单向形式 (x:

.M)N

[N/x]M通常没有

归约规则

x:

.M

y:

.

y

x

M1.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

表达式上的归纳表达式文法

e::=0|1|v|e+e|e

e表达式都有一棵分析树如果P是表达式的性质，Q是自然数的性质Q(n)

=def

树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归纳法BAn---A1证明树示意图证明上的结构归纳对该证明系统中的每个公理，证明P成立假定对证明

1,…,

k，P成立，证明P(

)也为真。

是这样的证明，它结束于用一个推理规则，并且是从证明

1,…,

k延伸出来的一个证明1.4归纳法1.4.3良基归纳集合A的良基关系是A上的一个二元关系

，它具有这样的性质：A上不存在无穷递减序列a0

a1

a2

…例：在自然数上，如果j

i+1，则i

j，则这个关系是一个良基关系良基关系的一些特点良基关系不一定有传递性良基关系都是非自反的，即对任何a

A，a

a不成立；否则会出现无穷递减序列a

a

a

…1.4归纳法引理1.1

如果

是集合A上的二元关系，那么

是良基的当且仅当A的每个非空子集都有一个极小元证明

令B

A是任意非空子集。用反证法证明B有极小元如果B无极小元，那么对每个a

B，可以找到某个a

B使得a

a。这样,可以从任意的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)为真证明如果存在某个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)为真（即：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)为真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

的子表达式基于证明的归纳

，如果

是证明

的最后一步推导规则的某个前提的证明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,

…,mliffk<l或者k

l并且存在一个

i

k，使得对所有的

j<i有

nj

mj

并且ni

<mi2.1引言主要议题如下通过例子来介绍类型化

演算及相关语言的语法和语义用不动点算子来处理函数的递归定义讨论PCF的公理语义、操作语义和指称语义一些基本的编程方法都可以用PCF来实现用操作语义来研究PCF的表达能力和局限介绍PCF的一些扩充和衍生2.2语法2.2.1

概述由列出PCF的类型来概括其构造基本类型：nat和bool类型构造符笛卡儿积

函数类型

规定：

右结合，

的优先级高于

等同于

(

)

等同于(

)

2.2语法2.2.2

布尔值和自然数布尔类型常量：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?50false

2.2语法例:if

bool_exp

then

x:nat.Melse

x:nat.N

_exp

::=…|if

bool_exp

then

_exp

else

_exp

尚未列出PCF自然数类型表达式和布尔类型表达式的所有可能形式2.2语法自然数类型和布尔类型的等式公理0+0=0,0+1

1,…,1+0=1,1+1=2,…与条件表达式有关的公理模式iftruethenMelseN=MiffalsethenMelseN=N

相等测试也有无数个公理，其形式如下：对任意数码n，Eq?nn=true对任意不相同数码m,n，Eq?mn=false没有等式公理Eq?MM=true2.2语法操作语义由一组归约公理来定义，把每个等式公理自左向右定向可得到对应的归约公理，归约公理通常用对表达式求值可归约式：匹配一个归约公理左部的项例： ifEq?(6+6)7

then(2+2)else36

ifEq?127

then(2+2)else36

iffalsethen(2+2)else36

362.2语法2.2.3配对和函数有序对（也称二元组）,笛卡儿积类型

M,N

:

射影操作

Proj1:

和Proj2:

等式公理Proj1

M,N=M和Proj2

M,N=N (proj)

(Proj1P),(Proj2P)=P (满射配对，sp)2.2语法满射配对对显式二元组是多余的 (Proj1

M,N),(Proj2

M,N) =M,(Proj2

M,N) =M,N

但是没有这个公理不可能证明 (Proj1x),(Proj2x)=x

2.2语法二元组的归约规则可以通过将proj公理从左到右定向得到没有sp归约规则它不是非要不可当和函数的递归定义合在一起时，该规则会导致合流性的失败2.2语法函数PCF函数由抽象表示任何PCF类型都可以作为PCF函数的论域或值域例comp=def

f:nat

nat.g:nat

nat.x:nat.f(gx)add=def

p:nat

nat.(Proj1

p)+(Proj2

p)2.2语法类型化

表达式的代换的精确定义[N/x]x=N[N/x]

=

，对

x的变量和常量[N/x](PQ)=([N/x]P)([N/x]Q)[N/x]x:

.M=x:

.M[N/x]y:

.M=y:

.[N/x]M，只要x

y并且y

FV(N)[N/x]y:

.M=(z:

.[N/x][z/y]M)，其中z

FV(M

N)并且y,z

x加上加法和条件算符等后，代换可拓广 [N/x](P+Q)=([N/x]P)+([N/x]Q)2.2语法函数的等式公理

x:

.M=

y:

.[y/x]M，y在M中不是自由的 (

)(x:

.M)N=[N/x]M (

)

x:

.Mx=M，x

在M中不是自由的(

)

公理对显式函数表达式也是冗余的如果M有y:

.P的形式，并且x

在M中不是自由的，可以用

公理证明

x:

.Mx=M如果M是函数类型的变量，没有

公理不可能证明x:.Mx=M2.2语法函数的归约公理仅把

公理定向为从左到右的归约规则

归约用于

演算的许多版本中2.2语法curry算子将多元函数变换成高阶函数Curry=def

f:nat

nat

nat.x:nat.y:nat.f

x,y

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+y2.2语法2.2.4声明和语法美化

演算可作为程序设计的一种模型语言 beginfunctionf(x:nat):nat; returnx; end;

body

end对应的

表达式 (

f:nat

nat.

body)(x:nat.x)2.2语法let声明

let

x:

=MinN在声明体N中，x被约束到M把let看成一种缩写，或者称为“语法美化”

可以在PCF表达式中使用let，但又不把它看成PCF真正语法的一部分let

x:

=MinN=def

(x:

.N)M不需要规定任何有关let的额外的等式公理和归约规则2.2语法例：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

composehh5翻译成纯PCF表达式：(compose:(nat

nat) (nat

nat)nat

nat. (h:nat

nat.composehh5)x:nat.x+x)

f:nat

nat.g:nat

nat.x:nat.f(gx)2.2语法(compose:(nat

nat) (nat

nat)nat

nat. (h:nat

nat.composehh5)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))hh5)(

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) 202.2语法另一种语法扩充let

f(x:

):

=M

in

N=def

let

f:

=x:

.Min

N

2.2语法2.2.5

递归函数和不动点算子 将递归函数定义看成let和一种新的基本函数的组合递归使得表达式可能没有范式选择哪个归约成为一件重要的事，因为有的选择会导致归约不终止递归函数的声明

letrec

f:

=M

in

N例：letrec

f:nat

nat=y

:nat.(ifEq?y0then1elsey

f(y–1))inf5(阶乘函数)2.2语法把整个等式看成一个关于f的方程

f:nat

nat=

y

:nat.ifEq?y0then1elsey

f(y–1)让表达式中f5中的f指称该方程的一个解把求解递归定义的等式转化为求高阶函数的不动点2.2语法如果F:

是某类型

到它自己的函数，那么F的不动点是使得F(x)=x的值x:

自然数上平方函数的不动点有0和1恒等函数有无数个不动点后继函数没有不动点

阶乘函数是方程(f:nat

nat=

y

:nat.ifEq?y0then1elsey

f(y–1))的解阶乘函数是F=def

f:nat

nat.y

:nat.ifEq?y0then1elsey

f(y–1)的不动点2.2语法不动点算子fix

:(

)

, 对每个类型

函数fix

为

到

的函数产生一个不动点把letrec看成是let和不动点算子组合的美化

letrec

f

:

M

in

N

=def

letf

:

=(fix

f:

.M)in

Nfix

:(

)

的等式公理fix

=f:

.f(fix

f) (fix)fix

M

M(fix

M) （使用(

)可得）(fix)归约规则fix

f:

.f(fix

f)2.2语法继续阶乘函数的例子F=def

f:nat

nat.y

:nat.ifEq?y0then1elsey

f(y–1)fact=deffixnatnatFfactn(fix

F)n

F(fix

F)n (f:nat

nat.y

:nat.ifEq?y0then1 elsey

f(y–1))(fix

F)n ifEq?n0then1elsen(fix

F)(n-1)对任何自然数n，最终得到factn=n!2.3

程序和语义2.3.1程序和结果PCF语言有两个语法范畴：类型和项可观测的类型：自然数类型和布尔类型像nat

nat这样的函数类型不是可观测的类型程序：PCF语言中合式的、可观测类型的闭项进一步限制：“不需要加输入和输出的程序”结果：计算或执行程序的可观测的效果（可观测类型的闭范式）语言语义的一般定义：程序集合和结果集合之间的一种关系2.3

程序和语义2.3.2

公理语义公理语义是一个证明系统，用它可以推导程序及其组成部分的性质这些性质可以用等式表示、用给定输入下的输出断言表示、或用其它形式表示注意力放在等式公理语义上两个程序在一个公理语义中等价，只要为它们推导出来的断言正好完全相同2.3

程序和语义公理自反(ref) M=M基本类型nat和bool(add) 0+0=0,0+1=1,…,3+5=8,…(Eq?) Eq?nn=true,Eq?nm=false

（n和m是不同的数码）(cond) iftruethenMelseN=M, iffalsethenMelseN=N二元组(proj) Proj1

M,N=MProj2

M,N=N(sp) Proj1

P,Proj2P=P重新命名约束变量 (

) x:

.M=y:

.y

x

M，y在M中不是自由的2.3

程序和语义公理函数(

) (x:

.M)N=N/x

M(

) x:

.Mx=M，x在M中不是自由的递归(fix) fix

=

f:

.f(fix

f)2.3

程序和语义推理规则等价(sym),(trans)同余nat和boolM=NN=MM=N,N=PM=PM=N,P=QM+P=N+QM=N,P=QEQ?MP=EQ?NQM1=M2,N1=N2,P1=P2ifM1thenN1elseP1=ifM2thenN2elseP22.3

程序和语义二元组函数M=NProjiM=ProjiNM=N,P=Q

M,P

=

N,Q

M=Nx:.M=x:.NM=N,P=QMP=NQ2.3

程序和语义除了

抽象和

应用外，其它同余规则都是多余的例：针对+的同余规则是多余的假定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

2.3

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

程序和语义2.3.3

指称语义概述PCF的指称语义，以便三种语义形式可以比较为每个类型选择一个值集来给出项的指称nat的语义论域是自然数值集N

{

nat}letrec

f(x:nat):nat=f(x+1)

inf(0)计算不终止

bool的语义论域是布尔值集B

{

nat}nat和bool类型的任何项指派相应语义论域上的一个值，也称为它们的语义解释2.3

程序和语义积类型

的数学值是有序对集合函数类型

的数学值是从

到

的函数集合如果

=

，那么函数有不动点约定：对任何n

N，用⌈n⌉表示其数码

例：

x:nat.M 如果对任何自然数n

N,都有 [⌈n⌉

/x]M

⌈f(n)⌉那么

x:nat.M的指称就是数值函数f:N

N2.3

程序和语义环境

是指从变量到值的映射若x:

,

(x)是类型

的值集上的元素通过归纳可以定义表达式M在环境

中的含义〖M〗

〖x〗

是变量x在环境

中的值函数应用〖MN〗

的含义是通过把M指称的函数〖M〗

应用到N指称的变元〖N〗

来获得其它情况可类似地定义2.3

程序和语义指称语义是可合成的，即任何表达式的含义由它子表达式的含义决定如果〖B〗

是true， 那么〖ifBthenMelseN〗

=〖M〗

如果〖B〗

是false， 那么〖ifBthenMelseN〗

=〖N〗

否则，〖ifBthenMelseN〗

=

如果B

，M

和N

同B，M和N分别有同样的指称，那么〖ifB

thenM

elseN

〗

=〖ifBthenMelseN〗

2.3

程序和语义2.3.4操作语义eval(M)=N当且仅当经若干步（含零步）归约，M可以归约到范式N类型nat和bool(add) 0+0

0,0+1

1,…, 3+5

8,…(Eq?) Eq?nn

true,Eq?nm

false

n和m是不同的数码(cond) iftruethenMelseN

M iffalsethenMelseN

N2.3

程序和语义二元组(proj) Proj1

M,N

MProj2

M,N

N重新命名约束变量(

)

x:

.M=

y:

.

y

x

M

y在M中不是自由的函数(

) (

x:

.M)N

N/x

M递归(fix) fix

f:

.f(fix

f)2.3

程序和语义这个操作语义并没有指定计算步骤，因而显得抽象一些保留了重新命名约束变量的等式公理的形式对于二元组的满射配对公理(sp)和函数的外延公理(

)，没有相应的归约规则2.3

程序和语义2.3.5由各种形式的语义定义的等价关系各种等价关系公理等价：M=N是可证明的 用M=ax

N表示指称等价：M和N对自由变量的任何取值都有相同的指称 用M=denN表示操作等价：eval(M)≃eval(N)（程序M和N求值的结果一样，或者求值结果都没有定义

）

用M=opN表示2.3

程序和语义操作等价M=opN可以从程序推广到一般项上下文C[]是一个项，但其中有一个洞例：C0[]=def

x:nat.x+[]例：C0[x]是

x:nat.x+x项M和N操作等价：

如果对任意使得C[M]和C[N]都是程序的上下文C[]，都有eval(C[M])≃eval(C[N])2.3

程序和语义等式证明系统的可靠性： 如果在公理语义中能证明M和N相等，那么在指称语义中，M和N应该有同样的含义=ax

=den这是判断公理系统正确性的基本标准对PCF语言而言，公理语义对指称语义是可靠的2.3

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

程序和语义对PCF语言的程序而言，要满足的最小要求是(

programs

M)(

results

N)M=ax

NiffM=den

NiffM=op

N对任意的项，希望满足的要求是=ax

=den

=op操作等价是三者中最粗糙的一个，和指称等价或可证明的等价相比，可能有更多的项操作等价若=op

=ax，可能会出现不一致的证明系统2.4归约和符号解释器本节讨论基于操作语义的PCF程序的执行已经讨论的操作语义是不确定的符号解释器本节讨论其它形式的符号解释器确定的：急切归约、最左归约、惰性归约并行归约2.4归约和符号解释器2.4.1

归约的合流性每当M

N1

并且M

N2，那么存在项P，使得N1

P

并且N2

P

PCF归约是合流的合流性也叫做Church-Rosser性质MN2N1P2.4归约和符号解释器如果

由一组等式公理定向来确定如果M

N，那么可以证明等式M=N从M

N和P

N，可以证明M

P合流隐含着，一个等式是可证明的当且仅当它的两个项都可以归约到一个公共项如果两个不同的项都不能归约，那么不可能证明它们相等2.4归约和符号解释器例：letrec

f(x:nat):nat=ifEq?x0then0elsex+f(x-1)in

f2F=def

f:nat

nat.

x:nat.ifEq?x0then0elsex+f(x-1)(fixF)2

(

f:nat

nat.

x:nat.ifEq?x0 then0elsex+f(x-1))(fixF)2

ifEq?2

0then0else2

+(fixF)1

2+ifEq?1

0then0else1+(fixF)0

2+1+(fixF)0

2+1+0

32.4归约和符号解释器例：这种形式的程序执行和大家熟悉的方式略有点区别let

f(x:nat):nat=5in

letrec

g(x:nat):nat=g(x+x)in

f(g3)在大多数程序设计语言中，该程序不会终止

2.4归约和符号解释器2.4.2归约策略归约策略：项到项的部分函数F，如果F(M)=N，那么M

N

与归约策略F对应的部分计算函数evalF:PCF

PCF是：evalF

(M)= ifF(M)isnotdefinedthenM elseifF(M)=MandevalF

(M

)=NthenNevalF在数学上等价于遵循策略F逐步进行归约，直到该策略不能再遵循为止2.4归约和符号解释器感兴趣的是一步归约策略只要有可能便选择一步归约的策略程序M的计算eval(M)是M的范式或者eval(M)没有定义基于项本身的形式来选择一步归约先“优化”函数

x:

.M

最左归约（惰性归约）急切归约(

x:

.M)N(

x:

.M)N

(

x:

.M

)N[N/x]M2.4归约和符号解释器2.4.3最左归约和惰性归约最左归约：对项中尽可能左边的符号进行归约遵循的是结构化操作语义的风格每条规则正好作用到一种形式的项考察项的结构就知道该用哪条规则2.4归约和符号解释器例((

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

16+5

left

212.4归约和符号解释器例(

x:nat.

y:nat.x+y)((

z:nat.z)20)

left

y:nat.((

z:nat.z)20)+y

left

y:nat.20+y2.4归约和符号解释器PCF的最左归约公理 M

N是归约公理子项规则nat和bool N是范式

M

leftM

M+N

leftM

+NM

NM

leftNM

leftM

N+M

leftN

+

M

2.4归约和符号解释器

N是范式M

leftM

Eq?MN

leftEq?

M

NM

leftM

Eq?NM

leftEq?N

M

2.4归约和符号解释器

M是范式 M,N是范式M

leftM

ifMthenNelseP

leftifM

thenNelsePN

leftN

ifMthenNelseP

leftifMthenN

elsePP

leftP

ifMthenNelseP

leftifMthenNelseP

2.4归约和符号解释器二元组

M是范式M

leftM

M,N

left

M

,N

N

leftN

M,N

left

M,N

M

leftM

Proji

M

leftProji

M

2.4归约和符号解释器函数

M是范式M

leftM

MN

left

M

NN

leftN

MN

leftMN

M

leftM

x:.

M

left

x:.

M

2.4归约和符号解释器命题

令M是任意类型的PCF项。那么对任何范式N，M

left

N当且仅当M

N命题令M是任意类型的PCF项。那么evelleft(M)=N当且仅当M

N并且N是范式如果仅要求这两个命题对PCF程序（而不是所有的项）成立，可以采用惰性归约不能再进行惰性归约的项叫做惰性范式。nat和bool的惰性范式正是它们的范式

在实际实现中惰性归约比最左归约用得更普遍2.4归约和符号解释器PCF的惰性归约公理 M

N是归约公理子项规则nat和bool n是数码M

lazyM

M+N

lazyM

+NM

NM

lazyNM

lazyM

n+M

lazyn

+

M

2.4归约和符号解释器

n是数码M

lazyM

Eq?MN

lazyEq?

M

NM

lazyM

Eq?nM

lazyEq?n

M

2.4归约和符号解释器下面两条规则不再需要

M是范式 M,N是范式M

lazyM

ifMthenNelseP

lazyifM

thenNelsePN

leftN

ifMthenNelseP

leftifMthenN

elsePP

leftP

ifMthenNelseP

leftifMthenNelseP

2.4归约和符号解释器二元组前两条规则不再需要

M是范式M

leftM

M,N

left

M

,N

N

leftN

M,N

left

M,N

M

lazyM

Proji

M

lazyProji

M

2.4归约和符号解释器函数下面两条规则不再需要

M是范式M

lazyM

MN

lazy

M

NN

leftN

MN

leftMN

M

leftM

x:.

M

left

x:.

M

2.4归约和符号解释器命题如果M

是PCF闭项，但它不是

x:

.M1或

M1,M2

的形式，那么对任何项N，M

lazy

N当且仅当M

left

N

推论

如果P是PCF程序，R是结果，那么P

lazy

R当且仅当P

left

R和最左归约相比，由于惰性归约的规则集合小一些，因此有可能得到一个效率相对较高的实现2.4归约和符号解释器2.4.4并行归约对PCF来说，当能独立地归约两个子表达式中的任意一个时，就应该可以同时归约它们MNM

NM1

N1,…,Mk

Nk

C[M1,…,Mk]

C[N1,…,Nk]2.4归约和符号解释器并行归约的特点在PCF中，M

N当且仅当M

N并行归约可以较快到达范式2.4归约和符号解释器2.4.5急切归约最左归约和PCF的公理语义一致，并且允许不确定地或并行地实现更通常的次序是急切归约，它和PCF的公理语义不一致let

f(x:nat):nat=5in

letrec

g(x:nat):nat=g(x+x)in

f(g3)2.4归约和符号解释器值：指不能再进行急切归约的项，即已经完全计算了的项常量、变量和

抽象都是值，值的二元组也是值二元组中至少有一元不是值的情况，还有函数应用都不能称为值急切归约与其它归约策略的主要区别只有当函数变元是值时才能使用

归约，只有当二元组的两个元素都是值时才能使用Proji归约fix归约也不同，它会暂停fix作用于其变元的归约2.4归约和符号解释器值如果V是常量、变量、

抽象或值的二元组，那么V是一个值delay

M

=def

x:

.Mx

x在M:

中不是自由的公理(

x:

.M)V

eager

V

x

M

V是值Proji(V1,V2)

eager

Vi

V1,V2是值fix

V

eager

V(delay

fix

V

) V是值

2.4归约和符号解释器0+0

eager0,0+1

eager1,…,3+5

eager8,…

Eq?nn

eager

true,Eq?nm

eager

false n,m是不同的数码iftruethenMelseN

eager

M

iffalsethenMelseN

eager

N

x:

.M=

y:

.

y

x

M，y在M中不是自由的

2.4归约和符号解释器子项规则nat n是数码M

eagerM

M+N

eagerM

+NM

eagerM

n+M

eagern

+M

2.4归约和符号解释器

bool

n是数码M

eagerM

Eq?MN

eagerEq?

M

NM

leftM

Eq?nM

leftEq?n

M

M

eagerM

ifMthenNelseP

eagerifM

thenNelseP2.4归约和符号解释器 二元组

V是值M

eagerM

M,N

eager

M

,N

N

eagerN

V,N

eager

V,N

M

eagerM

Proji

M

eagerProji

M

2.4归约和符号解释器 函数

V是值下面一条规则不再需要M

eagerM

MN

eager

M

NN

eagerN

VN

eagerVN

M

leftM

x:.

M

left

x:.

M

2.4归约和符号解释器(fix(

x:nat

nat.

y:nat.y))((

z:nat.z+1)2)(fix(

x:nat

nat.

y:nat.y))

eager(

x:nat

nat.

y:nat.y) (delay

fix(

x:nat

nat.

y:nat.y)

)

eager

y:nat.y(

z:nat.z+1)2

eager2+1

eager3整个项变成了(

y:nat.y)3，归约到32.4归约和符号解释器急切归约会发散的例子 letf(x:nat):nat=5in letrecg(x:nat):nat=g(x+1)inf(g3)在实际中用急切计算而不是用最左计算的主要原因最左归约的实现通常是低效的。当像fx这样的变元传给函数g时（g(fx)），必须传递f

的代码的指针并记住适当的词法环境最左归约和赋值的组合令人混淆，副作用的出现使得最左计算与不确定计算和并行计算不一致

2.5程序设计实例、表达能力和局限2.5.1记录和n元组记录是多个成分的聚集，每个成分有不同的标记记录的类型写成

l1

:

1,…,lk:

k

记录写成

l1

=M1,…,lk=Mk

记录r中的成分li的选择可用加点的记号r.li来表示等式公理

l1=M1,…,lk=Mk

.li=

Mi2.5程序设计实例、表达能力和局限使用记录的优点一个方便之处是其成分次序无关紧要另一个优点是，可以选择助记忆的名字作为标记记录和记录类型可以翻译成PCF的二元组和笛卡儿积为了简化n个成分的记录到PCF的翻译，可以定义n元组作为一种语法美化2.5程序设计实例、表达能力和局限引入n元积记号

1

…

n=def

1

(

2

…(

n-1

n)…)引入n元组记号

M1,…,Mn

=def

M1,

M2,…

Mn-1,Mn

…

很容易检查，如果Mi

:

i，那么

M1,…,Mn

:

1

…

n取n元组的成分

=def

x:

1

…

n.Proj1(x)(i<n)

=def

x:

1

…

n.(x)

1

…

nProjii-1Proj2

1

…

nProjnn-1Proj22.5程序设计实例、表达能力和局限使用n元组，可以把多于两个成分的记录翻译成PCF表达式

l1

:

1

,…,lk:

k

=def

1

…

k

l1

=M1

,…,lk=Mk

=def

M1,…,Mk

M.li

=def

M例：let

r:

A:int,B:bool

=

A=5,B=false

inifr.Bthenr.Aelser.A+1 去掉记录的语法美化，得到： let

r:int

bool=

5,false

inifProj2rthenProj1

relse(Proj1

r)+1

1

…

nProji2.5程序设计实例、表达能力和局限2.5.6并行运算的不可定义性并行或计算M∨N的方式是：并行地归约M和N，如果其中一个终止且值为true，那么另一个计算流产，并返回true否则继续归约它们，希望它们都能归约到范式2.5程序设计实例、表达能力和局限并行或是不能由PCF定义的定理

不存在PCF表达式POR，它对任意的闭布尔表达式M和N有下面的行为PORMN

true， 如果M

true或N

true；PORMN

false， 如果M

false并且N

false；PORMN

没有范式 否则2.6衍生和扩充2.6.1单元类型与和类型单元类型unit：只有一个元素的类型unit类型的常量：

unit类型的等式公理：M

:unit(对任何M:unit)unit类型的归约公理：M

:unit单元类型好像没有什么意义，但是当它同和类型及其它形式的类型组合起来时，显得非常有用2.6衍生和扩充和类型

: 类型

和

的可区分的并可区分的并：例如，如果取int和int的并集，得到的仍然是int；但是，int和int的可区分的并有int的两个“拷贝”

内射函数

Inleft

,

:

Inright

,

:

分情况函数

Case

,

,

:(

+

)

(

)

(

)

2.6衍生和扩充和类型的等式公理（Case

,

,

:(

+

)

(

)

(

)

）Case

,

,

(Inleft

,

x)fg=fxCase

,

,

(Inright

,

x)fg=gx外延公理 Case

,

,

x(foInleft

,

)

(foInright

,

)=fx

其中f:(

+

)

(

+

)和类型的归约公理Case

,

,

(Inleft

,

x)fg

fxCase

,

,

(Inright

,

x)fg

gx2.6衍生和扩充单元类型与和类型加入PCF后，bool可以省略bool=def

unit+unittrue=defInleft

false=defInright

ifMthenNelseP=def

Caseunit,unit,

M(K

,unitN)(K

,unitP)

其中N,P:

并且K

,unit是

项

x:

.

y:unit.x可以检验下面两个公理 iftruethenMelseN=M iffalsethenMelseN=N2.6衍生和扩充2.6.2递归类型类型等式t=

，其中t出现在

中也可以为递归定义的类型引入不动点算子，并且用fix(

t.

)表示方程t=

的一个解用

t.

作为fix(

t.

)的语法美化在

t.

中

约束t类型表达式也可以有自由变量，这是会导致多态性（第七章介绍）没有任何项可以约束类型变量，在项中仅使用闭类型2.6衍生和扩充若把PCF中nat和bool类型删除,把单元类型、和类型及递归类型加入，PCF的类型表达式则是由文法

::=t|unit|

+

|

|

|

t.

产生的闭表达式有递归类型时，需要仔细考虑类型相等问题2.6衍生和扩充等式t=

意味着fix(

t.

)=

fix(

t.

)

t

用

记号表示为

t.

=

t.

t

对类型等式

t.

=

t.

t

有两种不同的观点等式左右两边是真正不可区分的类型等式左右两边是同构的类型

t.

t.

t

2.6衍生和扩充nat作为递归类型的定义自然数的一个显著特征是，如果加一个元素到自然数集合，所得到的集合和自然数集合同构unit

比

多一个元素，因此nat

unit+nat，即nat=def

t.unit+tnat

unit+nat

unit+(unit+nat)

…

unit+(unit+(unit+(unit+(unit+…+nat)…)))PCF表达式翻译到只含递归的类型定义、单元类型与和类型的表达式3.1引言代数数据类型包括一个或多个值集一组在这些集合上的函数基本限制是其函数不能有函数变元基本“类型”(type)符号被称为“类别”(sort)泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数据类型时的作用

3.1引言本章主要内容：代数项和它们在多类别代数中的解释等式规范（也叫代数规范）和等式证明系统等式证明系统的可靠性和完备性（公理语义和指称语义的等价）代数之间的同态关系和初始代数数据类型的代数理论从代数规范导出的重写规则（操作语义）大多数逻辑系统中一些公共的议题将被覆盖3.2

代数、基调和项3.2.1代数代数一个或多个集合，叫做载体一组特征元素和一阶函数，也叫做代数函数

f:A1

…

Ak

A例：N

N,0,1,+,

载体N是自然数集合特征元素0,1

N，也叫做零元函数函数+,

:N

N

N3.2

代数、基调和项多个载体的例子Apcf

N,B,0,1,…,+,true,false,Eq?,…

下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要定义数据类型证明性质进行化简还必须讨论这种语法描述的语义A5pcf

N5,B,0,1,2,3,4,+5,true,false,Eq?,…

3.2

代数、基调和项3.2.2

代数项的语法基调

S，F

S是一个集合，其元素叫做类别函数符号f:s1

…

sk

s的集合F，其中表达式s1

…

sk

s叫做类型