第4章類(lèi)型化?演算的模型-資料下載頁(yè)
2024-09-28 16:04本頁(yè)面
【導(dǎo)讀】PCF語(yǔ)言由三部分組成。–帶函數(shù)類(lèi)型和積類(lèi)型的純類(lèi)型化?第2章對(duì)代數(shù)數(shù)據(jù)類(lèi)型進(jìn)行了透徹的研究。本章先研究遞歸函數(shù)和不動(dòng)點(diǎn)算子。演算的模型，因?yàn)榈?章的?；谕耆蚣系?，帶不動(dòng)點(diǎn)算子的類(lèi)型。不動(dòng)點(diǎn)歸納法，這是一種對(duì)遞歸定義進(jìn)行推。–M的類(lèi)型必須是?，否則等式f=M沒(méi)有意義。例：定義階乘函數(shù)和計(jì)算5的階乘。把該等式看成關(guān)于f的方程：f:nat?–含PCF表達(dá)式M的方程f:?–若有若干個(gè)解的話，選擇哪個(gè)解？點(diǎn)是使得F=x的值x:?–方程f=M的求解轉(zhuǎn)化為找函數(shù)?PCF的最后一個(gè)基本構(gòu)造。繼續(xù)階乘函數(shù)的例子。fixFn//計(jì)算factn的前幾步。–若V是常量、變量、?抽象或值的序?qū)?，則V是值。–0=1，1=1，n對(duì)n?}，真包含所有的fix[i]F(i?–尚不足以相信，對(duì)任意的F，
【正文】 續(xù)的 ? 結(jié)論 – PCF的每個(gè)項(xiàng)在 APCF中都有含義 論域理論模型和不動(dòng)點(diǎn) ? 定理 令 M和 N是 G上的 PCF表達(dá)式 ， 若 G ? M =N :?從 PCF的公理可證 ， 則 APCF滿足等式 G ? M = N : ? ? 推論 若 G?M:?是良類(lèi)型的 PCF項(xiàng) ， 且 M?N， 則 PCF模型 APCF滿足等式 G ? M = N : ? 論域理論模型和不動(dòng)點(diǎn) ? 例 階乘函數(shù)可以寫(xiě)成 fact ? fixnat?nat F， 其中 F ? ?f :nat?nat. ?y:nat. if Eq? y 0 then 1 else y?f (y1) – 可以 證明 ， APCF? F?是連續(xù)的 – APCF ?fact? =∨ {(APCF ?fact?)n (?) | n?0} – (APCF ?fact?)0(?) = ?nat?nat – 直接用 ?項(xiàng)來(lái)表示相應(yīng)論域中元素的名字 論域理論模型和不動(dòng)點(diǎn) (APCF ?fact?)1(?) = ?y:nat. if Eq? y 0 then 1 else y? ((APCF ?fact?)0(?) )(y1) = ?y:nat. if Eq? y 0 then 1 else y ? (?nat?nat) (y1) = ?y:nat. if Eq? y 0 then 1 else ?nat 論域理論模型和不動(dòng)點(diǎn) ? 例 考慮函數(shù) F : (nat?nat) ? (nat?nat)， 其定義為 F ??f :nat?nat. ?x:nat. if Eq? x 1 then 1 else f (x2) 滿足下列條件的函數(shù) g:nat?nat都是上面 F的不動(dòng)點(diǎn) g(1) = 1 g(x+2) = g(x) 最小不動(dòng)點(diǎn)是： 當(dāng) x是奇數(shù)時(shí) ， 結(jié)果是 1 當(dāng) x是偶數(shù)時(shí) ， 計(jì)算不終止 不動(dòng)點(diǎn)歸納 ? 例 如果 f : D ?D和 g : D ?D是某個(gè) CPO D上的連續(xù)函數(shù) ， 則 fix (f ?g) = f (fix (g?f)) fix (f ?g) = ∨ {( f ?g)i (?) | i ? 0} = ∨ {?, ( f ?g) (?), ( f ? g ? f ? g) (?), … } = ∨ {f (?), (f ? (g ? f ))(?), (f ? (g ? f )2)(?),... } = ∨ {( f ? (g ? f )i ) (?) | i ? 0} = f (fix (g?f)) 僅使用 PCF的等式證明系統(tǒng)不可能證明 fix (f ?g) = f (fix (g?f)) 不動(dòng)點(diǎn)歸納 ? 基于項(xiàng)的 CPO解釋來(lái)擴(kuò)展證明系統(tǒng) 在 CPO模型 A中 ， 近似 G ? M ? N ? ?對(duì)環(huán)境 ? ? G是滿足的 ， 如果 A ?M?? ? A ?N?? (eq) (asym) G ? M = N : ? G ? M ? N: ? G ? M ?N : ?, G ? N ? M : ? G ? M = N: ? 不動(dòng)點(diǎn)歸納 (trans) G ? ??? M ? ? (bot) G ? ?? ? ? = ?x : ?. ?? : ? ? ? (botf) (acong) (fcong) G ? M ?N : ?, G ? N ? P : ? G ? M ? P : ? G ? M1 ? M2 : ? ??, G ? N1 ? N2 : ? G ? M1 N1 ? M2 N2 : ? G, x : ? ? M ? N :? G ? ?x : ?. M ? ?x : ?. N : ? ?? 不動(dòng)點(diǎn)歸納 用 F ? A表示從一組等式和近似 F可以證明等式或近 似 A G ? MN = N : ? G ? fix M ? N : ? F ?[?/x] A, F, [c/x]A ?[F(c)/x]A F ?[fix F/x]A 常量 c不在 A中 (fpind) 不動(dòng)點(diǎn)歸納 例 證明 ,如果 N是 M的一個(gè)不動(dòng)點(diǎn) ,那么 fix M ? N – 假定 G ? MN ?N ? ?， 這就有 G ? MN ? N ? ? – 令 A ? G, x :? ? x ? N :?， 其中 x在 N中不是自由的 – 令不動(dòng)點(diǎn)歸納規(guī)則中 F是 M 首先證明 [?/x]A ? G ? ? ? N :? 然后取 [c/x]A ? G ? c ? N :?作為假設(shè) ， 證明 [Mc/x]A ? G ? Mc ? N :? 根據(jù)假設(shè) c ? N,由單調(diào)性 ， 有 G ? Mc ? MN :? 因?yàn)?MN ? N， 所以 G ? Mc ? N :? 第一次： ， ， 第二次： ， 第三次： (a)， (b) 習(xí) 題
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1