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 to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
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.
Dedicated to Dieter Pumplün on the occasion of his 60th birthday
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
Mathematics Subject Classifications (1991)
- Data type equation
- complete metric space
- Banach's theorem
- categories enriched over metric spaces