In mathematical logic, fixedpoint 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 languages, in particular to Datalog.
Least fixedpoint logic was first studied systematically by Yiannis N. Moschovakis in 1974,^{[1]} and it was introduced to computer scientists in 1979, when Alfred Aho and Jeffrey Ullman suggested fixedpoint logic as an expressive database query language.^{[2]}
YouTube Encyclopedic

1/5Views:3 0376 51810 7989 4951 351

FixedPoint Theorems in Analysis, Logic, and Computer Science

Ep 017: Fixed Point Notation Basics

What is a fixed point?

Lecture 20. Fixed Point Numbers

L21: Fixed Points
Transcription
Partial fixedpoint logic
For a relational signature X, FO[PFP](X) is the set of formulas formed from X using firstorder connectives and predicates, secondorder variables as well as a partial fixed point operator used to form formulas of the form , where is a secondorder variable, a tuple of firstorder variables, a tuple of terms and the lengths of and coincide with the arity of .
Let k be an integer, be vectors of k variables, P be a secondorder variable of arity k, and let φ be an FO(PFP,X) function using x and P as variables. We can iteratively define such that and (meaning φ with substituted for the secondorder variable P). Then, either there is a fixed point, or the list of s is cyclic.^{[3]}
is defined as the value of the fixed point of on y if there is a fixed point, else as false.^{[4]} Since Ps are properties of arity k, there are at most values for the s, so with a polynomialspace counter we can check if there is a loop or not.^{[5]}
It has been proven that on ordered finite structures, a property is expressible in FO(PFP,X) if and only if it lies in PSPACE.^{[6]}
Least fixedpoint logic
Since the iterated predicates involved in calculating the partial fixed point are not in general monotone, the fixedpoint may not always exist. FO(LFP,X), least fixedpoint logic, is the set of formulas in FO(PFP,X) where the partial fixed point is taken only over such formulas φ that only contain positive occurrences of P (that is, occurrences preceded by an even number of negations). This guarantees monotonicity of the fixedpoint construction (That is, if the second order variable is P, then always implies ).
Due to monotonicity, we only add vectors to the truth table of P, and since there are only possible vectors we will always find a fixed point before iterations. The ImmermanVardi theorem, shown independently by Immerman^{[7]} and Vardi,^{[8]} shows that FO(LFP,X) characterises P on all ordered structures.
The expressivity of leastfixed point logic coincides exactly with the expressivity of the database querying language Datalog, showing that, on ordered structures, Datalog can express exactly those queries executable in polynomial time.^{[9]}
Inflationary fixedpoint logic
Another way to ensure the monotonicity of the fixedpoint construction is by only adding new tuples to at every stage of iteration, without removing tuples for which no longer holds. Formally, we define as where .
This inflationary fixedpoint agrees with the leastfixed point where the latter is defined. Although at first glance it seems as if inflationary fixedpoint logic should be more expressive than least fixedpoint logic since it supports a wider range of fixedpoint arguments, in fact, every FO[IFP](X)formula is equivalent to an FO[LFP](X)formula.^{[10]}
Simultaneous induction
While all the fixedpoint operators introduced so far iterated only on the definition of a single predicate, many computer programs are more naturally thought of as iterating over several predicates simultaneously. By either increasing the arity of the fixedpoint operators or by nesting them, every simultaneous least, inflationary or partial fixedpoint can in fact be expressed using the corresponding singleiteration constructions discussed above.^{[11]}
Transitive closure logic
Rather than allow induction over arbitrary predicates, transitive closure logic allows only transitive closures to be expressed directly.
FO[TC](X) is the set of formulas formed from X using firstorder connectives and predicates, secondorder variables as well as a transitive closure operator used to form formulas of the form , where and are tuples of pairwise distinct firstorder variables, and tuples of terms and the lengths of , , and coincide.
TC is defined as follows: Let k be a positive integer and be vectors of k variables. Then is true if there exist n vectors of variables such that , and for all , is true. Here, φ is a formula written in FO(TC) and means that the variables u and v are replaced by x and y.
Over ordered structures, FO[TC] characterises the complexity class NL.^{[12]} This characterisation is a crucial part of Immerman's proof that NL is closed under complement (NL = coNL).^{[13]}
Deterministic transitive closure logic
FO[DTC](X) is defined as FO(TC,X) where the transitive closure operator is deterministic. This means that when we apply , we know that for all u, there exists at most one v such that .
We can suppose that is syntactic sugar for where .
Over ordered structures, FO[DTC] characterises the complexity class L.^{[12]}
Iterations
The fixedpoint operations that we defined so far iterate the inductive definitions of the predicates mentioned in the formula indefinitely, until a fixed point is reached. In implementations, it may be necessary to bound the number of iterations to limit the computation time. The resulting operators are also of interest from a theoretical point of view since they can also be used to characterise complexity classes.
We will define firstorder with iteration, ; here is a (class of) functions from integers to integers, and for different classes of functions we will obtain different complexity classes .
In this section we will write to mean and to mean . We first need to define quantifier blocks (QB), a quantifier block is a list where the s are quantifierfree FOformulae and s are either or . If Q is a quantifiers block then we will call the iteration operator, which is defined as Q written time. One should pay attention that here there are quantifiers in the list, but only k variables and each of those variable are used times.^{[14]}
We can now define to be the FOformulae with an iteration operator whose exponent is in the class , and we obtain the following equalities:
 is equal to FOuniform AC^{i}, and in fact is FOuniform AC of depth .^{[15]}
 is equal to NC.^{[16]}
 is equal to PTIME. It is also another way to write FO(IFP).^{[17]}
 is equal to PSPACE. It is also another way to write FO(PFP). ^{[18]}
Notes
 ^ Moschovakis, Yiannis N. (1974). "Elementary Induction on Abstract Structures". Studies in Logic and the Foundations of Mathematics. 77. doi:10.1016/s0049237x(08)x70922. ISBN 9780444105370. ISSN 0049237X.
 ^ Aho, Alfred V.; Ullman, Jeffrey D. (1979). "Universality of data retrieval languages". Proceedings of the 6th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages  POPL '79. New York, New York, USA: ACM Press: 110–119. doi:10.1145/567752.567763. S2CID 3242505.
 ^ Ebbinghaus and Flum, p. 121
 ^ Ebbinghaus and Flum, p. 121
 ^ Immerman 1999, p. 161
 ^ Abiteboul, S.; Vianu, V. (1989). "Fixpoint extensions of firstorder logic and dataloglike languages". [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. IEEE Comput. Soc. Press. pp. 71–79. doi:10.1109/lics.1989.39160. ISBN 0818619546. S2CID 206437693.
 ^ Immerman, Neil (1986). "Relational queries computable in polynomial time". Information and Control. 68 (1–3): 86–104. doi:10.1016/s00199958(86)800298.
 ^ Vardi, Moshe Y. (1982). "The complexity of relational query languages (Extended Abstract)". Proceedings of the fourteenth annual ACM symposium on Theory of computing  STOC '82. New York, NY, USA: ACM. pp. 137–146. CiteSeerX 10.1.1.331.6045. doi:10.1145/800070.802186. ISBN 9780897910705. S2CID 7869248.
 ^ Ebbinghaus and Flum, p. 242
 ^ Yuri Gurevich and Saharon Shelah, Fixedpointed extension of first order logic, Annals of Pure and Applied Logic 32 (1986) 265280.
 ^ Ebbinghaus and Flum, pp. 179, 193
 ^ ^{a} ^{b} Immerman, Neil (1983). "Languages which capture complexity classes". Proceedings of the fifteenth annual ACM symposium on Theory of computing  STOC '83. New York, New York, USA: ACM Press. pp. 347–354. doi:10.1145/800061.808765. ISBN 0897910990. S2CID 7503265.
 ^ Immerman, Neil (1988). "Nondeterministic Space is Closed under Complementation". SIAM Journal on Computing. 17 (5): 935–938. doi:10.1137/0217058. ISSN 00975397.
 ^ Immerman 1999, p. 63
 ^ Immerman 1999, p. 82
 ^ Immerman 1999, p. 84
 ^ Immerman 1999, p. 58
 ^ Immerman 1999, p. 161
References
 Ebbinghaus, HeinzDieter; Flum, Jörg (1999). Finite Model Theory. Perspectives in Mathematical Logic (2 ed.). Springer. doi:10.1007/9783662031827. ISBN 9783662031841.
 Neil, Immerman (1999). Descriptive complexity. Springer. ISBN 0387986006. OCLC 901297152.