程序設(shè)計(jì)語言理論課件

程式設(shè)計(jì)語言理論

第1章引言

本章介紹一個非常簡單的，以自然數(shù)和布爾值作為基本類型的，基於類型化

演算的語言，介紹該語言的語法、操作語義和它在程式設(shè)計(jì)中的能力主要議題如下：

表示法和

演算系統(tǒng)概述類型和類型系統(tǒng)的扼要討論基於運(yùn)算式的歸納、基於證明的歸納和良基歸納1.1基本概念1.1.1模型語言對程式設(shè)計(jì)語言進(jìn)行數(shù)學(xué)分析通常是從設(shè)計(jì)模型語言開始 突出感興趣的程式構(gòu)造，忽略一些無關(guān)的細(xì)節(jié)程式設(shè)計(jì)語言形式化為兩部分能抓住該語言本質(zhì)機(jī)制的一個非常小的核心演算：

演算理解導(dǎo)出部分：通過把它們翻譯成核心演算用類型化

演算的框架來研究程式設(shè)計(jì)語言的各種概念1.1基本概念1.1.2

表示法

表示法的主要特徵

抽象：用於定義函數(shù)

應(yīng)用：使用定義的函數(shù)例（自然數(shù)類型上的幾個例子）恒等函數(shù)：x:nat.x (Id(x:nat)=x)後繼函數(shù)：

x:nat.x

1常函數(shù)：

x:nat.10

x:nat.x

true不是合式運(yùn)算式

表示法寫出的運(yùn)算式叫做

運(yùn)算式或

項(xiàng)1.1基本概念

項(xiàng)

x:

.M和謂詞演算公式

x:A.

是一個約束算子x是一個占位符，約束變元，可以重新命名約束變元而不改變運(yùn)算式的含義在x:

.x

+

y中，x的出現(xiàn)是約束的，y的出現(xiàn)是自由的不含自由變元的運(yùn)算式稱為閉運(yùn)算式用項(xiàng)的並置來表示函數(shù)應(yīng)用(

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基本概念

表示法中有兩個約定函數(shù)應(yīng)用是左結(jié)合的 MNP應(yīng)看成(MN)P每個

的約束範(fàn)圍盡可能地大，一直到運(yùn)算式的結(jié)束或碰到不能配對的右括弧為止例

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等式、歸約和語義

表示法是演算的一部分，

演算是關(guān)於

運(yùn)算式的一個推理系統(tǒng)除了語法外，這個形式系統(tǒng)有三個主要部分公理語義：推導(dǎo)運(yùn)算式之間等式的一個形式系統(tǒng)操作語義：基於一個方向的等式推理（歸約、符號計(jì)算） 兩者都稱為證明系統(tǒng)指稱語義：形式系統(tǒng)的模型1.2等式、歸約和語義1.2.1公理語義一個等式公理系統(tǒng)約束變元改名公理（公理）

x:

.M

y:

.

y

x

M，M中無自由出現(xiàn)的y

N

x

M表示M中的x用運(yùn)算式N代換的結(jié)果

例如

x:.x

y:.y函數(shù)應(yīng)用公理（

公理）(x:

.M)N[N/x]M例如(x:nat.x+4)4

[4/x](x+4)4+4

1.2等式、歸約和語義自反公理對稱性規(guī)則、傳遞性規(guī)則同餘規(guī)則相等的函數(shù)作用於相等的變元產(chǎn)生相等的結(jié)果等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論

M1=M2,N1=N2M1N1=M2N21.2等式、歸約和語義1.2.2

操作語義語言的操作語義可用不同的方式給出定義一個抽象機(jī),通過一系列的機(jī)器狀態(tài)變換來計(jì)算程式演繹出最終結(jié)果的證明系統(tǒng)前面所列的等式公理的單向形式給出了歸約規(guī)則最核心的歸約規(guī)則是(

)的單向形式 (x:

.M)N

[N/x]M通常沒有

歸約規(guī)則

x:

.M

y:

.

y

x

M1.2等式、歸約和語義1.2.3指稱語義先確定指稱物，然後給出語言成分到指稱物的語義映射，這個映射要滿足：每個成分都有對應(yīng)的指稱物複合成分的指稱只依賴於它的子成分的指稱類型化

演算的指稱語義每個類型運(yùn)算式對應(yīng)到一個集合類型

的項(xiàng)解釋為其值集上的一個元素類型

的值集是函數(shù)集合，項(xiàng)

x:

.M解釋為一個數(shù)學(xué)函數(shù)1.3類型和類型系統(tǒng)類型提供了所有可能值的全體的一種分類：一個類型是一群有某些公共性質(zhì)的值對於不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同1.3類型和類型系統(tǒng)1.3.1

類型和類型系統(tǒng)類型語言：變數(shù)都被給定類型未類型化的語言：不限制變數(shù)值的範(fàn)圍類型系統(tǒng)語言的一個組成部分由一組定型規(guī)則構(gòu)成類型系統(tǒng)的研究有兩個分支類型系統(tǒng)在程式設(shè)計(jì)語言中的應(yīng)用“純類型化

演算”和不同邏輯之間的對應(yīng)關(guān)係1.3類型和類型系統(tǒng)設(shè)計(jì)類型系統(tǒng)的目的用來證明程式不會出現(xiàn)不良行為類型可靠的語言（安全語言）所有程式運(yùn)行時都沒有不良行為出現(xiàn)類型系統(tǒng)的研究也需要形式化的方法許多語言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過類型檢查後接受的程式也會崩潰顯式類型化的語言：類型是語法的一部分隱式類型化的語言1.3類型和類型系統(tǒng)1.3.2

類型語言的優(yōu)點(diǎn)開發(fā)時的實(shí)惠可以較早發(fā)現(xiàn)錯誤類型資訊具有文檔作用（比程式注解精確，比形式規(guī)範(fàn)容易理解）編譯時的實(shí)惠程式模組可以相互獨(dú)立地編譯運(yùn)行時的實(shí)惠更有效的空間安排和訪問方式，提高了目標(biāo)代碼的運(yùn)行效率1.3類型和類型系統(tǒng)類型系統(tǒng)的其他應(yīng)用電腦和網(wǎng)路安全許多程式分析工具使用類型檢查或類型推斷演算法類型系統(tǒng)用來表示邏輯命題和證明1.4歸納法1.4.1

運(yùn)算式上的歸納運(yùn)算式文法

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

e運(yùn)算式都有一棵分析樹如果P是運(yùn)算式的性質(zhì)，Q是自然數(shù)的性質(zhì)Q(n)

=def

樹t.如果height(t)=n並且t是e的分析樹，那麼P(e)為真首先必須為高度是0的分析樹直接證明P然後，對於分析樹高度至少為1的運(yùn)算式e，假定對於分析樹高度較小的運(yùn)算式，P都為真，證明P(e)為真1.4歸納法結(jié)構(gòu)歸納（形式1）對每個原子運(yùn)算式e，證明P(e)對直接子運(yùn)算式為e1,…,ek的任何複合運(yùn)算式e，證明，如果P(ei)（i=1,…,k）都為真，那麼P(e)也為真結(jié)構(gòu)歸納（形式2）證明：對任何運(yùn)算式e，如果P(e)對e的任何子運(yùn)算式e

都成立，那麼P(e)也成立形式2的歸納假設(shè)包含了所有的子運(yùn)算式，並非只是直接子運(yùn)算式1.4歸納法1.4.2證明上的歸納證明系統(tǒng)由公理和推理規(guī)則組成證明是一個公式序列，該序列中的每個公式都是公理或者是由前面的公式通過一個推理規(guī)則得到的結(jié)論基於證明的長度，用自然數(shù)歸納法來討論證明的性質(zhì)另一種觀點(diǎn)把證明看成是某種形式的樹

1.4歸納法BAn---A1證明樹示意圖證明上的結(jié)構(gòu)歸納對該證明系統(tǒng)中的每個公理，證明P成立假定對證明

1,…,

k，P成立，證明P(

)也為真。

是這樣的證明，它結(jié)束於用一個推理規(guī)則，並且是從證明

1,…,

k延伸出來的一個證明1.4歸納法1.4.3良基歸納集合A的良基關(guān)係是A上的一個二元關(guān)係

，它具有這樣的性質(zhì)：A上不存在無窮遞減序列a0

a1

a2

…例：在自然數(shù)上，如果j

i+1，則i

j，則這個關(guān)係是一個良基關(guān)係良基關(guān)係的一些特點(diǎn)良基關(guān)係不一定有傳遞性良基關(guān)係都是非自反的，即對任何a

A，a

a不成立；否則會出現(xiàn)無窮遞減序列a

a

a

…1.4歸納法引理1.1

如果

是集合A上的二元關(guān)係，那麼

是良基的當(dāng)且僅當(dāng)A的每個非空子集都有一個極小元證明

令B

A是任意非空子集。用反證法證明B有極小元如果B無極小元，那麼對每個a

B，可以找到某個a

B使得a

a。這樣,可以從任意的a0

B開始,構(gòu)造一個無窮遞減序列a0

a1

a2

…反過來，假定每個子集有一個極小元，那麼不可能存在a0

a1

a2

…，因?yàn)樵撔蛄薪o出了無極小元的集合{a0,a1,a2,…}

1.4歸納法命題1.2（良基歸納）

令

是集合A上的一個良基關(guān)係，令P是A上的某個性質(zhì)。若每當(dāng)所有的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歸納法良基歸納法的使用

如何理解：若每當(dāng)所有的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)等價(jià)於P(a) （因?yàn)?/p>

b:.P(b)為真，其中

表示空集）對另一些a,存在b，使得b

a，則

b.(b

a

P(b))P(a)的證明是從

b.(b

a

P(b))為真來推導(dǎo)P(a)為真1.4歸納法表1.1常用歸納形式的良基關(guān)係歸納形式良基關(guān)係自然數(shù)歸納（形式1）m

n，如果m+1

n自然數(shù)歸納（形式2）m

n，如果m

n結(jié)構(gòu)歸納（形式1）e

e

，如果e是e

的直接子運(yùn)算式結(jié)構(gòu)歸納（形式2）e

e

，如果e是e

的子運(yùn)算式基於證明的歸納

，如果

是證明

的最後一步推導(dǎo)規(guī)則的某個前提的證明1.4歸納法自然數(shù)歸納（形式1）：為證明對所有自然數(shù)n，P(n)為真，只需證明P(0)以及證明對任何自然數(shù)m,如果P(m)為真則P(m+1)必定為真自然數(shù)歸納（形式2）：為證明對所有自然數(shù)n，P(n)為真，只需證明對任何自然數(shù)m，如果所有的P(i)(i

m)為真則P(m)必定為真字典序（以自然數(shù)序列為例）

n1,n2,

…,nk

m1,m2,

…,mliffk<l或者k

l並且存在一個

i

k，使得對所有的

j<i有

nj

mj

並且ni

<mi2.1引言主要議題如下通過例子來介紹類型化

演算及相關(guān)語言的語法和語義用不動點(diǎn)算子來處理函數(shù)的遞歸定義討論P(yáng)CF的公理語義、操作語義和指稱語義一些基本的編程方法都可以用PCF來實(shí)現(xiàn)用操作語義來研究PCF的表達(dá)能力和局限介紹PCF的一些擴(kuò)充和衍生2.2語法2.2.1

概述由列出PCF的類型來概括其構(gòu)造基本類型：nat和bool類型構(gòu)造符笛卡兒積

函數(shù)類型

規(guī)定：

右結(jié)合，

的優(yōu)先順序高於

等同於

(

)

等同於(

)

2.2語法2.2.2

布爾值和自然數(shù)布爾類型常量：true，false布爾類型條件運(yùn)算式if

bool_exp

then

bool_exp

else

bool_exp

自然數(shù)類型常量0,1,2,3,…,

（數(shù)碼）自然數(shù)類型條件運(yùn)算式if

bool_exp

then

nat_exp

else

nat_exp

自然數(shù)相等測試Eq? 如Eq?50false

2.2語法例:if

bool_exp

then

x:nat.Melse

x:nat.N

_exp

::=…|if

bool_exp

then

_exp

else

_exp

尚未列出PCF自然數(shù)類型運(yùn)算式和布爾類型運(yùn)算式的所有可能形式2.2語法自然數(shù)類型和布爾類型的等式公理0+0=0,0+1

1,…,1+0=1,1+1=2,…與條件運(yùn)算式有關(guān)的公理模式iftruethenMelseN=MiffalsethenMelseN=N

相等測試也有無數(shù)個公理，其形式如下：對任意數(shù)碼n，Eq?nn=true對任意不相同數(shù)碼m,n，Eq?mn=false沒有等式公理Eq?MM=true2.2語法操作語義由一組歸約公理來定義，把每個等式公理自左向右定向可得到對應(yīng)的歸約公理，歸約公理通常用對運(yùn)算式求值可歸約式：匹配一個歸約公理左部的項(xiàng)例： ifEq?(6+6)7

then(2+2)else36

ifEq?127

then(2+2)else36

iffalsethen(2+2)else36

362.2語法2.2.3配對和函數(shù)有序?qū)Γㄒ卜Q二元組）,笛卡兒積類型

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語法二元組的歸約規(guī)則可以通過將proj公理從左到右定向得到?jīng)]有sp歸約規(guī)則它不是非要不可當(dāng)和函數(shù)的遞歸定義合在一起時，該規(guī)則會導(dǎo)致合流性的失敗2.2語法函數(shù)PCF函數(shù)由抽象表示任何PCF類型都可以作為PCF函數(shù)的論域或值域例comp=def

f:nat

nat.g:nat

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

p:nat

nat.(Proj1

p)+(Proj2

p)2.2語法類型化

運(yùn)算式的代換的精確定義[N/x]x=N[N/x]

=

，對

x的變數(shù)和常量[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語法函數(shù)的等式公理

x:

.M=

y:

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

)(x:

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

)

x:

.Mx=M，x

在M中不是自由的(

)

公理對顯式函數(shù)運(yùn)算式也是冗餘的如果M有y:

.P的形式，並且x

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

公理證明

x:

.Mx=M如果M是函數(shù)類型的變數(shù)，沒有

公理不可能證明x:.Mx=M2.2語法函數(shù)的歸約公理僅把

公理定向?yàn)閺淖蟮接业臍w約規(guī)則

歸約用於

演算的許多版本中2.2語法curry算子將多元函數(shù)變換成高階函數(shù)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聲明和語法美化

演算可作為程式設(shè)計(jì)的一種模型語言 beginfunctionf(x:nat):nat; returnx; end;

body

end對應(yīng)的

運(yùn)算式 (

f:nat

nat.

body)(x:nat.x)2.2語法let聲明

let

x:

=MinN在聲明體N中，x被約束到M把let看成一種縮寫，或者稱為“語法美化”

可以在PCF運(yùn)算式中使用let，但又不把它看成PCF真正語法的一部分let

x:

=MinN=def

(x:

.N)M不需要規(guī)定任何有關(guān)let的額外的等式公理和歸約規(guī)則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運(yùn)算式：(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語法另一種語法擴(kuò)充let

f(x:

):

=M

in

N=def

let

f:

=x:

.Min

N

2.2語法2.2.5

遞歸函數(shù)和不動點(diǎn)算子 將遞歸函數(shù)定義看成let和一種新的基本函數(shù)的組合遞歸使得運(yùn)算式可能沒有範(fàn)式選擇哪個歸約成為一件重要的事，因?yàn)橛械倪x擇會導(dǎo)致歸約不終止遞歸函數(shù)的聲明

letrec

f:

=M

in

N例：letrec

f:nat

nat=y

:nat.(ifEq?y0then1elsey

f(y–1))inf5(階乘函數(shù))2.2語法把整個等式看成一個關(guān)於f的方程

f:nat

nat=

y

:nat.ifEq?y0then1elsey

f(y–1)讓運(yùn)算式中f5中的f指稱該方程的一個解把求解遞歸定義的等式轉(zhuǎn)化為求高階函數(shù)的不動點(diǎn)2.2語法如果F:

是某類型

到它自己的函數(shù)，那麼F的不動點(diǎn)是使得F(x)=x的值x:

自然數(shù)上平方函數(shù)的不動點(diǎn)有0和1恒等函數(shù)有無數(shù)個不動點(diǎn)後繼函數(shù)沒有不動點(diǎn)

階乘函數(shù)是方程(f:nat

nat=

y

:nat.ifEq?y0then1elsey

f(y–1))的解階乘函數(shù)是F=def

f:nat

nat.y

:nat.ifEq?y0then1elsey

f(y–1)的不動點(diǎn)2.2語法不動點(diǎn)算子fix

:(

)

, 對每個類型

函數(shù)fix

為

到

的函數(shù)產(chǎn)生一個不動點(diǎn)把letrec看成是let和不動點(diǎn)算子組合的美化

letrec

f

:

M

in

N

=def

letf

:

=(fix

f:

.M)in

Nfix

:(

)

的等式公理fix

=f:

.f(fix

f) (fix)fix

M

M(fix

M) （使用(

)可得）(fix)歸約規(guī)則fix

f:

.f(fix

f)2.2語法繼續(xù)階乘函數(shù)的例子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)對任何自然數(shù)n，最終得到factn=n!2.3

程式和語義2.3.1程式和結(jié)果PCF語言有兩個語法範(fàn)疇：類型和項(xiàng)可觀測的類型：自然數(shù)類型和布爾類型像nat

nat這樣的函數(shù)類型不是可觀測的類型程式：PCF語言中合式的、可觀測類型的閉項(xiàng)進(jìn)一步限制：“不需要加輸入和輸出的程式”結(jié)果：計(jì)算或執(zhí)行程式的可觀測的效果（可觀測類型的閉範(fàn)式）語言語義的一般定義：程式集合和結(jié)果集合之間的一種關(guān)係2.3

程式和語義2.3.2

公理語義公理語義是一個證明系統(tǒng)，用它可以推導(dǎo)程式及其組成部分的性質(zhì)這些性質(zhì)可以用等式表示、用給定輸入下的輸出斷言表示、或用其他形式表示注意力放在等式公理語義上兩個程式在一個公理語義中等價(jià)，只要為它們推導(dǎo)出來的斷言正好完全相同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是不同的數(shù)碼）(cond) iftruethenMelseN=M, iffalsethenMelseN=N二元組(proj) Proj1

M,N=MProj2

M,N=N(sp) Proj1

P,Proj2P=P重新命名約束變數(shù) (

) x:

.M=y:

.y

x

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

程式和語義公理函數(shù)(

) (x:

.M)N=N/x

M(

) x:

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

=

f:

.f(fix

f)2.3

程式和語義推理規(guī)則等價(jià)(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

程式和語義二元組函數(shù)M=NProjiM=ProjiNM=N,P=Q

M,P

=

N,Q

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

程式和語義除了

抽象和

應(yīng)用外，其他同餘規(guī)則都是多餘的例：針對+的同餘規(guī)則是多餘的假定M=N

和P=Q由自反公理，有等式

x:nat.y:nat.x

y=x:nat.y:nat.x

y由

應(yīng)用的同餘規(guī)則可得(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

程式和語義該公理語義強(qiáng)到足以確定程式的含義該系統(tǒng)證明不了加法是可交換的，也證明不了遞歸函數(shù)間的許多有意義的等價(jià)對於這些性質(zhì)需要用歸納法來證明PCF語言對類型並不需要證明系統(tǒng)，因?yàn)閮蓚€類型相同當(dāng)且僅當(dāng)它們在語法上相同2.3

程式和語義2.3.3

指稱語義概述PCF的指稱語義，以便三種語義形式可以比較為每個類型選擇一個值集來給出項(xiàng)的指稱nat的語義論域是自然數(shù)值集N

{

nat}letrec

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

inf(0)計(jì)算不終止

bool的語義論域是布爾值集B

{

nat}nat和bool類型的任何項(xiàng)指派相應(yīng)語義論域上的一個值，也稱為它們的語義解釋2.3

程式和語義積類型

的數(shù)學(xué)值是有序?qū)虾瘮?shù)類型

的數(shù)學(xué)值是從

到

的函數(shù)集合如果

=

，那麼函數(shù)有不動點(diǎn)約定：對任何n

N，用?n?表示其數(shù)碼

例：

x:nat.M 如果對任何自然數(shù)n

N,都有 [?n?

/x]M

?f(n)?那麼

x:nat.M的指稱就是數(shù)值函數(shù)f:N

N2.3

程式和語義環(huán)境

是指從變數(shù)到值的映射若x:

,

(x)是類型

的值集上的元素通過歸納可以定義運(yùn)算式M在環(huán)境

中的含義〖M〗

〖x〗

是變數(shù)x在環(huán)境

中的值函數(shù)應(yīng)用〖MN〗

的含義是通過把M指稱的函數(shù)〖M〗

應(yīng)用到N指稱的變元〖N〗

來獲得其他情況可類似地定義2.3

程式和語義指稱語義是可合成的，即任何運(yùn)算式的含義由它子運(yùn)算式的含義決定如果〖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當(dāng)且僅當(dāng)經(jīng)若干步（含零步）歸約，M可以歸約到範(fàn)式N類型nat和bool(add) 0+0

0,0+1

1,…, 3+5

8,…(Eq?) Eq?nn

true,Eq?nm

false

n和m是不同的數(shù)碼(cond) iftruethenMelseN

M iffalsethenMelseN

N2.3

程式和語義二元組(proj) Proj1

M,N

MProj2

M,N

N重新命名約束變數(shù)(

)

x:

.M=

y:

.

y

x

M

y在M中不是自由的函數(shù)(

) (

x:

.M)N

N/x

M遞歸(fix) fix

f:

.f(fix

f)2.3

程式和語義這個操作語義並沒有指定計(jì)算步驟，因而顯得抽象一些保留了重新命名約束變數(shù)的等式公理的形式對於二元組的滿射配對公理(sp)和函數(shù)的外延公理(

)，沒有相應(yīng)的歸約規(guī)則2.3

程式和語義2.3.5由各種形式的語義定義的等價(jià)關(guān)係各種等價(jià)關(guān)係公理等價(jià)：M=N是可證明的 用M=ax

N表示指稱等價(jià)：M和N對自由變數(shù)的任何取值都有相同的指稱 用M=denN表示操作等價(jià)：eval(M)?eval(N)（程式M和N求值的結(jié)果一樣，或者求值結(jié)果都沒有定義

）

用M=opN表示2.3

程式和語義操作等價(jià)M=opN可以從程式推廣到一般項(xiàng)上下文C[]是一個項(xiàng)，但其中有一個洞例：C0[]=def

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

x:nat.x+x項(xiàng)M和N操作等價(jià)：

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

程式和語義等式證明系統(tǒng)的可靠性： 如果在公理語義中能證明M和N相等，那麼在指稱語義中，M和N應(yīng)該有同樣的含義=ax

=den這是判斷公理系統(tǒng)正確性的基本標(biāo)準(zhǔn)對PCF語言而言，公理語義對指稱語義是可靠的2.3

程式和語義操作語義的計(jì)算適當(dāng)性如果M是個程式，並且M和作為結(jié)果的N有同樣的指稱，那麼在操作語義中，執(zhí)行程式M的結(jié)果是N計(jì)算適當(dāng)性表明已有足夠的歸約規(guī)則去確定任何程式的值對PCF語言而言，操作語義有計(jì)算的適當(dāng)性2.3

程式和語義對PCF語言的程式而言，要滿足的最小要求是(

programs

M)(

results

N)M=ax

NiffM=den

NiffM=op

N對任意的項(xiàng)，希望滿足的要求是=ax

=den

=op操作等價(jià)是三者中最粗糙的一個，和指稱等價(jià)或可證明的等價(jià)相比，可能有更多的項(xiàng)操作等價(jià)若=op

=ax，可能會出現(xiàn)不一致的證明系統(tǒng)2.4歸約和符號解釋器本節(jié)討論基於操作語義的PCF程式的執(zhí)行已經(jīng)討論的操作語義是不確定的符號解釋器本節(jié)討論其他形式的符號解釋器確定的：急切歸約、最左歸約、惰性歸約並行歸約2.4歸約和符號解釋器2.4.1

歸約的合流性每當(dāng)M

N1

並且M

N2，那麼存在項(xiàng)P，使得N1

P

並且N2

P

PCF歸約是合流的合流性也叫做Church-Rosser性質(zhì)MN2N1P2.4歸約和符號解釋器如果

由一組等式公理定向來確定如果M

N，那麼可以證明等式M=N從M

N和P

N，可以證明M

P合流隱含著，一個等式是可證明的當(dāng)且僅當(dāng)它的兩個項(xiàng)都可以歸約到一個公共項(xiàng)如果兩個不同的項(xiàng)都不能歸約，那麼不可能證明它們相等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歸約和符號解釋器例：這種形式的程式執(zhí)行和大家熟悉的方式略有點(diǎn)區(qū)別let

f(x:nat):nat=5in

letrec

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

f(g3)在大多數(shù)程式設(shè)計(jì)語言中，該程式不會終止

2.4歸約和符號解釋器2.4.2歸約策略歸約策略：項(xiàng)到項(xiàng)的部分函數(shù)F，如果F(M)=N，那麼M

N

與歸約策略F對應(yīng)的部分計(jì)算函數(shù)evalF:PCF

PCF是：evalF

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

(M

)=NthenNevalF在數(shù)學(xué)上等價(jià)於遵循策略F逐步進(jìn)行歸約，直到該策略不能再遵循為止2.4歸約和符號解釋器感興趣的是一步歸約策略只要有可能便選擇一步歸約的策略程式M的計(jì)算eval(M)是M的範(fàn)式或者eval(M)沒有定義基於項(xiàng)本身的形式來選擇一步歸約先“優(yōu)化”函數(shù)

x:

.M

最左歸約（惰性歸約）急切歸約(

x:

.M)N(

x:

.M)N

(

x:

.M

)N[N/x]M2.4歸約和符號解釋器2.4.3最左歸約和惰性歸約最左歸約：對項(xiàng)中盡可能左邊的符號進(jìn)行歸約遵循的是結(jié)構(gòu)化操作語義的風(fēng)格每條規(guī)則正好作用到一種形式的項(xiàng)考察項(xiàng)的結(jié)構(gòu)就知道該用哪條規(guī)則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是歸約公理子項(xiàng)規(guī)則nat和bool N是範(fàn)式

M

leftM

M+N

leftM

+NM

NM

leftNM

leftM

N+M

leftN

+

M

2.4歸約和符號解釋器

N是範(fàn)式M

leftM

Eq?MN

leftEq?

M

NM

leftM

Eq?NM

leftEq?N

M

2.4歸約和符號解釋器

M是範(fàn)式 M,N是範(fàn)式M

leftM

ifMthenNelseP

leftifM

thenNelsePN

leftN

ifMthenNelseP

leftifMthenN

elsePP

leftP

ifMthenNelseP

leftifMthenNelseP

2.4歸約和符號解釋器二元組

M是範(fàn)式M

leftM

M,N

left

M

,N

N

leftN

M,N

left

M,N

M

leftM

Proji

M

leftProji

M

2.4歸約和符號解釋器函數(shù)

M是範(fàn)式M

leftM

MN

left

M

NN

leftN

MN

leftMN

M

leftM

x:.

M

left

x:.

M

2.4歸約和符號解釋器命題

令M是任意類型的PCF項(xiàng)。那麼對任何範(fàn)式N，M

left

N當(dāng)且僅當(dāng)M

N命題令M是任意類型的PCF項(xiàng)。那麼evelleft(M)=N當(dāng)且僅當(dāng)M

N並且N是範(fàn)式如果僅要求這兩個命題對PCF程式（而不是所有的項(xiàng)）成立，可以採用惰性歸約不能再進(jìn)行惰性歸約的項(xiàng)叫做惰性範(fàn)式。nat和bool的惰性範(fàn)式正是它們的範(fàn)式

在實(shí)際實(shí)現(xiàn)中惰性歸約比最左歸約用得更普遍2.4歸約和符號解釋器PCF的惰性歸約公理 M

N是歸約公理子項(xiàng)規(guī)則nat和bool n是數(shù)碼M

lazyM

M+N

lazyM

+NM

NM

lazyNM

lazyM

n+M

lazyn

+

M

2.4歸約和符號解釋器

n是數(shù)碼M

lazyM

Eq?MN

lazyEq?

M

NM

lazyM

Eq?nM

lazyEq?n

M

2.4歸約和符號解釋器下麵兩條規(guī)則不再需要

M是範(fàn)式 M,N是範(fàn)式M

lazyM

ifMthenNelseP

lazyifM

thenNelsePN

leftN

ifMthenNelseP

leftifMthenN

elsePP

leftP

ifMthenNelseP

leftifMthenNelseP

2.4歸約和符號解釋器二元組前兩條規(guī)則不再需要

M是範(fàn)式M

leftM

M,N

left

M

,N

N

leftN

M,N

left

M,N

M

lazyM

Proji

M

lazyProji

M

2.4歸約和符號解釋器函數(shù)下麵兩條規(guī)則不再需要

M是範(fàn)式M

lazyM

MN

lazy

M

NN

leftN

MN

leftMN

M

leftM

x:.

M

left

x:.

M

2.4歸約和符號解釋器命題如果M

是PCF閉項(xiàng)，但它不是

x:

.M1或

M1,M2

的形式，那麼對任何項(xiàng)N，M

lazy

N當(dāng)且僅當(dāng)M

left

N

推論

如果P是PCF程式，R是結(jié)果，那麼P

lazy

R當(dāng)且僅當(dāng)P

left

R和最左歸約相比，由於惰性歸約的規(guī)則集合小一些，因此有可能得到一個效率相對較高的實(shí)現(xiàn)2.4歸約和符號解釋器2.4.4並行歸約對PCF來說，當(dāng)能獨(dú)立地歸約兩個子運(yùn)算式中的任意一個時，就應(yīng)該可以同時歸約它們MNM

NM1

N1,…,Mk

Nk

C[M1,…,Mk]

C[N1,…,Nk]2.4歸約和符號解釋器並行歸約的特點(diǎn)在PCF中，M

N當(dāng)且僅當(dāng)M

N並行歸約可以較快到達(dá)範(fàn)式2.4歸約和符號解釋器2.4.5急切歸約最左歸約和PCF的公理語義一致，並且允許不確定地或並行地實(shí)現(xiàn)更通常的次序是急切歸約，它和PCF的公理語義不一致let

f(x:nat):nat=5in

letrec

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

f(g3)2.4歸約和符號解釋器值：指不能再進(jìn)行急切歸約的項(xiàng)，即已經(jīng)完全計(jì)算了的項(xiàng)常量、變數(shù)和

抽象都是值，值的二元組也是值二元組中至少有一元不是值的情況，還有函數(shù)應(yīng)用都不能稱為值急切歸約與其它歸約策略的主要區(qū)別只有當(dāng)函數(shù)變元是值時才能使用

歸約，只有當(dāng)二元組的兩個元素都是值時才能使用Proji歸約fix歸約也不同，它會暫停fix作用於其變元的歸約2.4歸約和符號解釋器值如果V是常量、變數(shù)、

抽象或值的二元組，那麼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是不同的數(shù)碼iftruethenMelseN

eager

M

iffalsethenMelseN

eager

N

x:

.M=

y:

.

y

x

M，y在M中不是自由的

2.4歸約和符號解釋器子項(xiàng)規(guī)則nat n是數(shù)碼M

eagerM

M+N

eagerM

+NM

eagerM

n+M

eagern

+M

2.4歸約和符號解釋器

bool

n是數(shù)碼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歸約和符號解釋器 函數(shù)

V是值下麵一條規(guī)則不再需要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整個項(xiàng)變成了(

y:nat.y)3，歸約到32.4歸約和符號解釋器急切歸約會發(fā)散的例子 letf(x:nat):nat=5in letrecg(x:nat):nat=g(x+1)inf(g3)在實(shí)際中用急切計(jì)算而不是用最左計(jì)算的主要原因最左歸約的實(shí)現(xiàn)通常是低效的。當(dāng)像fx這樣的變元傳給函數(shù)g時（g(fx)），必須傳遞f

的代碼的指針並記住適當(dāng)?shù)脑~法環(huán)境最左歸約和賦值的組合令人混淆，副作用的出現(xiàn)使得最左計(jì)算與不確定計(jì)算和並行計(jì)算不一致

2.5程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限2.5.1記錄和n元組記錄是多個成分的聚集，每個成分有不同的標(biāo)記記錄的類型寫成

l1

:

1,…,lk:

k

記錄寫成

l1

=M1,…,lk=Mk

記錄r中的成分li的選擇可用加點(diǎn)的記號r.li來表示等式公理

l1=M1,…,lk=Mk

.li=

Mi2.5程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限使用記錄的優(yōu)點(diǎn)一個方便之處是其成分次序無關(guān)緊要另一個優(yōu)點(diǎn)是，可以選擇助記憶的名字作為標(biāo)記記錄和記錄類型可以翻譯成PCF的二元組和笛卡兒積為了簡化n個成分的記錄到PCF的翻譯，可以定義n元組作為一種語法美化2.5程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限引入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程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限使用n元組，可以把多於兩個成分的記錄翻譯成PCF運(yùn)算式

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程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限2.5.6並行運(yùn)算的不可定義性並行或計(jì)算M∨N的方式是：並行地歸約M和N，如果其中一個終止且值為true，那麼另一個計(jì)算流產(chǎn)，並返回true否則繼續(xù)歸約它們，希望它們都能歸約到範(fàn)式2.5程式設(shè)計(jì)實(shí)例、表達(dá)能力和局限並行或是不能由PCF定義的定理

不存在PCF運(yùn)算式POR，它對任意的閉布爾運(yùn)算式M和N有下麵的行為PORMN

true， 如果M

true或N

true；PORMN

false， 如果M

false並且N

false；PORMN

沒有範(fàn)式 否則2.6衍生和擴(kuò)充2.6.1單元類型與和類型單元類型unit：只有一個元素的類型unit類型的常量：

unit類型的等式公理：M

:unit(對任何M:unit)unit類型的歸約公理：M

:unit單元類型好像沒有什麼意義，但是當(dāng)它同和類型及其它形式的類型組合起來時，顯得非常有用2.6衍生和擴(kuò)充和類型

: 類型

和

的可區(qū)分的並可區(qū)分的並：例如，如果取int和int的並集，得到的仍然是int；但是，int和int的可區(qū)分的並有int的兩個“拷貝”

內(nèi)射函數(shù)

Inleft

,

:

Inright

,

:

分情況函數(shù)

Case

,

,

:(

+

)

(

)

(

)

2.6衍生和擴(kuò)充和類型的等式公理（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衍生和擴(kuò)充單元類型與和類型加入PCF後，bool可以省略bool=def

unit+unittrue=defInleft

false=defInright

ifMthenNelseP=def

Caseunit,unit,

M(K

,unitN)(K

,unitP)

其中N,P:

並且K

,unit是

項(xiàng)

x:

.

y:unit.x可以檢驗(yàn)下麵兩個公理 iftruethenMelseN=M iffalsethenMelseN=N2.6衍生和擴(kuò)充2.6.2遞歸類型類型等式t=

，其中t出現(xiàn)在

中也可以為遞歸定義的類型引入不動點(diǎn)算子，並且用fix(

t.

)表示方程t=

的一個解用

t.

作為fix(

t.

)的語法美化在

t.

中

約束t類型運(yùn)算式也可以有自由變數(shù)，這是會導(dǎo)致多態(tài)性（第七章介紹）沒有任何項(xiàng)可以約束類型變數(shù)，在項(xiàng)中僅使用閉類型2.6衍生和擴(kuò)充若把PCF中nat和bool類型刪除,把單元類型、和類型及遞歸類型加入，PCF的類型運(yùn)算式則是由文法

::=t|unit|

+

|

|

|

t.

產(chǎn)生的閉運(yùn)算式有遞歸類型時，需要仔細(xì)考慮類型相等問題2.6衍生和擴(kuò)充等式t=

意味著fix(

t.

)=

fix(

t.

)

t

用

記號表示為

t.

=

t.

t

對類型等式

t.

=

t.

t

有兩種不同的觀點(diǎn)等式左右兩邊是真正不可區(qū)分的類型等式左右兩邊是同構(gòu)的類型

t.

t.

t

2.6衍生和擴(kuò)充nat作為遞歸類型的定義自然數(shù)的一個顯著特徵是，如果加一個元素到自然數(shù)集合，所得到的集合和自然數(shù)集合同構(gòu)unit

比

多一個元素，因此nat

unit+nat，即nat=def

t.unit+tnat

unit+nat

unit+(unit+nat)

…

unit+(unit+(unit+(unit+(unit+…+nat)…)))PCF運(yùn)算式翻譯到只含遞歸的類型定義、單元類型與和類型的運(yùn)算式3.1引言代數(shù)數(shù)據(jù)類型包括一個或多個值集一組在這些集合上的函數(shù)基本限制是其函數(shù)不能有函數(shù)變元基本“類型”(type)符號被稱為“類別”(sort)泛代數(shù)（也叫做等式邏輯）定義和研究代數(shù)數(shù)據(jù)類型的一般數(shù)學(xué)框架本章研究泛代數(shù)和它在程式設(shè)計(jì)中定義常用數(shù)據(jù)類型時的作用

3.1引言本章主要內(nèi)容：代數(shù)項(xiàng)和它們在多類別代數(shù)中的解釋等式規(guī)範(fàn)（也叫代數(shù)規(guī)範(fàn)）和等式證明系統(tǒng)等式證明系統(tǒng)的可靠性和完備性（公理語義和指稱語義的等價(jià)）代數(shù)之間的同態(tài)關(guān)係和初始代數(shù)數(shù)據(jù)類型的代數(shù)理論從代數(shù)規(guī)範(fàn)導(dǎo)出的重寫規(guī)則（操作語義）大多數(shù)邏輯系統(tǒng)中一些公共的議題將被覆蓋3.2

代數(shù)、基調(diào)和項(xiàng)3.2.1代數(shù)代數(shù)一個或多個集合，叫做載體一組特徵元素和一階函數(shù)，也叫做代數(shù)函數(shù)

f:A1

…

Ak

A例：N

N,0,1,+,

載體N是自然數(shù)集合特徵元素0,1

N，也叫做零元函數(shù)函數(shù)+,

:N

N

N3.2

代數(shù)、基調(diào)和項(xiàng)多個載體的例子Apcf

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

下麵開始逐步給出代數(shù)的一種語法描述，有窮的語法表示在電腦科學(xué)中十分重要定義數(shù)據(jù)類型證明性質(zhì)進(jìn)行化簡還必須討論這種語法描述的語義A5pcf

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

3.2

代數(shù)、基調(diào)和項(xiàng)3.2.2

代數(shù)項(xiàng)的語法基調(diào)

S，F(xiàn)

S是一個集合，其元素叫做類別函數(shù)符號f:s1

…

sk

s的集合F，其中運(yùn)算式s1

…

sk

s叫做類型