| Autor: |
Chen, Zhibo, Pfenning, Frank |
| Rok vydání: |
2023 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has most general unifiers. We extend the algorithm to higher-order rational terms (a.k.a. regular B\"{o}hm trees, a form of cyclic $\lambda$-terms) and show that pattern unification on higher-order rational terms is decidable and has most general unifiers. We prove the soundness and completeness of the algorithm. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
