第4章类型化演算的模型

第4章类型化演算的模型内容摘要：

– 线性序 对所有的 x, yS，都有 x  y或 y  x 论域理论模型和不动点 • 例 偏序集合 {a0, b0, a1, b1, a2, b2, …} ， 其中对任意 i j 都有 ai  aj, bj并且 bi  aj, bj – 两个线性序 a0a1a2… ，和 b0b1b2… – {ai, bi} 有上界 ai+1和 bi+1等， 但没有最小上界 a0 a1 a2 b0 b1 b2 ai和 bi没有最小上界 论域理论模型和不动点 • 定义 – 完全偏序集合 D,  （简称 CPO） 若 每个有向集合 SD都有最小上界（ ∨ S） • 例 – 使用离散序，任何集合都可看成 CPO – 任何有限偏序集合都是 CPO – 考虑普通算术序，自然数集合不是 CPO – 有理数的非平凡闭区间不是 CPO， 所有 小于 的有理数的最小上界是无理数 – 若 S， TD都有向，且 S的每个元素都 T的某个元素，那么 ∨ S  ∨ T 2 论域理论模型和不动点 • 定义 – 有最小元 的 CPO D  D,  存在元素 a， 使得对 D的任何元素 b都有 a  b 最小元（也叫底元 ）用 D表示 – 提升集合 A A  {} – 提升 CPO D， 类似地可得到 有底元的 CPO D … 0 1 2 3 4  CPO 的图形表示 论域理论模型和不动点 • 引理 – 若 D是一个 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 的最小元 论域理论模型和不动点 连续函数 – CPO上的连续函数 – 包括了在程序设计中使用的所有普通函数 – 给出的是一类有不动点的函数 – 本节证明从一个 CPO到另一个 CPO的所有连续函数的集合形成一个 CPO – 在构造把每个类型看成一个 CPO的模型时 ， 这是最本质的一步 ， 因为构造这样的模型时 ， 函数类型必须解释成 CPO 论域理论模型和不动点 • 记号 – 如果 f : D  E是函数 ， 如果 S  D， 用记号 f(S)表示 E的子集： f (S) = { f (d ) | dS} • 定义 – 单调函数 若 D=D, D和 E=E, E都是 CPO， 且 f : D E 是它们基础集合上的函数 ， 若 dd蕴涵 f(d) f (d), 则 f 单调 若 f 单调且 S有向 ， 则 f (S)有向 论域理论模型和不动点 • 定义 – 连续函数 单调 ， 且 若对每个有向的 S D， 都有 f (∨ S)  ∨ f (S) • 例 – 在实轴闭区间 [x, y]上 ， 若把 [x, y]看成 CPO时 ， 则通常计算意义下的连续函数仍然连续 – 任何 CPO上的常函数是平凡地连续的 – 若 D是离散序 ， 则 D上每个函数都连续 – 从提升集合 A到任何 CPO的单调函数连续 论域理论模型和不动点 • 定义 – 提升函数 如果 D和 E都是 CPO， 且 f :D  E连续 ， 定义 f : (D  {})  (E  {})如下： f(d) = if d  D then f(d) else  – 严格函数 若 f 是有底元 CPO之间的函数 ， 且 f ()   • 引理 – 令 D和 E 都是 CPO, 若 f:DE连续 , 则 f:DE严格并连续 论域理论模型和不动点 • CPO之间的函数 集合上的偏序关系 – 若 D = D, D和 E = E, E都是 CPO， 对于连续函数 f, g:DE， 若对每个 dD， 都有 f(d)E g(d)， 就说f D E g（ 逐点地排序 ） • 记号 – 从 D 到 E 的连续函数集写成 DE  D  E, D E – 若 S  D  E是函数集合 ， 且 d D， 那么 S(d) E是由 S (d) = {f (d) | f S} 给出的集合 表 从 B到 B的单调函数 f () f (true) f (false) f () f (true) f (false) f0    f6  false true f1  true  f7  true false。