面向现实 CHR 程序基于不变式与等价性证明合流性的约束求解器

非确定性程序的合流性保证了函数式的输入输出关系，使程序员无需考虑实际调度策略，并允许优化乃至并行的实现。更一般的模等价合流性保证等价输入关联到等价输出，而输出不必相同。亦考虑了不变式下的合流性。Constraint Handling Rules（CHR）是基于重写的逻辑编程语言的重要范例，我们旨在获得一种可机械化的方法，用于证明终止程序的模等价合流性。先前针对 CHR 程序合流性的方法涉及理想化逻辑子集，而我们参照与标准基于 Prolog 的实现兼容的语义。我们指定了一种元级约束语言，可在其中表达与操作不变式和等价关系，从而将我们先前理论结果扩展向实际实现。