We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were obtained by replaying existing proofs for plain term rewrite systems in a constrained setting, involving a non-trivial effort. We present a simple transformation from logically constrained rewrite systems to term rewrite systems such that critical pairs of the latter correspond to constrained critical pairs of the former. The usefulness of the transformation is illustrated by lifting the advanced confluence results based on (almost) development closed critical pairs as well as on parallel critical pairs to the constrained setting.

翻译：我们证明了终止的局部约束重写系统的（局部）合流性是不可判定的，即使其底层理论是可判定的。目前已有若干针对逻辑约束重写系统的合流性判定准则，这些准则通过在约束环境下复现纯项重写系统的既有证明而获得，其间涉及大量非平凡的工作。本文提出一种从逻辑约束重写系统到项重写系统的简洁转换方法，使得后者的关键对恰好对应于前者的约束关键对。通过将基于（近似）开发封闭关键对及并行关键对的先进合流性结论提升至约束环境，我们展示了该转换方法的实用价值。