形式语义教材-Ch1 基本理论.doc

-1- 第一章理论基础§ 引言 1941 年 Church 创建了 Lambda 演算理论。它是一个形式系统, 可作为计算模型,如同 Turing 机可作为计算模型一样。 Lambda 演算形式系统主要由两部分组成: 其一是合法表达式的形式系统, 其二是变换规则的形式系统. Lambda 演算系统可有多种。其主要区别在于构成 Lambda 演算形式系统的两个组成部分的具体定义上。不同的 Lambda 演算系统会得到一些不同的定理。 Lambda 演算系统如同 Turing 机系统一样, 可描述任何一部分递归函数的计算过程。因此,Lambda 演算系统也可视为一种算法语言系统。其中的 Lambda 表达式相当于语言的一个程序。程序如何执行,由 Lambda 演算系统的机制来确定。 Lambda 演算理论是函数式语言的基础, 也是指称语义学的理论基础。§ Lambda 演算纯 Lambda 表达式( 以后简称λ表达式) 是最小的一种表达式, 主要由变量名和抽象符号λ以及括号等符号构成。若用 X 表示变量,用 Exp 表示纯 Lambda 表达式之集,则 Ex p 集的定义如下。■定义 . λ表达式(1) x∈ Exp, 其中 x 是变量名。(2) 若 E1 ∈ Exp, E2 ∈ Exp, 则 E1 E2 ∈ Exp 。(3) 若E∈ Exp, x 是变量,则? ∈ Exp 。(4) 若E∈ Exp, 则(E)∈ Exp 。若用 BNF 表示法, 则可描述如下(x∈ Var, E∈ Exp ): E ::= x| E1 E2 |? |(E) 从上述定义可知纯?_ 表达式是非常小的表达式, 以致于不能再小。但它将成为?_演算系统的基础。那么一个作为计算模型的形式系统应具备什么样的条件呢? 很显然它起码应具备二个条件: 其一是它有很强的功能, 以致于能够描述复杂的计算过程; 其二是它应-2- 非常小, 以致于其语义是非常清楚的。当然实用性的系统, 则应根据需求扩充相应的内容, 但其前提是它们可变换为纯?_ 表达式的形式。在我们这里 Lambda 演算系统主要是作为函数式语言和指称语义描述语言的基础。设L 为被描述的语言,L0 为描述 L 语义的语言, 则我们称 L0 为元语言。显然, 元语言不能是很复杂的, 否则又可提出 L0 语言的语义是什么? 因此, 元语言的基础应非常简单。而所使用的实际元语言则应从简单语言逐步扩充而来, 而且其语义是很清楚的。在我们的?_ 表达式中没有常量部分, 而且变量是广义的, 即它代表的也可以是一函数。称形如(E1E2) 的表达式为施用型表达式, 称形如?x .E 的表达式为抽象型表达式。表达式(E1E2) 相当于通常的函数调用 f(E), 其中 f 是函数名。现在不一样的是 E1 不一定是一个函数名, 可以是复杂的表达式, 但必须是抽象表达式或代表函数的变量名,如(? (X))(( ? )20 ), 其中有三个施用型子表达式; ▲(? )20 ▲ f(X) ▲(? (X))( (? )20 ) 抽象表达式主要是用来表示无名函数。通常的方法是首先定义函数名, 然后再使用它, 因此函数都有名, 而抽象表达式则表示一无名函数。假设有函数说明 func f(X)=X+1, 则显然也可把上述函数的定义写成:f= ? +1, 并且也能方便地表示哪个是函数名, 哪个是形参名, 哪部分是函数体, 其中?表示其后的变量为形参变量。这种说明是定义了一个函数名 f 。如果不想定义函数名, 那么应该怎么办? 这好办, 只要直接用表达式? +1 即可了。这就是抽象表达式的直接出因。我们称? 中的 E 表达式为上述抽象表达式的体部分。为了简单起见, 以后将(XY) 简写成 XY 。严格说的话, 不能写成 XY 形式, 因为这种写法, 使实现系统将无法识别 XY 是一个标识符还是两个标识符。但如果假设变量名均由一个字母组成, 则写成 XY 形式也能够分辨出来是 X和Y 的两个名字。因此我们以后在一般情况下将写成 XY 的形式。■定义 . ( 记法约定) (1) E1 E2 E3...En 〓(((E1 E2)E3)...)En ( 左结合规则) (2) ? x1... ?. 〓? x1.(...( ? )...)) (3) ? x1 x2... 〓? x1. ? x2.... ?. (4) ? x1... ?. E2...En 〓? x1... ?.xn.(E1 E2...En) 例 . 下面是一些简单的?_ 表达式例:? x.? (? )y ? ? x