事务逻辑程序的高效表列机制

本文提出了 Horn 事务逻辑（带有状态更新的常规 Horn 逻辑程序的推广）的高效求值算法。我们提出了两种互补的方法来优化事务逻辑的实现。第一种方法基于表列（tabling），我们修改了证明理论以对状态上的调用和答案进行表列处理（实际上等同于动态规划）。调用 - 答案表以调用及发出调用时的状态签名作为索引。答案列包含答案统一化以及执行调用后的状态签名。状态使用基于 trie 树和计数的技术进行高效签名。第二种方法基于增量求值，适用于数据预言机包含派生关系的情况。事务预言机中执行的删除和插入操作会改变数据库的状态。利用惯性启发式规则（只有部分状态响应基本更新而发生变化），在大多数情况下，仅计算状态的变化比从头重新计算整个状态更为廉价。这两种方法是互补的：第一种方法优化了在同一状态下重复调用时的求值，而第二种方法优化了当表列机制未找到调用 - 状态对（即第一种方法未命中）时新状态的求值。应用了表列和增量求值的事务逻辑证明理论，相对于其模型理论是可靠且完备的。