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

1、程序設(shè)計(jì)語言理論程序設(shè)計(jì)語言理論計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院陳意云，陳意云，3607043http:/ 程程 簡簡 介介計(jì)算機(jī)科學(xué)的理論體系計(jì)算機(jī)科學(xué)的理論體系1、模型理論、模型理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M，哪些問題可以由模型，哪些問題可以由模型M解決解決 如何比較模型的表達(dá)能力如何比較模型的表達(dá)能力 經(jīng)典計(jì)算經(jīng)典計(jì)算 確定的圖靈機(jī)，可計(jì)算性理論屬于模型理論確定的圖靈機(jī)，可計(jì)算性理論屬于模型理論 新型計(jì)算新型計(jì)算 本質(zhì)特點(diǎn)是交互本質(zhì)特點(diǎn)是交互( 并發(fā)、分布、網(wǎng)絡(luò)、網(wǎng)格、云并發(fā)、分布、網(wǎng)絡(luò)、網(wǎng)格、云 ) 計(jì)算和交互的統(tǒng)一模型理論尚未出現(xiàn)計(jì)算和交互的統(tǒng)一模型理論尚未出

2、現(xiàn)課課 程程 簡簡 介介計(jì)算機(jī)科學(xué)的理論體系計(jì)算機(jī)科學(xué)的理論體系2、程序理論、程序理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M，如何用模型，如何用模型M解決問題解決問題 包括的領(lǐng)域包括的領(lǐng)域 程序設(shè)計(jì)范型、程序設(shè)計(jì)語言、程序設(shè)計(jì)、形式程序設(shè)計(jì)范型、程序設(shè)計(jì)語言、程序設(shè)計(jì)、形式語義、類型論、程序驗(yàn)證、程序分析等語義、類型論、程序驗(yàn)證、程序分析等課課 程程 簡簡 介介計(jì)算機(jī)科學(xué)的理論體系計(jì)算機(jī)科學(xué)的理論體系3、計(jì)算理論、計(jì)算理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M和一類問題，解決該類問題需要多少和一類問題，解決該類問題需要多少資源資源 包括的領(lǐng)域包括的領(lǐng)域 計(jì)算復(fù)雜性理論計(jì)算復(fù)雜性理論課課

3、 程程 簡簡 介介圍繞程序設(shè)計(jì)語言的研究（課程涉及內(nèi)容用圍繞程序設(shè)計(jì)語言的研究（課程涉及內(nèi)容用綠色綠色表示）表示） 語法：形式語言和自動機(jī)理論，語法分析的實(shí)現(xiàn)語法：形式語言和自動機(jī)理論，語法分析的實(shí)現(xiàn)技術(shù)技術(shù) 語義：語義：公理語義、操作語義、指稱語義公理語義、操作語義、指稱語義 形式描述技術(shù)還有：形式描述技術(shù)還有：代數(shù)規(guī)范代數(shù)規(guī)范、范疇論范疇論、屬性、屬性文法文法 程序設(shè)計(jì)的范型程序設(shè)計(jì)的范型：命令式語言、函數(shù)式語言命令式語言、函數(shù)式語言、邏、邏輯程序設(shè)計(jì)語言、輯程序設(shè)計(jì)語言、面向?qū)ο蟪绦蛟O(shè)計(jì)語言面向?qū)ο蟪绦蛟O(shè)計(jì)語言、并行、并行程序設(shè)計(jì)語言程序設(shè)計(jì)語言課課 程程 簡簡 介介圍繞程序設(shè)計(jì)語言的研

4、究（課程涉及內(nèi)容用圍繞程序設(shè)計(jì)語言的研究（課程涉及內(nèi)容用綠色綠色表示）表示） 類型論與類型系統(tǒng)：多態(tài)類型、子類型、存在類類型論與類型系統(tǒng)：多態(tài)類型、子類型、存在類型型 程序驗(yàn)證：程序驗(yàn)證：程序正確性證明程序正確性證明 程序分析技術(shù)：數(shù)據(jù)流分析、控制流分析、模型程序分析技術(shù)：數(shù)據(jù)流分析、控制流分析、模型檢查、抽象解釋檢查、抽象解釋 程序的自動生成技術(shù)：程序變換程序的自動生成技術(shù)：程序變換課課 程程 簡簡 介介學(xué)習(xí)的意義學(xué)習(xí)的意義 掌握與程序設(shè)計(jì)語言有關(guān)的理論，為從事有關(guān)的掌握與程序設(shè)計(jì)語言有關(guān)的理論，為從事有關(guān)的研究起一個奠基的作用研究起一個奠基的作用應(yīng)用：應(yīng)用： 程序設(shè)計(jì)語言的設(shè)計(jì)和實(shí)現(xiàn)程序設(shè)

5、計(jì)語言的設(shè)計(jì)和實(shí)現(xiàn) 程序的自動生成程序的自動生成 程序分析與程序驗(yàn)證程序分析與程序驗(yàn)證 提高軟件的可信程度提高軟件的可信程度 協(xié)議的形式描述和驗(yàn)證協(xié)議的形式描述和驗(yàn)證課課 程程 簡簡 介介教材和參考書教材和參考書 陳意云、張昱，程序設(shè)計(jì)語言理論（第二版），陳意云、張昱，程序設(shè)計(jì)語言理論（第二版），高等教育出版社，高等教育出版社，2010.2 教學(xué)資源網(wǎng)頁：教學(xué)資源網(wǎng)頁：http:/ 馬世龍、眭躍飛等譯，類型和程序設(shè)計(jì)語言，電馬世龍、眭躍飛等譯，類型和程序設(shè)計(jì)語言，電子工業(yè)出版社，子工業(yè)出版社，2005.5 許滿武譯，程序設(shè)計(jì)語言理論基礎(chǔ)，電子工業(yè)出許滿武譯，程序設(shè)計(jì)語言理論基礎(chǔ)，電子工業(yè)出版社

6、，版社，2006.11 陳意云、張昱，編譯原理（第二版），高等教育陳意云、張昱，編譯原理（第二版），高等教育出版社，出版社，2008.6課課 程程 簡簡 介介教材和參考書教材和參考書 John C. Mitchell, Foundations For Programming Languages, MIT Press, 1996. Banjamin C. Pierce, Types and Programming Laungages, MIT Press, 2002. Robert Harper, Practical Foundations for Programming Languages,

7、working draft, 2009. John C. Reynolds, Theories of Programming Languages , Cambridge University Press, 1998. Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction , MIT Press, 1993. 課課 程程 簡簡 介介課程要求課程要求 講課進(jìn)展較快，平時不復(fù)習(xí)不加深理解，后面將講課進(jìn)展較快，平時不復(fù)習(xí)不加深理解，后面將聽不懂聽不懂 作業(yè)較多，要求獨(dú)立完成作業(yè)較多，要求獨(dú)立完成 沒有

8、上機(jī)實(shí)驗(yàn)沒有上機(jī)實(shí)驗(yàn) 考試開卷考試開卷 成績：考試成績成績：考試成績占占70%，作業(yè)占，作業(yè)占30% 第第1章章 引引 言言 介紹一個非常簡單的、以自然數(shù)和布爾值作介紹一個非常簡單的、以自然數(shù)和布爾值作為基本類型的、基于類型化為基本類型的、基于類型化 演算的語言演算的語言 介紹該語言的語法、公理語義和操作語義介紹該語言的語法、公理語義和操作語義 主要議題如下：主要議題如下： 表示法和表示法和 演算系統(tǒng)概述演算系統(tǒng)概述 類型和類型系統(tǒng)的扼要討論類型和類型系統(tǒng)的扼要討論 基于表達(dá)式的歸納、基于證明的歸納和良基歸納基于表達(dá)式的歸納、基于證明的歸納和良基歸納1.1 基基 本本 概概 念念1.1.1 模

9、型語言模型語言 對程序設(shè)計(jì)語言進(jìn)行數(shù)學(xué)分析對程序設(shè)計(jì)語言進(jìn)行數(shù)學(xué)分析 從設(shè)計(jì)模型語言開始從設(shè)計(jì)模型語言開始 突出感興趣的程序構(gòu)造，忽略無關(guān)的細(xì)節(jié)突出感興趣的程序構(gòu)造，忽略無關(guān)的細(xì)節(jié) 語言的形式化分為兩部分語言的形式化分為兩部分 能抓住語言本質(zhì)機(jī)制的非常小的核心：能抓住語言本質(zhì)機(jī)制的非常小的核心： 演算演算 導(dǎo)出部分：它們可以翻譯成核心的導(dǎo)出部分：它們可以翻譯成核心的 演算演算 用類型化用類型化 演算的框架來研究程序設(shè)計(jì)語言的演算的框架來研究程序設(shè)計(jì)語言的各種概念各種概念1.1 基基 本本 概概 念念1.1.2 表示法表示法 表示法的主要特征表示法的主要特征 抽象：抽象：用于定義函數(shù)用于定義函數(shù)

10、 應(yīng)用：應(yīng)用：將所定義的函數(shù)作用于變元將所定義的函數(shù)作用于變元 抽象的例子抽象的例子 （自然數(shù)類型上的幾個例子自然數(shù)類型上的幾個例子） 恒等函數(shù)：恒等函數(shù)： x : nat.x / 命令式表示命令式表示Id(x : nat) = x 后繼函數(shù)：后繼函數(shù)： x : nat.x 1 / 函數(shù)式無需給函數(shù)命名函數(shù)式無需給函數(shù)命名 常函數(shù)：常函數(shù)： x : nat.10 x : nat. .x true 不是良形的表達(dá)式不是良形的表達(dá)式 表示法寫出的表達(dá)式叫做表示法寫出的表達(dá)式叫做 表達(dá)式表達(dá)式或或 項(xiàng)項(xiàng)1.1 基基 本本 概概 念念 項(xiàng)項(xiàng) x: . .M 和謂詞演算公式和謂詞演算公式 x :A. .

11、 的比較的比較 是一個約束算子是一個約束算子 x是一個占位符是一個占位符，約束變元，可，約束變元，可以重新命名以重新命名 約束約束變元變元而不改變表達(dá)式的含義而不改變表達(dá)式的含義 在在 x: . .x + y中，中，x的出現(xiàn)是的出現(xiàn)是約束的，約束的， y的出現(xiàn)是的出現(xiàn)是自由的自由的 不含自由變元的表達(dá)式稱為閉表達(dá)式不含自由變元的表達(dá)式稱為閉表達(dá)式 應(yīng)用：應(yīng)用：用項(xiàng)的并置來表示函數(shù)應(yīng)用，例：用項(xiàng)的并置來表示函數(shù)應(yīng)用，例： ( x : nat. .x) 5 ( x : nat. .x) 5 5 / 應(yīng)用后面介紹的應(yīng)用后面介紹的 公理公理1.1 基基 本本 概概 念念 一個簡單的例子一個簡單的例子

12、( x : nat. ( y : nat. z : nat. ( x + y ) + z ) 3 ) 4 5= ( x : nat. z : nat. ( x + 3 ) + z ) 4 5= ( z : nat. ( 4 + 3 ) + z ) 5= ( 4 + 3 ) + 5= 121.1 基基 本本 概概 念念 表示法中有兩個約定表示法中有兩個約定 函數(shù)應(yīng)用是左結(jié)合的：函數(shù)應(yīng)用是左結(jié)合的： MNP 應(yīng)看成應(yīng)看成 (MN)P 每個每個 的約束范圍盡可能地大的約束范圍盡可能地大：一直到表達(dá)式的結(jié)束，或一直到表達(dá)式的結(jié)束，或碰到不能配對的右括號為止碰到不能配對的右括號為止 例例 x: . .M

13、N解釋為解釋為 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)于演算是關(guān)于 表表達(dá)式的一個推理系統(tǒng)達(dá)式的一個推理系統(tǒng) 除了語法外，該形式系統(tǒng)有三個主要部分除了語法外，該形式系統(tǒng)有三個主要部分 公理語義：公理語義：推導(dǎo)表達(dá)式相等的一個形式系統(tǒng)推導(dǎo)表達(dá)式相等的一個形式系

14、統(tǒng) 操作語義：操作語義：基于單方向的等式推理基于單方向的等式推理（歸約、符號（歸約、符號計(jì)算）計(jì)算）上述兩者都稱為證明系統(tǒng)上述兩者都稱為證明系統(tǒng) 指稱語義：形式系統(tǒng)的模型指稱語義：形式系統(tǒng)的模型1.2 等式、歸約和語義等式、歸約和語義1.2.1 公理語義公理語義一個等式公理系統(tǒng)一個等式公理系統(tǒng) 約束變元改名公理約束變元改名公理（ 公理公理） x: . .M y: . . y x M，M中無自由出現(xiàn)的中無自由出現(xiàn)的y其中其中 N x M表示表示M中的中的x用表達(dá)式用表達(dá)式N代換的結(jié)果代換的結(jié)果 例如例如 x: .x y: .y 函數(shù)應(yīng)用公理函數(shù)應(yīng)用公理（ 公理公理） ( x: . .M)N N/

15、xM 例如例如 ( x:nat.x+4) 4 4/x(x+4) 4 + 41.2 等式、歸約和語義等式、歸約和語義 自反公理、對稱性規(guī)則、傳遞性規(guī)則自反公理、對稱性規(guī)則、傳遞性規(guī)則 同余規(guī)則同余規(guī)則 相等的函數(shù)應(yīng)用于相等的變元產(chǎn)生相等的結(jié)果相等的函數(shù)應(yīng)用于相等的變元產(chǎn)生相等的結(jié)果 等式證明規(guī)則允許推導(dǎo)任何一組等式前提的等式證明規(guī)則允許推導(dǎo)任何一組等式前提的邏輯推論邏輯推論M1 = M2 N1 = N2 M1 N1 = M2 N21.2 等式、歸約和語義等式、歸約和語義1.2.2 操作語義操作語義語言的操作語義可用不同的方式給出語言的操作語義可用不同的方式給出 定義一個抽象機(jī)定義一個抽象機(jī), ,

16、通過一系列的機(jī)器狀態(tài)變換通過一系列的機(jī)器狀態(tài)變換來計(jì)算程序來計(jì)算程序 演繹出最終結(jié)果的證明系統(tǒng)演繹出最終結(jié)果的證明系統(tǒng) 前面所列的等式公理的單向形式給出了歸約規(guī)則前面所列的等式公理的單向形式給出了歸約規(guī)則 最核心的歸約規(guī)則是最核心的歸約規(guī)則是( )的單向形式的單向形式( x: .M)N N/xM 通常沒有通常沒有 歸約規(guī)則：歸約規(guī)則： x: .M y: . y x M1.2 等式、歸約和語義等式、歸約和語義1.2.3 指稱語義指稱語義 確定語言構(gòu)造（程序、語句、表達(dá)式等）到確定語言構(gòu)造（程序、語句、表達(dá)式等）到指稱物（各種集合）的語義映射，滿足：指稱物（各種集合）的語義映射，滿足： 各種語言構(gòu)

17、造的實(shí)例都有對應(yīng)的指稱物各種語言構(gòu)造的實(shí)例都有對應(yīng)的指稱物 復(fù)合構(gòu)造的指稱只依賴于它的子構(gòu)造的指稱復(fù)合構(gòu)造的指稱只依賴于它的子構(gòu)造的指稱 類型化類型化 演算的指稱語義演算的指稱語義 每個類型表達(dá)式對應(yīng)到一個集合每個類型表達(dá)式對應(yīng)到一個集合 類型類型 的項(xiàng)解釋為其值集上的一個元素的項(xiàng)解釋為其值集上的一個元素 類型類型 的值集是函數(shù)集合，項(xiàng)的值集是函數(shù)集合，項(xiàng) x: .M解釋為解釋為一個數(shù)學(xué)函數(shù)一個數(shù)學(xué)函數(shù)1.3 類型和類型系統(tǒng)類型和類型系統(tǒng) 類型論類型論 為避免集合論悖論而建立起來的數(shù)學(xué)理論為避免集合論悖論而建立起來的數(shù)學(xué)理論 主要研究集合的分層、分類方法主要研究集合的分層、分類方法 在程序設(shè)計(jì)

18、語言理論中，類型論是指類型系統(tǒng)的在程序設(shè)計(jì)語言理論中，類型論是指類型系統(tǒng)的設(shè)計(jì)、分析和研究設(shè)計(jì)、分析和研究 類型提供了所有可能值的一種劃分類型提供了所有可能值的一種劃分 一個類型是一群有某些公共性質(zhì)的值一個類型是一群有某些公共性質(zhì)的值 對于不同的類型系統(tǒng)，類型的多少和值所屬對于不同的類型系統(tǒng)，類型的多少和值所屬的類型可能不同的類型可能不同1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)1.3.1 類型和類型系統(tǒng)類型和類型系統(tǒng) 類型語言類型語言：變量都被給定類型：變量都被給定類型 未未類類型化的型化的語語言言：不限制變量值的范圍：不限制變量值的范圍 類型系統(tǒng)類型系統(tǒng) 語言的一個組成部分語言的一個組成部分 由

19、一組定型規(guī)則構(gòu)成由一組定型規(guī)則構(gòu)成 類型系統(tǒng)的研究有兩個分支類型系統(tǒng)的研究有兩個分支 類型系統(tǒng)在程序設(shè)計(jì)語言中的應(yīng)用類型系統(tǒng)在程序設(shè)計(jì)語言中的應(yīng)用 “純類型化純類型化 演算演算”和各種邏輯之間的對應(yīng)關(guān)系和各種邏輯之間的對應(yīng)關(guān)系1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)設(shè)計(jì)類型系統(tǒng)的目的設(shè)計(jì)類型系統(tǒng)的目的 用來證明程序不會出現(xiàn)不良行為用來證明程序不會出現(xiàn)不良行為 類型可靠的語言（安全語言）類型可靠的語言（安全語言） 所有程序運(yùn)行時都沒有不良行為出現(xiàn)所有程序運(yùn)行時都沒有不良行為出現(xiàn) 類型系統(tǒng)的研究也需要形式化的方法類型系統(tǒng)的研究也需要形式化的方法 許多語言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過許多語言定義被

20、發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過類型檢查后接受的程序也會崩潰類型檢查后接受的程序也會崩潰 顯式類型化的語言：顯式類型化的語言：類型是語法的一部分類型是語法的一部分 隱式類型化的語言隱式類型化的語言1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)1.3.2 類型語言的優(yōu)點(diǎn)類型語言的優(yōu)點(diǎn) 開發(fā)時的實(shí)惠開發(fā)時的實(shí)惠 可以較早發(fā)現(xiàn)錯誤可以較早發(fā)現(xiàn)錯誤 類型信息具有文檔作用（比程序注解精確，比形類型信息具有文檔作用（比程序注解精確，比形式規(guī)范容易理解）式規(guī)范容易理解） 編譯時的實(shí)惠編譯時的實(shí)惠 程序模塊可以相互獨(dú)立地編譯程序模塊可以相互獨(dú)立地編譯 運(yùn)行時的實(shí)惠運(yùn)行時的實(shí)惠 更有效的空間安排和訪問方式，提高了目標(biāo)代碼更有

21、效的空間安排和訪問方式，提高了目標(biāo)代碼的運(yùn)行效率的運(yùn)行效率1.3 類型和類型系統(tǒng)類型和類型系統(tǒng)類型系統(tǒng)的其他應(yīng)用類型系統(tǒng)的其他應(yīng)用 許多程序分析工具使用類型檢查或類型推斷許多程序分析工具使用類型檢查或類型推斷算法算法 類型系統(tǒng)用來表示邏輯命題和證明類型系統(tǒng)用來表示邏輯命題和證明1.4 歸歸 納納 法法本節(jié)介紹本書常用的歸納法本節(jié)介紹本書常用的歸納法 自然數(shù)歸納法（有兩種形式，不專門介紹）自然數(shù)歸納法（有兩種形式，不專門介紹） 結(jié)構(gòu)歸納（介紹表達(dá)式上的歸納，有兩種形結(jié)構(gòu)歸納（介紹表達(dá)式上的歸納，有兩種形式）式） 證明上的歸納證明上的歸納 良基歸納法（重點(diǎn)介紹）良基歸納法（重點(diǎn)介紹）1.4 歸歸

22、納納 法法1.4.1 表達(dá)式上的歸納表達(dá)式上的歸納 表達(dá)式文法表達(dá)式文法 e := 0 | 1 | v | e + e | e e 每個表達(dá)式都有各自的語法樹每個表達(dá)式都有各自的語法樹 如果如果P是表達(dá)式的性質(zhì)，是表達(dá)式的性質(zhì)，Q是是自然數(shù)的性質(zhì)自然數(shù)的性質(zhì) Q(n) 語言語言樹樹t. .如果如果height(t) = n 并且并且t是是e的的語法樹，那么語法樹，那么P(e)為真為真 首先必須為高度是首先必須為高度是0的語法樹直接證明的語法樹直接證明P 然后，對于語法樹高度至少為然后，對于語法樹高度至少為1的表達(dá)式的表達(dá)式e，假定，假定對于語法樹高度較小的表達(dá)式，對于語法樹高度較小的表達(dá)式，P

23、都為真，證明都為真，證明P(e)為真為真1.4 歸歸 納納 法法 結(jié)構(gòu)歸納結(jié)構(gòu)歸納（形式（形式1） 對每個原子表達(dá)式對每個原子表達(dá)式e，證明證明P(e) 對直接子表達(dá)式為對直接子表達(dá)式為e1, ek的任何復(fù)合表達(dá)式的任何復(fù)合表達(dá)式e，證明，如果證明，如果P(ei)（i=1, k）都為真，那么都為真，那么P(e) 也為真也為真 結(jié)構(gòu)歸納結(jié)構(gòu)歸納（形式（形式2） 證明：對任何表達(dá)式證明：對任何表達(dá)式e，如果如果P(e )對對e的任何子表的任何子表達(dá)式達(dá)式e 都成立，那么都成立，那么P(e)也成立也成立 形式形式2的歸納假設(shè)包含了所有的子表達(dá)式，并的歸納假設(shè)包含了所有的子表達(dá)式，并非只是直接子表達(dá)式

24、非只是直接子表達(dá)式1.4 歸歸 納納 法法1.4.2 證明上的歸納證明上的歸納 證明系統(tǒng)證明系統(tǒng)由公理和推理規(guī)則組成由公理和推理規(guī)則組成 證明是一個公式序列，該序列中的每個公式證明是一個公式序列，該序列中的每個公式都是公理或者是由前面的公式通過一個推理都是公理或者是由前面的公式通過一個推理規(guī)則得到的結(jié)論規(guī)則得到的結(jié)論 基于證明的長度，用自然數(shù)歸納法來討論證基于證明的長度，用自然數(shù)歸納法來討論證明的性質(zhì)明的性質(zhì) 另一種觀點(diǎn)把證明看成是某種形式的樹另一種觀點(diǎn)把證明看成是某種形式的樹1.4 歸歸 納納 法法 證明上的結(jié)構(gòu)歸納證明上的結(jié)構(gòu)歸納 對該證明系統(tǒng)中的每個公理，證明對該證明系統(tǒng)中的每個公理，證

25、明P成立成立 假定對證明假定對證明 1, , k，P成立，證明成立，證明P( )也為真也為真 是這樣的證明，它結(jié)束于用一個推理規(guī)則，并是這樣的證明，它結(jié)束于用一個推理規(guī)則，并且是從證明且是從證明 1, , k延伸出來的一個證明延伸出來的一個證明BAn- - -A1證明樹示意圖證明樹示意圖1.4 歸歸 納納 法法1.4.3 良基歸納良基歸納 集合集合A的二元關(guān)系被稱為是良基的的二元關(guān)系被稱為是良基的 ：若：若A上上不存在無窮遞減序列不存在無窮遞減序列a0 a1 a2 例：在自然數(shù)上，如果例：在自然數(shù)上，如果j i +1，則則i j。這個。這個關(guān)系是良基關(guān)系關(guān)系是良基關(guān)系 良基關(guān)系的一些特點(diǎn)良基關(guān)

26、系的一些特點(diǎn) 良基關(guān)系不一定有傳遞性良基關(guān)系不一定有傳遞性 良基關(guān)系都是非自反的，即對任何良基關(guān)系都是非自反的，即對任何a A，a a不不成立；否則會出現(xiàn)無窮遞減序列成立；否則會出現(xiàn)無窮遞減序列a a a 1.4 歸歸 納納 法法 引理引理1.1 若若 是集合是集合A上的二元關(guān)系，上的二元關(guān)系， 是良基是良基的，的，當(dāng)且僅當(dāng)當(dāng)且僅當(dāng)A的每個非空子集都有極小元的每個非空子集都有極小元 證明證明 假定假定 是良基的，是良基的，證明非空子集證明非空子集B(B A)有極小元有極小元 用反證法。如果用反證法。如果B無極小元，那么對每個無極小元，那么對每個a B，可以找到某個可以找到某個aB使得使得a a

27、。則可以從任意的則可以從任意的a0 B開始，構(gòu)造一個無窮遞減序列開始，構(gòu)造一個無窮遞減序列a0 a1 a2 假定每個子集都有極小元假定每個子集都有極小元 則不可能存在則不可能存在a0 a1 a2 ，因該序列給出了因該序列給出了無極小元的集合無極小元的集合a0, a1, a2, 。故。故 是良基的是良基的1.4 歸歸 納納 法法 命題命題1.2（良基歸納）（良基歸納）令令 是集合是集合A上的良基關(guān)系，上的良基關(guān)系，令令P是是A上某個性質(zhì)，上某個性質(zhì)，若每當(dāng)所有的若每當(dāng)所有的P(b) (b a)為真，則為真，則P(a)為真，即為真，即 a.( b.(b a P(b) P(a)那么，對所有的那么，對所有的a A，P(a)為真為真1.4 歸歸 納納 法法 命題命題1.2（良基歸納）（良基歸納）若若 a.( b.(b a P(b) P(a)，則，則 a.P(a) 證明證明 若存在某個若存在某個x A使得使得 P(x)成立，則下面集合非空成立，則下面集合非空B a A | P(a) 由引理由引理1.1，B一定有極小元一定有極小元a B 但是，對所有的但是，對所有的b a，P(b)一定成立（否則一定成立（否則a不是