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 languages, in particular to Datalog.

Least fixed-point 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 fixed-point logic as an expressive database query language.^[2]

Partial fixed-point logic

For a relational signature X, FO(X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a partial fixed point operator ${\displaystyle \operatorname {PFP} }$ used to form formulas of the form ${\displaystyle {\vec {t}}}$, where ${\displaystyle P}$ is a second-order variable, ${\displaystyle {\vec {x}}}$ a tuple of first-order variables, ${\displaystyle {\vec {t}}}$ a tuple of terms and the lengths of ${\displaystyle {\vec {x}}}$ and ${\displaystyle {\vec {t}}}$ coincide with the arity of ${\displaystyle P}$.

Let k be an integer, ${\displaystyle x,y}$ be vectors of k variables, P be a second-order variable of arity k, and let φ be an FO(PFP,X) function using x and P as variables. We can iteratively define ${\displaystyle (P_{i})_{i\in N}}$ such that ${\displaystyle P_{0}(x)=false}$ and ${\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}$ (meaning φ with ${\displaystyle P_{i-1}}$ substituted for the second-order variable P). Then, either there is a fixed point, or the list of ${\displaystyle (P_{i})}$s is cyclic.^[3]

${\displaystyle }$ is defined as the value of the fixed point of ${\displaystyle (P_{i})}$ on y if there is a fixed point, else as false.^[4] Since Ps are properties of arity k, there are at most ${\displaystyle 2^{n^{k}}}$ values for the ${\displaystyle P_{i}}$s, so with a polynomial-space 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 fixed-point logic

Since the iterated predicates involved in calculating the partial fixed point are not in general monotone, the fixed-point may not always exist. FO(LFP,X), least fixed-point 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 fixed-point construction (That is, if the second order variable is P, then ${\displaystyle P_{i}(x)}$ always implies ${\displaystyle P_{i+1}(x)}$).

Due to monotonicity, we only add vectors to the truth table of P, and since there are only ${\displaystyle n^{k}}$ possible vectors we will always find a fixed point before ${\displaystyle n^{k}}$ iterations. The Immerman-Vardi theorem, shown independently by Immerman^[7] and Vardi,^[8] shows that FO(LFP,X) characterises P on all ordered structures.

The expressivity of least-fixed 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 fixed-point logic

Another way to ensure the monotonicity of the fixed-point construction is by only adding new tuples to ${\displaystyle P}$ at every stage of iteration, without removing tuples for which ${\displaystyle P}$ no longer holds. Formally, we define ${\displaystyle \operatorname {IFP} (\phi _{P,x})}$ as ${\displaystyle \operatorname {PFP} (\psi _{P,x})}$ where ${\displaystyle \psi (P,x)=\phi (P,x)\vee P(x)}$.

This inflationary fixed-point agrees with the least-fixed point where the latter is defined. Although at first glance it seems as if inflationary fixed-point logic should be more expressive than least fixed-point logic since it supports a wider range of fixed-point arguments, in fact, every FO(X)-formula is equivalent to an FO(X)-formula.^[10]

Simultaneous induction

While all the fixed-point 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 fixed-point operators or by nesting them, every simultaneous least, inflationary or partial fixed-point can in fact be expressed using the corresponding single-iteration 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(X) is the set of formulas formed from X using first-order connectives and predicates, second-order variables as well as a transitive closure operator ${\displaystyle \operatorname {TC} }$ used to form formulas of the form ${\displaystyle {\vec {s}}{\vec {t}}}$, where ${\displaystyle {\vec {x}}}$ and ${\displaystyle {\vec {y}}}$ are tuples of pairwise distinct first-order variables, ${\displaystyle {\vec {t}}}$ and ${\displaystyle {\vec {s}}}$ tuples of terms and the lengths of ${\displaystyle {\vec {x}}}$, ${\displaystyle {\vec {y}}}$, ${\displaystyle {\vec {s}}}$ and ${\displaystyle {\vec {t}}}$ coincide.

TC is defined as follows: Let k be a positive integer and ${\displaystyle u,v,x,y}$ be vectors of k variables. Then ${\displaystyle {\mathsf {TC}}(\phi _{u,v})(x,y)}$ is true if there exist n vectors of variables ${\displaystyle (z_{i})}$ such that ${\displaystyle z_{1}=x,z_{n}=y}$, and for all Zdroj:https://en.wikipedia.org?pojem=Fixed-point_logic
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.