The Fixed-Point Theorem of Priess-Crampe and Ribenboim in Computational Logic
by
Anthony Seda
University College Cork, Ireland.
Coauthors: Pascal Hitzler (University College Cork)

Computational Logic is concerned with the use of logic as a programming language. In practice, this means making deductions from sets of clauses by means of an interpreter or automated theorem prover. In fact, there are four main aspects of the subject: (i) syntax or expressiveness of the system and its computational adequacy (the ability to compute all partial recursive functions); (ii) the procedural semantics of the system or, in other words, what is output by the interpreter; (iii) the declarative semantics or logical meaning of the output; (iv) the fixed-point semantics. These four issues just mentioned are, of course, highly interconnected and, in particular, it is important that the three semantics coincide in some sense.

In fact, what is meant by the ``declarative semantics" is usually some natural model canonically associated with each program permitted by the syntax, and realized as the (least, minimal, unique etc.) fixed point of an operator determined by the program. Unfortunately, most systems with enhanced syntax permit many canonical models, and it is by no means clear which of them is the most satisfactory. One solution to this problem is to consider syntax which obtains computational adequacy but which forces each operator to have a unique fixed point, for then all the canonical models coincide. This raises the question of characterizing classes of programs which have such unique fixed points, and this is a question investigated by the authors by various techniques including the use of many-valued logics.

However, one approach to the problem is to borrow ideas from domain theory and to turn spaces of valuations into generalized ultrametric spaces in the sense of Priess-Crampe and Ribenboim. It then turns out that the operators involved are sometimes strictly contracting and, consequently, have unique fixed points by the fixed-point theorem of Priess-Crampe and Ribenboim. We therefore obtain a rather simple solution to the question posed above, and the purpose of this talk is to discuss the use of the theorem of Priess-Crampe and Ribenboim in theoretical computer science by illustrating, in particular, its use in solving the problem just described.

Date received: June 22, 1999