| Autor: |
Niederhauser, Johannes, Hirokawa, Nao, Middeldorp, Aart |
| Rok vydání: |
2024 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
