數(shù)學(xué)形式語義學(xué)之論域基礎(chǔ)課件

形式語義學(xué)FormalSemanticsofProgrammingLanguages2011.09形式語義學(xué)FormalSemantics內(nèi)容回顧形式語義學(xué)什么是形式語義學(xué)？形式語義學(xué)的分類；程序設(shè)計語言的基本概念語法和語義不同程序設(shè)計范例及其特點(diǎn)命令式語言不同結(jié)構(gòu)的抽象語法定義2023/1/42內(nèi)容回顧形式語義學(xué)2022/12/282形式語義學(xué)的分類從不同角度研究程序的含義操作語義：用機(jī)器模型語言來解釋語言語義。即設(shè)定一個抽象機(jī)，用語言成分在該機(jī)器上的執(zhí)行來解釋語言成分的含義。（實(shí)現(xiàn)或執(zhí)行）指稱語義：采用形式系統(tǒng)方法，用相應(yīng)的數(shù)學(xué)對象對一個語言的語義進(jìn)行注釋?？紤]每個語言成分的執(zhí)行效果(數(shù)學(xué)對象-指稱)；（效果）公理語義：把程序設(shè)計語言視為一個數(shù)學(xué)對象，建立它的公理系統(tǒng)，在此基礎(chǔ)上對程序進(jìn)行推理驗證。從而使程序設(shè)計語言具有堅實(shí)的邏輯基礎(chǔ)。（邏輯）代數(shù)語義：采用代數(shù)的方法進(jìn)行語義注釋的方法。主要基于范疇論、類別代數(shù)理論、抽象數(shù)據(jù)類型；（數(shù)據(jù)和操作行為）2023/1/43形式語義學(xué)的分類從不同角度研究程序的含義2022/12/28程序設(shè)計語言的基本概念詞法(lexeme)定義語言所允許的單詞的種類及其構(gòu)成(spelling)標(biāo)識符，保留字，整數(shù)，實(shí)數(shù)等語法(syntax)定義程序所允許的語法結(jié)構(gòu)(grammar)表達(dá)式，語句，聲明，函數(shù)等語義(semantics)定義語法結(jié)構(gòu)正確的程序的含義(meaning)重復(fù)聲明，作用域，類型檢查等2023/1/44程序設(shè)計語言的基本概念詞法(lexeme)2022/12/2第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)2.2Lambda演算2.3函數(shù)式抽象語言2.4函數(shù)式抽象語言的應(yīng)用

2023/1/45第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)2022/12第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialorderset,CPO)2.1.2連續(xù)函數(shù)(continuousfunctions)2.1.3最小不動點(diǎn)(leastfixedpoint)2023/1/46第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)(Domain第二章函數(shù)式抽象描述方法2.2Lambda演算(calculus)2.2.1Lambda演算介紹表達(dá)式自由變量freevariables(FV)替換substitution變換規(guī)則conversionrules歸約reduction2.2.2Lambda演算作為計算模型2.2.3Lambda演算系統(tǒng)的擴(kuò)充2023/1/47第二章函數(shù)式抽象描述方法2.2Lambda演算(ca第二章函數(shù)式抽象描述方法2.3函數(shù)式抽象語言2.3.1函數(shù)式語言概述2.3.2類型及其操作2.3.3無模式表達(dá)式2.3.4模式及其模式匹配2.3.5基于模式的純函數(shù)式語言2023/1/48第二章函數(shù)式抽象描述方法2.3函數(shù)式抽象語言2022/12.1.1完全半序集---半序集定義(半序集)

設(shè)D是一個集合，?是定義在D上的二元關(guān)系，?滿足下面性質(zhì)：自反性：xD,有x?x;傳遞性：x,y,zD,若有x?y和y?z，則必有x?z；反對稱性：x,y,zD,若有x?y和y?x，則必有x=y；稱?為半序關(guān)系(partial_orderrelation),(D，?)為半序集(partial_orderset)2023/1/492.1.1完全半序集---半序集定義(半序集)2022/半序集例1D={1，2}，pow(D)是D的所有子集構(gòu)成的集合，是定義在D上的子集關(guān)系，pow(D)={,{1},{2},{1,2}}是pow(D)上的半序關(guān)系；(pow(D)，)為半序集；可以用圖表示：2023/1/410{1}{2}{1，2}半序集例12022/12/2810{1}{2}{1，2}半序集例2數(shù)學(xué)上的和構(gòu)成半序關(guān)系集合A上的恒等關(guān)系IA是A上的半序關(guān)系正整數(shù)集合上的整除關(guān)系也是半序關(guān)系和不能構(gòu)成半序關(guān)系2023/1/411半序集的特點(diǎn)是：不要求對于半序集中的任意兩個元素都有半序關(guān)系，即允許有些元素之間不存在半序關(guān)系！若半序集(D,?)中的任意兩個元素之間都存在半序關(guān)系，則稱(D,?)為全序集。

半序集例22022/12/2811半序集的特點(diǎn)是：不要求對于最小上屆上/下界：設(shè)(D,?)為任意半序集，而且D’D,dD,則子集D’的上界和下界的定義如下：上界：若對任意d’D’,都有d’?d,則稱d為D’的上界；下界：若對任意d’D’,都有d?d’,則稱d為D’的下界；最小上界/最大下界：設(shè)(D,?)為任意半序集，而且D’D,則子集D’的最小上界和最大下界的定義如下：最小上界：設(shè)d是D’的一個上界，若對D’的任意一個上界d’,都有d?d’,則稱d為D’的最小上界，并記為D’；最大下界：設(shè)d是D’的一個下界，若對D’的任意一個下界d’,都有d’?d,則稱d為D’的最大下界，并記為D’；2023/1/412最小上屆上/下界：設(shè)(D,?)為任意半序集，而且D’D,特殊元素及其性質(zhì)下界、上界、最大下界、最小上界不一定存在下界、上界存在不一定惟一最大下界、最小上界如果存在，則惟一最小元：設(shè)(D,?)為任意半序集,dD,如果對于任意D中的元素d’都有d?d’，則稱d為D的最小元。集合的最小元就是它的最大下界，最大元就是它的最小上界；反之不對.

2023/1/413特殊元素及其性質(zhì)下界、上界、最大下界、最小上界不一定存在20半序集的特殊元素例3設(shè)<D,?>是偏序集，其中D={a,b,c,d,e,f,g,h},?={<b,d>,<b,e>,<b,f>,<c,d>,<c,e>,<c,f>,<d,f>,<e,f>,<g,h>}∪ID

設(shè)A＝{b,c,d},求A的下界、上界、最大下界、最小上界.2023/1/414A的下界和最大下界都不存在，A也沒有最小元上界有d和f,最小上界為d.半序集的特殊元素例3設(shè)<D,?>是偏序集，其中2022/鏈，遞增鏈，遞減鏈定義鏈設(shè)<D,?>為任意半序集,<X0,X1,…,Xn,…>

是D上的一個序列，簡記為{Xi},則遞增鏈和遞減鏈定義如下：遞增鏈：若對任意i都有Xi?Xi+1

，則稱序列{Xi}為遞增鏈；遞減鏈：若對任意i都有Xi+1?Xi

，則稱序列{Xi}為遞減鏈；鏈的最小上屆記為：{Xi}或

iXi

或Xi

2023/1/415鏈，遞增鏈，遞減鏈定義鏈2022/12/28152.1.1完全半序集定義完全半序集(completepartialorderset,CPO)設(shè)<D,?>為一個半序集,若滿足下面兩個條件，則稱<D,?>為完全半序集：D有最小元；對于D的任一遞增鏈

{Xi}都有最小上屆{Xi}。2023/1/4162.1.1完全半序集定義完全半序集(complete2.1.1完全半序集例4

完全半序集如果D是任意有窮整數(shù)集，是定義在D上的小于等于關(guān)系，則(D,)為完全半序集；有最小元的有窮半序集是完全半序集；如果D表示開區(qū)間(a,b)，其中a和b是實(shí)數(shù)，則(D,)不是完全半序集；2023/1/4172.1.1完全半序集例4完全半序集2022/12/282.1.1完全半序集為什么引入完全半序集？在形式地描述程序設(shè)計語言的語義時(指稱語義方法)，要求所考慮的集合都滿足完全半序集的條件；建立論域的數(shù)學(xué)模型：滿足一定條件的定義了關(guān)系的集合(完全半序集)；如何構(gòu)造完全半序集？平坦集一定是完全半序集擴(kuò)展任意集合為平坦集的方法非常簡單

2023/1/4182.1.1完全半序集為什么引入完全半序集？2022/12/平坦集定義平坦集設(shè)<D,?>為一個半序集,若滿足下面兩個條件，則稱<D,?>為平坦半序集(平坦集)：D有最小元；只有下面的關(guān)系(平坦關(guān)系)：?，?d，d?d,其中d是D中非的元素。2023/1/419……平坦集定義平坦集2022/12/2819……平坦集擴(kuò)展任意一個集合為平坦集的方法任意一個集合D;引進(jìn)一個最小元D；在集合D’=D{D}上定義平坦關(guān)系?：

D

?D，D?d，d?d；<D’,?>為一個平坦集，簡記為D

；2023/1/420性質(zhì)：平坦集一定是完全半序集。平坦集擴(kuò)展任意一個集合為平坦集的方法2022/12/2820平坦集的例子例5D={{1},{1,2},{1,3}},關(guān)系是集合包含關(guān)系，則(D,)是一個平坦集；其中最小元是{1};BOOL={true,false},可以擴(kuò)充為平坦集：引入最小元；定義一個平坦關(guān)系?：?

,?

true,?

false,true?

true,false?

false；則(BOOL

,?)是平坦集2023/1/421平坦集的例子例5D={{1},{1,2},{1,3論域問題引子試編制一個程序?qū)崿F(xiàn)下面有限自動機(jī)的功能。2023/1/422XBA100011論域問題引子試編制一個程序?qū)崿F(xiàn)下面有限自動機(jī)的功能。2022state=‘X’;readone(ch);whilech’#’doifch=‘1’thenout(state)elseifstate=‘X’thenstate=‘A’elseifstate=‘A’thenstate=‘B’elseifstate=‘B’thenstate=‘A’elseskipfififi;fi;readone(ch);od

2023/1/423XBA100011可將程序看作是一個函數(shù)，函數(shù)：定義域值域即輸入到輸出的映射。程序的編者主觀上認(rèn)定輸入域是{0，1，#}，其實(shí)還可以輸入其它字符。顯然，一個正確的程序設(shè)計必須給出在輸入不是集合{0，1，#}中的一個元素時，應(yīng)指出是“無定義”的錯誤處理。

----論域做大了state=‘X’;2022/12/2823XBA100論域引入目的：描述類型的數(shù)學(xué)模型；指稱語義學(xué)和函數(shù)式語言中都要用到。Scott論域及其構(gòu)造2023/1/424論域引入目的：2022/12/2824Scott論域及其構(gòu)造論域(Domain)：定義了關(guān)系的,滿足一定條件的集合(CPO)；論域分為原始域和非原始域(構(gòu)造域)原始域：有限集或可枚舉集都是原始域{true,false},{…,-1,0,1,…}

非原始域：可以從已知論域，應(yīng)用論域構(gòu)造符進(jìn)行構(gòu)造。2023/1/425可以證明，如果每個成分是完全半序集，則保證構(gòu)造符作用后得到的仍然是完全半序集.Scott論域及其構(gòu)造論域(Domain)：2022/12/論域構(gòu)造符設(shè)(Di,?i)是完全半序集,i=1,…,n,則我們定義了如下論域構(gòu)造符：,+,*和，通過它們的作用可以得到新的論域；(1)元組域(乘積域或卡氏域)(D1…Dn,?)定義如下:D1…Dn={(d1,…,dn)|diDi,i=1,…,n}；關(guān)系?

：(d1,…,dn)?

(d1’,…,dn’)當(dāng)且僅當(dāng)di?i

di’，i=1,…,n；稱為n元組域，簡記為[D1…Dn]或D1…Dn最小元：(D1，…，Dn

)對應(yīng)沒有域名的結(jié)構(gòu)類型(struct)

2023/1/426論域構(gòu)造符設(shè)(Di,?i)是完全半序集,i=1,元組域的例子例6：{1，2}BOOLD1={1，2}，1?1，1?2，2?2(整數(shù)上的)D2=BOOL，false?bfalse，false?btrue，true?btrue集合：D={(1,true),(1,false),(2,true),(2,false)}關(guān)系：?x:自身:(1,true)?x(1,true),….

(1,false)?x(1,true),(2,false)?x(2,true)

(1,true)?x(2,true),(1,false)?x(2,false)

(1,false)?x(2,true)最小元：(1,false)2023/1/427元組域的例子例6：{1，2}BOOL2022/12/2論域構(gòu)造符(2)聯(lián)合域

(D1…Dn,?)定義如下:D1…Dn={(j,dj)|djDj,j=1,…,n}{}；關(guān)系?

：

?

;

?(j,dj);(i,di)?(j,dj)當(dāng)且僅當(dāng)i=j而且di?i

dj，

i(j)=1,…,n；簡記為[D1…Dn］或D1…Dn最小元：對應(yīng)聯(lián)合類型(union)2023/1/428論域構(gòu)造符(2)聯(lián)合域(D1…Dn,?)定義如下聯(lián)合域的例子例7：{1，2}BOOLD1={1，2}，1?1，1?2，2?2(整數(shù)上的)D2=BOOL，false?bfalse，false?btrue，true?btrue集合：D={(1,1),(1,2),(2,true),(2,false),}關(guān)系：?+:自身:(1,1)?+(1,1),….

(1,1)?+(1,2),(2,false)?+(2,true)

?+i{(1,1),(1,2),(2,true),(2,false)}最小元：

2023/1/429聯(lián)合域的例子例7：{1，2}BOOL2022/12/2論域構(gòu)造符(3)序列域

(D*

,?)定義如下:D*

={<d1,…,dn>|diDi

,n0,i=1,2,…};關(guān)系?

：

<>

?<>;

<>

?<d1,…,dn>;<d1,…,dn>?<d1’,…,dm’>,當(dāng)且僅當(dāng)n=m而

且di?i

di’

,i=1,…,n；簡記為D*最小元：<>對應(yīng)表類型2023/1/430論域構(gòu)造符(3)序列域(D*,?)定義如下:2022序列域的例子例8：{1，2}*D1={1，2}，1?1，1?2，2?2(整數(shù)上的)集合：D={<>,<1>,<2>,<1,1>,<1,2>,……}關(guān)系：?*:自身:<>?*<>,<1>?*<1>….元素個數(shù)相同的序列之間滿足條件的關(guān)系有：<1>?*<2>,<1,1>?*<1,2>,<1,1>?*<2,2>,<1,2>?*<2,2>,<1,1,1>?*<2,2,2>,<1,1,1>?*<1,2,1>,……最小元：

<>2023/1/431序列域的例子例8：{1，2}*2022/12/2831論域構(gòu)造符(4)函數(shù)空間

(DD’

,?)定義如下:DD’

={f|dD,f(d)=d’D’};關(guān)系?

：對于任意f,h

[DD’]，f?h,當(dāng)且僅當(dāng)dD，f(d)?D

h(d)簡記為[DD’]或DD’最小元：dD，

(d)=D2023/1/432論域構(gòu)造符(4)函數(shù)空間(DD’,?)定義如下:2函數(shù)域的例子例9：{1，2}BOOLD1={1，2}，1?1，1?2，2?2(整數(shù)上的)D2=BOOL，false?bfalse，false?btrue，true?btrue集合：函數(shù)的集合，其中每個函數(shù)的定義域是D1，值域是D2；{f1,f2,f3,f4}f1={1false,2false}f2={1false,2true}f3={1true,2false}f4={1true,2true}關(guān)系：?f:自身:f1?ff1,f2?ff2….f?fg:應(yīng)滿足f(1)?fg(1),f(2)?fg(2)，即f1?ff2,f1?ff3,f1?ff4,f2?ff4,f3?ff4最小元：

=f12023/1/433函數(shù)域的例子例9：{1，2}BOOL2022/12/28論域表達(dá)式語法定義原始域是完全半序集，則論域表達(dá)式定義的集合仍然是完全半序集。通常表示論域時就把關(guān)系省略掉了。2023/1/434<論域表達(dá)式>::=<原始域>|<論域表達(dá)式><論域表達(dá)式>|<論域表達(dá)式>+<論域表達(dá)式>|<論域表達(dá)式><論域表達(dá)式>|<論域表達(dá)式>*|<論域表達(dá)式>論域表達(dá)式語法定義2022/12/2834<論域表達(dá)式>:論域舉例形式語義學(xué)研究的論域可以是數(shù)據(jù)域、字符域、布爾域、函數(shù)域、表域等，其中函數(shù)域也稱函數(shù)空間最為復(fù)雜；原始域是完全半序集，則論域表達(dá)式定義的集合仍然是完全半序集。通常表示論域時就把關(guān)系省略掉了。2023/1/435基本域(原始域)：INT,BOOL,[x,y]…集合域：{a1,…,an}{}元組域：INTBOOL聯(lián)合域：BOOL+REAL序列域:(INTBOOL)*函數(shù)域(函數(shù)空間)：INT*INTBOOL

論域舉例形式語義學(xué)研究的論域可以是數(shù)據(jù)域、字符域、布爾域、函總結(jié)知識點(diǎn)：基本概念完全半序集平坦集論域及其構(gòu)造符任何一個集合可以擴(kuò)展成平坦集，因此任何一個集合可以擴(kuò)展成一個完全半序集；論域理解為完全半序集；通過論域構(gòu)造符定義的仍然是完全半序集；論域用于定義數(shù)據(jù)類型；2023/1/436總結(jié)知識點(diǎn)：2022/12/2836形式語義學(xué)FormalSemanticsofProgrammingLanguages2011.09形式語義學(xué)FormalSemantics內(nèi)容回顧形式語義學(xué)什么是形式語義學(xué)？形式語義學(xué)的分類；程序設(shè)計語言的基本概念語法和語義不同程序設(shè)計范例及其特點(diǎn)命令式語言不同結(jié)構(gòu)的抽象語法定義2023/1/438內(nèi)容回顧形式語義學(xué)2022/12/282形式語義學(xué)的分類從不同角度研究程序的含義操作語義：用機(jī)器模型語言來解釋語言語義。即設(shè)定一個抽象機(jī)，用語言成分在該機(jī)器上的執(zhí)行來解釋語言成分的含義。（實(shí)現(xiàn)或執(zhí)行）指稱語義：采用形式系統(tǒng)方法，用相應(yīng)的數(shù)學(xué)對象對一個語言的語義進(jìn)行注釋。考慮每個語言成分的執(zhí)行效果(數(shù)學(xué)對象-指稱)；（效果）公理語義：把程序設(shè)計語言視為一個數(shù)學(xué)對象，建立它的公理系統(tǒng)，在此基礎(chǔ)上對程序進(jìn)行推理驗證。從而使程序設(shè)計語言具有堅實(shí)的邏輯基礎(chǔ)。（邏輯）代數(shù)語義：采用代數(shù)的方法進(jìn)行語義注釋的方法。主要基于范疇論、類別代數(shù)理論、抽象數(shù)據(jù)類型；（數(shù)據(jù)和操作行為）2023/1/439形式語義學(xué)的分類從不同角度研究程序的含義2022/12/28程序設(shè)計語言的基本概念詞法(lexeme)定義語言所允許的單詞的種類及其構(gòu)成(spelling)標(biāo)識符，保留字，整數(shù)，實(shí)數(shù)等語法(syntax)定義程序所允許的語法結(jié)構(gòu)(grammar)表達(dá)式，語句，聲明，函數(shù)等語義(semantics)定義語法結(jié)構(gòu)正確的程序的含義(meaning)重復(fù)聲明，作用域，類型檢查等2023/1/440程序設(shè)計語言的基本概念詞法(lexeme)2022/12/2第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)2.2Lambda演算2.3函數(shù)式抽象語言2.4函數(shù)式抽象語言的應(yīng)用

2023/1/441第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)2022/12第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialorderset,CPO)2.1.2連續(xù)函數(shù)(continuousfunctions)2.1.3最小不動點(diǎn)(leastfixedpoint)2023/1/442第二章函數(shù)式抽象描述方法2.1論域理論基礎(chǔ)(Domain第二章函數(shù)式抽象描述方法2.2Lambda演算(calculus)2.2.1Lambda演算介紹表達(dá)式自由變量freevariables(FV)替換substitution變換規(guī)則conversionrules歸約reduction2.2.2Lambda演算作為計算模型2.2.3Lambda演算系統(tǒng)的擴(kuò)充2023/1/443第二章函數(shù)式抽象描述方法2.2Lambda演算(ca第二章函數(shù)式抽象描述方法2.3函數(shù)式抽象語言2.3.1函數(shù)式語言概述2.3.2類型及其操作2.3.3無模式表達(dá)式2.3.4模式及其模式匹配2.3.5基于模式的純函數(shù)式語言2023/1/444第二章函數(shù)式抽象描述方法2.3函數(shù)式抽象語言2022/12.1.1完全半序集---半序集定義(半序集)

設(shè)D是一個集合，?是定義在D上的二元關(guān)系，?滿足下面性質(zhì)：自反性：xD,有x?x;傳遞性：x,y,zD,若有x?y和y?z，則必有x?z；反對稱性：x,y,zD,若有x?y和y?x，則必有x=y；稱?為半序關(guān)系(partial_orderrelation),(D，?)為半序集(partial_orderset)2023/1/4452.1.1完全半序集---半序集定義(半序集)2022/半序集例1D={1，2}，pow(D)是D的所有子集構(gòu)成的集合，是定義在D上的子集關(guān)系，pow(D)={,{1},{2},{1,2}}是pow(D)上的半序關(guān)系；(pow(D)，)為半序集；可以用圖表示：2023/1/446{1}{2}{1，2}半序集例12022/12/2810{1}{2}{1，2}半序集例2數(shù)學(xué)上的和構(gòu)成半序關(guān)系集合A上的恒等關(guān)系IA是A上的半序關(guān)系正整數(shù)集合上的整除關(guān)系也是半序關(guān)系和不能構(gòu)成半序關(guān)系2023/1/447半序集的特點(diǎn)是：不要求對于半序集中的任意兩個元素都有半序關(guān)系，即允許有些元素之間不存在半序關(guān)系！若半序集(D,?)中的任意兩個元素之間都存在半序關(guān)系，則稱(D,?)為全序集。

半序集例22022/12/2811半序集的特點(diǎn)是：不要求對于最小上屆上/下界：設(shè)(D,?)為任意半序集，而且D’D,dD,則子集D’的上界和下界的定義如下：上界：若對任意d’D’,都有d’?d,則稱d為D’的上界；下界：若對任意d’D’,都有d?d’,則稱d為D’的下界；最小上界/最大下界：設(shè)(D,?)為任意半序集，而且D’D,則子集D’的最小上界和最大下界的定義如下：最小上界：設(shè)d是D’的一個上界，若對D’的任意一個上界d’,都有d?d’,則稱d為D’的最小上界，并記為D’；最大下界：設(shè)d是D’的一個下界，若對D’的任意一個下界d’,都有d’?d,則稱d為D’的最大下界，并記為D’；2023/1/448最小上屆上/下界：設(shè)(D,?)為任意半序集，而且D’D,特殊元素及其性質(zhì)下界、上界、最大下界、最小上界不一定存在下界、上界存在不一定惟一最大下界、最小上界如果存在，則惟一最小元：設(shè)(D,?)為任意半序集,dD,如果對于任意D中的元素d’都有d?d’，則稱d為D的最小元。集合的最小元就是它的最大下界，最大元就是它的最小上界；反之不對.

2023/1/449特殊元素及其性質(zhì)下界、上界、最大下界、最小上界不一定存在20半序集的特殊元素例3設(shè)<D,?>是偏序集，其中D={a,b,c,d,e,f,g,h},?={<b,d>,<b,e>,<b,f>,<c,d>,<c,e>,<c,f>,<d,f>,<e,f>,<g,h>}∪ID

設(shè)A＝{b,c,d},求A的下界、上界、最大下界、最小上界.2023/1/450A的下界和最大下界都不存在，A也沒有最小元上界有d和f,最小上界為d.半序集的特殊元素例3設(shè)<D,?>是偏序集，其中2022/鏈，遞增鏈，遞減鏈定義鏈設(shè)<D,?>為任意半序集,<X0,X1,…,Xn,…>

是D上的一個序列，簡記為{Xi},則遞增鏈和遞減鏈定義如下：遞增鏈：若對任意i都有Xi?Xi+1

，則稱序列{Xi}為遞增鏈；遞減鏈：若對任意i都有Xi+1?Xi

，則稱序列{Xi}為遞減鏈；鏈的最小上屆記為：{Xi}或

iXi

或Xi

2023/1/451鏈，遞增鏈，遞減鏈定義鏈2022/12/28152.1.1完全半序集定義完全半序集(completepartialorderset,CPO)設(shè)<D,?>為一個半序集,若滿足下面兩個條件，則稱<D,?>為完全半序集：D有最小元；對于D的任一遞增鏈

{Xi}都有最小上屆{Xi}。2023/1/4522.1.1完全半序集定義完全半序集(complete2.1.1完全半序集例4

完全半序集如果D是任意有窮整數(shù)集，是定義在D上的小于等于關(guān)系，則(D,)為完全半序集；有最小元的有窮半序集是完全半序集；如果D表示開區(qū)間(a,b)，其中a和b是實(shí)數(shù)，則(D,)不是完全半序集；2023/1/4532.1.1完全半序集例4完全半序集2022/12/282.1.1完全半序集為什么引入完全半序集？在形式地描述程序設(shè)計語言的語義時(指稱語義方法)，要求所考慮的集合都滿足完全半序集的條件；建立論域的數(shù)學(xué)模型：滿足一定條件的定義了關(guān)系的集合(完全半序集)；如何構(gòu)造完全半序集？平坦集一定是完全半序集擴(kuò)展任意集合為平坦集的方法非常簡單

2023/1/4542.1.1完全半序集為什么引入完全半序集？2022/12/平坦集定義平坦集設(shè)<D,?>為一個半序集,若滿足下面兩個條件，則稱<D,?>為平坦半序集(平坦集)：D有最小元；只有下面的關(guān)系(平坦關(guān)系)：?，?d，d?d,其中d是D中非的元素。2023/1/455……平坦集定義平坦集2022/12/2819……平坦集擴(kuò)展任意一個集合為平坦集的方法任意一個集合D;引進(jìn)一個最小元D；在集合D’=D{D}上定義平坦關(guān)系?：

D

?D，D?d，d?d；<D’,?>為一個平坦集，簡記為D

；2023/1/456性質(zhì)：平坦集一定是完全半序集。平坦集擴(kuò)展任意一個集合為平坦集的方法2022/12/2820平坦集的例子例5D={{1},{1,2},{1,3}},關(guān)系是集合包含關(guān)系，則(D,)是一個平坦集；其中最小元是{1};BOOL={true,false},可以擴(kuò)充為平坦集：引入最小元；定義一個平坦關(guān)系?：?

,?

true,?

false,true?

true,false?

false；則(BOOL

,?)是平坦集2023/1/457平坦集的例子例5D={{1},{1,2},{1,3論域問題引子試編制一個程序?qū)崿F(xiàn)下面有限自動機(jī)的功能。2023/1/458XBA100011論域問題引子試編制一個程序?qū)崿F(xiàn)下面有限自動機(jī)的功能。2022state=‘X’;readone(ch);whilech’#’doifch=‘1’thenout(state)elseifstate=‘X’thenstate=‘A’elseifstate=‘A’thenstate=‘B’elseifstate=‘B’thenstate=‘A’elseskipfififi;fi;readone(ch);od

2023/1/459XBA100011可將程序看作是一個函數(shù)，函數(shù)：定義域值域即輸入到輸出的映射。程序的編者主觀上認(rèn)定輸入域是{0，1，#}，其實(shí)還可以輸入其它字符。顯然，一個正確的程序設(shè)計必須給出在輸入不是集合{0，1，#}中的一個元素時，應(yīng)指出是“無定義”的錯誤處理。

----論域做大了state=‘X’;2022/12/2823XBA100論域引入目的：描述類型的數(shù)學(xué)模型；指稱語義學(xué)和函數(shù)式語言中都要用到。Scott論域及其構(gòu)造2023/1/460論域引入目的：2022/12/2824Scott論域及其構(gòu)造論域(Domain)：定義了關(guān)系的,滿足一定條件的集合(CPO)；論域分為原始域和非原始域(構(gòu)造域)原始域：有限集或可枚舉集都是原始域{true,false},{…,-1,0,1,…}

非原始域：可以從已知論域，應(yīng)用論域構(gòu)造符進(jìn)行構(gòu)造。2023/1/461可以證明，如果每個成分是完全半序集，則保證構(gòu)造符作用后得到的仍然是完全半序集.Scott論域及其構(gòu)造論域(Domain)：2022/12/論域構(gòu)造符設(shè)(Di,?i)是完全半序集,i=1,…,n,則我們定義了如下論域構(gòu)造符：,+,*和，通過它們的作用可以得到新的論域；(1)元組域(乘積域或卡氏域)(D1…Dn,?)定義如下:D1…Dn={(d1,…,dn)|diDi,i=1,…,n}；關(guān)系?

：(d1,…,dn)?

(d1’,…,dn’)當(dāng)且僅當(dāng)di?i

di’，i=1,…,n；稱為n元組域，簡記為[D1…Dn]或D1…Dn最小元：(D1，…，Dn

)對應(yīng)沒有域名的結(jié)構(gòu)類型(struct)

2023/1/462論域構(gòu)造符設(shè)(Di,?i)是完全半序集,i=1,元組域的例子例6：{1，2}BOOLD1={1，2}，1?1，1?2，2?2(整數(shù)上的)D2=BOOL，false?bfalse，false?btrue，true?btrue集合：D={(1,true),(1,false),(2,true),(2,false)}關(guān)系：?x:自身:(1,true)?x(1,true),….

(1,false)?x(1,true),(2,false)?x(2,true)

(1,true)?x(2,true),(1,false)?x(2,false)

(1,false)?x(2,true)最小元：(1,false)2023/1/463元組域的例子例6：{1，2}BOOL2022/12/2論域構(gòu)造符(2)聯(lián)合域

(D1…Dn,?)定義如下:D1…Dn={(j,dj)|djDj,j=1,…,n}{}；關(guān)系?

：

?

;

?(j,dj);(i,di)?(j,dj)當(dāng)且僅當(dāng)i=j而且di?i

dj，

i(j)=1,…,n；簡記為[D1…Dn］或D1…Dn最小元：對應(yīng)聯(lián)合類型(union)2023/1/464論域構(gòu)造符(2)聯(lián)合域(D1…Dn,?)定義如下聯(lián)合域的例子例7：{1，2}BOOLD1={1，2}，1?1，1?2，2?2(整數(shù)上的)D2=BOOL，false?bfalse，false?btrue，true?btrue集合：D={(1,1),(1,2),(2,true),(2,false),}關(guān)系：?+:自身:(1,1)?+(1,1),….

(1,1)?+(1,2),(2,false)?+(2,true)

?+i{(1,1),(1,2),(2,true),(2,false)}最小元：

2023/1/465聯(lián)合域的例子例7：{1，2}BOOL2022/12/2論域構(gòu)造符(3)序列域

(D*

,?)定義如下:D*

={<d1,…,dn>|diDi

,n0,i=1,2,…};關(guān)系?

：

<>

?<>;

<>

?<d1,…,dn>;<d1,…,dn>?<d1’,…,dm’>,當(dāng)且僅當(dāng)n=m而

且di?i

di’

,i=1,…,n；簡記為D*最小元：<>對應(yīng)表類型2023