一种具有相等性的数据集求值算法
An Evaluation Algorithm for Datalog with Equality
摘要：
我们描述了一个关系Horn逻辑（RHL）的评估算法。RHL扩展了Datatron的量化排序，结论中的存在量化，以及至关重要的是，推断等式的能力。这些功能允许RHL评估，以取代和扩展应用程序的数据包和同余闭包算法。我们解释了如何方面的快速同余闭包算法可以被纳入数据库评估，以获得一个有效的RHL评估算法。然后，我们概述了如何Steensgaard的点到分析和类型推断可以使用RHL评估实现。这里描述的RHL和评估算法是Eqlog数据库引擎的基础。
英文摘要：
We describe an evaluation algorithm for relational Horn logic (RHL). RHL extends Datalog with quantification over sorts, existential quantification in conclusions and, crucially, the ability to infer equalities. These capabilities allow RHL evaluation to subsume and expand applications of Datalog and congruence closure algorithms. We explain how aspects of a fast congruence closure algorithm can be incorporated into Datalog evaluation to obtain an efficient RHL evaluation algorithm. We then sketch how Steensgaard's points-to analysis and type inference can be implemented using RHL evaluation. RHL and the evaluation algorithm described here are the foundation of the Eqlog Datalog engine.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
