Abstract
For a categoryK of data types, solutions of recursive data-type equationsX ℞T(X), whereT is an endofunctor ofK, can be constructed by iteratingT on the unique arrowT1 → 1. This is well-known forK enriched over complete posets and forT locally continuous (an application of the Kleene Fixed-Point Theorem). We prove this forK enriched over complete metric spaces and forT contracting (an application of the Banach Fixed-Point Theorem). Moreover, we prove that each such recursive equation has a unique solution. Our results generalize the approach of P. America and J. Rutten.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
J. Adámek: Free algebras and automata realizations in the language of categories,Comm. Math. Univ. Carolinae 15 (1974), 589–602.
J. Adámek: Data-type equations in algebraically ω-complete categories,Information and Computation, to appear.
P. America and J. Rutten: Solving reflexive domain equations in a category of complete metric spaces,J. Comp. Syst. Sciences 39 (1989), 343–375.
J. Adámek and V. Trnková:Automata and Algebras in a Category, Kluwer Publ. Dordrecht, 1990.
A. Arnold and M. Nivat: Metric interpretations of infinite trees and semantics of non deterministic recursive programs,Theor. Comp. Science 11 (1980), 181–205.
J. W. Bakker and J. I. Zucker: Processes and the denotational semantics of concurrency,Inform. and Control 54 (1982), 70–120.
D. Lehmann and M. B. Smyth: Data types, University of Warwick,Theory of Comp. Rep. 19 (1977).
E. G. Manes and M. A. Arbib:Algebraic Approaches to Program Semantics, Springer-Verlag, New York, 1986.
D. S. Scott:Continuous Lattices, Lect. N. Mathem. 274, Springer-Verlag, 1972, pp. 97–136.
M. B. Smyth and G. D. Plotkin: The category-theoretic solutions of recursive domain equations,SIAM J. Comp. 11 (1982), 761–783.
M. Wand: Fixed-point constructions in order-enriched categories,Theor. Comp. Sci. 8 (1979), 13–30.
Author information
Authors and Affiliations
Additional information
Dedicated to Dieter Pumplün on the occasion of his 60th birthday
Rights and permissions
About this article
Cite this article
Adamek, J., Reiterman, J. Banach's Fixed-Point Theorem as a base for data-type equations. Appl Categor Struct 2, 77–90 (1994). https://doi.org/10.1007/BF00878504
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF00878504