The Fixed-Point Theory of Strictly Contracting Functions on Generalized Ultrametric Semilattices

TL;DR

This paper introduces generalized ultrametric semilattices and proves a constructive fixed-point theorem for strictly contracting functions, with applications in logic programming and timed computation.

Contribution

It develops a new class of structures and a constructive fixed-point theorem, extending prior non-constructive results in ultrametric semilattices.

Findings

Constructive fixed-point theorem for strictly contracting functions.

Introduction of generalized ultrametric semilattices.

Applications in logic programming and timed computation.

Abstract

We introduce a new class of abstract structures, which we call generalized ultrametric semilattices, and in which the meet operation of the semilattice coexists with a generalized distance function in a tightly coordinated way. We prove a constructive fixed-point theorem for strictly contracting functions on directed-complete generalized ultrametric semilattices, and introduce a corresponding induction principle. We cite examples of application in the semantics of logic programming and timed computation, where, until now, the only tool available has been the non-constructive fixed-point theorem of Priess-Crampe and Ribenboim for strictly contracting functions on spherically complete generalized ultrametric semilattices.