4.3论域理论模型和不动点 (xmF)和F的不动点 让fact=n(ficlmF)是有直观计算意义的 -尚不足以相信，对任意的F, (xm侧F)就是F的不动点 一强加一些相对自然的条件到F才能保证这一点 当用集合包含对部分函数排序时， n(fixclnl F将 是F的最小不动点
4.3 论域理论模型和不动点 • n ( fix[n]F)和F的不动点 – 让fact = n ( fix[n]F)是有直观计算意义的 – 尚不足以相信，对任意的F， n ( fix[n]F)就是F的不动点 – 强加一些相对自然的条件到F才能保证这一点 – 当用集合包含对部分函数排序时， n ( fix[n]F)将 是F的最小不动点
4.3论域理论模型和不动点 论域 一用集合之间的包含 关系来定义部分函数 常函数1 阶乘函数 之间的偏序 KoDIDCD RoDGD22 -在类型化入演算的 论域理论模型中， {《0,1),X1,1》 类型指称值的偏 K0,18 序集合，叫做论域
4.3 论域理论模型和不动点 • 论域 – 用集合之间的包含 关系来定义部分函数 之间的偏序 – 在类型化演算的 论域理论模型中， 类型指称值的偏 序集合，叫做论域 {0,1,1,1,2,1} 常函数1 阶乘函数 {0,1,1,1,2,2} {0,1,1,1} {0,1} {0,5} . . . . . . . . . . . . . . . . . . . . . . .