Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-29T02:10:43.641Z Has data issue: false hasContentIssue false
  • English
  • Français

On the complexity of stream equality

Part of: JFP Research Articles

Published online by Cambridge University Press:  20 January 2014

JÖRG ENDRULLIS ,
DIMITRI HENDRIKS ,
RENA BAKHSHI  and
GRIGORE ROŞU
JÖRG ENDRULLIS
Affiliation:
VU University Amsterdam, The Netherlands (e-mail: [email protected])
DIMITRI HENDRIKS
Affiliation:
VU University Amsterdam, The Netherlands (e-mail: [email protected])
RENA BAKHSHI
Affiliation:
VU University Amsterdam, The Netherlands (e-mail: [email protected])
GRIGORE ROŞU
Affiliation:
University of Illinois at Urbana-Champaign, USAUniversity Alexandru Ioan Cuza, Iaşi, Romania
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We study the complexity of deciding the equality of streams specified by systems of equations. There are several notions of stream models in the literature, each generating a different semantics of stream equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy. Their complexity ranges from low levels of the arithmetical hierarchy such as Π02 for the most relaxed stream models, to levels of the analytical hierarchy such as Π11 and up to subsuming the entire analytical hierarchy for more restrictive but natural stream models. Since all these classes properly include both the semi-decidable and co-semi-decidable classes, it follows that regardless of the stream semantics employed, there is no complete proof system or algorithm for determining equality or inequality of streams. We also discuss several related problems, such as the existence and uniqueness of stream solutions for systems of equations, as well as the equality of such solutions.

Type
Articles
Information
Journal of Functional Programming , Volume 24 , Issue 2-3: ICFP 2012 , May 2014 , pp. 166 - 217
Copyright
Copyright © Cambridge University Press 2014 

References

Aczel, P. (1988) Non-well-founded Sets, Lecture Notes, no. 14. Stanford, CA: Center for the Study of Language and Information, Stanford University.Google Scholar
Bidoit, M., Hennicker, R. & Kurz, A. (2003) Observational logic, constructor-based logic, and their duality. Theor. Comput. Sci. 298, 471–510.Google Scholar
Böhm, C. (ed.) (1975) Lambda-Calculus and Computer Science Theory: Proceedings of the Symposium Held in Rome, March 25-27, 1975, LNCS, vol. 37. Berlin: Springer.CrossRefGoogle Scholar
Buss, S. R. & Roşu, G. (2000) Incompleteness of behavioral logics. Electron. Notes Theor. Comput. Sci. 33, 61–79.Google Scholar
Castro, J. & Cucker, F. (1989) Nondeterministic ω-computations and the analytical hierarchy. Logik und Grundlagen der Mathematik 35, 333–342.Google Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J. & Talcott, C. (2003) The Maude 2.0 system. In Proceedings of the Conference on Rewriting Techniques and Applications (RTA 2003), Nieuwenhuis, R. (ed.), Lecture Notes in Computer Science, vol. 2706. Berlin: Springer, pp. 76–87.CrossRefGoogle Scholar
Coquand, Th. (1993) Infinite objects in type theory. In Proceedings of the Conference on Types for Proofs and Programs (TYPES 1993), Barendregt, H. & Nipkow, T. (eds), Lecture Notes in Computer Science, vol. 806. Berlin: Springer, pp. 62–78.Google Scholar
Danielsson, N. A. (2010) Beating the productivity checker using embedded languages. EPTCS 43, 29–48.Google Scholar
Dershowitz, N., Kaplan, S. & Plaisted, D. A. (1991) Rewrite, rewrite, rewrite, rewrite, rewrite. Theor. Comput. Sci. 83, 71–96.Google Scholar
Ehrig, H. & Mahr, B. (1985) Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science. Berlin: Springer.Google Scholar
Endrullis, J., Geuvers, H., Simonsen, J. G. & Zantema, H. (2011b) Levels of undecidability in rewriting. Inf. Comput. 209 (2), 227–245.CrossRefGoogle Scholar
Endrullis, J., Grabmayer, C. & Hendriks, D. (2008) Data-oblivious stream productivity. In Proceedings of the Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2008), Cervesato, I., Veith, H. & Voronkov, A. (eds), Lecture Notes in Computer Science, vol. 5330. Berlin: Springer, pp. 79–96.Google Scholar
Endrullis, J., Grabmayer, C. & Hendriks, D. (2009) Complexity of fractran and productivity. In Proceedings of ther Conference on Automated Deduction (CADE 22), Schmidt, R. A. (ed.), LNCS, vol. 5663. Berlin: Springer, pp. 371–387.Google Scholar
Endrullis, J., Grabmayer, C., Hendriks, D., Isihara, A. & Klop, J. W. (2010a) Productivity of stream definitions. Theor. Comput. Sci. 411, 765–782.Google Scholar
Endrullis, J., Grabmayer, C., Hendriks, D., Klop, J. W. & van Oostrom, V. (2010b) Unique normal forms in infinitary weakly orthogonal rewriting. LIPIcs 6, 85–102.Google Scholar
Endrullis, J., Hendriks, D. & Bakhshi, R. (2012b) On the complexity of equivalence of specifications of infinite objects. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). New York: ACM, pp. 153–164.CrossRefGoogle Scholar
Endrullis, J., Hendriks, D. & Bodin, M. (2013) Circular coinduction in Coq using bisimulation-up-to techniques. In Proceedings of the Conference on Interactive Theorem Proving (ITP 2013), Lecture Notes in Computer Science, vol. 7998. Berlin: Springer, pp. 354–369.Google Scholar
Endrullis, J., Hendriks, D. & Klop, J. W. (2011a) Degrees of streams. J. Integers 11B (A6), 1–40.Google Scholar
Endrullis, J., Hendriks, D. & Klop, J. W. (2012a) Highlights in infinitary rewriting and lambda calculus. Theor. Comput. Sci. 464, 48–71.Google Scholar
Finkel, O. & Lecomte, D. (2009) Decision problems for Turing machines. Inf. Process. Lett. 109 (23–24), 1223–1226.Google Scholar
Friedman, D. P. & Wise, D. S. (1976) CONS should not evaluate its arguments. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP 1976), Edinburgh: Edinburgh University Press, pp. 257–284.Google Scholar
Geuvers, H. (1992) Inductive and coinductive types with iteration and recursion. Paper presented at the Proceedings of the Workshop on Types for Proofs and Programs (TYPES 1992), Sweden, pp. 193–217.Google Scholar
Goguen, J. (1991) Types as theories. In Topology and Category Theory in Computer Science. Oxford: Oxford University Press, pp. 357–390.Google Scholar
Goguen, J. & Malcolm, G. (2000) A hidden agenda. Theor. Comput. Sci. 245 (1), 55–101.CrossRefGoogle Scholar
Goguen, J. A., Thatcher, J. W., Wagner, E. G. & Wright, J. B. (1977) Initial algebra semantics and continuous algebras. JACM 24 (1), 68–95.Google Scholar
Grabmayer, C., Endrullis, J., Hendriks, D., Klop, J. W. & Moss, L. S. (2012) Automatic sequences and zip-specifications. In Proceedings of the Symposium on Logic in Computer Science (LICS 2012). Washington, DC: IEEE Computer Society, pp. 335–344.Google Scholar
Harel, D. (1985). Recurring dominoes: Making the highly undecidable highly understandable. In Topics in the Theory of Computation, Selected Papers of the International Conference on Foundations of Computation Theory, FCT 1983, vol. 102. Amsterdam: North-Holland, pp. 51–71.Google Scholar
Harel, D., Kozen, D. & Tiuryn, J. (2000) Dynamic Logic. Foundations of Computing. Cambridge, MA: MIT Press.Google Scholar
Henderson, P. & Morris, J. H. Jr. (1976) A lazy evaluator. In Proceedings of the ACM SIGACT-SIGPLAN Symposium on Principles on Programming Languages (POPL 1976). New York: ACM, pp. 95–103.Google Scholar
Hennicker, R. (1991) Context induction: A proof principle for behavioural abstractions and algebraic implementations. Form. Asp. Comput. 3 (4), 326–345.Google Scholar
Hinman, P. G. (1978) Recursion-Theoretic Hierarchies. Perspectives in Mathematical Logic, vol. 9. Berlin: Springer.Google Scholar
Kennaway, J. R., Klop, J. W., Sleep, M. R. & de Vries, F.-J. (1997) Infinitary lambda calculus. Theor. Comput. Sci. 175 (1), 93–125.Google Scholar
Ketema, J. & Simonsen, J. G. (2010) Infinitary combinatory reduction systems: Normalising reduction strategies. Logical Methods Comput. Sci. 6 (1:7), 1–35.Google Scholar
Klop, J. W. & de Vrijer, R. (2005) Infinitary normalization. In We Will Show Them: Essays in Honour of Dov Gabbay (2). College Publications, pp. 169–192. Available at: ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R0516.pdf.Google Scholar
Landin, P. J. (1965) Correspondence between Algol 60 and Churchs lambda-notation: Part I. Commun. ACM 8 (2), 89–101.Google Scholar
Lucanu, D., Goriac, E.-I., Caltais, G. & Rosu, G. (2009) CIRC: A behavioral verification tool based on circular coinduction. In Proceedings of the Conference on Algebra and Coalgebra in Computer Science (CALCO 2009), Lecture Notes in Computer Science, vol. 5728. Berlin: Springer, pp. 433–442.Google Scholar
Malcolm, G. (1997) Hidden algebra and systems of abstract machines. Paper presented at the Proceedings of the Symposium on New Models for Software Architecture (IMSA).Google Scholar
Meyer, A. R., Streett, R. S. & Mirkowska, G. (1981) The deducibility problem in propositional dynamic logic. In Proceedings of the 8th Colloquium on Automata, Languages and Programming (ICALP 1981), Even, S. & Kariv, O. (eds), Lecture Notes in Computer Science, vol. 115. Berlin: Springer, pp. 238–248.Google Scholar
Niqui, M. (2009) Coalgebraic reasoning in Coq: Bisimulation and the λ-coiteration scheme. In Proceedings of the Workshop on Types for Proofs and Programs (TYPES 2008), Lecture Notes in Computer Science, vol. 5497. Berlin: Springer, pp. 272–288.Google Scholar
Odifreddi, P. G. (1992) Classical recursion theory. In The Theory of Functions and Sets of Natural Numbers, vol. 1, Studies in Logic and the Foundations of Mathematics, vol. 125. Amsterdam: Elsevier.Google Scholar
Odifreddi, P. G. (1999) Classical recursion theory. In The Theory of Functions and Sets of Natural Numbers, vol. 2, Studies in Logic and the Foundations of Mathematics, vol. 143. Amsterdam: Elsevier.Google Scholar
Peyton-Jones, S. (2003) Haskell 98 Language and Libraries, The Revised Report. Cambridge: Cambridge University Press.Google Scholar
Rogers, H. Jr. (1967) Theory of Recursive Functions and Effective Computability. New York: McGraw-Hill.Google Scholar
Roşu, G. (2000) Hidden Logic. Ph.D. thesis, University of California.Google Scholar
Roşu, G. (2006) Equality of streams is a Π02-complete problem. In Proceedings of the ACM SIGPLAN Conference on Functional Programming (ICFP 2006). New York: ACM, pp. 184–191.Google Scholar
Rutten, J. J. M. M. (2000) Universal coalgebra: A theory of systems. Theor. Comput. Sci. 249 (1), 3–80.Google Scholar
Rutten, J. J. M. M. (2003) Behavioural differential equations: A coinductive calculus of streams, automata, and power series. Theor. Comput. Sci. 308 (1–3), 1–53.Google Scholar
Rutten, J. J. M. M. (2005) A coinductive calculus of streams. Math. Struct. Comput. Sci. 15, 93–147.Google Scholar
Shoenfield, J. R. (1971) Degrees of Unsolvability. New York: North-Holland.Google Scholar
Sijtsma, B. A. (1989) On the productivity of recursive list definitions. ACM Trans. Program. Lang. Syst. 11 (4), 633–649.Google Scholar
Sleep, M. R., Plasmeijer, M. J. & van Eekelen, M. C. J. D. (eds) (1993) Term Graph Rewriting: Theory and Practice. Chichester: John Wiley.Google Scholar
Terese. (2003) Term Rewriting Systems. Cambridge: Cambridge University Press.Google Scholar
Turner, D. A. (1986) An overview of Miranda. SIGPLAN Not. 21 (12), 158–166.Google Scholar
Zantema, H. & Endrullis, J. (2011) Proving equality of streams automatically. Paper presented at the Proceedings of the Conference on Rewriting Techniques and Applications (RTA 2011), pp. 393–408.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.