Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Problems Dual to Unification: The String-Rewriting Case

Zümrüt Akçam, Kimberly A. Cornell, Daniel S. Hono, Paliath Narendran, Andrew Pulver

TL;DR

The paper analyzes three problems—Fixed Point (FP), Common Term (CT), and Common Equation (CE)—as duals of unification within string rewriting systems (SRS), focusing on how complexity bounds shift across system classes. It establishes a tight landscape: FP is undecidable for finite convergent SRS but polynomial-time for dwindling SRS; CT is undecidable for dwindling convergent SRS, while CE is polynomial-time decidable for finite, monadic, convergent SRS and undecidable for dwindling SRS, with both one- and two-mapping variants addressed for monadic systems. The authors connect FP to CT and use PCP/GPCP reductions to prove undecidability results, and they provide constructive polynomial-time algorithms for CE in the monadic setting via regular-language machinery around RF and MP constructs. These results demarcate tractability boundaries for computing fixed points and shared terms/equations in rewriting frameworks, with implications for loop invariants and protocol analysis in finite, monadic, and dwindling regimes. Overall, the work clarifies when dual unification problems are efficiently solvable and when they inherit classic undecidability from PCP-type problems, enriching the theoretical understanding of invariants in rewriting-based systems.

Abstract

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.

On Problems Dual to Unification: The String-Rewriting Case

TL;DR

The paper analyzes three problems—Fixed Point (FP), Common Term (CT), and Common Equation (CE)—as duals of unification within string rewriting systems (SRS), focusing on how complexity bounds shift across system classes. It establishes a tight landscape: FP is undecidable for finite convergent SRS but polynomial-time for dwindling SRS; CT is undecidable for dwindling convergent SRS, while CE is polynomial-time decidable for finite, monadic, convergent SRS and undecidable for dwindling SRS, with both one- and two-mapping variants addressed for monadic systems. The authors connect FP to CT and use PCP/GPCP reductions to prove undecidability results, and they provide constructive polynomial-time algorithms for CE in the monadic setting via regular-language machinery around RF and MP constructs. These results demarcate tractability boundaries for computing fixed points and shared terms/equations in rewriting frameworks, with implications for loop invariants and protocol analysis in finite, monadic, and dwindling regimes. Overall, the work clarifies when dual unification problems are efficiently solvable and when they inherit classic undecidability from PCP-type problems, enriching the theoretical understanding of invariants in rewriting-based systems.

Abstract

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.

Paper Structure

This paper contains 8 sections, 28 theorems, 56 equations, 6 figures, 1 table, 1 algorithm.

Table of Contents

  1. Fixed Point Problem
  2. Fixed Point Problem for Finite and Convergent Systems:
  3. Fixed Point Problem for Dwindling Convergent Systems:
  4. Common Term Problem
  5. Common Term Problem for Convergent and Dwindling Systems
  6. Common Equation Problem
  7. Two-mapping CE Problem for Monadic Systems
  8. One-mapping CE Problem for Monadic Systems

Key Result

Lemma 1

The fixed point problem is reducible to the common term problem.

Figures (6)

  • Figure 1: Some of the classes of String Rewriting Systems
  • Figure 2: DFA $M$ concatenation with a single letter $a$.
  • Figure 3: DFA $M_{}^{\prime}$ can have less than $|F|$ states.
  • Figure 4: DFA $M$ concatenation with a string $Z = a_1 a_2 \ldots a_n$.
  • Figure 5: Different Structures of Green and Orange States.
  • ...and 1 more figures

Theorems & Definitions (56)

  • Lemma 1
  • proof
  • Theorem 1.1
  • proof
  • Lemma 1.2
  • proof
  • Lemma 1.3
  • proof
  • Theorem 1.4
  • Lemma 1.5
  • ...and 46 more