论文标题
快速使用追逐
Fast Left Kan Extensions Using The Chase
论文作者
论文摘要
我们展示了如何将左KAN扩展的计算简化为笛卡尔（有限限制）理论的自由模型的计算。我们讨论了标准和并行追逐如何计算常规理论的弱自由模型和笛卡尔理论的自由模型，并将“自由模型”的概念与称为“通用模型”的数据库理论的类似概念进行比较。我们证明，作为计算笛卡尔理论有限模型的算法，在公平性假设下，标准和平行的追逐是完整的。最后，我们描述了专门针对左KAN扩展的平行追逐的优化实现，与我们知道的下一个最快的左KAN扩展算法相比，我们所知道的下一个最快的左KAN基准测试量可以改善我们的性能基准。
We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories, and compare the concept of "free model" with a similar concept from database theory known as "universal model". We prove that, as algorithms for computing finite free models of cartesian theories, the standard and parallel chase are complete under fairness assumptions. Finally, we describe an optimized implementation of the parallel chase specialized to left Kan extensions that achieves an order of magnitude improvement in our performance benchmarks compared to the next fastest left Kan extension algorithm we are aware of.
