A Note on a Unifying Proof of the Undecidability of Several Diagrammatic Properties of Term Rewriting Systems

TL;DR

This paper presents a simplified, unified proof demonstrating the undecidability of various diagrammatic properties in term rewriting systems by encoding Turing Machine configurations into terms.

Contribution

It introduces a unifying approach to prove undecidability of multiple properties in term rewriting systems through coding Turing Machine configurations.

Findings

Undecidability of local confluence, strong confluence, and diamond property.

Unified proof technique for multiple diagrammatic properties.

Encoding Turing Machines into terms to analyze properties.

Abstract

In this note we give a simple unifying proof of the undecidability of several diagrammatic properties of term rewriting systems that include: local confluence, strong confluence, diamond property, subcommutative property, and the existence of successor. The idea is to code configurations of Turing Machines into terms, and then define a suitable relation on those terms such that the termination of the Turing Machine becomes equivalent to the satisfiability of the diagrammatic property.