Charles Explorer logo
🇬🇧

Lambda-Confluence Is Undecidable for Clearing Restarting Automata

Publication at Faculty of Mathematics and Physics |
2013

Abstract

Clearing restarting automata are based on contextual rewriting. A word w is accepted by an automaton of this type if there is a computation that reduces the word w to the empty word λ by a finite sequence of rewritings.

Accordingly, the word problem for a clearing restarting automaton can be solved nondeterministically in quadratic time. If, however, the contextual rewritings happen to be λ-confluent, that is, confluent on the congruence class of the empty word, then the word problem can be solved deterministically in linear time.

Here we show that, unfortunately, λ-confluence is not even recursively enumerable for clearing restarting automata. This follows from the fact that λ-confluence is not recursively enumerable for finite factor-erasing string-rewriting systems.