4.2 递归函数和不动点算子 4.2.2有不动点算子的急切归约 考虑x对各种归约策略的影响 -最左归约、惰性归约、并行归约 只要在原来的公理中增加x归约公理即可 -急切归约 若沿用原来的x规测，则对变元先求值的要求 会导致归约不终止 引入“延迟”(dely)来暂停对递归定义函数 的归约，直到有变元提供给它为止
4.2 递归函数和不动点算子 4.2.2 有不动点算子的急切归约 考虑fix对各种归约策略的影响 – 最左归约、惰性归约、并行归约 只要在原来的公理中增加fix归约公理即可 – 急切归约 若沿用原来的fix规则，则对变元先求值的要求 会导致归约不终止 引入“延迟”（ delay）来暂停对递归定义函数 的归约，直到有变元提供给它为止
4.2 递归函数和不动点算子 值（在急切归约中需要引入值的概念） -若V是常量、变量、抽象或值的序对，则是值 delayM 入x:G.Mx,x在M:o→x中非自由的 公理 -(x:.M)V->eager [V/x]M V是值 -Proj(V1,V2)>eager Vi V和V是值 -i。→x→eager风dela'r_alfixa)V是值 子项规则 一和上一章一样
4.2 递归函数和不动点算子 值（在急切归约中需要引入值的概念） – 若V是常量、变量、抽象或值的序对，则V是值 – delay→ M x:.Mx, x在M : → 中非自由的 公理 – (x :.M)V →eager VxM V是值 – Proji (V1 , V2 ) →eager Vi V1和V2是值 – fix→V →eager V(delay → fix→V) V是值 – … … 子项规则 – 和上一章一样
4.2 递归函数和不动点算子 例：仅含一个平凡不动点 (fix (hx nat->nat.hy nat.y))((Az nat.3 +1)2) -→eager(2x:nat-→nat.入nai.2(dela[fix(2x:nat→>nL. Av nat.p))((Az nat.z +1)2) >eager(Ay:naty)((z nat.z +1)2) →eager(y:naty)(2+1)-→eager2:naty3→eager3 例：急切归约可能发散（无不动点》 let f(x nat)nat 5 in letrec g (x nat):nat=g (x+1)in f(g 3)
4.2 递归函数和不动点算子 • 例：仅含一个平凡不动点 (fix (x : nat → nat.y : nat.y)) ((z : nat.z +1)2) →eager(x:nat → nat.y:nat.y)(delayfix(x:nat → nat. y : nat.y)) ((z : nat.z +1)2) →eager(y:nat.y)((z : nat.z +1)2) →eager (y:nat.y)(2+1) →eager (y:nat.y)3 →eager 3 • 例：急切归约可能发散（无不动点） let f (x : nat) : nat = 5 in letrec g (x : nat) : nat = g (x +1) in f (g 3)
4.3论域理论模型和不动点 4.3.1递归定义和不动点算子 -用归约的特点来启发论域的主要性质 以阶乘函数为例： fact fixnatynat F,其中F是表达式 F 入f:nat-→nat.入y:nat.ifEq？y0then1 else y*f(y-1) -考虑xF的有限步展开，用另一种方式来理解 fact
4.3 论域理论模型和不动点 4.3.1 递归定义和不动点算子 – 用fix归约的特点来启发论域的主要性质 – 以阶乘函数为例： fact fixnat→nat F，其中F是表达式 F f :nat→nat.y:nat.if Eq? y 0 then 1 else yf (y-1) – 考虑fix F的有限步展开，用另一种方式来理解 fact
4.3论域理论模型和不动点 ·cF的有限步展开 fxlm网F描述F体的计算最多使用n次的递归计算 -ixF=diverge(表示处处无定义的函数) -fixlntilF=F(fixlmF) -fix2F0=1,(fi2F)1=1,(icl2Fn对n≥2没 有定义 把函数看成二元组的集合后，xl+F=(fxmF U{Kn,n)},真包含所有的fixliF(isn) 即☑≤{K0,0}s{K0,0),1,1}≤K0,0),1,1> 〈2,2》}三…
4.3 论域理论模型和不动点 • fix F的有限步展开 fix[n]F描述F体的计算最多使用n次的递归计算 – fix[0]F = diverge （表示处处无定义的函数） – fix[n+1]F = F(fix[n]F) – (fix[2]F) 0 = 1，(fix[2]F)1 = 1，(fix[2]F) n对n 2没 有定义 – 把函数看成二元组的集合后，fix[n+1]F = (fix[n]F) {n, n}，真包含所有的fix[i]F (in) – 即 {0, 0!} {0, 0!, 1, 1!} {0, 0!, 1, 1!, 2, 2!} …