On the Complexity of Equivalence of Specifications of Infinite Objects

J. Endrullis; R.D.A. Hendriks; R.R. Bakhshi

doi:10.1145/2364527.2364551

On the Complexity of Equivalence of Specifications of Infinite Objects

J. Endrullis, R.D.A. Hendriks, R.R. Bakhshi

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

Abstract

We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by λ-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 λ-terms we investigate Böhm-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 II

Original language	English
Title of host publication	Proc. Conf. International Conference on Functional Programming (ICFP 2012)
Publisher	ACM
Pages	153-164
DOIs	https://doi.org/10.1145/2364527.2364551
Publication status	Published - 2012
Event	International Conference on Functional Programming (ICFP) - Duration: 1 Jan 2012 → 1 Jan 2012

Conference

Conference	International Conference on Functional Programming (ICFP)
Period	1/01/12 → 1/01/12

Access to Document

10.1145/2364527.2364551

Persistent URL (handle)

Persistent link

Cite this

@inproceedings{670e9918f1b14780a4fe28ad5ba5d0ba,

title = "On the Complexity of Equivalence of Specifications of Infinite Objects",

abstract = "We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by λ-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 λ-terms we investigate B{\"o}hm-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 II",

author = "J. Endrullis and R.D.A. Hendriks and R.R. Bakhshi",

year = "2012",

doi = "10.1145/2364527.2364551",

language = "English",

pages = "153--164",

booktitle = "Proc. Conf. International Conference on Functional Programming (ICFP 2012)",

publisher = "ACM",

note = "International Conference on Functional Programming (ICFP) ; Conference date: 01-01-2012 Through 01-01-2012",

}

TY - GEN

T1 - On the Complexity of Equivalence of Specifications of Infinite Objects

AU - Endrullis, J.

AU - Hendriks, R.D.A.

AU - Bakhshi, R.R.

PY - 2012

Y1 - 2012

N2 - We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by λ-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 λ-terms we investigate Böhm-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 II

AB - We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by λ-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 λ-terms we investigate Böhm-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 II

U2 - 10.1145/2364527.2364551

DO - 10.1145/2364527.2364551

M3 - Conference contribution

SP - 153

EP - 164

BT - Proc. Conf. International Conference on Functional Programming (ICFP 2012)

PB - ACM

T2 - International Conference on Functional Programming (ICFP)

Y2 - 1 January 2012 through 1 January 2012

ER -

On the Complexity of Equivalence of Specifications of Infinite Objects

Abstract

Conference

Access to Document

Persistent URL (handle)

Fingerprint

Cite this