Editing Fixed-point theorem (section)

== In algebra and discrete mathematics ==

The [[Knaster&ndash;Tarski theorem]] states that any [[monotonic|order-preserving function]] on a [[complete lattice]] has a fixed point, and indeed a ''smallest'' fixed point.<ref>{{cite journal | author=Alfred Tarski | url=http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.pjm/1103044538 | title=A lattice-theoretical fixpoint theorem and its applications | journal = Pacific Journal of Mathematics | volume=5:2 | year=1955 | pages=285&ndash;309}}</ref> See also [[Bourbaki&ndash;Witt theorem]].

The theorem has applications in [[abstract interpretation]], a form of [[static program analysis]].

A common theme in [[lambda calculus]] is to find fixed points of given lambda expressions. Every lambda expression has a fixed point, and a [[fixed-point combinator]] is a "function" which takes as input a lambda expression and produces as output a fixed point of that expression.<ref>{{cite book|last=Peyton Jones|first=Simon L.|title=The Implementation of Functional Programming|year=1987|publisher=Prentice Hall International|url=http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/}}</ref> An important fixed-point combinator is the [[Fixed-point combinator#Y combinator|Y combinator]] used to give [[Recursion (computer science)|recursive]] definitions.

In [[denotational semantics]] of programming languages, a special case of the Knaster&ndash;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|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|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.

Every [[closure operator]] on a [[poset]] has many fixed points; these are the "closed elements" with respect to the closure operator, and they are the main reason the closure operator was defined in the first place.

Every [[involution (mathematics)|involution]] on a [[finite set]] with an odd number of elements has a fixed point; more generally, for every involution on a finite set of elements, the number of elements and the number of fixed points have the same [[parity (mathematics)|parity]]. [[Don Zagier]] used these observations to give a one-sentence proof of [[Fermat's theorem on sums of two squares]], by describing two involutions on the same set of triples of integers, one of which can easily be shown to have only one fixed point and the other of which has a fixed point for each representation of a given prime (congruent to 1 mod 4) as a sum of two squares. Since the first involution has an odd number of fixed points, so does the second, and therefore there always exists a representation of the desired form.<ref>{{citation
 | last = Zagier | first = D. | authorlink = Don Zagier
 | doi = 10.2307/2323918
 | issue = 2
 | journal = [[American Mathematical Monthly]]
 | mr = 1041893
 | page = 144
 | title = A one-sentence proof that every prime ''p''&nbsp;≡&nbsp;1&nbsp;(mod&nbsp;4) is a sum of two squares
 | volume = 97
 | year = 1990
}}.</ref>