On Problems Dual to Unification: The String-Rewriting Case
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913182399856640 |
|---|---|
| author | Akçam, Zümrüt Cornell, Kimberly A. Hono II, Daniel S. Narendran, Paliath Pulver, Andrew |
| author_facet | Akçam, Zümrüt Cornell, Kimberly A. Hono II, Daniel S. Narendran, Paliath Pulver, Andrew |
| contents | In this paper, we investigate problems which are dual to the unification problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the Common Equation (CE) problem for string rewriting systems. Our main motivation is computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point (FP) problem is reducible to the common term problem. Our new results are: (i) the fixed point problem is undecidable for finite convergent string rewriting systems whereas it is decidable in polynomial time for finite, convergent and dwindling string rewriting systems, (ii) the common term problem is undecidable for the class of dwindling string rewriting systems, and (iii) for the class of finite, monadic and convergent systems, the common equation problem is decidable in polynomial time but for the class of dwindling string rewriting systems, common equation problem is undecidable. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2103_00386 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | On Problems Dual to Unification: The String-Rewriting Case Akçam, Zümrüt Cornell, Kimberly A. Hono II, Daniel S. Narendran, Paliath Pulver, Andrew Logic in Computer Science In this paper, we investigate problems which are dual to the unification problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the Common Equation (CE) problem for string rewriting systems. Our main motivation is computing fixed points in systems, such as loop invariants in programming languages. We show that the fixed point (FP) problem is reducible to the common term problem. Our new results are: (i) the fixed point problem is undecidable for finite convergent string rewriting systems whereas it is decidable in polynomial time for finite, convergent and dwindling string rewriting systems, (ii) the common term problem is undecidable for the class of dwindling string rewriting systems, and (iii) for the class of finite, monadic and convergent systems, the common equation problem is decidable in polynomial time but for the class of dwindling string rewriting systems, common equation problem is undecidable. |
| title | On Problems Dual to Unification: The String-Rewriting Case |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2103.00386 |