第7章多態(tài)性(編輯修改稿)
2024-08-16 12:28 本頁面
【文章內(nèi)容簡介】 ? ? (?x : ?. M) : ? ? ?? 直謂式多態(tài)演算 (?Elim) （ t在 ?中不是自由的） (? Intro) (? Elim) ? ? M : ? ? ?? ? ? N : ? ? ? MN : ?? ? ? M : ? ? ? ?t . M : ?t.? ? ? M : ?t.? ? ? M ? : [?/t]? 直謂式多態(tài)演算 等式證明系統(tǒng)和歸約 ? ??, ?等式的形式是 ? ? M = N:?， 其中 M和 N都是類型 ?的項 ? ??,?的等式推理系統(tǒng)是 ??證明系統(tǒng)的一個拓展，增加了一些公理和推理規(guī)則 ? 該證明系統(tǒng)包含 – 自反公理，對稱和傳遞規(guī)則 – 同項形成規(guī)則對應(yīng)的推理規(guī)則 – 同普通的 ?抽象和應(yīng)用對應(yīng)的推理規(guī)則 直謂式多態(tài)演算 ? 增加了類型抽象和類型應(yīng)用公理 ? ? ?t. M = ?s. [s?t]M : ?t.? (?)? ? ? (?t. M)? = [??t]M : [??t]? (?)? ? ? ?t. Mt = M : ?t.? t在 M中沒有自由出現(xiàn) (?)? 直謂式多態(tài)演算 ? 對類型抽象和應(yīng)用，還有下面的同余規(guī)則 (?)? (?)? ? ? M = N : ? ? ? ?t. M = ?t. N : ?t.? ? ? M = N : ?t.? ? ? M? = N? : [?/t]? 直謂式多態(tài)演算 ? 這些等式公理可以從左向右定向 ,得到一個歸約系統(tǒng) ? 例 (?t.?x: ) ? y ? (?x: ?.x) y ? y ? 可以證明歸約多態(tài) ??,?項的合流性和強范式化 ? 命題 歸約保項的類型 直謂式多態(tài)演算 ML風(fēng)格的多態(tài)聲明 ? ML的類型系統(tǒng)可看成 ??? ?的一個拓展 – 主要區(qū)別是， ML包含多態(tài)的 let聲明 – 通過調(diào)查多態(tài)函數(shù)在 ??? ?中的使用來啟發(fā)這種 let聲明的形式 ? ??? ? – 可以寫出 Id ? (?t. ?x : ) : ?t. t ? t – Id nat 3和 Id bool true都是良類型的項 – 寫不出 (?f :(? ?t). … f nat 3… f bool true)?t.?x: 因為 ?t. t ? t是 U2的一個類型 直謂式多態(tài)演算 ? 對于 U2類型，使用一種非常有限的變量約束形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計來說已經(jīng)足夠了 ? 這種方式利用 let x: ? = N in M和 (?x:?.M)N在語義上都等價于 [N/x]M， 而定型卻不一樣 直謂式多態(tài)演算 ? 對于 U2類型，使用一種非常有限的變量約束形式，對需要多態(tài)函數(shù)的許多實際程序設(shè)計來說已經(jīng)足夠了 ? ML的方式 ??? ?, let 使用 let x : ? = N in M 表達式，增加規(guī)則和公理： (let) ? ? (let x:? = N in M) = [N/x]M:? (let)eq ?, x : ? ? M : ? ? ? N : ? ? ? (let x : ? = N in M) : ? 直謂式多態(tài)演算 ? 例 – 考慮 pose: ?r.?s.?t.? 其中 ? = (s?t) ? (r?s) ? (r?t) – pose在一個表達式中使用多次 ， 讓其函數(shù)體僅寫一次 – let x: (?r.?s.?t.?) = pose in M，則 – ? ? ( let x: (?r.?s.?t.?) = pose in M) = [pose/x]M: ? – 避免寫下面的表達式，并能達到同樣的效果 (?f :(? ?t). … f nat 3… f bool true)?t.?x: 非直謂式多態(tài)演算 引言 ? 非直謂式多 態(tài) ?演算忽略直謂式 ??? ?的全域 U1和 U2的區(qū)別 – 由所有類型的一個聚集 T來代替 U1和 U2 – 用 ????表示，以區(qū)別直謂式系統(tǒng) ? ???? – 類型由文法 ? ::= b | t | ? ? ? | ?t.? 定義，無須用公理和推理規(guī)則給出 非直謂式多態(tài)演算 ? ???? – 類型表達式的文法 ? ::= b | t | ? ? ? | ?t.? – 項的形成依據(jù) (var)、 常量公理 (cst)、 增加自 由變量類型假設(shè)的規(guī)則 (add var)、 規(guī)則 (? Intro)、 規(guī)則 (? Elim)、 規(guī)則 (? Intro)和規(guī)則 (? Elim) 這些規(guī)則中的 ?由 ?代替并且對有關(guān)的類型全域 沒有限制 非直謂式多態(tài)演算 ? 非直謂演算可能是最廣泛研究的一種多態(tài)性 其語法的簡單性 – 該語言語法上比 ??? ?簡單 ， 因為沒有全域的限制 – 但是 證明它的強范式性非常困難 語義的復(fù)雜性 – 想提供直觀和數(shù)學(xué)嚴(yán)格的語義 ， 本質(zhì)上很困難 – 多態(tài)恒等函數(shù) 可應(yīng)用到它自己的類型 ， 造成了不可能把這樣的類型解釋成普通集合論函數(shù)的集合 Id = {??, ?x: ?. x? | ? ?T}， 其中序?qū)? ?(?t: T. t ? t), ?x: (?t: T. t ? t). x ? 的第一元包含 Id 非直謂式多態(tài)演算 ? 非直謂演算可能是最廣泛研究的一種多態(tài)性 編程的靈活性 – 提供了一 個非常靈活的多態(tài)類型系統(tǒng) ， 象 Ada、CLU和 ML等語言的多態(tài)性特征都可以看成是作了某種限制的 ????多態(tài)性 – 可以 用 ????中的 ?抽象來模仿 ML的 let ? ? let x:?t.? = M in N:? （ ML方式 ） 它是項 ? ? (? x:?t.?.N)M:?的一種語法美化 非直謂式多態(tài)演算 非直謂式多態(tài) ?演算的表達能力 給出一個例子來展示非直謂式多態(tài) ?演算的表 達能力 在二階 Peano算術(shù)中 可證明為全函數(shù)的遞歸函數(shù)恰好是在非直謂式多態(tài) ?演算中可以定義的數(shù)值函數(shù) 這是多態(tài) ?演算和二階邏輯的證明論之間的聯(lián)系的一部分 在此僅概述數(shù)值函數(shù)的某些表示方面的內(nèi)容 非直謂式多態(tài)演算 ? 在 無 類型常量的純 ????中 ， 自然數(shù)類型 的 一種自然選擇 – 若有常量 zero:nat和 succ:nat?nat， 則可以用表達式 succ(succ… (succ zero)… ) 表示自然數(shù) n – 在純 ????中 ， 沒有常量 zero和 succ， 但是可以把這些符號當(dāng)作變量看待 ， 并且對它們進行 ?抽象 ?zero:nat.?succ:nat?(succ… (succ zero)… ) 非直謂式多態(tài)演算 – 類型 名 nat是任意選擇的 ， 把這個符號也當(dāng)作變量看待 ， 并且對它進行 ?抽象 ?nat.?zero:nat.?succ:nat?nat. succ(succ… (succ zero)… ) – 通常用 更簡單的變量名寫出 ， 作為自然數(shù)的一種有用表示 (Church數(shù)碼 ) n? ? ?t.?f : t ? t.?x : t. f nx – 所有 的 Church數(shù)碼都具有類型 nat ? ?t.
規(guī)章制度相關(guān)推薦
鄂ICP備17016276號-1