第4章類型化?演算的模型(編輯修改稿)
2024-11-03 16:04 本頁(yè)面
【文章內(nèi)容簡(jiǎn)介】 – 線性序 對(duì)所有的 x, y?S，都有 x ? y或 y ? x 論域理論模型和不動(dòng)點(diǎn) ? 例 偏序集合 {a0, b0, a1, b1, a2, b2, …} ， 其中對(duì)任意 i? j 都有 ai ? aj, bj并且 bi ? aj, bj – 兩個(gè)線性序 a0?a1?a2?… ，和 b0?b1?b2?… – {ai, bi} 有上界 ai+1和 bi+1等， 但沒(méi)有最小上界 a0 a1 a2 b0 b1 b2 ai和 bi沒(méi)有最小上界 論域理論模型和不動(dòng)點(diǎn) ? 定義 – 完全偏序集合 ?D, ?? （簡(jiǎn)稱 CPO） 若 每個(gè)有向集合 S?D都有最小上界（ ∨ S） ? 例 – 使用離散序，任何集合都可看成 CPO – 任何有限偏序集合都是 CPO – 考慮普通算術(shù)序，自然數(shù)集合不是 CPO – 有理數(shù)的非平凡閉區(qū)間不是 CPO， 所有 小于 的有理數(shù)的最小上界是無(wú)理數(shù) – 若 S， T?D都有向，且 S的每個(gè)元素都 ?T的某個(gè)元素，那么 ∨ S ? ∨ T 2 論域理論模型和不動(dòng)點(diǎn) ? 定義 – 有最小元 的 CPO D ? ?D, ?? 存在元素 a， 使得對(duì) D的任何元素 b都有 a ? b 最小元（也叫底元 ）用 ?D表示 – 提升集合 A? A ? {?} – 提升 CPO D， 類似地可得到 有底元的 CPO D? … 0 1 2 3 4 ? CPO ??的圖形表示 論域理論模型和不動(dòng)點(diǎn) ? 引理 – 若 D是一個(gè) CPO，那么 D?是有底元的 CPO ? 引理 – 若 D和 E都是 CPO并都有底元，則它們的積 D?E也是有底元的 CPO。 而且，若 S?D?E是有向的，則∨ S = ?∨ S1, ∨ S2?， 其中 Si= ProjiS 如果 D和 E分別有最小元 ?D和 ?E， 那么 ??D,?E?是D?E 的最小元 論域理論模型和不動(dòng)點(diǎn) 連續(xù)函數(shù) – CPO上的連續(xù)函數(shù) – 包括了在程序設(shè)計(jì)中使用的所有普通函數(shù) – 給出的是一類有不動(dòng)點(diǎn)的函數(shù) – 本節(jié)證明從一個(gè) CPO到另一個(gè) CPO的所有連續(xù)函數(shù)的集合形成一個(gè) CPO – 在構(gòu)造把每個(gè)類型看成一個(gè) CPO的模型時(shí) ， 這是最本質(zhì)的一步 ， 因?yàn)闃?gòu)造這樣的模型時(shí) ， 函數(shù)類型必須解釋成 CPO 論域理論模型和不動(dòng)點(diǎn) ? 記號(hào) – 如果 f : D ? E是函數(shù) ， 如果 S ? D， 用記號(hào) f(S)表示 E的子集： f (S) = { f (d ) | d?S} ? 定義 – 單調(diào)函數(shù) 若 D=?D, ?D?和 E=?E, ?E?都是 CPO， 且 f : D ?E 是它們基礎(chǔ)集合上的函數(shù) ， 若 d?d?蘊(yùn)涵 f(d)? f (d?), 則 f 單調(diào) 若 f 單調(diào)且 S有向 ， 則 f (S)有向 論域理論模型和不動(dòng)點(diǎn) ? 定義 – 連續(xù)函數(shù) 單調(diào) ， 且 若對(duì)每個(gè)有向的 S ?D， 都有 f (∨ S) ? ∨ f (S) ? 例 – 在實(shí)軸閉區(qū)間 [x, y]上 ， 若把 [x, y]看成 CPO時(shí) ， 則通常計(jì)算意義下的連續(xù)函數(shù)仍然連續(xù) – 任何 CPO上的常函數(shù)是平凡地連續(xù)的 – 若 D是離散序 ， 則 D上每個(gè)函數(shù)都連續(xù) – 從提升集合 A?到任何 CPO的單調(diào)函數(shù)連續(xù) 論域理論模型和不動(dòng)點(diǎn) ? 定義 – 提升函數(shù) 如果 D和 E都是 CPO， 且 f :D ? E連續(xù) ， 定義 f? : (D ? {?}) ? (E ? {?})如下： f?(d) = if d ? D then f(d) else ? – 嚴(yán)格函數(shù) 若 f 是有底元 CPO之間的函數(shù) ， 且 f (?) ? ? ? 引理 – 令 D和 E 都是 CPO, 若 f:D?E連續(xù) , 則 f?:D??E?嚴(yán)格并連續(xù) 論域理論模型和不動(dòng)點(diǎn) ? CPO之間的函數(shù) 集合上的偏序關(guān)系 – 若 D = ?D, ?D?和 E = ?E, ?E?都是 CPO， 對(duì)于連續(xù)函數(shù) f, g:D?E， 若對(duì)每個(gè) d?D， 都有 f(d)?E g(d)， 就說(shuō)f ?D ?E g（ 逐點(diǎn)地排序 ） ? 記號(hào) – 從 D 到 E 的連續(xù)函數(shù)集寫成 D?E ? ?D ? E, ?D ?E? – 若 S ? D ? E是函數(shù)集合 ， 且 d ?D， 那么 S(d) ?E是由 S (d) = {f (d) | f ?S} 給出的集合 表 從 B?到 B?的單調(diào)函數(shù) f (?) f (true) f (false) f (?) f (true) f (false) f0 ? ? ? f6 ? false true f1 ? true ? f7 ? true false
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1