Lean 中的追逐（The Chase）——为存在规则研究构建形式化库

追逐（the chase）是一种_sound_、_complete_ 但可能不终止的算法，用于推理存在规则（即 tuple-generating dependencies，又称 TGDS），这是一种高度表达力的知识表示语言。尽管该算法看似简单，然而关于其理论属性和实用实现优化的研究已发展到需要验证正确性、复现证据变得具有挑战性，而直觉有时也可能误导。在 Lean 中，是一个纯函数式编程语言和交互式定理证明器，其社区积极发展形式化数学库（Mathlib）和计算机科学库（CSLib）。本文，我们自行构建围绕存在规则和追逐算法的 Lean 框架。我们讨论了文献中常见的追逐定义细微差别，并展示了这些定义如何在 Lean 中实现。为说明框架的能力，我们展示追逐结果是通用模型，概述了在无“替代匹配”（alternative matches）情况下甚至是 core 模型的形式化证明。除已有文献之外，我们将足够的追逐终止条件（类似 Model-Faithful Acyclicity, MFA）统一纳入同一框架，同时支持规则中的常量。