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