On the Complexity of Deciding Call-by-Need

TL;DR

This paper advances the understanding of call-by-need computation by providing a simplified automata-based framework that improves decidability proofs and complexity bounds for related rewrite systems.

Contribution

It introduces a direct tree automata approach eliminating the need for ground tree transducers, leading to simpler proofs and better complexity bounds.

Findings

Decidability proofs are achieved using direct tree automata constructions.

The new approach simplifies previous automata-based methods.

Complexity bounds for call-by-need computations are improved.

Abstract

In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground tree transducers we obtained simple decidability proofs for classes of rewrite systems that are much larger than earlier classes defined using the complicated sequentiality concept. In this paper we show that we can do without ground tree transducers in order to arrive at decidability proofs that are phrased in direct tree automata constructions. This allows us to derive better complexity bounds.