类型化
第4章类型化演算的模型
– 线性序 对所有的 x, yS，都有 x y或 y x 论域理论模型和不动点 • 例 偏序集合 {a0, b0, a1, b1, a2, b2, …} ， 其中对任意 i j 都有 ai aj, bj并且 bi aj, bj – 两个线性序 a0a1a2… ，和 b0b1b2… – {ai, bi} 有上界 ai+1和 bi+1等， 但没有最小上界 a0 a1