简单类型化l演算.ppt

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * 3.6 各种归约策略 3.6.3 急切归约 最左归约和急切归约 最左归约和PCF的公理语义一致，并且允许不确定地或并行地实现 更常用的次序是急切归约，它和PCF的公理语义不一致 下面的表达式在最左归约下终止，但在急切归约下不终止 let f(x : nat) : nat = 5 in letrec g(x : nat) : nat = g(x + x) in f(g 3) 3.6 各种归约策略 值 指不能再进行急切归约的项，即已完全计算的项 常量、变量和?抽象都是值，值的序对也是值 序对中至少有一元不是值，以及函数应用都不能称为值 急切归约与其它归约策略的主要区别 只有当函数变元是值时才能使用? 归约，只有当序对的两个元素都是值时才能使用Proji归约 3.6 各种归约策略 PCF的急切归约 值 若V是常量、变量、?抽象或值的二元组，则V是一个值 公理 (?x : ?.M)V ?eager ?V?x?M V是值 Proji(V1,V2) ?eager Vi V1, V2是值 0 + 0 ?eager 0, 0 +1 ?eager 1, …, 3 + 5 ?eager 8,… Eq? n n ?eager true, Eq? n m ?eager false 3.6 各种归约策略 if true then M else N ?eager M if false then M else N ?eager N ?x : ?.M = ?y : ?.?y?x?M，y在M中不是自由的 子项规则 nat n是数码 M ?eager M? M + N ?eager M? + N M ?eager M? n + M ?eager n + M? 3.6 各种归约策略 bool n是数码 M ?eager M? Eq? M N ?eager Eq? M? N M ?left M? Eq? n M ?left Eq? n M? M ?eager M? if M then N else P ?eager if M? then N else P 3.6 各种归约策略 序对 V是值 M ?eager M? ?M, N? ?eager ?M?, N? N ?eager N? ?V, N? ?eager ?V, N?? M ?eager M? Proji M ?eager Proji M? 3.6 各种归约策略 函数 V是值 下面一条规则不再需要 M ?eager M? M N ?eager M? N N ?eager N? V N ?eager V N? M ?left M? ?x :? . M ?left ?x :? . M? 3.6 各种归约策略 在实际中用急切计算而不用最左计算的原因 最左归约的实现通常是低效的。当像fx这样的变元传给函数g时（g(fx)），必须传递f 的代码的指针并记住适当的词法环境 最左归约和赋值的组合令人混淆，副作用的出现使得最左计算与不确定计算和并行计算不一致 习 题 第一次：3.3(a)，3.6(b)， 3.9(a) 第二次：3.12，3.14(a)，3.21 第三次：3.22，3.23，3.24，3.27(a)(b)，3.28 * * * * * * * * * * * * * * * * * * * * * * * 3.5 可计算函数编程语言 同余 序对 函数 M = N Proji M = Proji N M = N P = Q ?M, P ? = ? N, Q ? M = N ?x:?. M = ?x:?. N M = N P = Q M P = N Q 3.5 可计算函数编程语言 部分同余规则多余 ?抽象和?应用必须有 例：+的同余规则多余 若M=N