Datalog Self Interpretation

Question

According to https://link.springer.com/article/10.1007%2Fs001530050135 (Logics that define their own semantics, Imhof 1999) the logic FO[LFP] can define its own semantics, though the proof (of corollary 6.4) is somehow fuzzy. It is known from finite model theory that Datalog is equivalent to FO[LFP] (on ordered structures). Can someone help me see (at least partially) how to write a Datalog self-interpreter? The main difficulty is to express modus-ponens considering unification without involving existential variables in heads (i.e. variables in heads which don't appear in bodies and are understood to be existentially quantified).

Another related puzzle of mine is, if LFP's data complexity is P, and its query complexity is EXPTIME, how come it can interpret itself indeed? (I have no doubt that it can as the paper above supplied two different proofs for that. also we know that provably P!=EXPTIME)

Answer 1

Partial answer only.

For me, the paper is behind a paywall. So I can base this only on its abstract and your question.

I believe you have a point with your complexity doubts. I can see how to write an FO[LFP] self-interpreter, provided there is a way to handle large arities. In particular, the self-interpreter has a single, fixed, maximum arity and number of variables while the interpreted formulae should be unbounded with respect to arity and number of variables. I can see a few ways to go about that:

1. There is in fact not a single self-interpreter, but a family of such, indexed by maximum arity.

2. The structure that encodes the input (the formula plus the original structure) has in its domain not only (subformulae of the formula and) elements of the original structure, but also tuples of the original structure up to the required arity. Then, converting the original input into its encoding structure already imposes an exponential blowup.

3. For infinite structures, tuples can be encoded as single elements using a pairing function. On well-ordered structures, FO[LFP] can define (ordinal) arithmetic and hence such a pairing function. Possibly, the statement in the paper does not address finite structures at all?

For the Datalog self-interpreter, I suggest you start with a Datalog interpreter written in FO[LFP] and then convert that formula into a Datalog query.