Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Banach's Fixed-Point Theorem as a base for data-type equations

  • 63 Accesses

  • 6 Citations


For a categoryK of data types, solutions of recursive data-type equationsXT(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.


  1. 1.

    J. Adámek: Free algebras and automata realizations in the language of categories,Comm. Math. Univ. Carolinae 15 (1974), 589–602.

  2. 2.

    J. Adámek: Data-type equations in algebraically ω-complete categories,Information and Computation, to appear.

  3. 3.

    P. America and J. Rutten: Solving reflexive domain equations in a category of complete metric spaces,J. Comp. Syst. Sciences 39 (1989), 343–375.

  4. 4.

    J. Adámek and V. Trnková:Automata and Algebras in a Category, Kluwer Publ. Dordrecht, 1990.

  5. 5.

    A. Arnold and M. Nivat: Metric interpretations of infinite trees and semantics of non deterministic recursive programs,Theor. Comp. Science 11 (1980), 181–205.

  6. 6.

    J. W. Bakker and J. I. Zucker: Processes and the denotational semantics of concurrency,Inform. and Control 54 (1982), 70–120.

  7. 7.

    D. Lehmann and M. B. Smyth: Data types, University of Warwick,Theory of Comp. Rep. 19 (1977).

  8. 8.

    E. G. Manes and M. A. Arbib:Algebraic Approaches to Program Semantics, Springer-Verlag, New York, 1986.

  9. 9.

    D. S. Scott:Continuous Lattices, Lect. N. Mathem. 274, Springer-Verlag, 1972, pp. 97–136.

  10. 10.

    M. B. Smyth and G. D. Plotkin: The category-theoretic solutions of recursive domain equations,SIAM J. Comp. 11 (1982), 761–783.

  11. 11.

    M. Wand: Fixed-point constructions in order-enriched categories,Theor. Comp. Sci. 8 (1979), 13–30.

Download references

Author information

Additional information

Dedicated to Dieter Pumplün on the occasion of his 60th birthday

Rights and permissions

Reprints 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).

Download citation

Mathematics Subject Classifications (1991)

  • 68Q65
  • 18D20

Key words

  • Data type equation
  • complete metric space
  • Banach's theorem
  • categories enriched over metric spaces