FMT 3: Fixpoint Logics

$% \usepackage{amsmath} % \usepackage{amsfonts} % \usepackage{amssymb} % create the definition symbol \def\bydef{\stackrel{\text{def}}{=}} \newcommand{\qed}{\mbox{ } \Box} \newcommand{\set}[1]{\{#1\}} \newcommand{\eps}{\varepsilon} \newcommand{\NN}{\mathbb N} \newcommand{\Nat}{\mathbb N} \newcommand{\RR}{\mathbb R} \newcommand{\Aa}{\mathcal A} \newcommand{\Bb}{\mathcal B} \newcommand{\Cc}{\mathcal C} \newcommand{\Dd}{\mathcal D} \newcommand{\Ll}{\mathcal L} \newcommand{\str}[1]{\mathbb {#1}} \renewcommand{\implies}{\rightarrow} \newcommand{\lor}{\vee} \newcommand{\land}{\wedge} \renewcommand{\phi}{\varphi} \renewcommand{\subset}{\subseteq} \newcommand{\models}{\vDash} \DeclareMathOperator{\dom}{Dom} \DeclareMathOperator{\ifp}{ifp} \DeclareMathOperator{\lfp}{lfp} \DeclareMathOperator{\gfp}{gfp} \DeclareMathOperator{\tcl}{tcl} \DeclareMathOperator{\ln}{ln} $

In view of Fagin’s Theorem, a the following question arises.

The big question. Does there exist a logic $\Ll$ such that a property of finite structures is definable in the logic $\Ll$ if and only if it is in PTime?

We will see that fixpoint logic offers a partial answer to this question.

Before giving the definitions, let’s see an example.

Example. Consider the signature of directed graphs. The following formula, with free variables $x,y$, says that there is a directed path from $x$ to $y$:

\text{let }&R(z)=\ifp  \left[(z=x)\lor \exists v.R(v)\land E(v,z)\right] \\\text { in }&R(y).

The semantics is as follows. Let $x,y$ be vertices of a graph. Start with $R$ being the empty set of vertices, treated as a unary relation. Repeat indefinitely the following inflationary step:

Add to $R$ those vertices $z$ which satisfy the subformula of ($\diamond$) delimited by the brackets $[\ ]$.

The formula $(\diamond)$ holds for the pair of vertices $(x,y)$ if $y$ belongs to $R$ in some step of the loop. Observe that the property described above is not first-order definable.

Relational operators. Fix a signature $\Sigma$ and let $R$ be an additional symbol for a $k$-ary relation with values in a finite set $Q$.

Let $\phi$ be a formula with values in $Q$, with $k$ distinguished free variables $\bar x$, over the signature $\Sigma\cup\set{R}$. Then $\phi$ defines a mapping of $k$-ary,  $Q$-valued relations over $\str A$, i.e. a self-mapping of the set $P(\str A^k\times Q)$:

$$F_\phi(\mathcal R)=\set{\bar a\in \str A^k: \str A, \mathcal R,\bar a\models \phi}.$$

Fixpoints. A fixpoint of a mapping $F:P(\str A^k\times Q)\to P(\str A^k\times Q)$ is a relation $\mathcal R$ such that $F(\mathcal R)=\mathcal R$.

In general, a mapping may have none or several fixpoints.

  1. Suppose that $F$ is monotone, i.e., $\mathcal R\subset\mathcal S\implies F(\mathcal R)\subset F(\mathcal S)$ for all relations $\mathcal R,\mathcal S$. Then, by the Knaster-Tarski theorem, $F$ has a least fixpoint, denoted $\lfp F$ and a greatest fixpoint, denoted $\gfp F$. Indeed, for the least fixpoint we consider the sequence $F^\alpha(\emptyset)$ defined by transfinite induction for all ordinals $\alpha$ (as usually: $F^{\alpha}=F\circ F^{\alpha-1}$ if $\alpha\ge 1$ is a successor ordinal and $F^{\alpha}(\mathcal R)=\bigcup_{\beta<\alpha}F^{\beta}(\mathcal R)$ if $\alpha$ is a limit point). If $F$ is monotone, then the sequence is increasing and reaches a fixpoint for some ordinal $\alpha$.
  2. Suppose that $F$ is increasing, i.e., $\mathcal R\subset F(\mathcal R)$ for all $\mathcal R$. Then the sequence $F^\alpha(\emptyset)$ is also increasing and reaches a fixpoint (possibly after an infinite ordinal number of steps). Note that this fixpoint need not be the least fixpoint of $F$.
  3. Even if $G$ is a mapping which is not necessarily increasing, then the mapping $F$ given by $\mathcal R\mapsto G(\mathcal R)\cup \mathcal R$ is clearly increasing. We call the fixpoint of the mapping $F$ the inflationary fixpoint of the mapping $G$. Warning: it does not need to be a fixpoint of $G$.


Observe that if $\str A,Q$ and $k$ are finite, then an increasing sequence of subsets of $\str A^k\times Q$ reaches a fixpoint after at most $|\str A|^k\cdot |Q|$ steps, i.e., polynomially many in terms of $|\str A|$ (for fixed $Q$ and $k$).

Inflationary Fixpoint Logic (IFP) is an extension of first-order logic by a fixpoint operation whose syntax is the following:

\text{let }&R(\bar x)=\text{ifp}\ \phi\\\text { in }&\psi,


  • $R$ is a $Q$-valued $k$-ary relation, where $Q$ is some finite set and $k$ is some finite number;
  • $\phi$ is a $Q$-valued formula, over the signature of $\str A$ extended by the symbol $R$. Recall that formally, $\phi$ is a tuple $(\phi_q)_{q\in Q}$ of formulas;
  • $\bar x=(x_1,\ldots,x_k)$ is a $k$-tuple of variables.

The free variables of $\gamma$ are those free variables of $\phi$ which do not occur in $\bar x$, together with the free variables of the formula $\psi$.

The semantics is defined so that the formula $\gamma$ holds in a structure $\str A$, with given valuations for its free variables, iff the formula $\psi$ holds in the structure $\str A$ extended by the relation $\ifp F_\phi$ as the interpretation for the symbol $R$. Note that in the fixpoint, the mapping $F_\phi$ may depend on several parameters – those free variables of $\phi$ which do not occur in the tuple $\bar x$. Note that the values of those parameters are fixed when computing the fixpoint.

A formula of the IFP logic may use the above fixpoint operation
— possibly in a nested way — apart from the usual constructs of first order logic.

The example given earlier demonstrates that the logic IFP is strictly more expressive than first order logic, since reachability cannot be expressed in FO. It turns out that over linearly-ordered structures, IFP is as expressive as polynomial time Turing machines.

Exercise. Show that two-colorability can be decided by a formula of IFP, by simulating the greedy algorithm.

Theorem (Immerman-Vardi). A property of linearly-ordered structures is definable in the logic IFP if and only if this property is in PTime.

Proof. As usual, one direction is easy: from logic to machines. Indeed, let $\phi$ be an IFP formula of linearly ordered structures. Then, for a given description of a structure $\str A$, a Turing machine can evan evaluate $\phi$ over $\str A$ in polynomial time. Since the mapping $\mathcal R\mapsto \mathcal R’$ is monotone (see definition of ifp), it follows that it stabilizes after at most $n^k$ steps, where $k$ is the arity of $\mathcal R$ and $n$ is the size of $\str A.$ Therefore, the computation of the least fixpoint can be executed in polynomial time (the parameter $k$ depends on the formula $\phi$, but not on the input structure $\str A$).

We show the other implication, by following the idea in the proof of Fagin’s theorem. Suppose that $M$ is a Turing machine which recognises a property of linearly-ordered structures in polynomial time. We assume that $M$ expects the adjacency matrix encoding of a structure $(\str A,<)$ on input.  Let $B$ be the work alphabet and $Q$ be the state space of the machine $M.$ Let $k$ be such a number that $M$ works in time at most $n^k$ for structures of size $n\ge 2.$ We will use $f$ as a symbol of a $k$-ary relation (in fact, a function) with values in $B\cup B\times Q$. The formula which holds in $(\str A,<)$ iff $M$ accepts the encoding of $(\str A,<)$ will have the following form:

\text{let }&f(\bar x,\bar y)=\ifp[\phi_1(\bar x,\bar y)\lor \phi_2(\bar x,\bar y)]\\
\text{in }&\exists \bar x,\bar y.T(\bar y),

We need to explain what the formulas $\phi_1,\phi_2$ and $T$ are. As in the proof of Fagin’s theorem, $f$ is intended to be a function encoding a run of the Turing machine, where $f(\bar x,\bar y)=b$ is interpreted as

the tape symbol in the $[x]$-th configuration, at its  $[y]$-th position is $b$,

and $f(\bar x,\bar y)=(b,q)$ additionally asserts that

the head of the machine is located at this position in state $q$.

The formulas $\phi_1(\bar x,\bar y)$ are a $B\cup B\times Q$-valued formulas.

The formula $\phi_1$ encodes the structure $(\str A,<)$ — the existence of such a formula was argued in the proof of Fagin’s theorem. The formula $\phi_2(\bar x,\bar y)$ yields for given $\bar x,\bar y$ the value $b$ or $(b,q)$ depending on the values $f(\bar x_{-1},\bar y_{-1}), f(\bar x_{-1},\bar y), f(\bar x_{-1},\bar y_{+1})$, where $\bar z_{\pm 1}$ denotes a tuple which encodes the number $[\bar z_{\pm 1}]$ which is the successor/predecessor of the number $[\bar z]$ encoded by $\bar z$ (see the proof of Fagin’s theorem). Recall that there are first order formulas $\phi_{\pm 1}(\bar z,\bar u)$ which hold if and only if $\bar u=\bar z_{\pm 1}$. This relies heavily on the given linear order.

The formula $\phi_2$ has the form:


where $\phi_b$ consists of a prefix

$$\exists \bar x_{-1},\bar y_{-1},\bar {y_{+1}}.\phi_{-1}(\bar x,\bar x_{-1})\land\phi_{-1}(\bar y,\bar y_{-1})\land \phi_{+1}(\bar y,\bar y_{+1})$$

followed by a disjunction of formulas of the form

$$f(\bar x_{-1},\bar y_{-1})=c\land f(\bar x_{-1},\bar y)=d\land f(\bar x_{+1},\bar y_{-1})=e,$$ where $c,d,e\in B\cup B\times Q$.

Least Fixpoint Logic.

Another fixpoint logic is the LFP logic. Its syntax and semantics are similar to IFP, but $\ifp$ is replaced by $\lfp$. However, there is one additional syntactic requirement. In order to assure that the mapping $F_\phi$ is monotone (and hence has a least fixpoint), it is required by the syntax that the symbol $R$ occurs positively in $\phi$, i.e., under the scope of an even number of negations.

Example. The formula from the previous example, with $\ifp$ replaced by $\lfp$, becomes a valid formula of LFP logic.

Observe that in the formula constructed in the proof of the theorem, the symbol $f$ appears positively. Therefore, the above proof also works for the LFP logic, giving the original formulation of the Immerman-Vardi theorem.

Theorem (Immerman-Vardi, original form). A property of linearly ordered structures is definable in the logic LFP if and only if this property is in PTime.

The two variants of the theorem together give the following.

Corollary. Over linearly ordered finite structures, the logics LFP and IFP are equally expressive.

Note that converting a formula of LFP into an equivalent formula of IFP is immediate. Indeed, it is enough to substitute $\lfp$ by $\ifp$. However, the conversion in other direction is not at all obvious, since in $\lfp$ the predicate needs to occur positively.

It is a theorem (of Gurevich and Shelah) that over all finite structures, IFP and LFP are equally expressive. Finally, Kreutzer proved that this also holds over all (finite and infinite) structures.

Transitive Closure Logic.

Let $\mathcal R \subset \str (A^k\times Q)\times (\str A^k\times Q)$, i.e., $\mathcal R$ is a $2k$-ary relation with values in $Q\times Q$, or, equivalently, is a binary relation over $\str A^k\times Q$. Then we denote by $\tcl \mathcal R$ the transitive closure of this binary relation, i.e., the relation $\mathcal R\cup \mathcal R^2\cup\ldots$.

The TCL logic is the logic obtained by extending first order logic by the transitive closure operation, whose syntax is as follows:

\text{let }&R(\bar x,\bar y)=\tcl \phi  \\\text { in }&\psi.

Example. Directed reachability can be easily phrased using the logic TCL. Observe that this decision problem is complete for the class NLogSpace.

Exercise. Show that two-colorability can be decided by a formula of IFP, by testing the existence of a cycle of odd-length.

Theorem (Immerman). A property of linearly ordered structures is definable in the logic TCL if and only if this property is in NLogSpace.

Recall that a machine working in NLogSpace has one read-only input tape, and one or more work tapes, whose length — for an input of length $n$ — can be bounded by $k\log n$ for some constant $k$.

We now sketch one direction of the proof: from formulas to machines.  This will not be as immediate as in the proofs of the previous theorems. The main reason is that, when proceeding by induction on the structure of the formula, we need to consider formulas of the form $(\ast)$ and their negations. It is not immediately clear that NLogSpace is capable of evaluating both. Luckily, this is possible, thanks to the Immerman-Szelepcsényi theorem.

First of all, it will be convenient to assume that in the construct $(\ast)$, the formulla $\psi$ is required to be of the form $R(\bar z)$. This can be achieved (with exponential blowup in the size of the formulas), since the formula $(\ast)$ is equivalent to the formula $\psi$, in which each occurrence of a predicate $R(\bar z)$ is replaced by the definition of $R$ as the transitive closure, i.e., by $\textrm{let } R(\bar x,\bar y)=\tcl \phi \textrm{ in }R(\bar z)$.

Note that usually, the set of valuations satisfying a formula $\phi$ cannot be stored in logarithmic space (for example, if $\phi=\top$). Therefore, the machine will need to simulate the evaluation of the formulas top-down, instead of bottom up. A universal/existential quantifier is simulated by a loop through all the elements of the universe. This way, everything boils down to evaluating formulas of the form $(\ast)$ and their negations. Formulas of the form $(\ast)$ can be easily evaluated in nondeterministic logarithmic space, by simply nondeterministically searching a directed path in the graph whose vertices are $k$-tuples of nodes, and edges are defined by the subformula $\phi$, so determining whether two nodes are connected by an edge can be done in LogSpace thanks to the inductive assumption, since $\phi$ is a simpler formula than $(\ast)$.

To deal with formulas of the form $\neg(\ast)$, we recall the following theorem.

Theorem (Immerman-Szelepcsényi). Non-reachability in a directed graph can be determined in NLogSpace. Equivalently, NLogSpace is equal to coNLogSpace.

This finishes the conversion of a formula of TCL into an equivalent machine working in NLogSpace.

For the other direction, it is convenient to note that a work tape can be simulated by variables ranging over the positions of the input word. Formally, let a slider be a variable capable of storing a position of the input word. The allowed operations on sliders are: increment, decrement, BOF and EOF tests (testing if the slider is a the first/last position) and equality tests. Initially, a slider is set to the first position of the input word. A two-way automaton with sliders has a finite number of control states and a finite number of sliders. One of the sliders is distinguished and is called the head. The head additionally has the operation of testing the input letter to which it points. In each step of its computation, basing on the current state and results of slider tests, it moves the sliders in some directions, and changes the current state. The automaton accepts when it reaches an accepting state.

Lemma. NLogSpace is equivalent in expressive power to nondeterministic two-way automata with sliders.

The proof is an exercise. Below is a sketch.

[Sketch. In one direction, sliders can be represented in logspace. In the other way, we want to represent the contents of the work tapes by sliders. Suppose for simplicity that there is one work tape, of size bounded by $\log n$, and storing binary digits.

The content of this work tape is a binary sequence of length $\log n$, which encodes a number in the range $[0,\ldots,n-1]$. This number can be therefore represented by a slider, denoted $c$. Also, the position of the head of this work tape will be interpreted as binary sequence of the form $0\ldots010\ldots 0$ with exactly one nonzero digit, corresponding to the position of the head. Let $d$ be a slider whose position is the binary encoding of this binary sequence.

We observe that the following operations on sliders can be performed by a deterministic two-way automaton with sliders (possibly using a constant number of auxiliary sliders):

  • Add two sliders $x,y$. This is done by repeatedly increasing $x$ and decreasing $y$, until $y$ reaches BOF.
  • Copy the content of a slider to another slider.
  • Duplicate the sliders value — by first copying it and then adding the two values.
  • Halve a sliders value — by initiating another slider to $1$ and then repeatedly duplicating its value, until it reaches the value of the target slider. Then the value in the previous step, which can be stored in an auxiliary slider, is half of the value of the target slider.
  • Test whether a slider is even — by scanning through all possible values $x$, whether $2x$ is equal to the sliders value.

Duplicating and halving a sliders value will be used to simulate moving the work heads position leftward or rightwards. To test the symbol under the work head, one can perform as follows: halve both counters $c$ and $d$ until $d$ becomes equal to $1$ (this can be easily tested). Then test whether $c$ is even or odd. Finally, writing a digit to the work tape at the head position can be simulated by adding or subtracting $c$ from $d$. This ends the sketch of the proof of the lemma.]

To finish the proof of Immerman’s theorem, it is enough to convert a two-way automaton with sliders into an equivalent formula of TCL. To this end, we observe that sliders can be encoded by variables, and the configuration of a two-way automaton with sliders can be encoded by a tuple of variables of fixed length, together with the information about the state of the automaton. Moreover, there is a first-order formula $\phi$ with values in $Q\times Q$ expressing whether there is a transition from one configuration to another. Using this formula, the formula $(\ast)$ expresses whether the automaton accepts the input, where $\psi$ is of the form $\exists \bar x\bar y. R(\bar x,q,\bar y,q’)\land \phi$ where $\phi$ tests that $\bar x,q$ is an initial configuration and $\bar y,q’$ is an accepting configuration.

Exercise. Show that a formula of LFP can be converted into a formula of ESO which is equivalent over arbitrary finite structures. Hint: start by showing how the formula $(\ast)$ of TCL can be expressed in ESO; the ESO formula might want to guess a linear order.



Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>