The knaster-tarski fixed-point theorem is not uniformly constructive

Abstract

Kleene's fixed-point theorem holds uniformly constructive (see [1]). On this basis, a fixed-point theory was developed for the semantics of recursive programs. However, there exist fixed-point theorems which fail to hold uniformly constructive, e.g. the computable transformation (induced by an integral) having no computable fixed-point ([2]). Our aim is to exhibit an example of a family of algorithmically computable functions satisfying the conditions of Knaster-Tarski fixed-point theorem, for which there is no uniform algorithmic way to pass from a function in the family to its least fixed-point. Accordingly, the Knaster-Tarski fixed-point theorem is not uniformly constructive in the sense of recursive analysis [3].

Keywords:

• Constructive proof
• fixed-point theorem

C.R. Categories:

• F.4.1
• 1.1.2