On the Complexity of Equivalence of Specifications of Infinite Objects

TL;DR

This paper analyzes the computational complexity of various notions of equality for infinite objects specified by equations and lambda-terms, revealing that some decision problems are highly complex, surpassing the entire analytical hierarchy.

Contribution

It precisely characterizes the complexity of different equality notions for infinite objects, showing that some are extremely high in the hierarchy, unlike previously known results.

Findings

Equality in all models is highly complex, surpassing the analytical hierarchy.

Equality of equationally specified streams is Pi^0_2-complete, contrasting with more complex notions.

Complexity varies significantly depending on the type of specification and equality notion.

Abstract

We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by lambda-terms. For equational specifications there are several natural notions of equality: equality in all models, equality of the sets of solutions, and equality of normal forms for productive specifications. For lambda-terms we investigate Boehm-tree equality and various notions of observational equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy. We show that the complexity of deciding equality in all models subsumes the entire analytical hierarchy. This holds already for the most simple infinite objects, viz. streams over {0,1}, and stands in sharp contrast to the low arithmetical Pi^0_2-completeness of equality of equationally specified streams derived in [Rosu 2006] employing a different notion of equality.