為什么要加寬算子？
因為當格的偏序集合L不滿足升鏈條件，從最小元迭代計算最小不動點的過程是不收斂的，即迭代序列(fⁿ(⊥))ₙ不保證最終穩定，且其最小上界不保證等于最小不動點，因此需要一種近似lfp(f)的方法。引入加寬算子fw:L×L—>L, fw(x)=x▽f(x)，可以將L上的一個序列轉為收斂的升鏈，從L的最小元開始迭代不斷上升，直至lfp(f)的一個上近似即fw的最小不動點lfp(fw)，關系式為lfp(f)<=f(lfp(fw))<=fw(lfp(fw))=lfp(fw)。對上式反復應用f單調得到：lfp(f)<=fⁿ⁺¹(lfp(fw))<=fⁿ(lfp(fw))<=…<=f(lfp(fw))<=lfp(fw)，這表明對lfp(fw)使用f迭代可獲得更精確的上近似，其過程可看成沿一個遞降鏈進一步逼近lfp(f)，但L不一定滿足降鏈條件而導致上述過程不收斂，故需要引入變窄算子fn:L×L—>L, fn(x)=x△f(x)，將L的一個序列轉為收斂的降鏈，從lfp(fw)開始迭代，不斷下降直至fn的一個不動點fp(fn)，則有關系式：lfp(f)<=fp(fn)<=lfp(fw)。注意，這里根據加寬算子的定義可知fw是單調的，但根據變窄算子的定義不確定fn是否單調，故從lfp(fw)迭代求得的fp(fn)，不確定是最小還是最大不動點，只能說是一個不動點，這也反映了變窄算子不需要滿足單調性，就可以更加逼近lfp(f)
posted on 2023-09-06 22:45
春秋十二月 閱讀(95)
評論(0) 編輯 收藏 引用 所屬分類:
Compiler