Levels of Undecidability in Infinitary Rewriting: Normalization and Reachability

TL;DR

This paper explores the complexity of normalization and reachability in infinitary rewriting, revealing that weak normalization is computationally harder than strong normalization, with both problems situated high in the analytical hierarchy.

Contribution

It establishes the precise complexity levels of infinitary weak and strong normalization, showing weak normalization is Pi-1-2-complete, higher than the Pi-1-1-complete strong normalization.

Findings

Infinitary strong normalization is Pi-1-1-complete.

Infinitary weak normalization is Pi-1-2-complete.

Weak normalization is strictly more complex than strong normalization.

Abstract

In [EGZ09] it has been shown that infinitary strong normalization (SNi) is Pi-1-1-complete. Suprisingly, it turns out that infinitary weak normalization (WNi) is a harder problem, being Pi-1-2-complete, and thereby strictly higher in the analytical hierarchy.