ISSN:
1572-9095
Keywords:
68Q65
;
18D20
;
Data type equation
;
complete metric space
;
Banach's theorem
;
categories enriched over metric spaces
Source:
Springer Online Journal Archives 1860-2000
Topics:
Mathematics
Notes:
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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00878504
Permalink
