笔记：LP的自然层化和不动点语义（2）良基模型

Teodor C. Przymusinski: Every Logic Program Has a Natural Stratification  And an Iterated Least Fixed Point Model. PODS 1989: 11-21 (download)(citation)

==Well-Founded Model==

首先，翻译： Well-Founded Model=良基模型

（BTW，我搜索这个词，发现一本书叫《语义网的规划与规则记帐语言》。同志们啊，Rules and Rule Markup Languages for the Semantic Web这个会议伤不起啊！人家不是记帐的有木有！！）

这篇文章先定义良基模型的一个迭代不动点（Iterated Fixed Point）定义。比如现在有一个模型I。我们定义两个操作TI和FI。TI是从I中，我们可以直接得到的新的真T的事实。FI是从I中，我们可以直接得到的新的假F的事实。

具体来说，如果存在一个规则 B<-L1,L2…，如果L1，L2…都为T，那B为T。如果对所有的规则，L1或L2或…为F，那B为F。B的真值会加到I的扩展里。

TI和FI操作都是单调的：只加元素，不减元素。

开始我们假定所有的fact都是假的, 也就是 T0为空，F0包括所有的fact。

然后迭代，T_n+1 = TI (T_n), F_n+1 = FI (F_n)

T_i单调增，F_i单调减。所有{T_i}的并（union）是一个不动点Tfp，所有{F_i}的交（intersection）也是一个不动点Ffp。

Tfp包含了所有可能获得的真fact，Ffp包含了所有可能获得的假fact。

如果我们开始假定所有的fact都是U，然后用<TI,FI>操作，最后得到不断增大的模型。如果到第d步，再没有新的fact，那就进入不动点，d程序的深度depth。

定理：对一个程序P，最小三值模型也是<TI,FI>操作的最小不动点，同时也是P的良基模型。证明很长，跳过。

注意，perfect model（完美模型）也是用迭代最小不动点定义的——如果LP是局域层化的（locally stratified）。文章下一步就要论证，基于迭代最小不动点，其实所有的LP都有层化，称为动态层化。这就把完美模型语义扩展到所有的LP。