Vol. 82, No. 1, 1979

Recent Issues
Vol. 332: 1
Vol. 331: 1  2
Vol. 330: 1  2
Vol. 329: 1  2
Vol. 328: 1  2
Vol. 327: 1  2
Vol. 326: 1  2
Vol. 325: 1  2
Online Archive
Volume:
Issue:
     
The Journal
About the journal
Ethics and policies
Peer-review process
 
Submission guidelines
Submission form
Editorial board
Officers
 
Subscriptions
 
ISSN 1945-5844 (electronic)
ISSN 0030-8730 (print)
 
Special Issues
Author index
To appear
 
Other MSP journals
Constructive versions of Tarski’s fixed point theorems

Patrick Cousot and Radhia Cousot

Vol. 82 (1979), No. 1, 43–57
Abstract

Let F be a monotone operator on the complete lattice L into itself. Tarski’s lattice theoretical fixed point theorem states that the set of fixed points of F is a nonempty complete lattice for the ordering of L. We give a constructive proof of this theorem showing that the set of fixed points of F is the image of L by a lower and an upper preclosure operator. These preclosure operators are the composition of lower and upper closure operators which are defined by means of limits of stationary transfinite iteration sequences for F. In the same way we give a constructive characterization of the set of common fixed points of a family of commuting operators. Finally we examine some consequences of additional semi-continuity hypotheses.

Mathematical Subject Classification 2000
Primary: 06A23
Secondary: 03D20
Milestones
Received: 5 December 1977
Revised: 26 June 1978
Published: 1 May 1979
Authors
Patrick Cousot
Radhia Cousot