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

Least fixed-point logic was first studied systematically by Yiannis N. Moschovakis in 1974, 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.

Partial fixed-point logic

For a relational signature X, FO[PFP](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

PFP

{\displaystyle \operatorname {PFP} }

used to form formulas of the form

[

PFP

x

→

,

P

⁡

φ

]

t

→

{\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}

, where

P

{\displaystyle P}

is a second-order variable,

x

→

{\displaystyle {\vec {x}}}

a tuple of first-order variables,

t

→

{\displaystyle {\vec {t}}}

a tuple of terms and the lengths of

x

→

{\displaystyle {\vec {x}}}

and

t

→

{\displaystyle {\vec {t}}}

coincide with the arity of

P

{\displaystyle P}

.

Let k be an integer,

x

,

y

{\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

(

P

i

)

i

∈

N

{\displaystyle (P_{i})_{i\in N}}

such that

P

0

(

x

)

=

f

a

l

s

e

{\displaystyle P_{0}(x)=false}

and

P

i

(

x

)

=

φ

(

P

i

−

1

,

x

)

{\displaystyle P_{i}(x)=\varphi (P_{i-1},x)}

(meaning φ with

P

i

−

1

{\displaystyle P_{i-1}}

substituted for the second-order variable P). Then, either there is a fixed point, or the list of

(

P

i

)

{\displaystyle (P_{i})}

s is cyclic.

[

PFP

x

→

,

P

⁡

φ

]

t

→

{\displaystyle [\operatorname {PFP} _{{\vec {x}},P}\varphi ]{\vec {t}}}

is defined as the value of the fixed point of

(

P

i

)

{\displaystyle (P_{i})}

on

t

→

{\displaystyle {\vec {t}}}

if there is a fixed point, else as false. Since Ps are properties of arity k, there are at most

2

n

k

{\displaystyle 2^{n^{k}}}

values for the

P

i

{\displaystyle P_{i}}

s, so with a polynomial-space counter we can check if there is a loop or not.

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.

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.