正则表达式行为距离的完整定量公理化

确定性自动机通常从语言等价性的角度进行研究，但另一种视角是通过衡量状态之间最短区分词距离的标准方法。直观地说，当观察两个状态差异所需的词越长，则它们的行为越接近。本文给出正则语言之间最短区分词距离的完整、可靠的公理化。我们的公理化依赖于一种新近发展的等式逻辑的定量类比，允许操作形式为 $e \equiv_\varepsilon f$ 的有理指数判决，即术语 $e$ 在误差容限 $\varepsilon$ 内近似等价于术语 $f$。论文的技术核心专注于完备性论证，通过借助序论和巴拿赫空间中的技术简化行为距离的计算，使其能够被公理化推理所仿真。