軟件形式化方法第2章 數學基礎

第2章數學基礎2.1命題和謂詞演算

2.2集合和關系2.3函數2.4語法2.5結構歸納2.6

演算2.7論域理論基礎注：本章部分內容具有復習性質2.1命題和謂詞演算命名約定和注釋定義和相等關系表達式中的輔助名字命題演算謂詞演算命題邏輯的回顧合適公式的歸納定義

::=p|(

)|(

)|(

)|(

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

(i)

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

1,2,…,n

可以證明

，表示成

1,2,…,n

|-

, 簡寫成|-

邏輯等價

|-

并且

|-

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

若

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

值也為真,寫成

1,2,…,n

|=

, 簡寫成|=

語義等價

|=

并且

|=

可滿足性

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

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

若

|-

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

|=

成立命題邏輯的完備性

若

|=

成立，則

|-

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

|-

有效，當且僅當

|=

成立謂詞邏輯的回顧合式公式謂詞符號集合

、函數符號集合

（包括常量符號）基于

定義項集

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

,

）的合適公式

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

)|(

)|(

)|(

)|(x

)

|(x

) (P

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

|-

和

|=

的含義與前面的一致

|=

表示

在模型

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

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

1，2，3，4，5

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

集合的運算

集合的并

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

I–A=｛x｜x∈I，｝求補集的運算稱為補（運算）求補集的運算稱為補（運算）

例5.4若I=｛x｜–5﹤x﹤5｝，A=｛x｜0﹤x﹤1｝，求。解：=I–A=｛x｜–5﹤x﹤0∨1﹤x﹤5｝集合的運算集合的乘積集合A1，A2，…，An的乘積一般用法國數學家笛卡爾（ReneDescartes）的名字命名，即笛卡爾積。該乘積表示如下：A1×A2×…An={（a1，a2，…，an）｜ai∈Ai，i＝1，…，n}A1×A2×…An的結果是一個有序元組的集合。例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）}關系關系是一個謂詞，其定義域為k元組的集合。通常的關系為二元關系，其定義域為有序對的集合，在這個集合中，我們說有序對的第一個元素和第二個元素有關系。如學生選課：

學生

課程

成績

張三

文學90

張三

哲學95

李四

數學80

李四

藝術85

王五

歷史92

王五

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

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

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

X→Y{r：X

Y|

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

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

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

{f：X→Y|finite(domf)}定義有限函數的一種方式是列出對論域的每個變元所取的值這類似于由外延定義有限集合

由表達式定義函數對于集合，還可由概括定義，即由特征性質而不是由枚舉來定義對于函數，等價的機制是，由形式變元上的表達式定義一個函數，對任何實在變元的值，由這個值代替形式變元可得到相應的函數值例子：函數的基調f：--對一個函數f：--對一個全函數注意不要把f：和S

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

，那么：

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

兩個函數的并可能不是一個函數關系這種現象發(fā)生在兩個函數的論域相交，并且它們中至少在一個變元上不一致的情況下例如，對于3.2節(jié)的f1和f2，它們對c的值有沖突，因此,不是一個函數（b的兩個函數值不會引起問題，因為它們一樣）

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

，使得：

domh=Adomf并且對adom

h，h(a)=f(a)換句話說，f\A和f是一樣的函數，但是它的源集被限制到A函數的合成函數上的另一種運算是合成，它可以推廣到關系上中綴算符作為函數在處理函數時，還有一種約定將是有用的在普通的數學和程序設計語言中，許多二元函數使用中綴記號，也就是說，一個算符放在兩個變元的中間而不是它們的前面

謂詞和商運算特征函數

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

平行作用平行作用是基調為：的泛函對任意函數f：U—>X和g：V—>Y，f＃g是函數:換句話說，f＃g平行地把f和g分別作用于出自U的一個變元和出自V的一個變元，產生X×Y的一個二元組。

curry另一個重要的泛函是curry（以數學家H.B.Curry命名）。這個泛函把任意的兩個變元的函數翻譯成一個變元的函數，后者的結果也是一個變元的函數。curry本身的基調是：

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

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

Tright_hand_side

聚集產生式一個聚集產生式定義一個構造，它的實例有固定數目的帶標志成分例如，可以通過下面的Meta聚集產生式定義表示條件命令的抽象構造：

Conditional

thenbranch：Command；

elsebranch：Command；

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

Variable

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

CommandΔSkip|Assignment|Compound|Loop表產生式

一個構造可以定義為另一個構造的實例序列的集合，序列長度大于或等于零，表產生式對應這種情況例如，Pascal中的復合語句可以有下面的產生式定義：

Compound

Command*Compound的實例是零個、一個或多個命令的序列如果一個構造的實例是至少有一個元素的表，那么星號由加號代替例如：

NumberΔDigit＋預定義的構造

如果文法定義的是實際語言，那么它的所有構造最終需要由最基本的且意義明確的集合（即終結構造）來定義在Meta中用的四個預定義的終結構造，對應到標準的數學集合：非負整數集：N整數集：Z布爾值集：B字符串集：S一個完整的抽象文法

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

這個文法是遞歸定義的例如，Command的一種選擇是Conditional；后者是一個聚集，有兩個Command成分這樣的循環(huán)定義是否有意義？定義符號“Δ”在這里的使用是否正確？這些問題在后面回答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抽象語法表達式我們需要一種方式描述和操作遵守某抽象文法的程序，為此，Meta提供了抽象語法表達式。各種抽象語法表達式對應到各類抽象語法產生式。

聚集構造實例的表達式選擇構造實例的表達式表構造實例的表達式終結類型的表達式復雜語法的表達式

聚集構造實例的表達式我們需要一種方式描述和操作遵守某抽象文法的程序。為此，Meta提供了抽象語法表達式。各種抽象語法表達式對應到各類抽象語法產生式、先從聚集構造開始?？紤]一個聚集產生時，例如，Kernel文法的第一個產生式

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

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

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

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

caseiof

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

end

選擇構造實例的表達式右部表達式(skip_exp，assign_exp等）可以叫做“分支表達式”，這種分支表達式通常引用分情形變量I例如，assign_exp可以引用i.target和i.source。為了使這樣的記號有意義，必須把assign_exp中出現的i看成是Assignment類型而不是Command類型表構造實例的表達式考慮表產生式，例如：

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

結構編輯器

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

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

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

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

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

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

前面的抽象語法用非形式的定義引入了構造和抽象語法表達式等概念及相應的Meta表示法下面討論它們的數學含義對于三類產生式的每一種，我們不僅應為對應的產生式的右部提供數學模型，而且應為定義在相應構造的實例上的運算提供適當的解釋模型基于初等集合論，它們把每種構造解釋為一個集合，它的成員是該構造的實例，每種在實例上的運算看成是在對應集合成員上的運算基于抽象語法的語義定義

聚集可以表示為“帶標記的笛卡兒積”。這種集合對處理元組是方便的，因為元組的每個成分都被命名，增強了可讀性。例：見講義P20基于抽象語法的語義定義

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

”，使得結果集合的每個成員能指示它自己源于哪個集合。

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

表可以采用“遞歸定義”例：見講義P22復雜的語法表達式

反復使用上面的機制，可以構造出各種表達式來表示抽象的語法結構。對于復雜的表達式，使用輔助表達式可以使它們更清楚。例：見講義P22從上面的例子可以看出，對于復雜的表達式，抽象語法記號顯得有些笨拙。抽象語法是對程序進行推理的形式工具，而不是程序的可讀性的表示方法。對于后者，很顯然，標準的具體語法是恰當的選擇。2.5結構歸納

用于定義復雜對象的集合和證明這樣的對象的性質，叫做結構歸納對定義語言的結構并證明其性質特別有用Lisp的S表達式（作為該語言的數據和程序結構的基礎）提供了由結構歸納到對象的典型例子結構歸納：例子

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

更一般地，一個結構歸納定義定義一個集合S，其成員屬于下面兩種情況之一：

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

(2)由S先前的成員，經一種或多種明確定義的機制推導出來（如上面帶括號和點的形式）。這樣的定義有清楚的數學解釋，定義的這個集合S是一個無限集合族的并

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

例如，在S表達式中，S0是原子的集合；S1是形式為(a.b)的對象的集合，其中a和b是原子，S2也是形式為(a.b)的對象的集合，但是其中a和b在原子集中或者在S1中；等等某些對象可能出現在不同的Si中（事實上，在S表達式的例子中，每個Si是Si+1的子集），這不會引起問題。因為S定義為所有Si的并，因而S的成員來自哪個Si是無關緊要的。按這種觀點，結構歸納是通常的自然數歸納的直截了當的應用，歸納定義的是集合Si的序列。結構歸納證明

由結構歸納定義的集合有助于按同樣的方式組織證明。為了用結構歸納證明S的所有成員滿足某個性質p，可以按下面兩步進行：

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

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

這種歸納技術的有效性可以從普通的自然數歸納證明的有效性得出：“一個結構歸納證明直截了當地相當于用自然數歸納法證明性質：p(i；N)p(i；N)?“Si的所有成員滿足某個性質p”結構歸納證明：例

用結構歸納證明每個S表達式有相等個數的開括號和閉括號。這個證明包含兩部分：

(1)原子沒有括號，因此滿足這個性質；

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

n1,n2,

…,nk

m1,m2,

…,mliffk<l或者k

l并且存在一個

i

k，使得對所有的

j<i有

nj

mj

并且ni

<mi

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

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

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

=def

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

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

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

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

1,…,

k，P成立，證明P(

)也為真。

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

1,…,

k延伸出來的一個證明良基歸納定義：集合A的良基關系是A上的一個二元關系

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

a1

a2

…例：在自然數上定義，如果j

i+1，則i

j，則這個關系是一個良基關系良基關系的一些特點良基關系不一定有傳遞性良基關系都是非自反的，即對任何a

A，a

a不成立；否則會出現無窮遞減序列a

a

a

…良基歸納引理1:如果

是集合A上的二元關系，那么

是良基的，當且僅當A的每個非空子集都有一個極小元證明:令B

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

B，可以找到某個a

B使得a

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

B開始，構造一個無窮遞減序列a0

a1

a2

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

a1

a2

…，因為該序列給出了無極小元的集合{a0,a1,a2,…}

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

是集合A上的一個良基關系，令P是A上的某個性質。若每當所有的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，B一定有極小元a

B

但是，對所有的b

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

b.(b

a

P(b))P(a)矛盾歸納法總結表1.1常用歸納形式的良基關系歸納形式良基關系自然數歸納（形式1）m

n，如果m+1

n自然數歸納（形式2）m

n，如果m

n結構歸納（形式1）e

e

，如果e是e

的直接子表達式結構歸納（形式2）e

e

，如果e是e

的子表達式基于證明的歸納

，如果

是證明

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

演算

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

演算(JohnMcCarthy)

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

表達式：定義

表達式由變量名、抽象符號，.以及括號等符號構成，其語法為：

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

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

：函數調用，E1是函數定義，E2是實參抽象型表達式(Abstraction):x.E：定義無名函數，x對應形參,E是函數體

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

表達式：施用型和抽象型抽象表達式

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

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

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

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

E1E2E3

…En=(((E1E2)E3)…)En抽象型表達式的右結合規(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)

表達式：語義單從Lambda表達式的結構本身看不出任何意義，因為其中既沒有常量，也沒有函數名，無法知道如何進行計算究竟如何計算表達式值，將由Lambda變換部分來決定如果說Lambda表達式相當于程序，則Lambda變換部分就相當于程序的解釋系統(tǒng)

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

表達式：作用域

表達式中變量的作用域：

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

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

y；y的作用域是

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

xy；x的作用域是

xx；

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

自由約束約束自由約束出現出現出現出現出現

表達式：自由變量自由變量：稱x為表達式E的自由變量，如果E中至少包含一個x的自由出現；需要區(qū)分的概念：變量：<變量名，含義>，定義點確定變量名：標識符變量的出現：<變量名，位置>自由變量集合：用FV(E)表示E的自由變量集合，則其具體定義為：Ex，FV(x)={x}；EE1E2

，FV(E1E2)=FV(E1)FV(E2)；Ex.E’，FV(x.E’)=FV(E’)–{x}；E(E’)，FV((E’))=FV(E’)

計算自由變量集合例子表達式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}

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

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

,則稱E為開型表達式；

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

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

E0，E]E[E0/x]的計算規(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’

；

表達式：替換S6:Ey.E’，x

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

s6-1:(y.E’)[

E0/x]=y.(E’

[

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

s6-2:(y.E’)[

E0/x]=y.(E’[

E0/x])=y.E’

表達式：替換S6:Ey.E’，x

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

s6-3:(y.E’)[

E0/x]=z.((E’

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

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

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

表達式：替換例子((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

演算小結

演算的語法–

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

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

演算的變換系統(tǒng)變換系統(tǒng)給出了如何從一個表達式轉換成和其等價的另外一個表達式；變換系統(tǒng)定義了演算的語義；實際上給出了一種計算規(guī)則；不同的演算系統(tǒng)由不同的變換規(guī)則確定；變換規(guī)則應當是保結構和保值的；

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

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

--

變換

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

x.Ey.E[y/x]

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

x.x+y、z.z+y、w.w+y在變換下是等價的，它們定義的是同一個函數；條件：新的形參不是體表達式的自由變量，否則會改變函數的含義；

演算的變換系統(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)--變換

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

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

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

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

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

--變換

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

變換主要依據函數的外延(保值)等價性定義，即如果對于任意x,都有f(x)=h(x)，則認為f和h

等價；對于任意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)β變換的左部表達式(x.E)E0稱為β基(2)η變換的左部表達式(x.Mx)稱為η基(3)β基和η基統(tǒng)稱為歸約基歸約：對表達式中的某一歸約基施行某種變換稱為歸約；一個表達式中可以同時有多個歸約基；歸約過程不唯一；不同的歸約過程得到的結果不一定相同；

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

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

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)

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

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)

--范式范式：設E是一個表達式，且其中沒有任何歸約基，則稱該表達式為范式。如果一個表達式經過有限次變換能歸約成范式，則稱該表達式有范式舉例：

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

X.X((Y.X)Y)不是范式，因為有歸約基((Y.X)Y)

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

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

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

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)

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

演算的變換系統(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)

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

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

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

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

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

Y:經過有限次α變換，X變換為Y。表達式不一定都有范式范式的唯一性：如果有范式，則在變換下一定唯一范式的存在性：如果有范式，則最左歸約法一定能求出范式標準歸約：最左歸約，按歸約基中符號的出現順序

演算總結需要掌握的知識點表達式自由變量替換三種變換歸約范式范式的唯一性范式的存在性

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

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

演算作為計算模型在

演算系統(tǒng)中，

表達式相當于Turing機中的帶，它們扮演著操作對象的角色Lambda表達式的結構非常簡單，但它的功能和當代計算機的功能一樣強大??！

演算作為計算模型用

演算模擬整數用

演算模擬加法運算

演算的描述能力用

演算模擬整數正整數n的表達式：

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

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

……用

演算模擬加法運算加法的表達式：PLUS=xy.ab.(xa)((ya)b)驗證方法：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布爾運算AND,OR,NOT減法；比較運算條件函數最小不動點算子見講義P36-39

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

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

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

演算系統(tǒng)的擴充擴充的方法：擴充表達式常數：布爾常量true和false;整數引進標準函數：add,mul,and,or,equ其他：條件表達式擴充變換系統(tǒng)擴充數據結構:INT,BOOL,REAL……

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

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

自反性：

xD,有xx；傳遞性：

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

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

為半序關系(partialorder)，(D，

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

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

，

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

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

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

D,d

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

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

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

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

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