Felgenhauer, Bertram - Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently

lmcs:4035 - Logical Methods in Computer Science, October 29, 2018, Volume 14, Issue 4
Deciding Confluence and Normal Form Properties of Ground Term Rewrite Systems Efficiently

Authors: Felgenhauer, Bertram

It is known that the first-order theory of rewriting is decidable for ground term rewrite systems, but the general technique uses tree automata and often takes exponential time. For many properties, including confluence (CR), uniqueness of normal forms with respect to reductions (UNR) and with respect to conversions (UNC), polynomial time decision procedures are known for ground term rewrite systems. However, this is not the case for the normal form property (NFP). In this work, we present a cubic time algorithm for NFP, an almost cubic time algorithm for UNR, and an almost linear time algorithm for UNC, improving previous bounds. We also present a cubic time algorithm for CR.


Source : oai:arXiv.org:1710.10991
DOI : 10.23638/LMCS-14(4:7)2018
Volume: Volume 14, Issue 4
Published on: October 29, 2018
Submitted on: October 31, 2017
Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science,F.2,F.4


Versions

Share

Consultation statistics

This page has been seen 29 times.
This article's PDF has been downloaded 6 times.