第4章類型化?演算的模型-wenkub.com
2024-09-24 16:04 本頁面
【正文】 若 E 有最小元 ， 則 CPO D?E 有最小元 D?E 是一個(gè)偏序集合 若 E有最小元 ?E， 則 ?x:D.?E是 D ?E 的最小元 每個(gè)有向集合 S 都有最小上界 f f 是 連續(xù)的 ， 即對(duì)每個(gè)有向的 S ? D ?E ， 有 f (∨ S) ? ∨ f (S) 論域理論模型和不動(dòng)點(diǎn) ? 常用連續(xù)函數(shù) – n元函數(shù)： f :D1? … ?Dn?E 連續(xù) ， 當(dāng)且僅當(dāng)它在每個(gè)變元上連續(xù) – 配對(duì)函數(shù)：若 S ? D和 T ? E都有向 ， 則 ?∨ S, ∨ T? =∨ {?s, t? | s?S, t?T} – 射影函數(shù)： 若 S ? D?E有向 ， 則 Proji(∨ S)=∨ { Proji(x) | x?S} – 函數(shù)應(yīng)用： 若 S ? D?E和 T ? D都有向 ， 則 ∨ S(∨ T) = ∨ {f (x) | f?S, x?T} – 函數(shù)合成： 若 S ? D?E和 T ? E?F都有向 , 則 (∨ S) ? (∨ T) =∨ {g ? f | f?S, g?T} 論域理論模型和不動(dòng)點(diǎn) 不動(dòng)點(diǎn)和完備連續(xù)層級(jí) ? 完備連續(xù) ????層級(jí) – 若有 CPO?Ab0, ?0?, … , ?Abk, ?k?， 則取 Ab0, … , Abk為基類型 – A? ?? ? A? ?A?， 由 ?? ??逐坐標(biāo)地定序 – A??? ? 所有連續(xù)的 f : ?A?, ??? ? ?A?, ???， 由 ????逐點(diǎn)地定序 – 由先前引理 ， 每個(gè) ?A?, ???都是一個(gè) CPO 這是在 CPO?Ab0, ?0?, … , ?Abk, ?k?上 構(gòu)造的類型框架 論域理論模型和不動(dòng)點(diǎn) ? 主要結(jié)論 任何 若干 CPO上的完備連續(xù)類型層級(jí)形成通用模型 ， 并在所有有底元的類型上有最小不動(dòng)點(diǎn)算子 ? 引理 若 D是有底元 CPO， 且 f :D?D連續(xù) ， 則 f 有最小不動(dòng)點(diǎn) fixD f = ∨ {f n (?) | n ? 0}。第 4章 類型化 ?演算的模型 ? PCF語言由三部分組成 – 帶函數(shù)類型和積類型的純類型化 ?演算 – 自然數(shù)類型和布爾類型 – 不動(dòng)點(diǎn)算子 ? 第 2章對(duì)代數(shù)數(shù)據(jù)類型進(jìn)行了透徹的研究 ? 第 3章研究簡單類型化 ?演算 ? 本章先研究遞歸函數(shù)和不動(dòng)點(diǎn)算子 ? 然后研究類型化 ?演算 的 模型，因?yàn)榈?3章的模型不能解釋不動(dòng)點(diǎn)算子 引 言 本章的主要內(nèi)容 ? 遞歸函數(shù)和不動(dòng)點(diǎn)算子 ， 以及 PCF語言的編程實(shí)例 ? 基于完全偏序集合的 ， 帶不動(dòng)點(diǎn)算子的類型化 ?演算的論域理論模型 ? 不動(dòng)點(diǎn)歸納法 ， 這是一種對(duì)遞歸定義進(jìn)行推理的證明方法 遞歸函數(shù) 和不動(dòng)點(diǎn)算子 遞歸函數(shù)和不動(dòng)點(diǎn)算子 ? 在類型化 ?演算中，可以加遞歸定義 letrec f :? = M in N –f可以出現(xiàn)在 M中 –M的類型必須是 ?，否則等式 f = M沒有意義 ? 例： 定義階乘函數(shù)和計(jì)算 5的階乘 letrec f : nat ? nat = ? y : nat.(if Eq? y 0 then 1 else y ? f (y – 1)) in f 5 把該等式看成關(guān)于 f的方程： f : nat ? nat = ?y : nat. if Eq? y 0 then 1 else y ? f (y – 1) 遞歸函數(shù) 和不動(dòng)點(diǎn)算子 ? 從數(shù)學(xué)的觀點(diǎn)看 – 含 PCF表達(dá)式 M的方程 f :? = M是否都有解？ – 若 有若干個(gè)解的話，選擇哪個(gè)解？ – 在討論 PCF的指稱語義時(shí)解決這些問題 ? 從計(jì)算的觀點(diǎn)看 – 遞歸函數(shù)聲明有清楚的計(jì)算解釋 – 因此 ， 暫且假定每個(gè)這樣的等式都有解，并在PCF中增加上述表示它的語法 遞歸函數(shù) 和不動(dòng)點(diǎn)算子 ? 函數(shù)的不動(dòng)點(diǎn) 若 F :? ??是類型 ? 到它 自身 的函數(shù)， 則 F的不動(dòng)點(diǎn)是使得 F (x) = x的值 x :? 例如，自然數(shù)上 – 平方函數(shù)的不動(dòng)點(diǎn)有 0和 1 – 恒等函數(shù)有無數(shù)個(gè)不動(dòng)點(diǎn) – 后繼函數(shù)沒有不動(dòng)點(diǎn) 遞歸函數(shù) 和不動(dòng)點(diǎn)算子 ? 重要聯(lián)系 – 遞歸定義 f :? = M可以用函數(shù) ?f :?.M來表示，因?yàn)楹瘮?shù) ?f :?.M的不動(dòng)點(diǎn)正好是方程 f = M的 解 (?f :?.M)N = N，即 [N/f]M = N， N是 f = M的 解 – 方程 f = M的求解轉(zhuǎn)化 為 找函數(shù) ?f :?.M的不動(dòng) 點(diǎn) 例： 階乘函數(shù)是 F ? ?f : nat ? nat.?y : Eq? y 0 then 1 else y ? f (y – 1) 的不動(dòng)點(diǎn) 遞歸函數(shù) 和不動(dòng)點(diǎn)算子 ? PCF的最后 一個(gè) 基本構(gòu)造 fix? : (? ? ?) ?? , 對(duì)每個(gè)類型 ? – fix?為任何 ? 到 ? 的函數(shù)產(chǎn)生一個(gè)不動(dòng)點(diǎn) – letrec聲明形式看成是 let和不動(dòng)點(diǎn)算子組合的一 種語法美化 letrec f :? ? M in N ?
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1