In
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
, 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
Descriptive complexity is a branch of computational complexity theory and of finite model theory that characterizes complexity classes by the type of logic needed to express the languages in them. For example, PH, the union of all complexity clas ...
and their relationship to
database query languages, in particular to
Datalog
Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties ...
.
Least fixed-point logic was first studied systematically by
Yiannis N. Moschovakis
Yiannis Nicholas Moschovakis ( el, Γιάννης Μοσχοβάκης; born January 18, 1938) is a set theorist, descriptive set theorist, and recursion (computability) theorist, at UCLA.
His book ''Descriptive Set Theory'' (North-Holland) is ...
in 1974, and it was introduced to computer scientists in 1979, when
Alfred Aho
Alfred Vaino Aho (born August 9, 1941) is a Canadian computer scientist best known for his work on programming languages, compilers, and related algorithms, and his textbooks on the art and science of computer programming.
Aho was elected into ...
and
Jeffrey Ullman
Jeffrey David Ullman (born November 22, 1942) is an American computer scientist and the Stanford W. Ascherman Professor of Engineering, Emeritus, at Stanford University. His textbooks on compilers (various editions are popularly known as the d ...
suggested fixed-point logic as an expressive database query language.
Partial fixed-point logic
For a
relational signature ''X'', FO
FP''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
used to form formulas of the form
, where
is a second-order variable,
a tuple of first-order variables,
a tuple of terms and the lengths of
and
coincide with the arity of
.
Let be an integer,
be vectors of variables, be a second-order variable of arity , and let be an FO(PFP,X) function using and as variables. We can iteratively define
such that
and
(meaning with
substituted for the second-order variable ). Then, either there is a fixed point, or the list of
s is cyclic.