HOME

TheInfoList



OR:

In
order theory Order theory is a branch of mathematics that investigates the intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article intr ...
, a branch of
mathematics Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a
partially ordered set In mathematics, especially order theory, a partially ordered set (also poset) formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary ...
to itself is the fixed point which is less than each other fixed point, according to the order of the poset. A function need not have a least fixed point, but if it does then the least fixed point is unique. For example, with the usual order on the
real number In mathematics, a real number is a number that can be used to measure a ''continuous'' one-dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Every ...
s, the least fixed point of the real function ''f''(''x'') = ''x''2 is ''x'' = 0 (since the only other fixed point is 1 and 0 < 1). In contrast, ''f''(''x'') = ''x'' + 1 has no fixed points at all, so has no least one, and ''f''(''x'') = ''x'' has infinitely many fixed points, but has no least one.


Examples

Let G = (V, A) be a
directed graph In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs. Definition In formal terms, a directed graph is an ordered pa ...
and v be a vertex. The
set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...
of vertices accessible from v can be defined as the least fixed-point of the function f: \wp(V) \to \wp(V), defined as f(X) = \ \cup \ . The set of vertices which are co-accessible from v is defined by a similar least fix-point. The
strongly connected component In the mathematical theory of directed graphs, a graph is said to be strongly connected if every vertex is reachable from every other vertex. The strongly connected components of an arbitrary directed graph form a partition into subgraphs that ...
of v is the
intersection In mathematics, the intersection of two or more objects is another object consisting of everything that is contained in all of the objects simultaneously. For example, in Euclidean geometry, when two lines in a plane are not parallel, thei ...
of those two least fixed-points. Let G = (V, \Sigma, R, S_0) be a
context-free grammar In formal language theory, a context-free grammar (CFG) is a formal grammar whose production rules are of the form :A\ \to\ \alpha with A a ''single'' nonterminal symbol, and \alpha a string of terminals and/or nonterminals (\alpha can be em ...
. The set E of symbols which produces the
empty string In formal language theory, the empty string, or empty word, is the unique string of length zero. Formal theory Formally, a string is a finite, ordered sequence of characters such as letters, digits or spaces. The empty string is the special c ...
\varepsilon can be obtained as the least fixed-point of the function f: \wp(V) \to \wp(V), defined as f ( X ) = \, where \wp(V) denotes the
power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is post ...
of V.


Applications

Many
fixed-point theorem In mathematics, a fixed-point theorem is a result saying that a function ''F'' will have at least one fixed point (a point ''x'' for which ''F''(''x'') = ''x''), under some conditions on ''F'' that can be stated in general terms. Some authors cla ...
s yield algorithms for locating the least fixed point. Least fixed points often have desirable properties that arbitrary fixed points do not.


Denotational semantics

In
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, the ''
denotational semantics In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations' ...
'' approach uses least fixed points to obtain from a given program text a corresponding mathematical function, called its semantics. To this end, an artificial mathematical object, \bot, is introduced, denoting the exceptional value "undefined". Given e.g. the program datatype int, its mathematical counterpart is defined as \mathbb_\bot = \mathbb \cup \ ; it is made a partially ordered set by defining \bot \sqsubset n for each n \in \mathbb and letting any two different members n,m \in \mathbb be uncomparable w.r.t. \sqsubset, see picture. The semantics of a program definition int f(int n) is some mathematical function f: \mathbb_\bot \to \mathbb_\bot . If the program definition f does not terminate for some input n, this can be expressed mathematically as f(n) = \bot . The set of all mathematical functions is made partially ordered by defining f \sqsubseteq g if, for each n , the relation f(n) \sqsubseteq g(n) holds, that is, if f(n) is less defined or equal to g(n) . For example, the semantics of the expression x+x/x is less defined than that of x+1, since the former, but not the latter, maps 0 to \bot , and they agree otherwise. Given some program text f, its mathematical counterpart is obtained as least fixed point of some mapping from functions to functions that can be obtained by "translating" f. For example, the C definition int fact(int n) is translated to a mapping :F: (\mathbb_\bot \to \mathbb_\bot) \to (\mathbb_\bot \to \mathbb_\bot) , defined as (F(f))(n) = \begin 1 & \text n = 0, \\ n \cdot f(n-1) & \text n \neq \bot \text n \neq 0, \\ \bot & \text n = \bot. \\ \end The mapping F is defined in a non-recursive way, although fact was defined recursively. Under certain restrictions (see
Kleene fixed-point theorem In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following: :Kleene Fixed-Point Theorem. Suppose (L, \sqsubseteq) is a directed-complete pa ...
), which are met in the example, F necessarily has a least fixed point, \operatorname, that is (F(\operatorname))(n) = \operatorname(n) for all n \in \mathbb_\bot. It is possible to show that :\operatorname(n) = \begin n! & \text n \geq 0, \\ \bot & \text n < 0 \text n = \bot. \end A larger fixed point of F is e.g. the function \operatorname_0 , defined by :\operatorname_0(n) = \begin n! & \text n \geq 0, \\ 0 & \text n < 0, \\ \bot & \text n = \bot, \end however, this function does not correctly reflect the behavior of the above program text for negative n ; e.g. the call fact(-1) will not terminate at all, let alone return 0. Only the ''least'' fixed point, \operatorname , can reasonably be used as a mathematical program semantic.


Descriptive complexity

Immerman and Vardi independently showed the
descriptive complexity ''Descriptive Complexity'' is a book in mathematical logic and computational complexity theory by Neil Immerman. It concerns descriptive complexity theory, an area in which the expressibility of mathematical properties using different types of l ...
result that the polynomial-time computable properties of linearly ordered structures are definable in
FO(LFP) In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query lan ...
, i.e. in
first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
with a least fixed point operator. However, FO(LFP) is too weak to express all polynomial-time properties of unordered structures (for instance that a structure has
even Even may refer to: General * Even (given name), a Norwegian male personal name * Even (surname) * Even (people), an ethnic group from Siberia and Russian Far East **Even language, a language spoken by the Evens * Odd and Even, a solitaire game wh ...
size).


Greatest fixed points

Greatest fixed points can also be determined. In the case of the real numbers the definition is symmetric with the least fixed point, but in
computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
they are less commonly used than least fixed points. Specifically, the posets found in
domain theory Domain theory is a branch of mathematics that studies special kinds of partially ordered sets (posets) commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer ...
usually do not have a greatest element, hence there may be multiple, mutually incomparable maximal fixed points, and the greatest fixed point may not exist. To address this issue, the ''optimal fixed point'' has been defined as the most-defined fixed point compatible with all other fixed points. The optimal fixed point always exists, and is the greatest fixed point if the greatest fixed point exists. The optimal fixed point allows formal study of recursive and corecursive functions that do not converge with the least fixed point. Unfortunately the optimal fixed point of an effective recursive definition may be a non-computable function Here: Example 12.1, pp. 12.2–3 so it is primarily of theoretical interest.


See also

*
Knaster–Tarski theorem In the mathematical areas of order and lattice theory, the Knaster–Tarski theorem, named after Bronisław Knaster and Alfred Tarski, states the following: :''Let'' (''L'', ≤) ''be a complete lattice and let f : L → L be an monotonic function ...
*
Fixed-point logic In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query l ...


Notes

{{reflist


References

* Immerman, Neil. ''
Descriptive Complexity ''Descriptive Complexity'' is a book in mathematical logic and computational complexity theory by Neil Immerman. It concerns descriptive complexity theory, an area in which the expressibility of mathematical properties using different types of l ...
'', 1999, Springer-Verlag. * Libkin, Leonid. ''Elements of Finite Model Theory'', 2004, Springer. Order theory Fixed points (mathematics)