Fixed-point theorem: Difference between revisions

Revision as of 14:05, 12 April 2017

Revision as of 01:18, 20 June 2017

Line 63:

In [[denotational semantics]] of programming languages, a special case of the Knaster–Tarski theorem is used to establish the semantics of recursive definitions. While the fixed-point theorem is applied to the "same" function (from a logical point of view), the development of the theory is quite different.

The same definition of recursive function can be given, in [[computability theory]], by applying [[Kleene's recursion theorem]].<ref>Cutland, N.J., ''Computability: An introduction to recursive function theory'', Cambridge University Press, 1980. ISBN {{isbn|0-521-29465-7}}</ref> These results are not equivalent theorems; the Knaster&ndash;Tarski theorem is a much stronger result than what is used in denotational semantics.<ref>''The foundations of program verification'', 2nd edition, Jacques Loeckx and Kurt Sieber, John Wiley & Sons, ISBN {{isbn|0-471-91282-4}}, Chapter 4; theorem 4.24, page 83, is what is used in denotational semantics, while Knaster&ndash;Tarski theorem is given to prove as exercise 4.3&ndash;5 on page 90.</ref> However, in light of the [[Church&ndash;Turing thesis]] their intuitive meaning is the same: a recursive function can be described as the least fixed point of a certain functional, mapping functions to functions.

The above technique of iterating a function to find a fixed point can also be used in [[set theory]]; the [[fixed-point lemma for normal functions]] states that any continuous strictly increasing function from [[ordinal number|ordinals]] to ordinals has one (and indeed many) fixed points.