程序設(shè)計(jì)語(yǔ)言理論-全文預(yù)覽
【正文】 間的對(duì)應(yīng)關(guān)系 類型和類型系統(tǒng) 設(shè)計(jì)類型系統(tǒng)的目的 ? 用來(lái)證明程序不會(huì)出現(xiàn)不良行為 ? 類型可靠的語(yǔ)言（安全語(yǔ)言） – 所有程序運(yùn)行時(shí)都沒(méi)有不良行為出現(xiàn) – 類型系統(tǒng)的研究也需要形式化的方法 – 許多語(yǔ)言定義被發(fā)現(xiàn)不是類型可靠的，甚至經(jīng)過(guò)類型檢查后接受的程序也會(huì)崩潰 ? 顯式類型化的語(yǔ)言： 類型是語(yǔ)法的一部分 ? 隱式類型化的語(yǔ)言 類型和類型系統(tǒng) 類型語(yǔ)言的優(yōu)點(diǎn) ? 開(kāi)發(fā)時(shí)的實(shí)惠 – 可以較早發(fā)現(xiàn)錯(cuò)誤 – 類型信息具有文檔作用（比程序注解精確，比形式規(guī)范容易理解） ? 編譯時(shí)的實(shí)惠 – 程序模塊可以相互獨(dú)立地編譯 ? 運(yùn)行時(shí)的實(shí)惠 – 更有效的空間安排和訪問(wèn)方式，提高了目標(biāo)代碼的運(yùn)行效率 類型和類型系統(tǒng) 類型系統(tǒng)的其他應(yīng)用 ? 許多程序分析工具使用類型檢查或類型推斷算法 ? 類型系統(tǒng)用來(lái)表示邏輯命題和證明 歸 納 法 本節(jié)介紹本書(shū)常用的歸納法 ? 自然數(shù)歸納法（有兩種形式，不專門(mén)介紹） ? 結(jié)構(gòu)歸納（介紹表達(dá)式上的歸納，有兩種形式） ? 證明上的歸納 ? 良基歸納法（重點(diǎn)介紹） 歸 納 法 表達(dá)式上的歸納 ? 表達(dá)式文法 e ::= 0 | 1 | v | e + e | e ? e ? 每個(gè)表達(dá)式都有各自的語(yǔ)法樹(shù) ? 如果 P是表達(dá)式的性質(zhì)， Q是 自然數(shù)的性質(zhì) – Q(n) ? ?語(yǔ)言 樹(shù) height(t) = n 并且 t是 e的語(yǔ)法樹(shù)，那么 P(e)為真 – 首先必須為高度是 0的語(yǔ)法樹(shù)直接證明 P – 然后，對(duì)于語(yǔ)法樹(shù)高度至少為 1的表達(dá)式 e，假定對(duì)于語(yǔ)法樹(shù)高度較小的表達(dá)式， P都為真，證明P(e)為真 歸 納 法 ? 結(jié)構(gòu)歸納 （形式 1） – 對(duì)每個(gè)原子表達(dá)式 e， 證明 P(e) – 對(duì)直接子表達(dá)式為 e1,…, ek的任何復(fù)合表達(dá)式 e，證明，如果 P(ei)（ i=1,…, k） 都為真，那么 P(e) 也為真 ? 結(jié)構(gòu)歸納 （形式 2） – 證明：對(duì)任何表達(dá)式 e， 如果 P(e?)對(duì) e的任何子表達(dá)式 e?都成立，那么 P(e)也成立 ? 形式 2的歸納假設(shè)包含了所有的子表達(dá)式，并非只是直接子表達(dá)式 歸 納 法 證明上的歸納 ? 證明系統(tǒng) 由公理和推理規(guī)則組成 ? 證明是一個(gè)公式序列，該序列中的每個(gè)公式都是公理或者是由前面的公式通過(guò)一個(gè)推理規(guī)則得到的結(jié)論 ? 基于證明的長(zhǎng)度，用自然數(shù)歸納法來(lái)討論證明的性質(zhì) ? 另一種觀點(diǎn)把證明看成是某種形式的樹(shù) 歸 納 法 ? 證明上的結(jié)構(gòu)歸納 – 對(duì)該證明系統(tǒng)中的每個(gè)公理，證明 P成立 – 假定對(duì)證明 ?1, …, ?k， P成立，證明 P(?)也為真 – ?是這樣的證明，它結(jié)束于用一個(gè)推理規(guī)則，并且是從證明 ?1, …, ?k延伸出來(lái)的一個(gè)證明 B An A1 證明樹(shù)示意圖 歸 納 法 良基歸納 ? 集合 A的二元關(guān)系被稱為是良基的 ?：若 A上不存在無(wú)窮遞減序列 a0 ? a1 ? a2 ? … ? 例：在自然數(shù)上，如果 j ? i +1， 則 i ? j。 故 ?是良基的
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1