軟件形式化方法第2章 數(shù)學(xué)基礎(chǔ)

第2章數(shù)學(xué)基礎(chǔ)2.1命題和謂詞演算

2.2集合和關(guān)系2.3函數(shù)2.4語法2.5結(jié)構(gòu)歸納2.6

演算2.7論域理論基礎(chǔ)注：本章部分內(nèi)容具有復(fù)習(xí)性質(zhì)2.1命題和謂詞演算命名約定和注釋定義和相等關(guān)系表達(dá)式中的輔助名字命題演算謂詞演算命題邏輯的回顧合適公式的歸納定義

::=p|(

)|(

)|(

)|(

)推理規(guī)則（包括公理）

(i)

(e1) (e2)語法推論若從

1,2,…,n

可以證明

，表示成

1,2,…,n

|-

, 簡寫成|-

邏輯等價(jià)

|-

并且

|-

命題邏輯的回顧命題邏輯的語義定義真值集合（給p,q指派真值）把各邏輯連接詞映射到真值集合上的運(yùn)算（真值表方式）各推理規(guī)則在該模型中成立語義推論

若

1,2,…,n的值都為真,則

值也為真,寫成

1,2,…,n

|=

, 簡寫成|=

語義等價(jià)

|=

并且

|=

可滿足性

是可滿足的，若存在一種指派使

的值為真命題邏輯的回顧命題邏輯是可靠的和完備的命題邏輯的可靠性

若

|-

是有效的（可證明的），則

|=

成立命題邏輯的完備性

若

|=

成立，則

|-

是有效的命題邏輯的可靠性和完備性

|-

有效，當(dāng)且僅當(dāng)

|=

成立謂詞邏輯的回顧合式公式謂詞符號(hào)集合

、函數(shù)符號(hào)集合

（包括常量符號(hào)）基于

定義項(xiàng)集

t::=x|c|f(t,…,t)歸納地定義基于（

,

）的合適公式

::=P(t1,t2,…,tn)|(

)|(

)|(

)|(

)|(x

)

|(x

) (P

)自由變量、約束變量、代換謂詞邏輯的回顧新增推理規(guī)則（包括公理）項(xiàng)相等的證明規(guī)則全稱量詞證明規(guī)則存在量詞證明規(guī)則量詞間的等價(jià)規(guī)則語義模型、可靠性、完備性它們都可以基于命題邏輯相應(yīng)概念進(jìn)行拓展

|-

和

|=

的含義與前面的一致

|=

表示

在模型

中成立2.2集合和關(guān)系基本集合定義集合集合上的運(yùn)算序列、元組和笛卡兒積關(guān)系的定義關(guān)系的論域和值域關(guān)系的逆和像集合集合的概念

構(gòu)造性數(shù)學(xué)方法的基礎(chǔ)。集合就是一組無重復(fù)的對(duì)象的全體。集合中的對(duì)象稱為集合元素。集合的描述方法通常用大寫字母表示集合，用小寫字母表示元素描述集合的三種方法枚舉法：列出所有元素的表示方法。如1至5的整數(shù)集合可表示為：

1，2，3，4，5

；外延表示法：當(dāng)集合中所列元素的一般形式很明顯時(shí)，可只列出部分元素，其他則用省略號(hào)表示。如斐波那契數(shù)列可表示為：{0，1，1，2，3，5，8，13，21，34，…}；謂詞表示法：用謂詞來概括集合中元素的屬性。如斐波那契數(shù)列可表示為：{Fn|Fn+2=Fn+1+Fn，F(xiàn)0=0，F(xiàn)1=1，n≥0}

集合的運(yùn)算

集合的并

設(shè)A、B為兩個(gè)任意集合，所有屬于A或?qū)儆贐的元素構(gòu)成的集合C，稱為A和B的并集?？杀硎緸椋篊＝A∪B＝｛x｜x∈A∨x∈B｝。求并集的運(yùn)算稱為并（運(yùn)算）。例:若A={a，b，c，d}，B={b，d，e}，求集合A和B的并。解：A∪B＝｛a，b，c，d，e｝集合的運(yùn)算集合的差設(shè)A、B為兩個(gè)任意集合，所有屬于A而不屬于B的一切元素構(gòu)成的集合S，稱為A和B的差集?？杀硎緸椋篠=A－B=｛x｜x∈A∨x∈B｝。求差集的運(yùn)算稱為差（運(yùn)算）。例:若A={a，b，c，d}，B={b，d，e}，求集合A和B的差。解：A－B={a，c}集合的運(yùn)算交集的交設(shè)A、B為兩個(gè)任意集合，由和的所有相同元素構(gòu)成的集合C，稱為A和B的交集。可表示為：C＝A∩B＝｛x｜x∈A∧x∈B｝。求交集的運(yùn)算稱為交（運(yùn)算）。例5.3若A={x|x>-5}，B={x|x<1}，求集合和B的交。解：A∩B＝｛x｜x>﹣5｝∩｛x｜x<1｝＝｛x｜–5<x<1｝集合的運(yùn)算集合的補(bǔ)設(shè)I為全集，A為I的任意一子集，I–A則為A的補(bǔ)集，記為?？杀硎緸?/p>

I–A=｛x｜x∈I，｝求補(bǔ)集的運(yùn)算稱為補(bǔ)（運(yùn)算）求補(bǔ)集的運(yùn)算稱為補(bǔ)（運(yùn)算）

例5.4若I=｛x｜–5﹤x﹤5｝，A=｛x｜0﹤x﹤1｝，求。解：=I–A=｛x｜–5﹤x﹤0∨1﹤x﹤5｝集合的運(yùn)算集合的乘積集合A1，A2，…，An的乘積一般用法國數(shù)學(xué)家笛卡爾（ReneDescartes）的名字命名，即笛卡爾積。該乘積表示如下：A1×A2×…An={（a1，a2，…，an）｜ai∈Ai，i＝1，…，n}A1×A2×…An的結(jié)果是一個(gè)有序元組的集合。例5.5若A={1，2，3}，B={a，b}，求A×B。解：A×B={（1，a），（1，b），（2，a），（2，b），（3，a），（3，b）}關(guān)系關(guān)系是一個(gè)謂詞，其定義域?yàn)閗元組的集合。通常的關(guān)系為二元關(guān)系，其定義域?yàn)橛行驅(qū)Φ募?，在這個(gè)集合中，我們說有序?qū)Φ牡谝粋€(gè)元素和第二個(gè)元素有關(guān)系。如學(xué)生選課：

學(xué)生

課程

成績

張三

文學(xué)90

張三

哲學(xué)95

李四

數(shù)學(xué)80

李四

藝術(shù)85

王五

歷史92

王五

文學(xué)88等價(jià)關(guān)系在關(guān)系中，有一種特殊的關(guān)系，即等價(jià)關(guān)系，它滿足以下3個(gè)條件：自反性，即對(duì)集合中的每一個(gè)元素a，都有aRa；對(duì)稱性，即對(duì)集合中的任意元素a，b，aRb成立當(dāng)且僅當(dāng)bRa成立；傳遞性，即對(duì)集合中的任意元素a，b，c，若aRb和bRc成立，則aRc一定成立。等價(jià)關(guān)系的一個(gè)重要性質(zhì)是：集合A上的一個(gè)等價(jià)關(guān)系R可將A劃分為若干個(gè)互不相交的子集，稱為等價(jià)類。2.3函數(shù)函數(shù)的定義有限函數(shù)由表達(dá)式定義函數(shù)函數(shù)的交覆蓋并限制合成中綴算符作為函數(shù)謂詞和商運(yùn)算逆和像泛函分派和平行作用curry函數(shù)函數(shù)又稱映射，是指把輸入轉(zhuǎn)變成輸出的運(yùn)算，該運(yùn)算也可理解為從某一“定義域”的對(duì)象到某一“值域”的對(duì)象的映射。函數(shù)是程序設(shè)計(jì)的基礎(chǔ)，程序定義了計(jì)算函數(shù)的算法，而定義函數(shù)的方法又影響著程序語言的設(shè)計(jì)，好的程序設(shè)計(jì)語言一般都便于函數(shù)的計(jì)算。設(shè)f為一個(gè)函數(shù)，當(dāng)輸入值為a時(shí)輸出值為b，則記作：函數(shù)的定義一般來說，給出X

Y的一個(gè)關(guān)系r和一個(gè)對(duì)象x∈X，存在零個(gè)、一個(gè)或多個(gè)對(duì)象y∈Y，使得二元組<x，y>從屬于r（甚至可能有無限多個(gè)這樣的y）如果對(duì)每個(gè)x，最多只有一個(gè)這樣的y，那么就把這樣的關(guān)系叫做函數(shù)。關(guān)系finrel不是函數(shù)，但關(guān)系pm_double是函數(shù)。函數(shù)的定義X和Y間的函數(shù)關(guān)系的集合記為：

X→Y這個(gè)集合是X←→Y的一個(gè)子集，可以精確地定義為：

X→Y{r：X

Y|

x：X·givenimage_of_xr(·{x}·)thenfiniteimage_of_x

(cardimage_of_x≤1) end}函數(shù)的定義對(duì)于函數(shù)f：X→Y，如果domf＝X，我們說f是個(gè)全函數(shù)從X到Y(jié)的全函數(shù)的集合用

X→tY表示注意，本書中函數(shù)和全函數(shù)的定義分別對(duì)應(yīng)到一些書上部分函數(shù)和函數(shù)的定義有限函數(shù)如果函數(shù)的論域有限，則把它們叫做有限函數(shù)，從X到Y(jié)的有限函數(shù)集合記為：定義為：

{f：X→Y|finite(domf)}定義有限函數(shù)的一種方式是列出對(duì)論域的每個(gè)變?cè)〉闹颠@類似于由外延定義有限集合

由表達(dá)式定義函數(shù)對(duì)于集合，還可由概括定義，即由特征性質(zhì)而不是由枚舉來定義對(duì)于函數(shù)，等價(jià)的機(jī)制是，由形式變?cè)系谋磉_(dá)式定義一個(gè)函數(shù)，對(duì)任何實(shí)在變?cè)闹?，由這個(gè)值代替形式變?cè)傻玫较鄳?yīng)的函數(shù)值例子：函數(shù)的基調(diào)f：--對(duì)一個(gè)函數(shù)f：--對(duì)一個(gè)全函數(shù)注意不要把f：和S

相混淆前者給出f的基調(diào)，聲明f是從X到Y(jié)的一個(gè)函數(shù)，而后者是把S定義為從X到Y(jié)的所有函數(shù)的集合函數(shù)的交前面把函數(shù)定義為特殊的關(guān)系，而關(guān)系是一類特殊的集合這使得有可能定義兩個(gè)函數(shù)的交為一個(gè)函數(shù)，即同時(shí)屬于兩個(gè)函數(shù)的<變?cè)?，結(jié)果>二元組的集合兩個(gè)函數(shù)的交定義如下：令f，g：，令h

，那么：

domh={x:domfdomg|f(x)=g(x)};對(duì)xdomh，h(x)=f(x)=g(x)函數(shù)的覆蓋并

兩個(gè)函數(shù)的并可能不是一個(gè)函數(shù)關(guān)系這種現(xiàn)象發(fā)生在兩個(gè)函數(shù)的論域相交，并且它們中至少在一個(gè)變?cè)喜灰恢碌那闆r下例如，對(duì)于3.2節(jié)的f1和f2，它們對(duì)c的值有沖突，因此,不是一個(gè)函數(shù)（b的兩個(gè)函數(shù)值不會(huì)引起問題，因?yàn)樗鼈円粯樱?/p>

限制函數(shù)f到其源集的子集A的限制記為f\A，定義如下：令f：和A：P(X)，那么hf\A是一個(gè)函數(shù)h：

，使得：

domh=Adomf并且對(duì)adom

h，h(a)=f(a)換句話說，f\A和f是一樣的函數(shù)，但是它的源集被限制到A函數(shù)的合成函數(shù)上的另一種運(yùn)算是合成，它可以推廣到關(guān)系上中綴算符作為函數(shù)在處理函數(shù)時(shí)，還有一種約定將是有用的在普通的數(shù)學(xué)和程序設(shè)計(jì)語言中，許多二元函數(shù)使用中綴記號(hào)，也就是說，一個(gè)算符放在兩個(gè)變?cè)闹虚g而不是它們的前面

謂詞和商運(yùn)算特征函數(shù)

函數(shù)的逆和像函數(shù)是特殊的關(guān)系，因此逆和像算符也可以定義在函數(shù)上泛函如上面合成的算符所示，泛函，也叫做高階函數(shù)，是允許函數(shù)作為變?cè)蚪Y(jié)果（或同時(shí)作為變?cè)蚪Y(jié)果）的函數(shù)。術(shù)語“泛函”在本書中之用于高階全函數(shù)。在指稱語義中，泛函起著重要的作用，因此，必須熟悉泛函的使用分派分派是基調(diào)為：的泛函對(duì)于任意函數(shù)f：U—>X和g：U－>Y，f&g是函數(shù)：換句話說，f&g通過f把變?cè)猽到分派給X，同時(shí)通過g把u分派給Y。

平行作用平行作用是基調(diào)為：的泛函對(duì)任意函數(shù)f：U—>X和g：V—>Y，f＃g是函數(shù):換句話說，f＃g平行地把f和g分別作用于出自U的一個(gè)變?cè)统鲎訴的一個(gè)變?cè)a(chǎn)生X×Y的一個(gè)二元組。

curry另一個(gè)重要的泛函是curry（以數(shù)學(xué)家H.B.Curry命名）。這個(gè)泛函把任意的兩個(gè)變?cè)暮瘮?shù)翻譯成一個(gè)變?cè)暮瘮?shù)，后者的結(jié)果也是一個(gè)變?cè)暮瘮?shù)。curry本身的基調(diào)是：

curry對(duì)于全函數(shù)，curry定義如下：對(duì)于任意的集合X、Y和Z，如果f是基調(diào)為：全函數(shù)。那么curry（f）是基調(diào)為:的函數(shù)g，使得對(duì)于任意x：X和y：Y，有：g（x）（y）＝f（x，y）

2.4語法具體語法抽象語法基于抽象語法的語義定義抽象語法的數(shù)學(xué)基礎(chǔ)具體語法說明語言語法的習(xí)慣方法是用Backus-Naur形式（BNF）,使用BNF，可用文法描述語言的語法文法由一組產(chǎn)生式組成，每個(gè)產(chǎn)生式描述了某類程序結(jié)構(gòu)的形式，如表達(dá)式、命令、例程等等例如，下面的產(chǎn)生式用標(biāo)準(zhǔn)的BNF表示法定義了某個(gè)語言中條件命令的語法：<conditional>::=if<boolen_expression>then<command>else<command>end具體語法BNF和它的各種衍變（尤其是NiklausWirth為定義Pascal語言而引入的圖形表示）提供了廣為接受的語法描述機(jī)制然而，它們不是更深入地研究語言的最好基礎(chǔ)BNF產(chǎn)生式包括了許多無關(guān)緊要的細(xì)節(jié)，如關(guān)鍵字和其他的外部語法約定BNF規(guī)范實(shí)際描述的是程序員看見的程序的外部形式，而不是程序的結(jié)構(gòu)抽象語法為了描述程序的內(nèi)部結(jié)構(gòu)而不是它們的外部形式，使用抽象語法比較合理抽象語法直接給出各種語言構(gòu)造的各個(gè)成分，而無關(guān)其表示細(xì)節(jié)例如，條件命令的抽象語法描述將直截了當(dāng)?shù)卣f明條件命令有三個(gè)成分：兩個(gè)命令和一個(gè)布爾表達(dá)式條件命令的其他東西稱為“語法作料”，它們只影響人們讀寫程序Meta抽象文法Meta抽象文法由以下兩部分組成：構(gòu)造名的有限集合，為了方便起見，構(gòu)造名用大寫字母開頭，如Command和Variable產(chǎn)生式的有限集合，每個(gè)產(chǎn)生式和一個(gè)構(gòu)造對(duì)應(yīng)Meta抽象文法由文法定義的語言是該文法的頂層構(gòu)造（在下面定義）的所有實(shí)例的集合產(chǎn)生式的形式：

Tright_hand_side

聚集產(chǎn)生式一個(gè)聚集產(chǎn)生式定義一個(gè)構(gòu)造，它的實(shí)例有固定數(shù)目的帶標(biāo)志成分例如，可以通過下面的Meta聚集產(chǎn)生式定義表示條件命令的抽象構(gòu)造：

Conditional

thenbranch：Command；

elsebranch：Command；

test：Boolean_expression不同成分的次序是無關(guān)緊要的，這是抽象語法和具體語法的一個(gè)區(qū)別聚集產(chǎn)生式一個(gè)構(gòu)造的定義可能僅根據(jù)一個(gè)其它的構(gòu)造，這種情況將被看成聚集產(chǎn)生式的特殊情況，如：

Variable

name:Identifier聚集構(gòu)造定義類似于語言中記錄類型的定義，即都是根據(jù)成分來描述它們選擇產(chǎn)生式選擇產(chǎn)生式通過一組選擇定義一個(gè)構(gòu)造，在一種語言中，各種可能的命令可以由產(chǎn)生式，來定義，例如，Command的實(shí)例是右部給出的某個(gè)構(gòu)造的一個(gè)實(shí)例：

CommandΔSkip|Assignment|Compound|Loop表產(chǎn)生式

一個(gè)構(gòu)造可以定義為另一個(gè)構(gòu)造的實(shí)例序列的集合，序列長度大于或等于零，表產(chǎn)生式對(duì)應(yīng)這種情況例如，Pascal中的復(fù)合語句可以有下面的產(chǎn)生式定義：

Compound

Command*Compound的實(shí)例是零個(gè)、一個(gè)或多個(gè)命令的序列如果一個(gè)構(gòu)造的實(shí)例是至少有一個(gè)元素的表，那么星號(hào)由加號(hào)代替例如：

NumberΔDigit＋預(yù)定義的構(gòu)造

如果文法定義的是實(shí)際語言，那么它的所有構(gòu)造最終需要由最基本的且意義明確的集合（即終結(jié)構(gòu)造）來定義在Meta中用的四個(gè)預(yù)定義的終結(jié)構(gòu)造，對(duì)應(yīng)到標(biāo)準(zhǔn)的數(shù)學(xué)集合：非負(fù)整數(shù)集：N整數(shù)集：Z布爾值集：B字符串集：S一個(gè)完整的抽象文法

下面是一個(gè)小的但有代表性的語言的抽象文法，它的結(jié)構(gòu)類似于流行語言Pascal，Ada和C等的公共核心，該語言起名為KernelKernel的頂層構(gòu)造是Program

這個(gè)文法是遞歸定義的例如，Command的一種選擇是Conditional；后者是一個(gè)聚集，有兩個(gè)Command成分這樣的循環(huán)定義是否有意義？定義符號(hào)“Δ”在這里的使用是否正確？這些問題在后面回答Kernel的抽象文法

ProgramΔdecpart:Declaration_list;body:CommandDeclaration_listΔDeclaration*DeclarationΔv:Variable;t:TypeTypeΔBoolean_type|Integer_typeCommandΔSkip|Assignment|Compound|Conditional|LoopAssignmentΔtarget:Variable；source:expressionCompoundΔCommand*ConditionalΔthenbranch，elsebranch:Command；

test:ExpressionKernel的抽象文法

LoopΔbody:Command；test:ExpressionExpressionΔConstant|Variable|BinaryConstantΔInteger_constant|Boolean_constantBinaryΔterm1，term2:Expression；op:OperatorOperatorΔBoolean_op|Relationa_op|Arithmetic_opBoolean_opΔNot|And|OrRelational_opΔLt|Le|Eq|Ne|Ge|GtArithmetic_opΔPlus|Minus|Times|DivBoolean_constantΔvalue:BInteger_constantΔValue:ZVariableΔid:S抽象語法表達(dá)式我們需要一種方式描述和操作遵守某抽象文法的程序，為此，Meta提供了抽象語法表達(dá)式。各種抽象語法表達(dá)式對(duì)應(yīng)到各類抽象語法產(chǎn)生式。

聚集構(gòu)造實(shí)例的表達(dá)式選擇構(gòu)造實(shí)例的表達(dá)式表構(gòu)造實(shí)例的表達(dá)式終結(jié)類型的表達(dá)式復(fù)雜語法的表達(dá)式

聚集構(gòu)造實(shí)例的表達(dá)式我們需要一種方式描述和操作遵守某抽象文法的程序。為此，Meta提供了抽象語法表達(dá)式。各種抽象語法表達(dá)式對(duì)應(yīng)到各類抽象語法產(chǎn)生式、先從聚集構(gòu)造開始。考慮一個(gè)聚集產(chǎn)生時(shí)，例如，Kernel文法的第一個(gè)產(chǎn)生式

ProgramΔdecpart:Declaration_list;body:Command它描述了一類對(duì)象——程序，每個(gè)程序有兩個(gè)成分：聲明表和命令。假定聲明dl和命令cmd給定，那么我們可以定義一個(gè)以dl和cmd為成分的程序p；

pΔProgram(decpart：dl;body：cmd)聚集構(gòu)造實(shí)例的表達(dá)式更一般地，當(dāng)要處理由聚集產(chǎn)生式定義的構(gòu)造時(shí)，可以通過含構(gòu)造名（這里是Program）和后隨的擴(kuò)號(hào)中成分表的表達(dá)式來描述這種構(gòu)造的實(shí)例。必須在每個(gè)成分前放上相應(yīng)的標(biāo)志（這里是decpart和body），用冒號(hào)把各成分和它們的標(biāo)志隔開，并用分號(hào)把各成分隔開。例如，語法類型Program的p。在Meta中，這樣的對(duì)象的成分通過點(diǎn)記號(hào)作為它們的標(biāo)志標(biāo)識(shí)。這是借助于語言中引用記錄的域的方式。例如，p的成分可以記為p.decpart和p.body。這些成分分別屬Declaration_list類型和Command類型。對(duì)于p，相應(yīng)的對(duì)象是dl和cmd。選擇構(gòu)造實(shí)例的表達(dá)式考慮選擇產(chǎn)生式，例如：

CommandΔSkip|Assignment|Compound|Conditional|Loop為了構(gòu)造Command的一個(gè)實(shí)例，首先必須有Skip或Assignment等的實(shí)例b，然后必須把b提升到Command狀態(tài)。b提升后的版本記為Command(b)。例如，假定v是變量，e式表達(dá)式，那么下面的表達(dá)式描述一個(gè)命令：

Command(Assignment(target；v;source；e))在最外層栝號(hào)里面的表達(dá)式定義了Assignment的一個(gè)實(shí)例，其目標(biāo)變量是v，源表達(dá)式是e。整個(gè)表達(dá)式代表同樣的賦值命令，但是看成Command的實(shí)例。選擇構(gòu)造實(shí)例的表達(dá)式現(xiàn)在考慮選擇構(gòu)造的實(shí)例(如類型Command的i)，幾乎所有定義在這樣的對(duì)象上的表達(dá)式都依賴于這個(gè)對(duì)象的“子類型”，在Command的情況下，也就是依據(jù)它是Skip、Assignment還是其它情況。分情形表達(dá)式在Meta中用于區(qū)分子類型。在Meta的變量i上的分情形表達(dá)式有這樣的形式：

caseiof

Skip->skip_expAssignment->assign_exp|Compound->comp_exp|Conditional->cond_exp|Loop->Loop_exp

end

選擇構(gòu)造實(shí)例的表達(dá)式右部表達(dá)式(skip_exp，assign_exp等）可以叫做“分支表達(dá)式”，這種分支表達(dá)式通常引用分情形變量I例如，assign_exp可以引用i.target和i.source。為了使這樣的記號(hào)有意義，必須把a(bǔ)ssign_exp中出現(xiàn)的i看成是Assignment類型而不是Command類型表構(gòu)造實(shí)例的表達(dá)式考慮表產(chǎn)生式，例如：

CompoundΔCommand*構(gòu)造復(fù)合命令Compound的實(shí)例的最明顯方式是列出若干數(shù)目的基構(gòu)造Command的對(duì)象如選擇構(gòu)造的實(shí)例那樣，最終對(duì)象的類型由Compound顯式地說明用這種方式說明的對(duì)象可以是空，記為Compound(<>)終結(jié)類型的表達(dá)式因?yàn)榻K結(jié)構(gòu)造沒有進(jìn)一步的描述，構(gòu)造名將代表這種構(gòu)造的實(shí)例而不加以進(jìn)一步說明例如，Kernel的Skip命令就記為Skip復(fù)雜的語法表達(dá)式反復(fù)使用上面的機(jī)制，可以構(gòu)造出各種表達(dá)式，它們表示抽象的語法結(jié)構(gòu)對(duì)于復(fù)雜表達(dá)式，使用輔助表達(dá)式可以使它們更清楚例:見講義P22-23從上面的例子可以看出，對(duì)于復(fù)雜表達(dá)式，抽象語法記號(hào)顯得有些笨拙。注意：抽象語法是對(duì)程序進(jìn)行推理的形式工具，而不是程序的可讀性的表示方法。對(duì)于后者，很顯然，標(biāo)準(zhǔn)的具體語法是恰當(dāng)?shù)倪x擇。下面介紹抽象語法的兩個(gè)重要應(yīng)用。

結(jié)構(gòu)編輯器

結(jié)構(gòu)編輯器是一種軟件工具，也叫做語法制導(dǎo)編輯器。結(jié)構(gòu)編輯器是構(gòu)造和處理如程序、程序設(shè)計(jì)或形式規(guī)范這樣的結(jié)構(gòu)文檔的系統(tǒng)。和標(biāo)準(zhǔn)的正文編輯器（它把任何正文堪稱是無結(jié)構(gòu)的字符序列）不同，結(jié)構(gòu)編輯器知道被處理的文檔的結(jié)構(gòu)。例如，Pascal的結(jié)構(gòu)編輯器知道Pascal的語法，因而能維持程序的語法合法性。結(jié)構(gòu)編輯器

對(duì)用戶來說，結(jié)構(gòu)編輯器免除了許多和語法有關(guān)的瑣碎事務(wù)。例如，Pascal編輯器可以為用戶輸入的begin配上end。結(jié)構(gòu)編輯器便于自動(dòng)的程序處理和系統(tǒng)的變換，可用于軟件工程環(huán)境。所有這樣的工具依靠基于抽象語法的語言描述，用于表示程序的內(nèi)部數(shù)據(jù)結(jié)構(gòu)是對(duì)應(yīng)的抽象語法樹。語言和系統(tǒng)的設(shè)計(jì)

軟件的設(shè)計(jì)者經(jīng)常需要設(shè)計(jì)語言，以便用戶和他們的系統(tǒng)通訊。在這個(gè)活動(dòng)中的一個(gè)典型錯(cuò)誤是過早地把注意力集中到交互的具體形式上，其結(jié)果是模糊了問題的焦點(diǎn)，過早地處理細(xì)節(jié)問題。語言和系統(tǒng)的設(shè)計(jì)

許多系統(tǒng)實(shí)際上需要三個(gè)接口，以不同的形式提供相同的功能，此時(shí)，這樣的錯(cuò)誤危害更大，這三種接口是：(1)批命令接口，它使系統(tǒng)通過封裝的命令序列成為可用；(2)交互接口，用戶在終端給出命令并立即見到結(jié)果；(3)例程接口，通常通過例程庫，使得其它程序可用系統(tǒng)的功能。語言和系統(tǒng)的設(shè)計(jì)

這三種接口雖然在功能上等價(jià)，但使用的“語言”在外部形式上區(qū)別相當(dāng)大。抽象語法提供了一種便利的形式，使我們能先集中注意力于重要的方面，而推遲具體細(xì)節(jié)的設(shè)計(jì)。靜態(tài)語義和動(dòng)態(tài)語義靜態(tài)語義是對(duì)不能由語法描述妥善地刻畫的程序結(jié)構(gòu)約束的描述。動(dòng)態(tài)語義是對(duì)程序執(zhí)行效果的描述。靜態(tài)語義覆蓋了形式體系和實(shí)際語言結(jié)構(gòu)描述需要間的間隙。當(dāng)我們無法用抽象語法產(chǎn)生式表達(dá)一個(gè)結(jié)構(gòu)性質(zhì)時(shí)，可以將其作為靜態(tài)語義來處理。為什么需要靜態(tài)語義在Kernel文法中，Conditional和Loop的產(chǎn)生式使語言描述的公共問題顯得突出。和普通的語言一樣，Kernel中的一個(gè)循環(huán)或條件的test分支必須是布爾表達(dá)式。可能已注意到，對(duì)應(yīng)的產(chǎn)生式中只把test申明為Expression，并且Expression的產(chǎn)生式包括了整數(shù)表達(dá)式和布爾表達(dá)式。這意味著值為整數(shù)的test作為循環(huán)的成分是遵守該文法的，雖然它明顯不該被接受。為什么需要靜態(tài)語義可由修改此文法來糾正這個(gè)缺陷：用兩個(gè)不同的構(gòu)造Boolean_expression和Integer_expression來代替Expression，在條件和循環(huán)命令的產(chǎn)生式中，讓Boolean_expression作為test的構(gòu)造，但是這種修改將使得文法大大地膨脹，很多Boolean_expression的產(chǎn)生式將簡單地重復(fù)Integer_expression的產(chǎn)生式。另一種方法是，仍保持簡單的文法，但是用非語法的機(jī)制來覆蓋類型規(guī)則和其它的約束。為什么需要靜態(tài)語義對(duì)于test表達(dá)式的類型規(guī)則，把約束分離出來是為了方便和簡單，原則上他們可以表達(dá)為該文法的一部分，但是，有些約束不能用純語法的記號(hào)來描述。例如：在Kernel中，變量不允許在一個(gè)程序中聲明兩次，這是一個(gè)不能用Meta抽象語法記號(hào)或BNF這樣的純語法形式體系表示的條件。任何實(shí)際的語言規(guī)范都包含這類約束，他們構(gòu)成了語言的靜態(tài)語義。基于抽象語法的語義定義

抽象語法可以用作定義靜態(tài)語義和動(dòng)態(tài)語義函數(shù)的基礎(chǔ)。使用抽象語法的主要優(yōu)點(diǎn)是可以把語義嫁接到語法軀干上，這個(gè)語法軀干已剪去了只反映程序外部形式的細(xì)節(jié)。語義函數(shù)的源集是構(gòu)造，也叫做語法論域。它們的目標(biāo)集合叫做語義論域，其實(shí)例指稱可能的“含義”。例：見講義P25抽象語法的數(shù)學(xué)基礎(chǔ)

前面的抽象語法用非形式的定義引入了構(gòu)造和抽象語法表達(dá)式等概念及相應(yīng)的Meta表示法下面討論它們的數(shù)學(xué)含義對(duì)于三類產(chǎn)生式的每一種，我們不僅應(yīng)為對(duì)應(yīng)的產(chǎn)生式的右部提供數(shù)學(xué)模型，而且應(yīng)為定義在相應(yīng)構(gòu)造的實(shí)例上的運(yùn)算提供適當(dāng)?shù)慕忉屇Ｐ突诔醯燃险摚鼈儼衙糠N構(gòu)造解釋為一個(gè)集合，它的成員是該構(gòu)造的實(shí)例，每種在實(shí)例上的運(yùn)算看成是在對(duì)應(yīng)集合成員上的運(yùn)算基于抽象語法的語義定義

聚集可以表示為“帶標(biāo)記的笛卡兒積”。這種集合對(duì)處理元組是方便的，因?yàn)樵M的每個(gè)成分都被命名，增強(qiáng)了可讀性。例：見講義P20基于抽象語法的語義定義

選擇可以表示為“不相交的并

”，使得結(jié)果集合的每個(gè)成員能指示它自己源于哪個(gè)集合。

例：見講義P20基于抽象語法的語義定義

表可以采用“遞歸定義”例：見講義P22復(fù)雜的語法表達(dá)式

反復(fù)使用上面的機(jī)制，可以構(gòu)造出各種表達(dá)式來表示抽象的語法結(jié)構(gòu)。對(duì)于復(fù)雜的表達(dá)式，使用輔助表達(dá)式可以使它們更清楚。例：見講義P22從上面的例子可以看出，對(duì)于復(fù)雜的表達(dá)式，抽象語法記號(hào)顯得有些笨拙。抽象語法是對(duì)程序進(jìn)行推理的形式工具，而不是程序的可讀性的表示方法。對(duì)于后者，很顯然，標(biāo)準(zhǔn)的具體語法是恰當(dāng)?shù)倪x擇。2.5結(jié)構(gòu)歸納

用于定義復(fù)雜對(duì)象的集合和證明這樣的對(duì)象的性質(zhì)，叫做結(jié)構(gòu)歸納對(duì)定義語言的結(jié)構(gòu)并證明其性質(zhì)特別有用Lisp的S表達(dá)式（作為該語言的數(shù)據(jù)和程序結(jié)構(gòu)的基礎(chǔ)）提供了由結(jié)構(gòu)歸納到對(duì)象的典型例子結(jié)構(gòu)歸納：例子

由結(jié)構(gòu)歸納定義S表達(dá)式如下：原子是S表達(dá)式；如果s1和s2是S表達(dá)式，那么(s1.s2)是S表達(dá)式。例如：(atom1.atom2)和((atom1.atom2).(atom3.(atom4.atom5)))都是S表達(dá)式結(jié)構(gòu)歸納定義的一般形式

更一般地，一個(gè)結(jié)構(gòu)歸納定義定義一個(gè)集合S，其成員屬于下面兩種情況之一：

(1)一個(gè)或多個(gè)預(yù)定義的集合的成員（如上面的原子集合）；

(2)由S先前的成員，經(jīng)一種或多種明確定義的機(jī)制推導(dǎo)出來（如上面帶括號(hào)和點(diǎn)的形式）。這樣的定義有清楚的數(shù)學(xué)解釋，定義的這個(gè)集合S是一個(gè)無限集合族的并

S?其中的Si由普通的歸納定義。S0是所有從(1)中得到的對(duì)象的集合；每個(gè)Si+1由所有如下的對(duì)象構(gòu)成：它們由Sj(0≤j≤i)的成員經(jīng)(2)導(dǎo)出結(jié)構(gòu)歸納定義的一般形式

例如，在S表達(dá)式中，S0是原子的集合；S1是形式為(a.b)的對(duì)象的集合，其中a和b是原子，S2也是形式為(a.b)的對(duì)象的集合，但是其中a和b在原子集中或者在S1中；等等某些對(duì)象可能出現(xiàn)在不同的Si中（事實(shí)上，在S表達(dá)式的例子中，每個(gè)Si是Si+1的子集），這不會(huì)引起問題。因?yàn)镾定義為所有Si的并，因而S的成員來自哪個(gè)Si是無關(guān)緊要的。按這種觀點(diǎn)，結(jié)構(gòu)歸納是通常的自然數(shù)歸納的直截了當(dāng)?shù)膽?yīng)用，歸納定義的是集合Si的序列。結(jié)構(gòu)歸納證明

由結(jié)構(gòu)歸納定義的集合有助于按同樣的方式組織證明。為了用結(jié)構(gòu)歸納證明S的所有成員滿足某個(gè)性質(zhì)p，可以按下面兩步進(jìn)行：

(1)（基本步）基集的所有成員滿足p；

(2)（歸納步）如果一組來自可能不同的Sj(0≤j≤i)的對(duì)象滿足p，那么用任何定義Si+1的構(gòu)造機(jī)制由它們得到的對(duì)象滿足p。結(jié)構(gòu)歸納證明

這種歸納技術(shù)的有效性可以從普通的自然數(shù)歸納證明的有效性得出：“一個(gè)結(jié)構(gòu)歸納證明直截了當(dāng)?shù)叵喈?dāng)于用自然數(shù)歸納法證明性質(zhì)：p(i；N)p(i；N)?“Si的所有成員滿足某個(gè)性質(zhì)p”結(jié)構(gòu)歸納證明：例

用結(jié)構(gòu)歸納證明每個(gè)S表達(dá)式有相等個(gè)數(shù)的開括號(hào)和閉括號(hào)。這個(gè)證明包含兩部分：

(1)原子沒有括號(hào)，因此滿足這個(gè)性質(zhì)；

(2)考慮兩個(gè)S表達(dá)式e1和e2，它們都滿足該性質(zhì)。令p1和p2分別是它們的開括號(hào)數(shù)。由假設(shè)，它們的閉括號(hào)數(shù)也分別是p1和p2。從e1和e2，構(gòu)造機(jī)制只能產(chǎn)生一個(gè)新的S表達(dá)式n?(e1.e2)。n的開括號(hào)和閉括號(hào)數(shù)都是p1+p2+1。結(jié)構(gòu)歸納定義是遞歸的簡單情況。自然數(shù)歸納形式1：為證明對(duì)所有自然數(shù)n，P(n)為真，只需證明P(0)以及證明對(duì)任何自然數(shù)m,如果P(m)為真則P(m+1)必定為真。形式2：為證明對(duì)所有自然數(shù)n，P(n)為真，只需證明對(duì)任何自然數(shù)m，如果所有的P(i)(im)為真則P(m)必定為真字典序（以自然數(shù)序列為例）

n1,n2,

…,nk

m1,m2,

…,mliffk<l或者k

l并且存在一個(gè)

i

k，使得對(duì)所有的

j<i有

nj

mj

并且ni

<mi

表達(dá)式上的歸納(2015-5-13)表達(dá)式文法

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

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

=def

樹t.如果height(t)=n并且t是e的分析樹，那么P(e)為真首先必須為高度是0的分析樹直接證明P然后，對(duì)于高度至少為1的樹，假定對(duì)于分析樹的高度較小的表達(dá)式，P都成立結(jié)構(gòu)歸納形式1對(duì)每個(gè)原子表達(dá)式e，證明P(e)對(duì)直接子表達(dá)式為e1,…,ek的任何復(fù)合表達(dá)式e，證明，如果P(ei)（i=1,…,k）都為真，那么P(e)也為真。

形式2證明:對(duì)任何表達(dá)式e，如果P(e)對(duì)e的任何子表達(dá)式e

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

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

1,…,

k，P成立，證明P(

)也為真。

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

1,…,

k延伸出來的一個(gè)證明良基歸納定義：集合A的良基關(guān)系是A上的一個(gè)二元關(guān)系

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

a1

a2

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

i+1，則i

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

A，a

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

a

a

…良基歸納引理1:如果

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

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

A是任意非空子集，用反證法證明B有極小元如果B無極小元，那么對(duì)每個(gè)a

B，可以找到某個(gè)a

B使得a

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

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

a1

a2

…反過來，假定每個(gè)子集有一個(gè)極小元，那么不可能存在a0

a1

a2

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

良基歸納命題（良基歸納）：令

是集合A上的一個(gè)良基關(guān)系，令P是A上的某個(gè)性質(zhì)。若每當(dāng)所有的P(b)(b

a)為真則P(a)為真(a.(b.(b

a

P(b))P(a)))，那么，對(duì)所有的a

A，P(a)為真證明：如果存在某個(gè)x

A使得P(x)成立，那么集合

B{a

A|P(a)}

非空。由引理1，B一定有極小元a

B

但是，對(duì)所有的b

a，P(b)一定成立（否則a不是B的極小元），這和假定

b.(b

a

P(b))P(a)矛盾歸納法總結(jié)表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

的直接子表達(dá)式結(jié)構(gòu)歸納（形式2）e

e

，如果e是e

的子表達(dá)式基于證明的歸納

，如果

是證明

的最后一步推導(dǎo)規(guī)則的某個(gè)前提的證明2.6

演算

演算是1941年Church定義的形式系統(tǒng)，可以作為一個(gè)可計(jì)算性模型的精確定義；可以看作是一個(gè)簡單的、語義清楚的形式語言；具有簡單而又有強(qiáng)大的描述能力，與Turing機(jī)等價(jià)，描述能力相同；可以描述任何一個(gè)部分遞歸函數(shù)的計(jì)算過程；適合用來描述程序設(shè)計(jì)語言的語義；是函數(shù)型程序設(shè)計(jì)語言及指稱語義的理論基礎(chǔ)；LISP語言就是基于

演算(JohnMcCarthy)

演算組成Lambda演算通常包括兩個(gè)部分：合法表達(dá)式(表達(dá)式)的形式系統(tǒng)(語法)變換規(guī)則的形式系統(tǒng)(語義)

表達(dá)式：定義

表達(dá)式由變量名、抽象符號(hào)，.以及括號(hào)等符號(hào)構(gòu)成，其語法為：

<表達(dá)式>::=<變量名> |<表達(dá)式><表達(dá)式>|<變量名>.<表達(dá)式>|(<表達(dá)式>)沒有類型；沒有常量；變量名不僅可以代表變量，還可以代表函數(shù)；

表達(dá)式：施用型和抽象型施用型表達(dá)式(APPLY):E1E2

：函數(shù)調(diào)用，E1是函數(shù)定義，E2是實(shí)參抽象型表達(dá)式(Abstraction):x.E：定義無名函數(shù)，x對(duì)應(yīng)形參,E是函數(shù)體

舉例：xx;x.xy;x(y.xy);x.y.x；

表達(dá)式：施用型和抽象型抽象表達(dá)式

x.E用來表示無名函數(shù)通常，定義函數(shù)的方法是首先定義函數(shù)名，然后再使用它，因此函數(shù)都有名，而抽象表達(dá)式則表示一無名函數(shù)假設(shè)有函數(shù)定義：funcf(x)=x+1則定義了這樣一個(gè)函數(shù)，既函數(shù)名是f，自變量（形參）是x，函數(shù)值是x+1的值當(dāng)然也可用別的方式定義出上述函數(shù)，例如

funcf=x.x+1這種表示法也能方便地表示哪個(gè)是函數(shù)名，哪個(gè)是自變量名，哪部分是函數(shù)體，其中表示其后的變量為自變量

表達(dá)式：施用型和抽象型假設(shè)有f(a*b)，則它應(yīng)等價(jià)于(x.x+1)(a*b)，而其中(x.x+1)和(a*b)都是表達(dá)式，這樣在Lambda表達(dá)式的定義中出現(xiàn)了E1E2形式的表達(dá)式從語義角度來說其中的E1必須是函數(shù)，而E1E2的含義是把函數(shù)E1作用于表達(dá)式E2稱x.E中的E表達(dá)式為函數(shù)x.E的體部分，而稱x為該函數(shù)的自變量

表達(dá)式：記法約定施用型表達(dá)式的左結(jié)合規(guī)則：

E1E2E3

…En=(((E1E2)E3)…)En抽象型表達(dá)式的右結(jié)合規(guī)則：

x1.x2.…xn.E=x1.(x2.(…(xn.E)…))x1x2…xn.E=x1.x2.…xn.Ex1.x2.…xn.E1E2E3…En

=x1.x2.…xn.(E1E2E3…En)

表達(dá)式：語義單從Lambda表達(dá)式的結(jié)構(gòu)本身看不出任何意義，因?yàn)槠渲屑葲]有常量，也沒有函數(shù)名，無法知道如何進(jìn)行計(jì)算究竟如何計(jì)算表達(dá)式值，將由Lambda變換部分來決定如果說Lambda表達(dá)式相當(dāng)于程序，則Lambda變換部分就相當(dāng)于程序的解釋系統(tǒng)

表達(dá)式：子表達(dá)式子表達(dá)式（針對(duì)不同的表達(dá)式形式）設(shè)E是一個(gè)表達(dá)式，則E的子表達(dá)式定義為：Ex，x就是E的子表達(dá)式；EE1E2，E1和E2以及它們的子表達(dá)式都是E的子表達(dá)式；Ex.E’，x.E’以及E’的子表達(dá)式都是E的子表達(dá)式；E(E’)，E’及其子表達(dá)式都是E的子表達(dá)式；用SUB(E)表示E的子表達(dá)式集；

表達(dá)式：作用域

表達(dá)式中變量的作用域：

x.E表達(dá)式中的變量x是被綁定的，它的作用域是體表達(dá)式E中去掉所有形如x.E’子表達(dá)式后的表達(dá)式部分；

x.E表達(dá)式中x.部分可以看作是變量x的定義點(diǎn)，在E中x的定義域中出現(xiàn)變量x為其使用點(diǎn)；舉例：表達(dá)式：y(xy.y(x.xy))(z(x.xx))x的作用域是

y；y的作用域是

y(x.xy)；x的作用域是

xy；x的作用域是

xx；

表達(dá)式：自由出現(xiàn)在表達(dá)式中相同的變量名，可以出現(xiàn)在表達(dá)式的不同位置，它們的含義可能不同；自由出現(xiàn)/約束出現(xiàn)：表達(dá)式E中變量名x的一次出現(xiàn)稱為自由出現(xiàn)，如果E中沒有任何一個(gè)形如x.E’的子表達(dá)式包含該出現(xiàn)；如果存在一個(gè)x.E’的子表達(dá)式包含該出現(xiàn)，稱為約束出現(xiàn)；y(xy.y(x.xy))(z(x.xx))

自由約束約束自由約束出現(xiàn)出現(xiàn)出現(xiàn)出現(xiàn)出現(xiàn)

表達(dá)式：自由變量自由變量：稱x為表達(dá)式E的自由變量，如果E中至少包含一個(gè)x的自由出現(xiàn)；需要區(qū)分的概念：變量：<變量名，含義>，定義點(diǎn)確定變量名：標(biāo)識(shí)符變量的出現(xiàn)：<變量名，位置>自由變量集合：用FV(E)表示E的自由變量集合，則其具體定義為：Ex，F(xiàn)V(x)={x}；EE1E2

，F(xiàn)V(E1E2)=FV(E1)FV(E2)；Ex.E’，F(xiàn)V(x.E’)=FV(E’)–{x}；E(E’)，F(xiàn)V((E’))=FV(E’)

計(jì)算自由變量集合例子表達(dá)式E=y(xy.y(x.xy))(z(x.xx))FV(E)=FV(y(xy.y(x.xy)))FV((z(x.xx)))

=FV(y)FV((xy.y(x.xy)))

FV(z)FV((x.xx))={y}

(

FV(y(x.xy))-{x,y}){z}(FV(xx)-{x})={y,z}

表達(dá)式：閉型表達(dá)式和開型表達(dá)式閉型表達(dá)式：如果一個(gè)表達(dá)式E不包含自由變量，即FV(E)=

,則稱E為閉型表達(dá)式；開型表達(dá)式：如果一個(gè)表達(dá)式E包含自由變量，即FV(E)

,則稱E為開型表達(dá)式；

表達(dá)式：替換替換(Substitution)：設(shè)E和E0是表達(dá)式，x是變量名，

替換E[E0/x]是表示把E中的所有x的自由出現(xiàn)替換成E0。代換的表示形式有多種：[E0/x]E；[E0/x，E]；[x

E0，E]E[E0/x]的計(jì)算規(guī)則為：S1:Ex，x[E0/x]=E0

；S2:Ey，y[E0/x]=y

，x

y

；S3:E(E’)，(E’)[

E0/x]=(E’[

E0/x])S4:EE1E2，E1E2[E0/x]=(E1[E0/x])(E2[E0/x])；S5:Ex.E’，x.E’[

E0/x]=x.E’

；

表達(dá)式：替換S6:Ey.E’，x

y如果E0中沒有y的自由出現(xiàn)，那么直接對(duì)E’進(jìn)行替換即，如果yFV(E0)，則

s6-1:(y.E’)[

E0/x]=y.(E’

[

E0/x])注：（y.E’）中的y和E0中的y是不同的；如果E’中沒有x的自由出現(xiàn)，則表示E’沒有可替換即如果xFV(E’)，則

s6-2:(y.E’)[

E0/x]=y.(E’[

E0/x])=y.E’

表達(dá)式：替換S6:Ey.E’，x

y，如果E0中有y的自由出現(xiàn)，E’中有可替換的x,則需要對(duì)y進(jìn)行改名，改變后的變量名z是不同于y的E0的非自由出現(xiàn)。即如果yFV(E0)xFV(E’)，則

s6-3:(y.E’)[

E0/x]=z.((E’

z/y])[E0/x])，

zFV(E0)，zy基本規(guī)則：只有自由出現(xiàn)的變量才允許被替換，而且替換不應(yīng)該把變量的自由出現(xiàn)變?yōu)榧s束出現(xiàn)。要避免出現(xiàn)(y.x+y)[y/x]=(y.y+y)，正確的替換，自動(dòng)改名：(y.x+y)[y/x]=z.y+z

表達(dá)式：替換例子x[xy/x]=xyS1y[M/x]=yS2x.xy[E/x]=x.xyS3;S5x.xz[w/y]=x.xzS6-2

表達(dá)式：替換例子((x.xyb.xy[a.ab/y]=x.xy[a.ab/y]b.xy[a.ab/y]S4=x.xa.abz.xy[z/b][a.ab/y]S6-1;S6-3=x.xa.abz.xy[a.ab/y]S6-2=x.xa.abz.xa.abS6-1

演算小結(jié)

演算的語法–

表達(dá)式形式定義一些相關(guān)概念子表達(dá)式作用域規(guī)則自由變量替換：是Lambda演算中最重要的一個(gè)概念；后面定義的轉(zhuǎn)換系統(tǒng)都是基于替換的；

演算通常包括兩個(gè)部分：合法表達(dá)式(表達(dá)式)的形式系統(tǒng)(語法)語法結(jié)構(gòu)；自由變量；替換變換規(guī)則的形式系統(tǒng)(語義)回顧

演算的變換系統(tǒng)變換系統(tǒng)給出了如何從一個(gè)表達(dá)式轉(zhuǎn)換成和其等價(jià)的另外一個(gè)表達(dá)式；變換系統(tǒng)定義了演算的語義；實(shí)際上給出了一種計(jì)算規(guī)則；不同的演算系統(tǒng)由不同的變換規(guī)則確定；變換規(guī)則應(yīng)當(dāng)是保結(jié)構(gòu)和保值的；

演算的變換系統(tǒng)給了一個(gè)表達(dá)式即可根據(jù)演算系統(tǒng)的變換規(guī)則進(jìn)行一系列的變換，其結(jié)果有兩種可能:一是不能進(jìn)一步的歸約二是變換無終止地進(jìn)行下去(相當(dāng)于程序不終止)不同的Lambda演算系統(tǒng)具有不同的變換規(guī)則，有的可能只有兩個(gè)變換規(guī)則，有的可能有三個(gè)變換規(guī)則，有的甚至可能有更多的變換規(guī)則這里介紹最常見的Lambda變換規(guī)則

演算的變換系統(tǒng)

--

變換

變換：設(shè)E是表達(dá)式，x是變量，則稱下面變換為α變換（其中y不在FV(x.E)中）

x.Ey.E[y/x]

變換只是改變了x.E型表達(dá)式的形參名；

x.x+y、z.z+y、w.w+y在變換下是等價(jià)的，它們定義的是同一個(gè)函數(shù)；條件：新的形參不是體表達(dá)式的自由變量，否則會(huì)改變函數(shù)的含義；

演算的變換系統(tǒng)

--

變換例子合法的變換

X.(ZX)Y.(ZY)

X.((Y.YX)X)Z.((Y.YZ)Z)

非法的變換

X.(Z(Y.X))Y.(Z(Y.Y))

X.(ZY)Y.(ZY)

演算的變換系統(tǒng)--變換

變換：設(shè)(x.E)和E0為表達(dá)式，則稱下面的變換為β變換（稱β變換規(guī)則的左部表達(dá)式為β基）

(x.E)E0E[E0/x]β變換是最重要的變換，所有演算系統(tǒng)都有β變換。β變換規(guī)則實(shí)際上定義了函數(shù)調(diào)用的語義。

演算的變換系統(tǒng)

--變換的例子(X.XY)XXY(X.XX)YYY(X.(Y.(Z.XYZ)))ABC(Y.(Z.AYZ))BC (Z.ABZ)C ABC

演算的變換系統(tǒng)

--變換

變換：設(shè)x.Mx是一個(gè)表達(dá)式，且滿足條件xFV(M)，則稱下面變換為η變換: (x.Mx)M

變換主要依據(jù)函數(shù)的外延(保值)等價(jià)性定義，即如果對(duì)于任意x,都有f(x)=h(x)，則認(rèn)為f和h

等價(jià)；對(duì)于任意y,xFV(M),(x.Mx)yMyη變換不是演算系統(tǒng)所必需的變換規(guī)則

演算的變換系統(tǒng)

--變換的例子合法變換

X.(Y.YY)X(Y.YY)非法變換

X.(Y.YX)X(Y.YX)

不滿足條件：XFV((Y.YX))

演算的變換系統(tǒng)

--歸約歸約基：(1)β變換的左部表達(dá)式(x.E)E0稱為β基(2)η變換的左部表達(dá)式(x.Mx)稱為η基(3)β基和η基統(tǒng)稱為歸約基歸約：對(duì)表達(dá)式中的某一歸約基施行某種變換稱為歸約；一個(gè)表達(dá)式中可以同時(shí)有多個(gè)歸約基；歸約過程不唯一；不同的歸約過程得到的結(jié)果不一定相同；

演算的變換系統(tǒng)

--歸約過程例子舉例不同的歸約過程得到相同的結(jié)果：表達(dá)式：(

y.y((a.xa)(

a.a))))(b.b)歸約過程1：

(

y.y((a.xa)(

a.a))))(b.b)

(

y.y((x(

a.a)))(b.b)

(

b.b)(x(a.a))

x(a.a)

演算的變換系統(tǒng)

--歸約過程例子舉例不同的歸約過程得到相同的結(jié)果：表達(dá)式：(

y.y((a.xa)(

a.a))))(b.b)歸約過程2：

(

y.y((a.xa)(

a.a))))(b.b)(

b.b)((

a.xa)(

a.a))

(

a.xa)(

a.a)

x(

a.a)

演算的變換系統(tǒng)

--范式范式：設(shè)E是一個(gè)表達(dá)式，且其中沒有任何歸約基，則稱該表達(dá)式為范式。如果一個(gè)表達(dá)式經(jīng)過有限次變換能歸約成范式，則稱該表達(dá)式有范式舉例：

X，XX，X.XX，X(X.XX)是范式

X.X((Y.X)Y)不是范式，因?yàn)橛袣w約基((Y.X)Y)

表達(dá)式有很多，范式是具有相同解釋的最簡表示；

演算的變換系統(tǒng)

--歸約過程一個(gè)表達(dá)式中可包含多個(gè)歸約基，因此，歸約過程不一定唯一，而且不同的歸約過程也可能得到不同的計(jì)算結(jié)果，也可能都得到同一個(gè)結(jié)果。下面是多個(gè)歸約過程得到同一結(jié)果的例子。

x(

a.a)(

b.b)(x(

a.a))(

b.b)(x(

a.a))(

a.xa)(

a.a)(

b.b((

a.xa)(

a.a))(

y.y((

a.xa)(

a.a)))(

b.b)(

y.y((x((

a.a)))(

b.b)

演算的變換系統(tǒng)

--歸約過程下面是多個(gè)歸約過程，并且不同歸約過程得到不同結(jié)果的例:(x.y)((x.xx)(x.xx))如果先歸約(x.xx)(x.xx)，則將無休止地變換下去，但如果先歸約(x.y)(....)部分，則歸約一次即可得到范式y(tǒng)原因是函數(shù)(x.y)并不真正用到實(shí)參值，但如果一定要先計(jì)算實(shí)參，然后再計(jì)算函數(shù)體的值，就會(huì)出現(xiàn)以上問題

演算的變換系統(tǒng)

--歸約過程下面是無范式的例子:(1)(x.xx)(x.xx)(x.xx)(x.xx) ...(不終止)(2)(x.xxx)(x.xxx)(x.xxx)(x.xxx)(x.xxx)(x.xxx)...(不終止)

演算的變換系統(tǒng)

--范式的性質(zhì)定理（Church-Rosser）：如果Ax和Ay成立，則一定存在z使得xz和yz成立。(合流性)證明：(略)定理（范式唯一性）：如果把通過α變換可互換的表達(dá)式視為同一表達(dá)式，那么如果Lambda表達(dá)式E存在范式，則其范式一定唯一證明：設(shè)表達(dá)式E有兩個(gè)范式x和y，則根據(jù)Church-Rosser定理，一定存在表達(dá)式z，使得xz和yz成立。因?yàn)閤和y是范式，只能xz，yz。而α變換是雙向的，因此有xy，也就是說范式x和y是同一種Lambda表達(dá)式。

演算的變換系統(tǒng)

--范式的性質(zhì)定義2.16(標(biāo)準(zhǔn)歸約)：如果每次歸約最左的歸約基，則稱這種歸約為標(biāo)準(zhǔn)歸約。定理2.17：如果表達(dá)式E有范式，則按標(biāo)準(zhǔn)歸約一定能求到其范式。證明:略

演算的變換系統(tǒng)

--范式的性質(zhì)表示法：XY:經(jīng)過有限次變換(α，β，η)，X變換為Y。XrY:經(jīng)過有限次歸約(β，η)，X變換為Y。X

Y:經(jīng)過有限次α變換，X變換為Y。表達(dá)式不一定都有范式范式的唯一性：如果有范式，則在變換下一定唯一范式的存在性：如果有范式，則最左歸約法一定能求出范式標(biāo)準(zhǔn)歸約：最左歸約，按歸約基中符號(hào)的出現(xiàn)順序

演算總結(jié)需要掌握的知識(shí)點(diǎn)表達(dá)式自由變量替換三種變換歸約范式范式的唯一性范式的存在性

演算作為計(jì)算模型Lambda演算系統(tǒng)由Lambda表達(dá)式和Lambda變換規(guī)則組成Lambda變換的主要作用是用來導(dǎo)出表達(dá)式的范式Turing機(jī)系統(tǒng)能夠描述部分遞歸函數(shù)的計(jì)算過程的事實(shí)，在可計(jì)算理論里已得以證實(shí)那么Lambda演算系統(tǒng)有無同樣的功能?結(jié)論是：能

演算作為計(jì)算模型在Turing機(jī)系統(tǒng)里有所謂的“帶”，它是Turing機(jī)的操作對(duì)象，操作結(jié)果將改變帶的內(nèi)容帶由有序“方格”組成，在每個(gè)方格里可寫所允許的符號(hào)帶的內(nèi)容究竟表示什么意思?系統(tǒng)本身并不知道，系統(tǒng)只知道在什么狀態(tài)下做什么動(dòng)作系統(tǒng)只提供一種用于演算的形式規(guī)則，帶的內(nèi)容究竟表示什么只有用戶才知道

演算作為計(jì)算模型在

演算系統(tǒng)中，

表達(dá)式相當(dāng)于Turing機(jī)中的帶，它們扮演著操作對(duì)象的角色Lambda表達(dá)式的結(jié)構(gòu)非常簡單，但它的功能和當(dāng)代計(jì)算機(jī)的功能一樣強(qiáng)大！！

演算作為計(jì)算模型用

演算模擬整數(shù)用

演算模擬加法運(yùn)算

演算的描述能力用

演算模擬整數(shù)正整數(shù)n的表達(dá)式：

n=ab.a(a(……(a(ab))……))n個(gè)簡寫為：

ab.anb0的表達(dá)式：0=ab.b1的表達(dá)式：1=ab.ab2的表達(dá)式：2=ab.a(ab)=ab.a2b

……用

演算模擬加法運(yùn)算加法的表達(dá)式：PLUS=xy.ab.(xa)((ya)b)驗(yàn)證方法：PLUSmn=〉m+nPLUSmn=(xy.ab.(xa)((ya)b))m

n

=〉(y.ab.(m

a)((ya)b))

n

=〉ab.(m

a)((na)b))

=〉

ab.((ab.amb)

a)((na)b))=〉

ab.((b.amb))(((ab.anb)a)b))=〉

ab.((b.amb))(((b.anb))b))=〉

ab.((b.amb))((anb))=〉

ab.(amanb)

=〉

ab.(am+nb)=m+n其他例子乘法布爾值true和false布爾運(yùn)算AND,OR,NOT減法；比較運(yùn)算條件函數(shù)最小不動(dòng)點(diǎn)算子見講義P36-39

演算系統(tǒng)的擴(kuò)充前面介紹了最基本的

演算系統(tǒng)，同時(shí)表明了它能夠描述部分遞歸函數(shù)的計(jì)算過程。其中實(shí)際上只有一種操作，即函數(shù)的施用，即β歸約。但其中連常數(shù)都沒有，因此，用起來很不方便，因此需要擴(kuò)充原來的

演算系統(tǒng)，擴(kuò)充后即可變成可使用的函數(shù)式抽象語言。

演算系統(tǒng)的擴(kuò)充擴(kuò)充的方法：擴(kuò)充表達(dá)式常數(shù)：布爾常量true和false;整數(shù)引進(jìn)標(biāo)準(zhǔn)函數(shù)：add,mul,and,or,equ其他：條件表達(dá)式擴(kuò)充變換系統(tǒng)擴(kuò)充數(shù)據(jù)結(jié)構(gòu):INT,BOOL,REAL……

演算系統(tǒng)的擴(kuò)充一種擴(kuò)充的表達(dá)式見講義P40

2.8論域理論基礎(chǔ)目的：描述類型的數(shù)學(xué)模型；論域理論主要應(yīng)用于函數(shù)式語言中的類型定義，并應(yīng)用于指稱語義學(xué)主要內(nèi)容基本概念：半序集合；完全半序集；平坦集Scott論域及其構(gòu)造問題的提出遞歸定義的解函數(shù)的遞歸定義；類型的遞歸定義；如何確定一個(gè)遞歸（函數(shù)）定義是否有解？確定唯一的解---最小不動(dòng)點(diǎn)什么樣的函數(shù)有最小不動(dòng)點(diǎn)（解）？連續(xù)函數(shù)什么樣的函數(shù)是連續(xù)函數(shù)？定義域和值域是論域滿足一定的條件什么樣的集合是論域，如何得到？完全半序集論域構(gòu)造符最小不動(dòng)點(diǎn)連續(xù)函數(shù)論域完全半序集基本概念半序集(partial-orderedset)最小(大)上(下)界(least(upper)bound)完全半序集(CPO)平坦集半序集定義設(shè)D是一個(gè)集合，是定義在D上的二元關(guān)系，滿足下面性質(zhì)：

自反性：

xD,有xx；傳遞性：

x,y,zD,如果存在xy和yz,則必有xz；反對(duì)稱性：

x,yD,如果存在xy和yx,則必有x=y； 稱

為半序關(guān)系(partialorder)，(D，

)為半序集半序集例子D={1，2}，pow(D)是D的所有子集構(gòu)成的集合，是定義在D上的子集關(guān)系，pow(D)={,{1},{2},{1,2}};

是pow(D)上的半序關(guān)系；(pow(D)

，

)為半序集；可以用圖表示：

{1}{2}{1，2}最小上界(2015-5-15)上/下界：設(shè)(D,

)為任意半序集，而且D’

D,d

D,則子集D’的上界和下界的定義如下：上界：若對(duì)任意d’D’,都有d’d,則稱d為D’的上界；下界：若對(duì)任意d’D’,都有dd’,則稱d為D’的下界；最小上界/最大下界：設(shè)(D,

)為任意半序集，而且D’

D,則子集D’的最小上界和最大下界的定義如下：最小上界：設(shè)d是D’的一個(gè)上界，若對(duì)D’的任意一個(gè)上界d’,都有dd’,則稱d為D’的最小上界，并記為D’；最大下界：設(shè)d是D’的一個(gè)下界，若對(duì)D’的任意一個(gè)下界d’,都有d’d,則稱d為D’的最大下界，并記為D’；最小上界最小上界唯一性：設(shè)(D,

)為任意半序集，而且D’

D。如果子集D’存在最小上界，則定唯一。最大下界也是。最小元