第2章 可计算函数程序设计语言.ppt

文档介绍：第2章可计算函数程序设计语言
介绍基于类型化演算的函数式语言PCF
该语言的设计目的是便于后面各章的分析和讨论,而不是把它作为实际语言
引言
主要议题如下
通过例子来介绍类型化演算及相关语言的语法和语义
用不动点算子来处理函数的递归定义
讨论PCF的公理语义、操作语义和指称语义
一些基本的编程方法都可以用PCF来实现
用操作语义来研究PCF的表达能力和局限
介绍PCF的一些扩充和衍生
语法
概述
由列出PCF的类型来概括其构造
基本类型:nat和bool
类型构造符
笛卡儿积
函数类型
规定:右结合,的优先级高于
等同于()
等同于()
语法
布尔值和自然数
布尔类型常量: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
语法
例: if  bool_exp  then x : else x :
_exp:: = …| if bool_exp then _exp else _exp
尚未列出PCF自然数类型表达式和布尔类型表达式的所有可能形式
语法
自然数类型和布尔类型的等式公理
0 + 0 = 0, 0 + 1 1, …, 1 + 0 = 1, 1 + 1 = 2, …
与条件表达式有关的公理模式
if true then M else N = M
if false then M else N = N
相等测试也有无数个公理,其形式如下:
对任意数码n,Eq? n n = true
对任意不相同数码m,n,Eq? m n = false
没有等式公理Eq? M M = true
语法
操作语义由一组归约公理来定义,把每个等式公理自左向右定向可得到对应的归约公理,归约公理通常用对表达式求值
可归约式:匹配一个归约公理左部的项
例: if Eq? (6 +6) 7 then (2+2) else 36
 if Eq? 12 7 then (2 + 2) else 36
 if false then (2 + 2) else 36
 36
语法
配对和函数
有序对(也称二元组),笛卡儿积类型
M, N: 
射影操作
Proj1 : 和 Proj2 : 
等式公理
Proj1M, N= M 和 Proj2M, N= N (proj)
(Proj1P), (Proj2P) = P (满射配对,sp )
语法
满射配对对显式二元组是多余的
(Proj1M, N), (Proj2M, N) 
= M, (Proj2M, N) 
= M, N
但是没有这个公理不可能证明
(Proj1x), (Proj2x) = x
语法
二元组的归约规则可以通过将proj公理从左到右定向得到
没有sp归约规则
它不是非要不可
当和函数的递归定义合在一起时,该规则会导致合流性的失败