形式语义教材Ch2 函数式语言.docx

形式语义教材Ch2 函数式语言.docx

《形式语义教材Ch2 函数式语言.docx》由会员分享，可在线阅读，更多相关《形式语义教材Ch2 函数式语言.docx（37页珍藏版）》请在冰点文库上搜索。

形式语义教材Ch2函数式语言

第二章函数式语言

§2.1概述

函数式程序设计是英文FunctionalProgramming的译文。

其中扮演过重要角色的是众所周知的LISP语言。

LISP语言的长期稳定性强有力地说明了函数式语言的意义不仅在于理论上。

该语言是由McCathy于1960年设计，并在人工智能方面广泛被使用的一种语言。

此外，还有不太熟悉的，由Landin设计出来的ISWIM语言，该语言尽管不那么熟悉，但对于70年代函数式语言的设计工作起到了重要的影响。

到了70年代，在美国兴起了对LISP语言的实质性的改进工作，并在当时的大、中型计算机上高速地运行。

这时在英国，也设计出BCPL，POP-2，SASL和ML等函数式程序设计语言。

其中BCPL语言经过被称之为B的语言被发展为所谓的C语言。

POP-2是面向人工智能的一种语言，后被发展成HOPE语言。

SASL语言对于70年代末以后的语言有着重要的影响，后来被发展为KRC语言。

从70年代中期到70年末期，是函数式语言研究的高潮时期，而该高潮的最后一个精彩的工作是Backus的图灵奖受奖纪念论文（1978）。

从受奖纪念论文开始，Backus连续发表了三篇有关函数式程序设计方面的论文。

这些文章的主要思想可归纳为以下三点:

一是指明VonNeumann计算机的瓶颈问题及其消除法；二是函数级的程序设计；三是提倡带类型的计算模型。

Backus的思想充分地体现于程序设计语言FP中。

过去的语言都以变量为程序的基本对象，而函数级程序语言FP，则取消了变量。

也就是说在程序里不出现变量。

这一点一般人是难以想到的，故他的论文也无疑的为函数式程序设计注入了新的思想。

§2.2函数式语言的主要特点

函数式语言的最大特点之一是引用的透明性。

换句话说，没有函数的付作用，也就是说，对于同一实参来说，函数调用的结果是一样的。

通常的过程式语言没有引用的透明性，即用相同的实参值调用函数可能得到不同的值。

这是破坏数学性质的最主要原因。

函数式语言所以具有好的引用的透明性是由于其中的变量只能被定义一次。

在通常的过程式语言中一个变量可被反复赋值多次，因此将产生同一表达式中的不同位置上的相同变量具有不同值。

过程式语言的最大优势就在于速度快。

由于在函数式语言中变量只能被赋值一次即不能改变量的值，将出现反复拷贝大量数据的现象（从实现角度来说），故会大大降低运行速度。

目前的一些函数式语言为了能产生较好的目标代码，也不同程度地引进非函数式成分，比如众所周知的LISP和ML。

函数式语言的第二个特点是并行性好。

在过程式语言中由于有函数的付作用，不能并行地计算一个操作（包括函数名）的所有参数值。

比如假设有表达式f（x）+g（y），那么就不能并行计算f（x）和g（y）。

故顺序计算和并行计算的结果将得到不同的值。

但对于函数式语言情形来说，由于没有函数的付作用，完全可以并行地计算其两个分量的值。

从长远的角度来看，语言是否具有较好的并行性是极为重要的问题。

函数式语言的第三个特点是具有所谓的高阶值。

通常的过程式语言没有值为一个函数的变量。

也就是说函数不能作为值，而函数式语言则不同，变量的值不仅可以是简单值，也可以是复杂类型的值，甚至也可以是函数。

假设在过程式语言中有函数说明

functionf（x，y，z:

real）:

real；beginreturn（x+y+z）end

则函数调用必须具有形式f（E1,E2,E3），其结果是一个整数。

若写成f（E1,E2），那么编译系统将会指出该函数调用的实参个数不对。

但是，假设在函数式语言程序里有函数定义

fxyz=x+y+z

则在表达式中可以写f也可以写（fE1），也可以写（fE1E2），当然也可以写（fE1E2E3）。

以上四种写法都是允许的表达式。

当然，上述不同表达式所得到的值并不一样，除了最后一种情形外，其结果值都是函数。

注意上面的函数定义（称之为curry化的定义）不等价于下面的函数定义:

f（x,y,z）=x+y+z

对于这种情形来说，其调用部分还是要写成f（E1,E2,E3）形式。

函数式语言的第四个特点是延迟性问题。

这一概念是由P.Henderson在1979年提出的。

所谓延迟计算的主要意思是指:

当调用函数时，不是盲目地首先计算所有实参的值，然后再进入函数体，而是先进入函数体，然后只当需要实参值时才进行计算（并且从实现角度来看每一个实参只被计算一次）。

一个函数式语言可按延迟式的定义来实现，也可按非延迟式来实现。

引进延迟性的目的是尽可能地避免无用的计算，从而提高代码的运行速度。

函数式语言的第五个特点是模式匹配。

这些特点在过程式语言里是见不到的。

就ML语言（其版本很多）来说，一个case表达式的例（其中有模式匹配）可如下:

CASESOF

ass（V，E）:

Exp1

if（E0，E1，E2）:

Exp2

while（E0，St）:

Exp3

END

其中变量S取的值是语句的内部表示。

case表达式的":

"左部部分称之为模式。

首先S的内容与模式ass（V，E）进行匹配，如果匹配成功，则执行相应的表达式Exp1（匹配结果模式中的变量V和E将得到相应的具体值），否则再与模式if（E0，E1，E2）进行匹配，以后的过程类似。

从上可知模式匹配是一较高级别的一种非常方便的操作。

§2.3类型及其操作

在函数式语言里，最早引进类型的是HOPE和ML语言（由英国爱丁堡大学设计）。

其中的类型实际上是以Scott论域为基础，主要是增加了抽象数据类型（即引进了类型变量）。

在第一章的论域理论部分里已经介绍了Scott的论域构造符×（元组域的构造符）、+（联合域的构造符）、*（序列域的构造符）、→（函数空间的构造符）等。

当然，在具体的语言里所使用的构造符不一定都一样。

在第一章介绍了几种论域的构造法，但那时我们只注重于研究论域的一些性质，因此至今并没有真正用到这些论域本身。

在PASCAL等过程式语言里给用户提供了自己定义类型的一些机制，同样在函数式语言里也可给用户提供类型的定义机制。

比如ML语言，提供了一些类型的构造符，提供了类型的递归定义机制，还提供了抽象类型的定义机制。

关于类型的引进有以下几个要点:

尽可能在运行以前完成类型检查；用户能够方便地定义所需的新类型；提供类型抽象（数据抽象）的功能。

著名的ML函数式语言很好地做到了上述几点。

在过程式语言里经常写函数或过程说明部分，其目的是实现过程（操作）的抽象化，以达到优化程序的目的。

对于类型同样也有类型的抽象化问题。

比如整数栈和实数栈，本质上是一样的故可把它们统一为一种抽象栈。

其抽象类型的定义部分可表示为如下:

abstypestT=nil+cons（T×st）

其中st为被定义的抽象类型的名字（如同被定义的函数名一样），而T则相当于函数中的一个形参变量。

一旦T的内容被确定，就出来一个具体的类型，称这种类型为实例类型。

我们不能直接使用抽象类型，而只能使用实例类型，比如st（INT），st（BOOL）等。

类型主要用来指明变量或值的类型，具体办法是在定义性变量的出现处加上类型，下面就是一个例子:

letx:

t＝ExinEb

其中t是类型标识符。

上面表达式的let部分表示变量x的类型是t类型，并且表示如果Ex的类型不与t类型等价，则有类型不相容错误。

如果没有写":

t"部分，则x的类型规定为Ex的类型。

下面也是使用类型的例子:

■x:

t.E

■fx1:

t1x2:

t2...xn:

tn＝E

其中第一个式子中的t指定变量x（无名函数的形参变量）的类型，而第二个式子中的ti则用来指定函数f的第i个形参的类型。

下面将重点介绍最主要的几种类型。

任何语言都有系统所规定好的标准类型，函数式语言也不例外。

标准类型可有

INT，REAL，BOOL，IDE，STRING

等。

这些类型都是最熟悉的类型，因此就不再赘述。

主要是考虑复杂类型的问题。

在第一章里已经介绍过几种论域的构造方法，因此，在此不再给出详细的说明，只是把其中的重点列出来。

元组类型

[1]类型的表示:

D1×D2×...×Dn

[2]值的表示:

（d1，d2，.....，dn），di是Di类型的值

[3]取成分操作↑:

（d1，d2，.....，dn）↑i=di

[4]元组类型例:

INT×REAL

元组值例:

（3，2.5），（5，5.5）

操作例:

（3，2.5）↑1=3，（3，2.5）↑2=2.5

元组类型通常也称乘积类型或卡氏积类型。

元组类型相当于PASCAL语言中的无变体记录类型。

联合类型

通常也称为直接合类型。

联合类型对应于PASCAL语言中的变体记录类型。

联合类型的表示法通常有两种方法。

方法1:

[1]类型的表示:

D1＋D2＋...＋Dn

[2]值的表示:

（i，di），其中di是Di类型的值

[3]三种操作:

is，to，ot（操作名字不是统一的）

_isDi:

（D1+D2+...+Dn）→BOOL

_toDi:

Di→D1+D2+...+Dn

_otDi:

D1+D2+...+Dn→Di

[4]类型例:

INT+REAL

值例:

（1，20），（2，0.5）

操作例:

（1，20）isINT=true

（1，20）isREAL=false

（1，20）otINT=20

20toINT=（1，20）

[5]联合类型当于PASCAL中的只有变体的记录类型

[6]D1+D2不等价于D1∪D2

方法2:

方法1的缺点是用序号表示几种情形中的哪种情形。

显然，用起来不方便，于是出现了第二种方法。

这种方法使用称之为构造子的助记符，而不使用序号。

例如，假设值域VALU表示整数域和布尔域的联合域，则用第二种方法可写成如下:

VALU=intValu（INT）+boolValu（BOOL）

这时VALU的元素被表示成intValu（20），boolValu（false）等形式。

显然，这种表示比方法1清楚多了。

[1]类型的表示:

ctr1（D1）＋ctr2（D2）＋...＋ctrn（Dn）

其中ctri是用户写的助记符，称为构造子

[2]值的表示:

ctri（di），其中di是Di类型的值

[3]操作:

is，to，ot

[4]类型例:

intV（INT）+realV（REAL）＋boolV（BOOL）

元素例:

intV（10），realV（1.5），boolV（false）

操作例:

intV（50）isintV=tt

:

intV（50）otintV=50

:

50tointV=intV（50）

[5]特别例子:

前例中，每构造子ctr后面跟着一类型部分。

但也有这样的特殊情

形，即后面没有类型跟上。

例如

TYPE＝intT+realT+boolT

这时TYPE集的具体定义是:

{intT，realT，boolT}

序列类型

[1]类型的表示:

D*

[2]元素的表示:

[d1,....,dn]，[]，di为D类型值。

[3]序列类型可用+和×以及递归来定义（即不用构造符*）:

LS=nil+cons（D×LS）

[4]操作:

hd（取头），tl（取尾），null（测空），:

（元素加表）等

hd:

D*→D□hd[d1,...,dn]=d1，

hd[]=⊥

tl:

D*→D*□tl[d1,....,dn]=[d2,...,dn]

hd[]=[]

null:

D*→BOOL□null[]=tt，

null[d1,...,dn]=ff

cons:

D×D*→D*□cons（d0,[d1,...,dn]=[d0,d1,...,dn]

[5]也称表类型，还可设取元素，表加表，表加元素等其他操作。

[6]空表表示为[]或<>或nil。

[1]类型的表示:

D1→D2

[2]元素的表示:

f，h，x.E，其中f，h是D1到D2的函数名，而x是D1域上的变量，E是D2上的表达式。

[3]操作:

复合，更新，选择，最小不动点，.......

复合:

（fog）x=f（g（x））

更新:

f[a/x]y=（y≡x→a，f（y））

选择:

（E→f，g）

最小不动点:

fix（f）

[1]类型表示:

typerecD=TE[D]，D的递归定义式

[2]类型例:

typerecL=nil+cons（INT×L）

[3]元素例:

nil...............................<>

cons（1，nil）...................<1>

cons（1，cons（2，nil））......<1，2>

cons（cons（1，nil），2）.......错误

[1]类型表示:

absttfx1...xn=TE[x1，..xn]

[2]实例类型:

标准类型是实例类型，自定义非抽象类型是实例类型，若tf是抽象类型名，tvi是实例类型，则tftv1tv2...tvn也是实例类型。

[3]抽象类型不能直接使用，只能用实例类型。

抽象类型的具体功能就是产生实例类型。

[4]抽象类型例子:

abstListtv=nil+cons（tv×List）

[5]实例类型例子:

Listint，Listbool，List（int，bool）

作为例子考虑程序树的表示问题。

设有如下语句和表达式

S:

:

=skip|id:

=E|ifEthenS1elseS2|whileEdoS

E:

:

=N|x|E1+E2|E1×E2

并准备将它转换成树型结构。

可用下面的联合域方程来很方便地表示出来，其中ST表示语句的树表示，ET表示表达式的树表示。

:

ST=skip+ass（IDEET）+if（ETSTST）+while（ETST）

ET=num（INT）+name（IDE）+sum（ET×ET）+mul（ET×ET）

前面的论域方程实际上是定义了类型ST和类型ET。

显然，这种写法比用指针表示树的方法简单而直观得多。

假设s是ST类型的变量，e是ET类型的变量，则可用下述CASE表达式很方便地表示对于语句树的操作。

而目前的过程式语言还做不到这一点。

casestof

skip:

skip_routine

ass（name，et）:

ass_routine

if（et，st1，st2）:

if_routine

where（et，st）:

where_routine

end

§2.4程序结构

函数式语言的程序主要由两部分组成，其一是一组函数定义部分，其二是所要计算的一个表达式，称之为目标表达式。

而函数定义部分则主要由表达式部分组成，因此，函数式语言的结构及其规模实际上是取决于该语言的表达式的结构与大小。

在概述部分里已介绍过多种函数式语言，它们的结构不尽相同，因此不可能给出统一的一种结构。

本书并不想介绍某个具体的函数式语言，而是想阐述如何以λ演算为基础构造函数式语言。

换言之，我们倾向于概念而不倾向于具体。

从实际语言的角度看，我们倾向于ML语言，而不倾向于LISP，也不倾向于Backus所提出的著名的函数型程序设计语言FP。

我们所以这样做，是因为ML语言是最成功地引进类型的一种函数式语言，而且其中用到的类型正是以Scott的论域理论为基础，同时它还有递归定义类型的机制。

现在的ML语言也有很多版本，有些版本则扩充了很多非函数性的成分，比如引进引用型变量（相当于PASCAL中的变参），甚至可以把C语言的程序部分嵌入到函数式ML程序中等等。

函数式语言的程序结构可以分成上面两种形式。

第一种形式是图2.4.1（上）所示的结构，第一部分是函数定义部分，第二部分是目标表达式部分。

第二种程序结构是图2.4.1（下）所示的结构，其中程序就是一个表达式。

在这种结构中，函数都被定义在目标表达式内。

换句话说，没有全程化的函数。

§2.5表达式的结构

从上一节的讨论中，已经看到函数式语言的主要成分就是表达式，因此，读者应充分地理解这里的表达式概念。

为此，这一节将专门地讨论表达式的问题，但我们不准备马上涉及复杂的概念。

主要是给出表达式的一种定义，尽管它不久将会被扩充。

所定义的语言主要是没有复杂模式，因此，在很大一方面不能显示出函数式语言的优点。

下面定义的表达式也可看作是第一章中扩展λ演算系统的再一次扩充。

我们要考虑什么样的成分可以成为表达式。

显然，标准常量应是允许的表达式。

在复杂结构的数据中空序列nil（或表示为<>）应是允许的表达式。

因为有元组类型，也应有元组式的表达式（E1，E2，..，E），元组类型有取成分的操作，因此还应有形如E1↑E2的表达式，其中E1是其值为元组型的表达式，而E2是整型表达式。

联合类型的值具有ctr（E）形式，并且联合类型有is，to，ot等三种操作，所以表达式里应包含下面形式的表达式:

ctr（E），Eisctr，Etoctr，Eotctr

其中ctr为构造子。

当E为元组式表达式（E1，..，En）时，ctr（E）理应写成ctr（（E2，..，En））形式，但很显然，其中的里层括号可以省略，因此，将联合类型式的表达式ctr（E）索性定义为ctr（E1，E2，...，En）形式。

关于表类型（序列类型），如果都用前缀式，那么它们都归结到E1E2情形。

但有时用中缀式更简短一些，所以在语言里也保留一些中缀式的表示，如元素加表的表达式E1:

E2。

系统应有一些标准函数。

我们把表的有关操作hd，tl，null等作为标准函数，因此在表达式定义里未出现它们的名字。

为方便计，以后将常见的二元运算写成中缀形式，不写成语法里所规定的前缀形式。

有时将条件表达式写成if_then_else的形式。

读者也许很难理解只有表达式而没有其他的成分，怎么能表示过程式语言中的那么多内容。

实际上过程式语言的主要特点是有赋值语句，再是有类型说明和变量说明等部分。

这里特别要注意的是，函数式语言中表达式不是一般的表达式，而是可带说明的表达式。

因此，函数式语言中也有说明部分。

其说明部分中可定义变量，也可定义类型，也可定义函数等。

■假设有表达式（E0）×（E0）+（E0）。

其中相同的表达式E0出现了三次，因此最好加以优化。

通常的办法是引进一个临时变量X，把表达式E0的值求出来赋给X，并把原表达式中的E0改为X。

如果用函数式语言来写的话，可以写成下面形式的带变量说明的表达式:

letX=E0inX×X+X

其中letX=E0in是变量X的说明部分，它说明了变量X的类型取E0的类型，而且其值是E0的当前值。

如果想强制性的规定X的类型为整型类型，则可在X的后面加上其类型。

具体可如下:

letX:

integer=E0inX×X+X

■假设有表达式f（5）×f（10）+f（20），其中的f是计算阶乘的函数，并且想把函数f定义为局部于本表达式的函数。

这时和前面类似地可写成如下的带函数说明的表达式:

letrecf=X.（X=0→1，f（X-1）×X）inf（5）×f（10）+f（20）

其中letrec……in部分定义了函数名f，且在in后面则使用了此函数名。

在这里没给函数名f确定其类型，这时它的类型自动由其右部表达式来确定。

从该表达式可推出形参变量X的类型应是整型，进而可推出函数结果值的类型也应是整型的，从而得出结论函数名f的类型是这样一个函数类型:

integer→integer。

在上面表示中，不能把letrec（其中rec表示递归）写成let。

否则LET表达式中的f不成为所定义的f，而是成为前面被定义的f。

in后面表达式中f则不管是哪种情形，总表示当前被定义的函数名f。

在前面我们已经用到了类型概念，并且在说明变量时用到了类型名。

这就是说，程序中应有个地方能定义类型名，如同定义变量名一样。

类型定义也分为递归（typerec）和非递归（type）两种情形。

在定义类型时自然要用到类型表达式，而类型表达式部分我们已具体介绍过，因此对此不必再费笔墨，而只需研究如何用类型表达式定义类型名。

下面是定义类型名的具体例子:

typepair=INT×INTinletX:

pair=（E1.E2）

in.......................

typereclist=nil+cons（INT×list）inS:

list=[1，2，3]

和以前一样，其中的typerec不能改成type，否则要出错。

综上所述，不带模式的表达式可定义成如下:

§2.6语言的语义

程序的功能应是，在输入设备上给出输入数据，则往输出设备上输出一些结果。

为了简单起见，没有设输入/输出语句，因此，把程序体表达式（目标表达式）的计算结果作为程序的执行结果。

表达式的值可以是简单值，也可以是复杂值。

复杂值可以是下列几种值:

元组值，联合值，序列值，函数值。

标识符分为两大类:

一是形参标识符，一是临时标识符。

其中临时标识符可分为变量和类型标识符。

临时变量（函数）标识符由保留字let或letrec定义，而临时类型标识符则由type或typerec保留字来定义。

在PASCAL等过程式语言中，函数不能作为类型，因此，变量的值不可能是函数；但函数式语言有函数类型，因此变量值可以是函数。

形参标识符的作用域是整个函数体，而临时标识符的作用域是let表达式的体部分。

例如，假设有let表达式

letx:

t=ExinEb

则let变量标识符x的作用域是体表达式Eb；但如果在体里面x又被定义为临时变量，则外层x的作用域不能覆盖整个Eb。

其中的类型t部分可省略。

在函数式语言里每个变量只能被赋值一次，这是与通常的过程式语言比较最有区别的一点。

由于有这一特点，函数式语言具有所谓的引用透明性。

当然，为了适应实用性，后来在ML里也增加了所谓的引用性变量，这种变量相当于通常语言中的变量。

递归LET表达式的特点是递归定义一些变量。

比如

letrecx=y+1andy=z+1andz=10inx+y+z

用联立递归方程定义了x、y和z。

方程式右部的y都是第二个等式所定义的y；x和z也类似。

解联立方程得如下解:

x=12，y=11，z=10，而整个表达式的值则为33。

上面表达式例的特点是，前面的方程用到后面定义的变量值。

实际上该表达式可写成如下的LET表达式

letz=10andy=z+1andx=y+1inx+y+z

对于递归LET表达式，需要注意的是其中的and和一般LET表达式中的解释并不相同。

LET表达式中的and表示“letin”的缩写。

假设有递