arXiv CSopen access

From Time to Space: The Impact of Linearity in Higher-Order Datalog

© The Author(s), 2021. Published by Cambridge University Press 2021

TPLP: Page 1–8.

1

doi:10.1017/xxxxx

From Time to Space: The Impact of Linearity in Higher-Order Datalog ANGELOS CHARALAMBIDIS, BABIS KOSTOPOULOS Harokopio University of Athens, Greece

(e-mails: [email protected], [email protected])

arXiv:2606.02394v1 [cs.PL] 1 Jun 2026

PANOS RONDOGIANNIS National and Kapodistrian University of Athens, Greece

(e-mail: [email protected])

Abstract We consider a fragment of Higher-Order Datalog with negation and argue that it generalizes the familiar and important fragment of Linear Datalog. We investigate the expressive power of this fragment, establishing a tight connection with the hierarchy of space complexity classes. In particular, we demonstrate that for all k ≥ 1, the (k + 1)-order fragment of Stratified Linear Higher-Order Datalog ¬ captures (k − 1)-EXPSPACE. This result suggests that restricting programs to linear recursion shifts the expressive power of the corresponding fragments from time to space, generalizing the classical result that (Stratified) Linear Datalog captures NL. Unlike the first-order setting where an ordering assumption is required to capture NL, our results hold without any such assumption on the input database. The proof relies on simulating space-bounded Turing machines using Stratified Linear Higher-Order Datalog¬ programs and providing a space-efficient evaluation of the query program. We argue that identifying such computationally well-behaved fragments is a crucial step towards paving the way for practical implementations of Higher-Order Datalog. Under consideration for publication in Theory and Practice of Logic Programming (TPLP). KEYWORDS: Higher-Order Datalog, Linear Datalog, Descriptive Complexity.

1 Introduction Over more than two decades, research in logic programming has shifted towards studying and efficiently implementing fragments that are sufficiently expressive for demanding practical applications. Answer Set Programming (ASP) exemplifies this trend: despite not being Turing-complete, ASP has found diverse applications and gained broad acceptance as a robust paradigm. Recent investigations have explored extending ASP “beyond NP” (Bogaerts et al. 2016; Amendola et al. 2019; Fandinno et al. 2021). More recently, Higher-Order Datalog with negation (Bogaerts et al. 2024) has been proposed as a powerful candidate for such an extension. In particular, it has been shown (Charalambidis et al. 2025) that k + 1-order Datalog with negation, k ≥ 1, captures k-EXPTIME under the well-founded semantics, and captures co-k-NEXPTIME and k-NEXPTIME under the stable model semantics for cautious and brave reasoning, respectively. However, this power comes at a cost: increased expressiveness inevitably places a significant burden

2

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

on implementation. Consequently, identifying a fragment of Higher-Order Datalog with negation that can express problems beyond NP and that is still amenable to efficient implementation, remains a major challenge. Table 1. Expressive power results (entries with a “∗” use the ordering assumption). Fragment

Order of the program 1

2

···

k+1

Higher-Order Datalog¬ Stratified Higher-Order Datalog¬

P∗

EXPTIME

···

k-EXPTIME

Stratified Linear Higher-Order Datalog¬

NL∗

PSPACE

···

(k − 1)-EXPSPACE

A promising avenue of research is the study of a linear fragment of Higher-Order Datalog with negation. In the first-order Datalog setting, linearity is a pivotal property defined by restricting every rule body to contain at most one recursive atom (Ullman 1989, Chapter 15). This restriction is practically significant for two reasons. First, it is widely recognized that Linear Datalog suffices to express most “real-life” recursive queries, see, e.g., (Consens and Mendelzon 1990, p. 405). Second, from an implementation standpoint, Linear Datalog is far more amenable to specialized optimizations than full Datalog (Ullman 1989). Theoretically, this efficiency is formalized by the fact that Linear Datalog captures NL (Nondeterministic Logarithmic Space) on ordered databases (Dantsin et al. 2001). Intuitively, this implies that a query can be evaluated using logarithmic space relative to the input size. In practical terms, the evaluation engine need not store the entire history of derivations, but only the current state of the computation (e.g., the “current node” in a traversal). This favorable complexity profile extends to programs with negation: it has been shown that Stratified Linear Datalog - where rules are limited to linear recursion within the same stratum - also captures NL on ordered databases (Consens and Mendelzon 1990). It is therefore interesting (and potentially practical) to investigate what linearity means in a higher-order setting and its precise expressive power. In this paper, we undertake the study of the above question. We generalize the concept of Stratified Linear Datalog to the higher-order setting, getting a language which in the rest of the paper we will refer to as Stratified Linear Higher-Order Datalog ¬ . Our extension is based on the notion of stratification introduced by Bogaerts et al. (2024), which ensures programs are stratified not only with respect to negation but also with respect to higherorder application. Our central contribution proves that for all k ≥ 1, the (k + 1)-order fragment of Stratified Linear Higher-Order Datalog¬ captures (k − 1)-EXPSPACE. Unlike the first-order setting where an ordered database is required to capture NL, our higherorder characterization holds without any such ordering assumption. Since k-EXPSPACE is a subset of the k-EXPTIME class captured by the unrestricted Higher-Order Datalog¬ language (Charalambidis et al. 2025), our results indicate that, potentially, linearity leads to a more “manageable” language from an implementation point of view. Table 1 shows more compactly the aforementioned results: the second row is new, the first one is from (Charalambidis et al. 2025). Surprisingly, our results have a direct correspondence with Neil Jones’ results (Jones 2001) on the expressive power of the tail-recursive fragments

From Time to Space: The Impact of Linearity in Higher-Order Datalog

3

of a restricted higher-order functional language. Given the close conceptual link between tail-recursion and linearity, it is remarkable but not totally unexpected that these distinct programming paradigms capture identical complexity hierarchies. In conclusion, the main contributions of the present paper can be summarized as follows: • Extension of Linearity: We extend the classical notion of linearity to the class of higher-order Datalog programs. We believe that this extension establishes the basis for developing novel optimizations for higher-order logic programming. • Lower Bound Simulation: We provide a simulation of space-bounded Turing machines using Stratified Linear Higher-Order Datalog¬ , using higher-order predicates to encode the counting of the tape-space of the Turing machine, its configurations, and its execution. The simulation is natural and does not require any tedious encodings. This simplicity suggests that the proposed language is not merely a theoretical construct, but a natural and intuitive fragment of Higher-Order Datalog¬ . • Upper Bound and Space Efficient Evaluation: We present a space-efficient proof procedure for computing queries. By using top-down evaluation, we avoid the full program interpretation, which would otherwise consume space that is towerexponential in the order of the program. We believe that a refinement of our proof procedure could lead to a viable implementation of the proposed language. Sections 2 and 3 introduce the syntax, semantics, and motivation for Stratified Linear Higher-Order Datalog¬ . Sections 4, 5, and the Appendix establish theoretical space complexity bounds and the correctness proof of the space-efficient evaluation algorithm.

2 Higher-Order Datalog with Negation: Preliminaries In this section we introduce the syntax of Higher-Order Datalog¬ , following Bogaerts et al. (2024). The language uses two base types: o, the Boolean domain, and ι, the domain of data objects. The composite types are partitioned into predicate ones (assigned to predicate symbols) and argument ones (assigned to parameters of predicates). Definition 2.1 Types are either predicate or argument, denoted by π and ρ respectively, and defined as: π := o | (ρ → π) ρ := ι | π The binary operator → is right-associative. Every predicate type π can be written in the form ρ1 → · · · → ρn → o, n ≥ 0 (for n = 0 we assume that π = o). Definition 2.2 The alphabet of Higher-Order Datalog¬ consists of: predicate variables of every predicate type π (denoted by capital letters such as P, Q, . . .); predicate constants of every predicate type π (denoted by lowercase letters such as p, q, . . .); individual variables of type ι (denoted by capital letters such as X, Y, . . .); individual constants of type ι (denoted by lowercase letters such as a, b, . . .); the equality constant ≈ of type ι → ι → o; the conjunction constant ∧ of type o → o → o; the inverse implication constant ← of type o → o → o; and the negation constant not of type o → o.

4

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis Arbitrary variables (either predicate or individual ones) will be denoted by R.

Definition 2.3 The expressions and literals of Higher-Order Datalog¬ are defined as follows. Every predicate variable/constant and every individual variable/constant is an expression of the corresponding type; if E1 is an expression of type ρ → π and E2 an expression of type ρ then (E1 E2 ) is an expression of type π. Every expression of type o is called an atom. If E is an atom, then E and (not E) are literals of type o; if E1 and E2 are expressions of type ι, then (E1 ≈ E2 ) and not (E1 ≈ E2 ) are literals of type o. We will omit parentheses when no confusion arises. Definition 2.4 A rule of Higher-Order Datalog¬ is a formula p R1 · · · Rn ← L1 ∧ . . . ∧ Lm , where p is a predicate constant of type ρ1 → · · · → ρn → o, R1 , . . . , Rn are distinct variables of types ρ1 , . . . , ρn respectively and the Li are literals. The literal p R1 · · · Rn is the head of the rule and L1 ∧ . . . ∧ Lm is the body of the rule. A program P of Higher-Order Datalog¬ is a finite set of rules. We will write L1 , . . . , Lm instead of L1 ∧ · · · ∧ Lm for the body of a rule. For brevity, we will often denote a rule as p R ← B, where R is a shorthand for a sequence of variables R1 · · · Rn and B represents the body of the rule. We will avoid using currying as much as possible and will use tuples instead, a syntax that is more familiar to logic programmers. The tuple syntax can be directly transformed to the curried one by a simple preprocessing. So, for example, instead of succ Ord X Y we will write succ(Ord,X,Y), instead of the partial application succ Ord we will write succ(Ord), and so on. More generally, the partial application p E1 · · · En will be written as p(E1 , . . . , En ). Example 1 The following is a Higher-Order Datalog¬ program defining the subset predicate of type (ι → o) → (ι → o) → o: it takes two first-order unary relations (ie., two sets) as arguments and checks if the first is a subset of the second: subset (P , Q ) ← not nonsubset (P , Q ). nonsubset (P , Q ) ← P ( X ) , not Q ( X ).

Note how we implement universal quantification in the body of a rule: to express that P is a subset of Q, i.e., that every X that belongs to P also belongs to Q, we just require that it is not the case that P is a nonsubset of Q, i.e., it is not the case that there exists X that belongs to the first relation but not the other. The formal semantics of Higher-Order Datalog¬ Bogaerts et al. (2024) is detailed in the appendix , but is not required to follow this paper. The programs considered here can be understood purely declaratively. The fragments of Higher-Order Datalog¬ we investigate are semantically well-behaved; the predicates we employ simply denote extensional higherorder relations. For instance, a unary second-order predicate denotes a relation that accepts a classical set as an argument and evaluates to true or false. The notion of order of a predicate, is formally defined as follows: Definition 2.5

From Time to Space: The Impact of Linearity in Higher-Order Datalog

5

The order of a type is recursively defined as follows: order(ι) = 0 order(o) = 1 order(ρ → π) = max{order (ρ) + 1, order (π)} The order of a predicate constant (or variable) is the order of its type. Definition 2.6 For all k ≥ 1, k-Order Datalog¬ is the fragment of Higher-Order Datalog¬ in which all variables have order less than or equal to k − 1 and all predicate constants in the program have order less than or equal to k.

3 Stratified Linear Higher-Order Datalog¬ In this section we formally define the class of Stratified Linear Higher-Order Datalog ¬ programs and illustrate it by examples. This class is a proper extension of the class of Stratified Linear Datalog programs, initially studied by Consens and Mendelzon (1990). We need a notion of stratification for higher-order programs. In analogy to Datalog, there exists a natural such notion for Higher-Order Datalog¬ (Bogaerts et al. 2024). Definition 3.1 A program P is called stratified if there exists a function S mapping predicate constants to natural numbers, such that for each rule p R ← L1 , . . . , Lm and any i ∈ {1, . . . , m}: • S(q) ≤ S(p) for every predicate constant q occurring in Li . • If Li is of the form (not E), then S(q) < S(p) for each predicate constant q occurring in E. • For any subexpression of Li of the form (E1 E2 ), S(q) < S(p) for every predicate constant q occurring in E2 . A distinctive feature of this definition is the third condition; the intuition behind this constraint is that Higher-Order Datalog¬ allows for the definition of higher-order predicates that simulate negation (e.g., via a rule such as neg P ← not P). Consequently, to ensure a well-defined semantics, predicate constants occurring as arguments in a higher-order application must be treated as if they occur within a negative context. As shown in Bogaerts et al. (2024), stratified Higher-Order Datalog¬ programs have a unique stable model which coincides with their well-founded model. For this reason, such programs are particularly appealing from a semantic point of view. We can now define the exact class of programs that we will be studying. Definition 3.2 (Stratified Linear Higher-Order Datalog¬ ) A Higher-Order Datalog¬ program P is called stratified linear if it is stratified with respect to a stratification function S and, for every rule p R1 · · · Rn ← L1 , . . . , Lm in P, the following conditions hold: 1. There exists at most one predicate constant q occurring in the body L1 , . . . , Lm such that S(q) = S(p). 2. If such a predicate q exists, it must appear in exactly one literal Li .

6

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

The class of all Stratified Linear Higher-Order Datalog¬ programs is called Stratified Linear Higher-Order Datalog ¬ . This condition implies that a rule can access any number of atoms from lower strata treating them as already computed data - but can pass the active computation state to at most one literal in the current stratum. We now give two examples of well-known problems that can be written very concisely in Stratified Linear Higher-Order Datalog¬ ; this underscores the naturalness and usefulness of the fragment. Example 2 We define the relation hamilton(X,Y) which is true iff there exists a Hamilton path from vertex X to vertex Y in a graph represented by a binary predicate e which specifies the edges of the graph. The first rule in the definition of hamilton is the following: hamilton (X , Y ) ← ordering ( Ord ) , first ( Ord , X ) , last ( Ord , Y ) , subset ( succ ( Ord ) , e ).

The above rule states that there exists a Hamilton path from vertex X to vertex Y if there exists a relation Ord that is a strict total ordering with first element X and last element Y and for every two consecutive elements in Ord the corresponding edge exists in e. We use the predicate subset of Example 1 modified to handle binary relations. Notice the use of Ord in the above rule: it is a predicate variable that does not appear in the head of the rule and therefore it is an existentially quantified variable of the body (i.e., the body can be read as “there exists a relation Ord such that . . . ”). To be a strict total ordering, Ord must be irreflexive, transitive, and every two different elements must be related. This can be expressed with the following rules: ordering ( Ord ) ← connected ( Ord ) , transitive ( Ord ) , irreflexive ( Ord ). connected ( Ord ) ← not disconnected ( Ord ). disconnected ( Ord ) ← not Ord (X , Y ) , not Ord (Y , X ) , not ( X ≈ Y ). transitive ( Ord ) ← not non_tran sitive ( Ord ). non_t ransiti ve ( Ord ) ← Ord (X , Y ) , Ord (Y , Z ) , not Ord (X , Z ). irreflexive ( Ord ) ← not n on _ ir re fl e xi ve ( Ord ). n on _i rr e fl ex iv e ( Ord ) ← Ord (X , X ).

We now define the predicates first, last and succ. Predicate first(Ord,X) is true for X being the individual constant that is the first element with respect to the ordering specified by Ord. Likewise, last(Ord,X) is true if X is the last element in Ord. The predicate succ(Ord,X,Y) is true for X and Y that are sequential in Ord. first ( Ord , X ) ← not nfirst ( Ord , X ). nfirst ( Ord , X ) ← Ord (Z , X ). last ( Ord , X ) ← not nlast ( Ord , X ). nlast ( Ord , X ) ← Ord (X , Y ). succ ( Ord ,X , Y ) ← Ord (X , Y ) , not nsequential ( Ord ,X , Y ). nsequential ( Ord ,X , Y ) ← Ord (X , Z ) , Ord (Z , Y ).

It is easy to check that this program is a Stratified Linear Higher-Order Datalog¬ one. Example 3 The Graph Recoloring problem asks whether it is possible to transform one valid vertex coloring of a graph into another valid target coloring by changing the color of exactly one vertex at a time. A crucial constraint is that every intermediate step in this sequence must also be a valid coloring (i.e., no two adjacent vertices may share the same color). Because the configuration space of all possible colorings for a graph is finite but exponentially

From Time to Space: The Impact of Linearity in Higher-Order Datalog

7

large, searching for a path between two colorings is an archetypal reachability problem. Bonsma and Cereceda (2009) prove that deciding whether such a reconfiguration path exists between two colorings is a PSPACE-complete problem. The following program solves the Graph Recoloring problem. In this program, a graph is defined by the predicates node and edge. A specific coloring of a graph is represented as a binary relation C, where the atom C(X,Col) indicates that node X is assigned color Col. The target coloring is represented by the relation target_coloring. Before we can determine if a graph can be recolored, we must first define what constitutes a structurally sound, valid coloring. We do this by defining the conditions that make a coloring invalid, and then concluding that a coloring is valid if none of those conditions apply. has_color (C , X ) ← C (X , Col ). i n v a l i d _ c o l o r i n g ( C ) ← edge (X , Y ) , C (X , Col ) , C (Y , Col ). i n v a l i d _ c o l o r i n g ( C ) ← C (X , Col1 ) , C (X , Col2 ) , not ( Col1 ≈ Col2 ). i n v a l i d _ c o l o r i n g ( C ) ← node ( X ) , not has_color (C , X ). valid _colori ng ( C ) ← not i n v a l i d _ c o l o r i n g ( C ).

The invalid_coloring predicate captures the three ways a coloring attempt can fail: (a) two distinct nodes connected by an edge share the exact same color; (b) a single node is simultaneously assigned two different colors, and (c) a node in the graph does not have any color assigned to it at all. A valid recoloring sequence requires changing the color of exactly one node at a time, ensuring that every intermediate state remains a valid graph coloring. Finally, the program must check if this sequence of transitions successfully reaches the target_coloring. valid_step ( C1 , C2 ) ← valid_ colorin g ( C1 ) , valid _colorin g ( C2 ) , one_diff ( C1 , C2 ). recolorable ( C ) ← eq (C , ta r ge t_ co l or in g ). recolorable ( C ) ← valid_step (C , NextC ) , recolorable ( NextC ).

The valid_step(C1,C2) enforces the rules that both the starting coloring (C1) and resulting coloring (C2) are valid colorings, and exactly one node changes color. The latter is checked by the predicate one_diff. Both one_diff and the auxiliary predicate eq that checks whether two binary relations are equal can be defined as follows. diff ( C1 , C2 , X ) ← C1 (X , Col ) , not C2 (X , Col ). has_diff ( C1 , C2 ) ← diff ( C1 , C2 , X ). multi ple_dif fs ( C1 , C2 ) ← diff ( C1 , C2 , X ) , diff ( C1 , C2 , Y ) , not ( X ≈ Y ). one_diff ( C1 , C2 ) ← has_diff ( C1 , C2 ) , not mult iple_di ffs ( C1 , C2 ). eq ( C1 , C2 ) ← not has_diff ( C1 , C2 ) , not has_diff ( C2 , C1 ).

It is easy to verify that the above program is stratified: every non-recursive predicate in the program can be assigned on its own stratum, and the sole recursive predicate, recolorable, depends only positively on itself, therefore preserving this hierarchy. Furthermore, the program maintains the linearity within every stratum. The only interesting case is the recursive rule of predicate recolorable, where the body contains exactly one predicate from the same stratum that is recolorable itself. This predicate appears exactly once, alongside valid_step which resides in a lower stratum. Languages such as Higher-Order Datalog¬ , are usually referred as formal query languages. A program in our language can be considered to compute a query in the following sense: a first-order predicate, like e in Example 2, will be called an input predicate and its denotation (as a set of ground atoms) constitutes what is called the input database,

8

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

usually denoted by Din ; a first-order predicate like hamilton in Example 2, will be an output one and its denotation constitutes the output database, usually denoted by Dout . Formally, a database schema σ is a finite set of first-order predicate symbols with associated arities. A database over a schema σ is a finite set of ground atoms whose predicate symbols belong to σ. A query is a mapping from databases over a schema σ1 to databases over a schema σ2 . A program P can be seen as a query QP such that Dout = QP (Din ). We are interested in queries that are generic (Immerman 1986), i.e., queries that do not depend on the names of the individual constants in the input database. Given a fragment of our language, we are interested in the expressive power of the fragment, namely the set of queries that can be defined by programs of the fragment. We want to demonstrate that the fragment captures a complexity class C, i.e., it can express exactly all the queries whose evaluation complexity belongs to C. Evaluation complexity is the complexity of checking whether a given atom belongs to the output database.

4 Simulation of Space-bounded Turing Machines In this section, we demonstrate how any query that belongs to (k − 1)-EXPSPACE (k ≥ 1), can be expressed by a (k + 1)-order Stratified Linear Datalog¬ program. Without loss of generality, we assume that the output schema of the query consists of a single output predicate, since every query can be decomposed into multiple queries of this form. By definition, since the query belongs to (k − 1)-EXPSPACE, there exists a Turing machine that given on its tape an input database under some sensible encoding, decides whether a tuple belongs to the output relation of the query; furthermore, it does so using at most expk−1 (nd ) tape cells, where n is the number of constant symbols in the input database and d is some sufficiently large constant (assume exp−1 (x) = ⌈log x⌉). We formalize this result as follows: Theorem 4.1 Every query in (k − 1)-EXPSPACE (k ≥ 1) can be expressed by a (k + 1)-order Stratified Linear Datalog¬ program. To establish this theorem, we construct a simulation of an arbitrary space-bounded Turing machine using Stratified Linear Higher-Order Datalog¬ . Our simulation strategy is to represent the tape as a function that maps an address of a tape cell to a symbol of the alphabet of the machine. To uniquely identify cells on an exponentially large tape, we require a mechanism to represent and manipulate equally large natural numbers as tape indices. We utilize higher-order variables to represent numbers; specifically, we construct “counting modules” where a predicate of order k can represent a number up to expk (nd+1 ) − 1 for some fixed d. We assume that the alphabet of the machine is the set of three symbols {0, 1, □} where □ denotes the blank symbol. We decompose the tape into two disjoint higher-order predicates. One predicate tracks the set of addresses where the tape bit is set to 1, while the other tracks addresses where the bit is set to 0. Any address not present in either set is implicitly treated as containing the □ symbol.

From Time to Space: The Impact of Linearity in Higher-Order Datalog

9

4.1 Representation of Numbers Indexing an exponentially large tape requires a mechanism for representing exponentially large natural numbers. We adopt the representation scheme described by Charalambidis et al. (2025) where predicates of order k are used to represent numbers of magnitude expk (nd ). As we will demonstrate later, this representation constitutes a Stratified Linear Higher-Order Datalog program. Natural numbers up to nd+1 − 1 are represented using tuples of individual constants with a fixed length of d + 1, where d is an arbitrary but fixed natural number. The following predicates define the “first” and “last” of such numbers (denoted by first0 and last0 ) and the “less-than” and “successor” relations on them (denoted by lt0 and succ0 ). Notice that the following definitions rely on the first and last predicates defined in Example 2. first 0 ( Ord , X 0 ,. . .,X d ) ← first ( Ord , X 0 ) ,. . ., first ( Ord , X d ). last 0 ( Ord , X 0 ,. . .,X d ) ← last ( Ord , X 0 ) ,. . ., last ( Ord , X d ). lt 0 ( Ord , X 0 ,. . .,X d ,Y 0 ,. . .,Y d ) ← Ord ( X d ,Y d ). lt 0 ( Ord , X 0 ,. . .,X d ,Y 0 ,. . .,Y d ) ← Ord ( X d−1 ,Y d−1 ) ,( X d ≈ Y d ). ... lt 0 ( Ord , X 0 ,. . .,X d ,Y 0 ,. . .,Y d ) ← Ord ( X 0 ,Y 0 ) ,( X 1 ≈ Y 1 ) ,. . . ,( X d ≈ Y d ). succ 0 ( Ord , X̄, Ȳ) ← lt 0 ( Ord , X̄, Ȳ) , not nsequential 0 ( Ord , X̄, Ȳ). nsequential 0 ( Ord , X̄, Ȳ) ← lt 0 ( Ord , X̄, Z̄) , lt 0 ( Ord , Z̄, Ȳ).

We extend this system to represent “exponentially-big” numbers using higher-order relations. Let N0 = nd+1 − 1 be the largest number that can be represented by (d + 1)tuples of individual constants and for k ≥ 1, let Nk be the largest number that can be represented by using k-order relations. We can exponentially increase the numbers up to the number Nk+1 = exp1 (Nk + 1) − 1 by using (k + 1)-order relations. Generally, it holds that Nk = expk (nd+1 ) − 1. If the k-order relations representing numbers up to Nk are of type ρ, then it suffices to use higher-order relations of type ρ → o in order to represent numbers up to Nk+1 . This is essentially a binary representation where the lower order numbers denote bit positions. Formally, let Z be a (k + 1)-order element and R0 , . . . , RNk be the ordering of the elements that represent numbers in the previous counting module. Let f be the function mapping true to 1 and false to 0. Then, we have num(Z) = f (Z(R0 )) + f (Z(R1 )) · 2 + · · · + f (Z(RNk )) · 2Nk . We begin with predicates testing for the first and the last number. first k+1 ( Ord , N ) ← not nfirst k+1 ( Ord , N ). nfirst k+1 ( Ord , N ) ← N ( X ). last k+1 ( Ord , N ) ← not nlast k+1 ( Ord , N ). nlast k+1 ( Ord , N ) ← not N ( X ).

The following definitions describe the “less than” relation between two elements that represent numbers. We examine if a number N is less than M by comparing the two numbers bit by bit in their binary representation. The successor of a number is defined with the use of less-than. lt k+1 ( Ord ,N , M ) ← last k ( Ord , X ) , bit k+1 ( Ord ,N ,M , X ). bit k+1 ( Ord ,N ,M , X ) ← not N ( X ) , M ( X ). bit k+1 ( Ord ,N ,M , X ) ← N ( X ) , M ( X ) , succ k ( Ord ,Y , X ) , bit k+1 ( Ord ,N ,M , Y ). bit k+1 ( Ord ,N ,M , X ) ← not N ( X ) , not M ( X ) , succ k ( Ord ,Y , X ) , bit k+1 ( Ord ,N ,M , Y ). succ k+1 ( Ord ,N , M ) ← lt k+1 ( Ord ,N , M ) , not nsequential k+1 ( Ord ,N , M ). nsequential k+1 ( Ord ,N , M ) ← lt k+1 ( Ord ,N , Z ) , lt k+1 ( Ord ,Z , M ).

For the case where k = 0 the variables X and Y in the code above must be substituted with the tuple vectors X̄ and Ȳ.

10

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

It is straightforward to verify that the counting modules of any order k ≥ 0 constitutes a stratified linear program. First, notice that there is a strict dependency on the order of the predicates: predicates of order k + 1 depend either on other predicates of order k + 1 or on predicates of strictly lower order. Consequently, all predicates of order k can be assigned to strata strictly lower than those of order k + 1. Second, within the specific order k + 1 we impose a stratification function S as: S(succk+1 ) > S(nsequentialk+1 ) > S(ltk+1 ) > S(bitk+1 ) Predicates such as firstk+1 and lastk+1 can be placed at the lowest stratum of the (k + 1)-order predicates. Finally, regarding linearity, the only recursive definition at order k + 1 is the bitk+1 . By inspection of its rules, we observe that it depends on exactly one literal of itself, satisfying the linearity condition. 4.2 The simulation of the Turing machine We now demonstrate how any query that belongs to (k − 1)-EXPSPACE (k ≥ 1), can be expressed by a stratified linear (k + 1)-order Datalog¬ program. The simulation is markedly different from that of Charalambidis et al. (2025) which was easier since it could utilize the full power of unrestricted Higher-Order Datalog¬ . Before presenting the simulation of the Turing machine M , we mention certain simplifying assumptions, which do not affect the generality of the subsequent results. • The input database consists of a single binary relation in and the output database is also a single binary relation out. In the following, the number of constants in the input database is denoted by n. • The alphabet of M that will be simulated is Σ = {0, 1, 2}. M expects the input relation in as the standard binary encoding of a graph, which is based on the ordering of the individual constants, in the first n2 cells of its tape. For example, if the pair (x, y) belongs to in, then the tape of M contains a “1” at cell position num(x) + num(y) · n, otherwise it contains “0”. • M decides whether a tuple (a, b) belongs to the output relation out. The next n2 cells of its tape are used to encode (a, b). All these cells contain the symbol “0”, except for the cell at position num(a) + num(b) · n + n2 which contains “1”. • M reaches its accepting state yes if and only if the tuple (a, b) belongs to the output relation out. We assume a Turing machine M of three symbols Σ = {0, 1, 2}. By convention, we use two predicates input0 and input1 to encode the input tape of M . Specifically, input0 holds at position X̄ iff the tape contains “0” at X̄, input1 holds at X̄ iff the tape contains “1” at X̄, and the tape contains the blank symbol “2” iff neither holds. By construction below, the two predicates are disjoint. The following two predicates encode the binary input relation in and the tuple (a, b) as a binary string. In the following rules, we pad the binary input relation with fixed constants to form (d + 1)-arity tuples representing valid tape addresses. input 0 (A ,B , Ord ,X ,Y , Z 2 ,. . .,Z d ) ← first ( Ord , Z 2 ) ,. . ., first ( Ord , Z d ) , not in (X , Y ). input 0 (A ,B , Ord , Z 0 ,Z 1 ,Z 2 ,. . .,Z d ) ← not ( Z 0 ≈ A ) , first ( Ord , Z ) , succ ( Ord ,Z , Z 2 ) , first ( Ord , Z 3 ) ,. . ., first ( Ord , Z d ). input 0 (A ,B , Ord , Z 0 ,Z 1 ,Z 2 ,. . .,Z d ) ← not ( Z 1 ≈ B ) , first ( Ord , Z ) , succ ( Ord ,Z , Z 2 ) ,

From Time to Space: The Impact of Linearity in Higher-Order Datalog

11

first ( Ord , Z 3 ) ,. . ., first ( Ord , Z d ). input 1 (A ,B , Ord ,X ,Y , Z 2 ,. . .,Z d ) ← first ( Ord , Z 2 ) ,. . ., first ( Ord , Z d ) , in (X , Y ). input 1 (A ,B , Ord , Z 0 ,Z 1 ,Z 2 ,. . .,Z d ) ← ( Z 0 ≈ A ) ,( Z 1 ≈ B ) , first ( Ord , Z ) , succ ( Ord ,Z , Z 2 ) , first ( Ord , Z 3 ) ,. . ., first ( Ord , Z d ).

We also need a higher-order predicate to lift the tuple representation of numbers to the (k − 1)-order numbering notation in order to transfer the input of the tape from a zero order relation to a (k − 1)-order relation. The predicate liftk−1 (Ord,X̄,M) transforms the number represented by the tuple X̄ in the zero-order notation to the same number M in the (k − 1)-order notation. lift k−1 ( Ord , X̄,M ) ← first 0 ( Ord , X̄) , first k−1 ( Ord , M ). lift k−1 ( Ord , X̄,M ) ← succ 0 ( Ord , Z̄, X̄) , lift k−1 ( Ord , Z̄,M′),succ k−1 ( Ord , M′,M ).

We then define the two predicates symbol0 and symbol1 that are the (k − 1)-order analogues of the input predicates input0 and input1 . symbol 0 (A ,B , Ord , P ) ← input 0 (A ,B , Ord , X̄) , lift k−1 ( Ord , X̄,P ). symbol 1 (A ,B , Ord , P ) ← input 1 (A ,B , Ord , X̄) , lift k−1 ( Ord , X̄,P ).

With the input prepared, we model the Turing machine’s execution as a reachability analysis on the graph of configurations. We adopt a forward approach: a configuration is valid if it leads to an accepting state. Consider the transition (s, 0) −→ (s′ , 1, R) which reads: “if the current state of the machine is s and its cursor reads the symbol “0”, then the machine changes its state to s′ , it writes “1” on the current cursor position onto the tape and then moves the cursor to the right.” We encode this logic such that the validity of the current state s depends on the validity of the successor state s′ . state s ( Ord , Tp 1 , Tp 0 ,P ) ← Tp 0 ( P ) , not Tp 1 ( P ) , succ k−1 ( Ord ,P , P′), state s′ ( Ord , flip 1 ( Tp 1 ,P ) , flip 0 ( Tp 0 ,P ) , P′).

This rule asserts that if the machine successfully accepts starting from state s′ , it also accepts starting from state s. The successor state s′ reflects the updated tape and the cursor moved to the right or left by enforcing succk−1 (Ord,P,P′ ) or succk−1 (Ord,P′ ,P) respectively. The transition rules above rely on the ability to modify the tape. Recall that the tape is encoded by the two disjoint relations Tp1 and Tp0 , holding the positions where the tape contains “1” and “0” respectively. Writing the symbol “b” at position P therefore involves updating both relations: P is added to Tpb and removed from the other; e.g., writing “1” at P puts P into Tp1 and removes it from Tp0 . We capture these two elementary set operations with the helper predicates flip1 and flip0 , defined as follows: flip 1 ( Tp ,P , X ) ← eq (P , X ). flip 1 ( Tp ,P , X ) ← Tp ( X ). flip 0 ( Tp ,P , X ) ← Tp ( X ) , neq (P , X ).

Intuitively, the partial application flip1 (Tp,P) denotes the relation Tp ∪ {P}, i.e., Tp extended so that P belongs to it, while flip0 (Tp,P) denotes Tp\{P}, i.e., Tp with P removed. Writing the symbol “1” at position P is then accomplished by passing flip1 (Tp1 ,P) and flip0 (Tp0 ,P) to the recursive call, as in the transition rule above; writing “0” is symmetric, with the roles of the two relations exchanged. Both definitions rely on the auxiliary predicates eq and neq, which check whether two relations (of the same type) are equal or not and are defined as:

12

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

neq (R , Q ) ← R ( X ) , not Q ( X ). neq (R , Q ) ← not R ( X ) , Q ( X ). eq (R , Q ) ← not neq (R , Q ).

The recursion defined in the transition rules must eventually terminate. We ground the simulation by defining the accepting state “yes” as true for any valid tape configuration: state yes ( Ord , Tp 1 , Tp 0 ,P ) ← not intersect ( Tp 1 , Tp 0 ). intersect (R , Q ) ← R ( X ) , Q ( X ).

Finally, we start the simulation by querying the initial configuration. The following query checks if the initial state s0 (with the initial cursor position and input symbols) can effectively “reach” the accepting state yes via the rules defined above: query (A , B ) ← ordering ( Ord ) , first k−1 ( Ord , P ) , state s0 ( Ord , symbol 1 (A ,B , Ord ) , symbol 0 (A ,B , Ord ) , P ).

This means that the query is true if the states0 is true for the initial tape state and with the cursor being at the beginning of the tape which in turn is true if this configuration is reachable by one accepting configuration. We conclude the construction by verifying that the simulation is a stratified linear program. The core of the simulation lies in the transition rules for the states predicates which form a single stratum of mutually recursive definitions. Crucially, each rule depends recursively on exactly one states predicate, satisfying the linearity constraint. All auxiliary predicates, such as succk+1 , flip0 and flip1 are defined without dependence on any states predicate allowing them to be placed on lower strata.

5 Space-Efficient Computation of Stratified Linear Higher-Order Programs Using a simple-minded bottom-up approach to compute the answer to a query, would require space tower-exponential in the order of the given program. To capture the precise space complexity of Stratified Linear Higher-Order Datalog¬ , we must avoid producing and storing the entire model of a program. In this section, we present a space-efficient computation that proceeds in a top-down fashion. We demonstrate that for a (k + 1)-order ¯ can be evaluated using memory bounded Stratified Linear Datalog¬ program, a query p(d) by (k − 1)-EXPSPACE. We formalize this result in the following theorem: Theorem 5.1 Let P be a Stratified Linear (k + 1)-Order Datalog¬ program that defines a query. Then, there exists a deterministic Turing machine that takes as input an encoding of a database D that uses n individual constant symbols and a ground atom p(ā), where p is a predicate constant of P and ā is a tuple of these individual constants, and decides whether p(ā) ∈ QP (D), while using at most expk−1 (nd ) tape cells, for some constant d. Our evaluation strategy relies on the stratified and linear nature of the program. The meaning of a stratified (k + 1)-order Datalog program can be computed stratum by stratum, starting from the lowest and moving upwards. To evaluate queries in the (m + 1)-th stratum, we employ two routines: • A query machine for the (m + 1)-th stratum that decides the truth of an atom (p d1 · · · dn ) where p is a predicate belonging to the (m + 1)-th stratum and the di

From Time to Space: The Impact of Linearity in Higher-Order Datalog

13

are representations of expression values (see explanation later in the section). For the initial query, the di are just individual constants. • An expression evaluator for the m-th stratum that, given a variable assignment, computes the value of a given expression E of a type with order at most k, with the restriction that E is formed using predicates solely from the first m strata. The query machine for the (m + 1)-th stratum requires that the corresponding expression evaluator for the m-th stratum is already defined since it invokes it. On the other hand, the evaluator routine for the m-th stratum requires the query routine for any stratum m′ ≤ m to be defined. If we take the first stratum to be the set of the (first-order) input predicates supplied from the database in the form of facts, then for m = 0 these routines are easily defined and thus omitted. We now define the above routines at a high level of abstraction. A more formal presentation and the corresponding correctness proofs, are given in the Appendix A . Query Machine for the (m + 1)-th Stratum: 1. Start with the atom (p d1 · · · dn ) written on the tape, where the di are representations of expression values, i.e., a string that describes the value (for example, a relation can be represented as a string listing all tuples in some predetermined order). 2. Non-deterministically select a rule p R1 · · · Rn ← L1 , . . . , Lr from P for predicate p and guess a valid assignment for the rule’s variables such that di is assigned to Ri for all i ∈ {1, . . . , n}. 3. Iterate through the literals Li in the rule body: • If Li is a negative literal then Li is of the form (not E). Invoke the expression evaluator for the m-th stratum, passing as parameter the guessed variable assignment, to compute E. If the evaluation returns true, then reject, otherwise proceed to the next literal. • If Li is a positive literal and there is no predicate in Li from the (m + 1)-th stratum, then invoke the expression evaluator for the m-th stratum, passing as parameter the guessed variable assignment, to compute Li . If the evaluation returns true, then proceed to the next literal, otherwise reject. • If there is a predicate in Li from the (m + 1)-th stratum, then this is the unique recursive literal q E1 · · · Et implied by linearity. Every Ej is of order at most k and includes predicates from the first m strata. Iterate through E1 , . . . , Et invoking each time the evaluator for the m-th stratum, passing as parameter the guessed variable assignment, to compute each Ej and store the representations d′1 , . . . , d′t . Construct a new ground atom q d′1 · · · d′t . 4. If all literals Li evaluate to true without encountering a recursive literal, then accept. 5. If one of the literals Li is a recursive one, overwrite the current goal with q d′1 · · · d′t and loop back to Step 2. Note that the aforementioned query machine is non-deterministic and may contain computational paths that do not terminate (e.g., consider the rule p←p). This machine is not technically a decider of whether (p d1 · · · dn ) is true or not. However, for machines that are space bounded (more specifically by a space constructible function f (n) (Sipser 2012)) there exists a corresponding non-deterministic Turing machine where every computational path terminates. By Savitch (1970), there also exists a deterministic machine that computes

14

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

the same query within the same space complexity class. In the following when we refer to the query machine we mean the deterministic version. We now define the expression evaluator for the m-th stratum. Let E be an expression of order at most k that includes predicates from the first m strata. The expression evaluator makes calls to query machines in order to construct a representation of the expression’s value. Expression Evaluator for the m-th Stratum: • If the expression E is an individual constant, then return the constant. • If the expression E is of the form (q E1 · · · Et ) where q belongs to the m′ -th stratum, m′ ≤ m, and its type is ρ1 → · · · → ρt → · · · → ρt′ → o. Then: 1. Evaluate the expressions E1 , . . . , Et sequentially to obtain and store their representations d1 , . . . , dt . This is performed by calling the evaluator recursively for each subexpression. 2. To determine the representation of the result, the machine enumerates all possible tuples dt+1 , . . . , dt′ of representations regarding the remaining arguments. For each tuple, it invokes the query machine for the m′ -th stratum with the goal (q d1 · · · dt dt+1 · · · dt′ ). • If the expression E is of the form (X E1 · · · Et ) where X is a variable (of order at most k) then it evaluates the expressions E1 , . . . , Et to obtain and store the representation of their values d1 , . . . , dt , and then uses the variable assignment of X to compute the representation of the value of the application. The last two bullets implicitly handle the cases where there are zero arguments. We now briefly comment on the space complexity; the full and precise arguments are given in the Appendix A . The query machine’s space complexity depends on storing the current goal, guessing variable assignments, and evaluating lower-strata subroutines. For a (k + 1)-order program, arguments are at most order k, belonging to a domain of size expk (poly(n)). Representing these arguments requires unique identifiers of logarithmic size, i.e., expk−1 (poly(n)) bits. Therefore, storing the current goal and variable assignments takes expk−1 (poly(n)) space. Crucially, program linearity allows the machine to overwrite the current goal during recursion, preventing depth-related memory blow-up. Furthermore, lower-strata expressions are evaluated sequentially (reusing memory), and since the number of strata is a fixed constant independent of the input size n, the call stack depth is strictly bounded. Consequently, the overall space complexity remains expk−1 (poly(n)). 6 Future Work: Implementation of 2nd-Order Stratified Linear Datalog¬ The space complexity results described in this paper are not merely theoretical; they provide the foundation for a practical implementation of the 2nd order fragment of Stratified Linear Datalog¬ . By capturing PSPACE, this fragment addresses many problems that remain out of reach for traditional ASP systems. The key idea behind our implementation is to compile any given 2nd order Stratified Linear Datalog¬ program and user query into a Quantified Boolean Formula (QBF). We can then use existing, efficient QBF solvers to evaluate the resulting formula and return

From Time to Space: The Impact of Linearity in Higher-Order Datalog

15

answers to the initial query. Because evaluating QBFs is the canonical PSPACE-complete problem (Sipser 2012), this translation offers a direct and highly feasible approach to implementing our source language. Due to space limitations, the remainder of this section provides only a high-level overview of this translation, leaving the formal generalization of this technique to a future paper. To better understand the mechanics of this approach, interested readers should consult Appendix B, which describes the steps of transforming a well-known PSPACE-complete problem written in 2nd order Stratified Linear Datalog¬ , into QBF. The space-efficient computation described in Section 5 models evaluation as a top-down procedure that avoids materializing the full program interpretation. We can conceptualize this evaluation as a reachability problem within a configuration graph. In the first-order setting, linearity implies that the evaluation engine only needs to store the current state of the computation (which is a classical Datalog atom). In the 2nd-order case, the active computation is, in general, a first-order relation. For an input database with a domain of size n, a first-order relation of arity d can be represented by a truth assignment to O(nd ) boolean variables. Therefore, a single recursive step in a 2nd-order Stratified Linear Datalog¬ program represents a transition from one boolean configuration to another. Because the program is linear, meaning there exists at most one predicate constant in the body from the same stratum, the core query evaluation simply asks whether there is a valid logical path from an initial configuration to an accepting configuration. The transformation to QBF relies on encoding these configurations as boolean vectors and capturing the linear recursion using a reachability formula. Let a variable X representing a first-order relation be encoded as a vector of boolean variables ⃗x of length nd . The linear recursive rules of the current stratum, along with any non-recursive rules or sequences of rules from strictly lower strata they depend on, can be compiled into a quantifier-free boolean formula T (⃗x, ⃗y ). This formula evaluates to true if and only if state ⃗y can be derived from state ⃗x in exactly one step. Because the state space of d d possible configurations has a size of 2n , a linear query might require up to 2n recursive steps to reach the target state. Unrolling the transition formula T (⃗x, ⃗y ) exponentially would require exponential space, which contradicts our PSPACE bounds. Fortunately, we can follow the principles of Savitch’s theorem and use the expressive power of universal quantifiers in QBF to compress the path search. A detailed explanation of how Savitch’s theorem is used for this compression, is given in Appendix B. This translation mechanism offers a practical evaluation pipeline. A compiler can map all first-order variables to boolean vectors, compile the linear recursive rules into the base transition formula T , and generate appropriate quantified reachability formulas based on Savitch’s theorem. The resulting formula can then be evaluated by modern QBF solvers. By avoiding the materialization of the full interpretation, this approach strictly adheres to the space-efficient nature of our fragment and provides a viable implementation pathway for 2nd order Stratified Linear Datalog¬ programs. As another promising direction for future work, it is worth investigating whether we can relax the stratification constraints by introducing a notion of local stratification for Higher-Order Datalog¬ . Although our current space complexity arguments rely on a fixed number of strata, we conjecture that if the number of strata are polynomial with respect to the input size, the resulting linear programs would still preserve their space efficiency.

16

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis References

Amendola, G., Ricca, F., and Truszczynski, M. 2019. Beyond NP: quantifying over answer sets. Theory Pract. Log. Program., 19, 5-6, 705–721. Bogaerts, B., Charalambidis, A., Chatziagapis, G., Kostopoulos, B., Pollaci, S., and Rondogiannis, P. 2024. The stable model semantics for higher-order logic programming. Theory Pract. Log. Program., 24, 4, 737–754. Bogaerts, B., Janhunen, T., and Tasharrofi, S. 2016. Stable-unstable semantics: Beyond NP with normal logic programs. Theory Pract. Log. Program., 16, 5-6, 570–586. Bonsma, P. and Cereceda, L. 2009. Finding paths between graph colourings: Pspacecompleteness and superpolynomial distances. Theoretical Computer Science, 410, 50, 5215–5226. Charalambidis, A., Kostopoulos, B., Nomikos, C., and Rondogiannis, P. 2025. The power of negation in higher-order datalog. Theory Pract. Log. Program., 25, 4, 595–611. Consens, M. P. and Mendelzon, A. O. Graphlog: a visual formalism for real life recursion. In Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems 1990, PODS90, 404–416. ACM. Dantsin, E., Eiter, T., Gottlob, G., and Voronkov, A. 2001. Complexity and expressive power of logic programming. ACM Comput. Surv., 33, 3, 374–425. Fandinno, J., Laferrière, F., Romero, J., Schaub, T., and Son, T. C. 2021. Planning with incomplete information in quantified answer set programming. Theory Pract. Log. Program., 21, 5, 663–679. Immerman, N. 1986. Relational queries computable in polynomial time. Information and Control, 68, 1-3, 86–104. Jones, N. D. 2001. The expressive power of higher-order types or, life without CONS. Journal of Functional Programming, 11, 1, 5–94. Savitch, W. J. 1970. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4, 2, 177–192. Sipser, M. 2012. Introduction to the theory of computation. Wadsworth Publishing, Belmont, CA, 3 edition. Ullman, J. D. 1989. Principles of Database and Knowledge-Base Systems, Volume II: The New Technologies. Computer Science Press, Rockville, MD.

From Time to Space: The Impact of Linearity in Higher-Order Datalog

17

A Proofs of Section 5 In this appendix, we supply the technical details omitted from the main text regarding the evaluation of Stratified Linear Higher-Order Datalog¬ . We define the precise semantics of the language and provide the proofs for the upper bound complexity characterized in Theorem 5.1. The semantics of the base type o is the classical Boolean domain {true, false} and that of the base type ι is UP , namely the set of individual constant symbols in P. We start by defining the meanings of types of Higher-Order Datalog¬ . Definition A.1 Let P be a Higher-Order Datalog¬ program. We define the meaning Jτ KUP of a type τ with respect to UP , as follows: • JoKUP = {true, false}. The partial order ≤o is the one induced by false <o true. • JιKUP = UP . The partial order ≤ι is the trivial one defined as d ≤ι d for all d ∈ UP . • Jρ → πKUP = JρKUP → JπKUP , namely the set of all functions from JρKUP to JπKUP . The partial order ≤ρ→π is defined as follows: for all f, g ∈ Jρ → πKUP , f ≤ρ→π g iff f (d) ≤π g(d) for all d ∈ JρKUP . The subscripts from the above partial order will be omitted when they are obvious from context. Moreover, we will omit the subscript UP assuming that our semantics is defined with respect to a specific program P. For every predicate type π, (JπK, ≤π ) is a W V complete lattice. We denote by ≤π and ≤π the corresponding lub and glb operations of the above lattice. To denote that an expression E has type ρ we will often write E : ρ. Definition A.2 A Herbrand interpretation I of a program P assigns to each individual constant c of P, the element I(c) = c, and to each predicate constant p : π of P, an element I(p) ∈ JπK. We will denote the set of Herbrand interpretations of a program P with HP . We define a partial order on HP as follows: for all I, J ∈ HP , I ≤ J iff for every predicate constant p : π that appears in P, I(p) ≤π J(p). Definition A.3 A Herbrand state s of a program P is a function that assigns to each argument variable R of type ρ, an element s(R) ∈ JρK. We denote the set of Herbrand states with SP . In the following, s[R1 /d1 , . . . , Rn /dn ] is used to denote a state that is identical to s the only difference being that the new state assigns to each Ri the corresponding value di ; for ¯ brevity, we will also denote it by s[R̄/d]. Definition A.4 Let P be a Higher-Order Datalog¬ program, I a Herbrand interpretation of P, and s a Herbrand state. The semantics of expressions, literals and bodies is defined as follows: 1. JRKs (I) = s(R) 2. JcKs (I) = I(c) = c 3. JpKs (I) = I(p) 4. J(E1 E2 )Ks (I) = JE1 Ks (I) JE2 Ks (I)

18

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis ( true, if JE1 Ks (I) = JE2 Ks (I) 5. J(E1 ≈ E2 )Ks (I) = false, otherwise 6. J(not E)Ks (I) = (JEKs (I))−1 , with true −1 = false, false −1 = true V 7. J(E1 ∧ · · · ∧ Em )Ks (I) = ≤o {JE1 Ks (I), . . . , JEm Ks (I)}

Definition A.5 Let P be a program and M be a Herbrand interpretation of P. Then, M is a Herbrand model of P iff for every rule p R ← B in P and for every Herbrand state s, JBKs (M ) ≤o Jp R̄Ks (M ).

Let (L, ≤) be a complete lattice. We define Lc = {(x, y) ∈ L × L | x ≤ y}. Moreover, we define the relations ≤ and ⪯ on Lc , so that for all (x, y), (x′ , y ′ ) ∈ Lc : (x, y) ≤ (x′ , y ′ ) iff x ≤ x′ and y ≤ y ′ , and (x, y) ⪯ (x′ , y ′ ) iff x ≤ x′ and y ′ ≤ y. We will denote the first and second selection functions on pairs with the more compact notation [·]1 and [·]2 : given any pair (x, y), it is [(x, y)]1 = x and [(x, y)]2 = y. It is easy W V to see that Lc is a complete lattice with respect to ≤ where ≤ and ≤ are defined in a V V pointwise way and Lc is a meet-semilattice with respect to ⪯ where ⪯ S = ( {[x]1 | W x ∈ S}, {[x]2 | x ∈ S}). The following definition defines an alternative but equivalent semantics of the expressions, literals and bodies with respect to a pair of interpretations. This is necessary for proceeding to the definition of the approximating operator and more convenient when doing proofs. This operator is ≺-monotonic. Definition A.6 Let P be a program, (I, J) ∈ HPc , and s ∈ SP . The pair semantics of expressions, literals and bodies is defined as follows: 1. JRKcs (I, J) = (s(R), s(R)) 2. JcKcs (I, J) = (I(c), J(c)) 3. JpKcs (I, J) = (I(p), J(p)) V W 4. J(E1 E2 )Kcs (I, J) = ( ≤π {f (d) | d ∈ [[ρ]], l ≤ d ≤ u}, ≤π {g(d) | d ∈ [[ρ]], l ≤ d ≤ u}), c where (f, g) = JE1 Kcs (I, ( J), (l, u) = JE2 Ks (I, J) for E1 : ρ → π and E2 : ρ. (true, true), if JE1 Kcs (I, J) = JE2 Kcs (I, J) 5. J(E1 ≈ E2 )Kcs (I, J) = (false, false), otherwise 6. J(not E)Kcs (I, J) = JEKcs (I, J)−1 , with (true, true)−1 = (false, false), (false, false)−1 = (true, true) and (false, true)−1 = (false, true) V 7. J(E1 ∧ · · · ∧ Em )Kcs (I, J) = ≤o {JE1 Kcs (I, J), . . . , JEm Kcs (I, J)} Definition A.7 Let P be a program. The approximating operator (or approximator) AP : HPc → HPc is defined for every predicate constant p : ρ1 → · · · → ρn → o in P and all d1 ∈ Jρ1 K, . . . , dn ∈ Jρn K, as AP (I, J) = (AP (I, J)1 , AP (I, J)2 ) where, for i ∈ {1, 2}: _ ¯ = AP (I, J)i (p)(d) {[JBKcs[R̄/d] ¯ (I, J)]i | s ∈ SP and (p R̄ ← B) in P} ≤o

Several fixpoints of the approximating operator are of interest (Bogaerts et al. 2024). In this section, we focus on the stable fixpoints of AP : a pair (I, J) is a stable fixpoint of AP if and only if I = lfp AP (·, J)1 and J = lfp AP (I, ·)2 .

From Time to Space: The Impact of Linearity in Higher-Order Datalog

19

Definition A.8 Let P be a Higher-Order Datalog¬ program. We call I a stable model of P if (I, I) is a stable fixpoint of AP . We can decompose the program into subprograms and study the stable models of each subprogram. The following definition formalizes this decomposition through the notion of a splitting set, which identifies a sub-program that can be evaluated independently of the remaining rules. Definition A.9 Let P be a program and U a set of predicate constants. We say that U is a splitting set of P if for every clause C of P, if a predicate constant of U appears in the head of C, then every predicate constant appearing in C is included in U . The set of clauses C ∈ P such that all predicate constants appearing in C are included in U is called the bottom of P relative to U and denoted by bU (P). The set P \ bU (P) is called the top of P relative to U . Lemma A.1 Let P be a program and U be a splitting set of P such that bU (P) contains all constants of type ι of P. If M is a stable model of P, then M restricted to U is a stable model of bU (P). Proof Let the pair (I, J) be a stable fixpoint for P and let (IU , JU ) be its restriction to the bottom program bU (P). We will show that (IU , JU ) is a stable fixpoint of bU (P) which directly implies the statement. It is easy to verify that (IU , JU ) is a fixpoint of the approximator AbU (P) . Therefore, AbU (P) (X, JU )1 and AbU (P) (IU , Y )2 are well-defined operators in the corresponding intervals. To see this is true, take for example any interpretation X ≤ JU . Then we have that AbU (P) (X, JU )1 ≤ AbU (P) (JU , JU )1 ≤ AbU (P) (JU , JU )2 ≤ AbU (P) (IU , JU )2 = JU . Similarly, for IU ≤ Y . For the sake of contradiction assume that (IU , JU ) is not a stable fixpoint of bU (P). Then, let IU′ = lfp AbU (P) (·, JU )1 and so IU′ < IU . We consider an interpretation I ′ defined as: ( IU′ (p) if p ∈ U ′ I (p) = I(p) otherwise It is easy to verify that I ′ < I. We will show that I ′ is a prefixpoint of AP (·, J)1 which is a contradiction since I is the least fixpoint (and therefore its least prefixpoint). Indeed, for any p in U we have that: _ ′ ¯ = AP (I ′ , J)1 (p)(d) {[JBKcs[R̄/d] ¯ (I , J)]1 | s ∈ SP and (p R̄ ← B) in P} ≤o _ ′ = {[JBKcsu [R̄/d] ¯ (IU , JU )]1 | su ∈ SbU (P) and (p R̄ ← B) in bU (P)} ≤o

¯ = I ′ (p)(d) ¯ = I ′ (p)(d) ¯ = AbU (P) (IU′ , JU )1 (p)(d) U This follows from the fact that all rules defining the predicate p are in bU (P) and that the bodies of these rules involve only predicates interpreted by (IU , JU ). For any p not in U it follows by the monotonicity of AP that AP (I ′ , J)1 (p) ≤ AP (I, J)1 (p) = I(p). Furthermore, since I(p) = I ′ (p) it follows AP (I ′ , J)1 (p) ≤ I ′ (p).

20

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

The case for JU is analogous. It is easy to see that for any program P that is stratified with a stratification function S, for every natural number n, the set Un = {p | S(p) < n} is a splitting set of P. Using these splitting sets, we can divide P into a finite number of disjoint subprograms P1 , . . . , Pm . In the rest of the section we will denote a stratified program P as P1 ∪ · · · ∪ Pm . A key property of such programs is that they possess a unique stable model. Lemma A.2 Let P be a stratified Higher-Order Datalog¬ program. Then, it has a unique stable model. Proof An immediate consequence of Theorems 7.3 and 7.4 from Bogaerts et al. (2024). In the following, whenever we decompose a program P into P1 ∪ · · · ∪ Pm , we will silently assume that every ι type constant appearing in P appears also in P1 and therefore in every P1 ∪ · · · ∪ Pi for any i ≤ m. This ensures that the Herbrand universe of every subprogram is the same as the Herbrand universe of P and so all types evaluate from the same sets in each subprogram. Definition A.10 Let P = P1 ∪ · · · ∪ Pm be a stratified Higher-Order Datalog¬ program, Um be the splitting set of the predicates defined in P1 ∪ · · · ∪ Pm−1 and Mm−1 be a Herbrand interpretation of M these predicates. The propositional program Pm m−1 called the reduct of Pm with respect to Mm−1 is defined as the set of all propositional rules ps(R̄) ← q1d¯1 , . . . , qkd¯k constructed for every rule p R̄ ← L1 , . . . , Ln in Pm and every Herbrand state s that satisfies the following conditions: 1. Every literal Li in the body whose predicates are in Um , JLi Ks (Mm−1 ) = true. 2. The body atoms qid¯i correspond exactly to the literals in the body of the form qi E1 . . . Et where qi is not in Um . Each literal maps to the propositional atom qid¯i where d¯i is the tuple ⟨JE1 Ks (Mm−1 ), . . . , JEt Ks (Mm−1 )⟩. The following lemma follows easily by the definition, so its proof is omitted. Lemma A.3 Let P = P1 ∪ · · · ∪ Pm be a stratified Higher-Order Datalog¬ program and Mm the unique stable model of P. Moreover, let Mm−1 be the unique stable model of P1 ∪ · · · ∪ Pm−1 . If P M M is stratified linear then Pm m−1 is also stratified linear. More specifically, Pm m−1 contains at most one atom in each body of a rule. We now establish the correspondence between the model of a stratified program P and those of its reducts with respect to the models of the previous subprograms. Lemma A.4 Let P = P1 ∪ · · · ∪ Pm be a stratified Higher-Order Datalog¬ program and Mm the unique stable model of P1 ∪ · · · ∪ Pm , Mm−1 be the unique stable model of P1 ∪ · · · ∪ Pm−1 and M M Nm be the minimum model of Pm m−1 . Then, for every propositional atom pd¯ in Pm m−1 , ¯ = true. Nm (pd¯) = true iff Mm (p)(d)

From Time to Space: The Impact of Linearity in Higher-Order Datalog

21

Proof Let Um be the splitting set containing all predicate constants defined in P1 ∪ · · · ∪ Pm−1 . By Lemma A.1, since Um is a splitting set, the restriction of the stable model Mm to the predicates in Um must coincide with Mm−1 . Let Hm,m−1 be the set of interpretations of P such that for every interpretation I ∈ Hm,m−1 , the restriction of I to Um is exactly Mm−1 . Since Mm extends Mm−1 , we M ∗ have Mm ∈ Hm,m−1 . Let Hm,m−1 be the set of interpretations of Pm m−1 . ∗ We define a bijection θ : Hm,m−1 → Hm,m−1 . For any interpretation I ∈ Hm,m−1 and any predicate p defined in Pm with arguments d: θ(I)(pd ) = true if and only if I(p)(d) = true. This mapping is a bijection because the atoms of the propositional reduct M Pm m−1 are constructed specifically for every tuple d¯ of possible inputs. Furthermore, θ is order preserving i.e., if I1 ≤ I2 then θ(I1 ) ≤ θ(I2 ) and vice versa as one can easily verify. We now show that I is a model of P extending Mm−1 if and only if θ(I) is a model M of the reduct Pm m−1 . Assume I ∈ Hm,m−1 is a model of P. Suppose, for the sake of M contradiction, that θ(I) is not a model of the reduct Pm m−1 . This implies there exists M m−1 a rule r′ of the form pd¯ ← q1d¯1 , . . . , qkd¯k in Pm , that is not satisfied by θ(I). That is, the body of the rule is true and the head is false. By the definition of the reduct, this rule was generated from a rule r in Pm and a Herbrand state s. The generation of this rule implies that all literals in r which consist of predicates of the first m − 1 strata evaluated to true under Mm−1 and this state s. Moreover, the body atoms qdi¯i in the reduct correspond to literals in r of the form qi (E1 , . . . , Eia ) where qi is a predicate symbol belonging to the current stratum Pm while E1 , . . . , Eia are expressions of lower stratum predicates which evaluate into d¯i = d1 , · · · , dia . Since the body is true in θ(I) for any qi it is θ(I)(qid¯i ) = true and so it must be I(qi )(d¯i ) = true by the definition of θ. Consequently, the body of r must be true for that specific state s. On the other hand, since pd¯ is false in θ(I), the head I(p) d¯ = false by definition of θ. This contradicts the assumption that I is a model of P since we found a rule and s that is not satisfied in I. M Now assume that θ(I) is a model of Pm m−1 and suppose I ∈ Hm,m−1 is not a model of P. The argument that leads to the contradiction follows a similar line of thought as the other direction and is omitted. From the previous statement it follows that θ−1 (Nm ) is a model of P. But since the M bijection is order preserving and Nm is minimum model of Pm m−1 then for any other model M ′ ∈ Hm,m−1 θ−1 (Nm ) ≤ M ′ . Since Mm ∈ Hm,m−1 and Mm is minimal then it must be Mm = θ−1 (Nm ) and the statement of the lemma follows. Before establishing the complexity bounds for query evaluation, we must first characterize the size of the underlying semantic domains and the space required to represent their elements. The following lemma provides an upper bound on the size and memory needed for storing values of the respective domain. Lemma A.5 Let P be a Higher-Order Datalog¬ program and let n = |UP |. Let ρ be any type of order i. Then |JρKUP | ≤ expi (|UP |d ) for some natural constant number d. Furthermore, for any ′ d ∈ JρKUP , we can store d in memory using at most expi−1 (|UP |d ) bits (or tape cells) for some constant d′ . Proof

22

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis

We prove the statement by induction on the order i of the type ρ. If i = 0 then we have the individual type ι . The size of the domain JιK is |UP | = n, which is ≤ exp0 (n1 ). Any element d ∈ JιK can be uniquely represented by an index requiring ⌈log n⌉ bits. An element of JoK requires 1 bit. Assume the hypothesis holds for all types of order j < i. Let ρ be a type of order i. Then, ρ is of the form ρ1 → · · · → ρm → o, where each argument type ρj has order kj < i (so kj ≤ i − 1). The case where ρ = o is trivial and omitted. The domain JρK consists of all functions Jρ1 K → · · · → Jρm K → JoK. The size of this domain is: |JρK| = |JoK||Jρ1 K|×···×|Jρm K| . By the induction hypothesis, for each j, |Jρj K| ≤ expkj (ncj ) ≤ expi−1 (ncj ) for some ′ constants cj . The product of these sizes is bounded by expi−1 (nd ) for some constant d′ . Consequently, d′

′

|JρK| ≤ 2expi−1 (n ) = expi (nd ) for defined constant d′ . Furthermore, to store an element f ∈ JρK, we can use its full function table representation (since domains are finite). The size of this representation is equal to the number of entries in the table, which is the size of the input domain: Qm d′ ′ j=1 |Jρj K| ≤ expi−1 (n ) bits for some constant d . Lemma A.6 Let P be a (k + 1)-Order stratified linear Datalog¬ program with k ≥ 1 that defines a generic query and let E with type ρ be some expression using predicates from P and ρ is of at most k order. There exists a deterministic Turing machine that takes as input an encoding of a database D that uses n individual constant symbols and the encoding of a state s for the variables and computes the meaning JEKs (M ) where M is the unique two-valued stable model of P ∪ D. Furthermore, it does so using at most expk−1 (nd ) tape cells for some constant d. Proof We will prove the statement by induction on the strata of the program P ∪ D. More formally the statement we will show is the following: Assume that for any expression E containing only predicates from the first m strata and some Herbrand state s there exists a Turing machine (an expression evaluator) that computes JEKs (M ), using at most expk−1 (nd ) tape cells for some constant d. Then for any expression E containing only predicates from the first m + 1 strata and some Herbrand state s there exists a Turing machine (an expression evaluator) that computes JE′ Ks′ (M ), ′ using at most expk−1 (nd ) tape cells for some constant d′ > d. We proceed with the base case of the induction. Without loss of generality, we can assume that the first stratum contains only the external predicates supplied by the input database D in the form of facts. These are first-order predicates and are not redefined in the query program P. Thus, we partition by strata the program as P∪D = D∪P1 ∪· · ·∪Pmmax . With this assumption the base of the induction is trivial to prove. We proceed with the induction step. Let M denote the unique stable model of P ∪ D. For each m ≤ mmax , we define Mm to be the unique stable model of D ∪ P1 · · · ∪ Pm and Um+1 the splitting set that corresponds to the predicates of the first m strata such that bUm+1 (P) = D ∪ P1 ∪ · · · ∪ Pm . Notice that each constant of type ι appearing in P must appear in the external predicates of database

From Time to Space: The Impact of Linearity in Higher-Order Datalog

23

D since the program defines a generic query (i.e., P contains no individual constants by itself). Therefore, for each m ≤ mmax , bUm+1 (P) contains every individual constant and so each bUm+1 (P) shares the same Herbrand universe. By Lemma A.1 the restriction of Mm+1 with respect to Um+1 is the unique stable model of bUm+1 (P) and thus coincides with Mm . We define helper routines which we call the “query machines” which we will then use to describe the expression evaluator. The query machines: For any 1 ≤ m′ ≤ m + 1 we define a Turing machine that computes each query of the form Mm′ (p) d1 , . . . , dj for p ∈ Pm′ when given the input database encoded in some sensible form and a set of di ∈ Jρi K as a function (or a higherorder set) representation and does so using at most expk−1 (poly(n)) tape cells. Notice that since the types of ρi are used as arguments and thus are of order at most k, writing down those elements in the input takes space at most j × expk−1 (poly(n)) by Lemma A.5. By Lemma A.4 it is enough to compute the least model of the propositional program M ′ Pm′m −1 and use the bijection to determine the truth value of Mm′ (p) d1 , . . . , dj for p ∈ Pm′ . But the machine cannot instantiate this program since each argument has a domain of cardinality of up to expk (poly(n)) thus the set of all different propositional atoms and rules will exceed the memory limit. The machine instead operates in a top-down fashion instantiating the rules as needed. The equivalence of this procedure with the bottom-up computation is well-known in literature for propositional programs. The machine operates as follows: 1. It starts with the atom (p d1 · · · dn ) written on the tape, where the di are representations of expression values, i.e., a string that describes the value1 . 2. Non-deterministically selects a rule p R1 · · · Rj ← L1 , . . . , Lr from Pm′ and guesses a valid assignment for the rule’s variables such that di is assigned to Ri for all i ∈ {1, . . . , j}. 3. Iterates through the literals Li in the rule body: • If Li = (not E) is a negative literal then the machine computes JLi Ks[R̄/d] ¯ (Mm′ −1 ) = JLi Ks[R̄/d] ¯ (M ) by invoking an expression evaluator for the m′ − 1 strata defined for E to compute the value of JEKs[R̄/d] ¯ (M ). The existance of this evaluator is given by the induction hypothesis since m′ − 1 ≤ m. Then it performs the negation operator to the output. The machine that is invoked uses at most expk−1 (poly(n)) space which is freed after the computation. • If Li = E is a positive literal of no predicates from stratum m′ then the machine computes JLi Ks[R̄/d] ¯ (Mm′ −1 ) = JLi Ks[R̄/d] ¯ (M ) by invoking an expression evaluator ′ for m −1 strata defined for E to compute the value of JEKs[R̄/d] ¯ (M ). The existence of this evaluator is given by the induction hypothesis since m′ − 1 ≤ m. The machine that is invoked uses at most expk−1 (poly(n)) space which is freed after each computation. • If there is a predicate in Li from the (m′ )-th stratum, then this is the unique recursive literal q E1 · · · Et implied by linearity. Every Ei is of order at most k and includes predicates from the first m strata. Iterate through E1 , . . . , Et invoking 1 For example, a relation can be represented as a string listing all tuples in some predetermined order.

24

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis each time the corresponding evaluator, passing as parameter the guessed variable assignment, to compute the value that corresponds to each Ei and store the representations d′1 , . . . , d′t . Construct a new ground atom q d′1 · · · d′t with those representations. The memory used for this atom is bounded by expk−1 (poly(n)) by Lemma A.5 given the order of the argument types. 4. If all literals Li evaluate to true without encountering a recursive literal, then evaluate the query result as true. 5. Otherwise, if one of the literals Li is a recursive one, overwrite the current goal with q d′1 · · · d′t and loop back to Step 2. The size of goal never exceeds expk−1 (poly(n)) cells.

Note that the aforementioned query machine is non-deterministic and may contain computational paths that do not terminate (e.g., consider the rule p←p). So, this machine is not technically a decider of whether Mm′ (p) d1 , . . . , dj for p ∈ Pm′ is true or false. However, for machines that are space bounded (more specifically by a space constructible function f (n) (Sipser 2012)) there exists a corresponding non-deterministic Turing machine where every computational path terminates. In particular, the machine includes an initial step that given the input size n it computes the the value expk (poly(n)) in expk−1 (poly(n)) space and uses this isolated space to simulate a step counter. Each computation path will then auto-reject if the number of steps has exceeded the number of possible configurations. Finally, by Savitch (1970), there also exists a deterministic machine that decides whether Mm′ (p) d1 , . . . , dj for p ∈ Pm′ is true or false in the same space complexity class. In the following text when we refer to the “query” machine we mean the deterministic version. The expression evaluator: We now show how to extend this computation to any arbitrary fixed expression E of order at most k that contains predicates of the first m + 1 strata while still using memory that is bounded by expk−1 (poly(n)). To be entirely formal the calculation of memory usage should also account for the length of the expression. For reasons of brevity, we avoid to account for that since we are interested in how bounded expressions (e.g., those appearing in the query program) behave under variable input database sizes. The evaluator machine for an expression E will invoke in sequence the previous query machines when needed. We show the existence of such machine and argue about the memory used by induction on the length of the expression. For the base case, assume that the length of E is 1. It is easy to verify that evaluators using at most expk−1 (poly(n)) space exist for all expressions of length 1. We have two cases: 1. E = X for some variable or E = c for some ι constant. 2. E = p for some constant predicate p. The first case is trivial since we use the variable assignment. For the second case, let p ∈ Pm′ for some m′ ≤ m + 1. By the order assumption of E, p has a type of order at most k. We generate the different tuples of possible arguments in an increasing manner. For each combination we invoke the m′ -query machine described previously to get the corresponding truth value forming a set of size expk−1 (poly(n)) in memory. The query machine itself operates in expk−1 (poly(n)) space that is reused for each separate query and the total result is stored in expk−1 (poly(n)) memory.

From Time to Space: The Impact of Linearity in Higher-Order Datalog

25

We proceed with the general step of the induction. Assume that for every expression of length at most l there exist evaluators that compute it in at most expk−1 (poly(n)) tape cells. Let E be an expression of size l + 1. We have two cases: 1. E = X E1 E2 . . . Et for some variable X. 2. E = q E1 E2 . . . Et for some predicate q. Both cases are easy to argue about. We show the second. Let q ∈ Pm′ with m′ ≤ m + 1. Notice how for each Ei it is an argument and thus the order of its type is at most k. We perform the following steps: 1. Evaluate the expressions E1 , . . . , Et sequentially to obtain and store their representations d1 , . . . , dt . Since every Ei has length at most l and type of order at most k, by inductive hypothesis each can be computed by an appropriate evaluator and stored using total memory bounded by expk−1 (poly(n)). 2. To determine the representation of the result, the machine enumerates all possible tuples dt+1 , . . . , dt′ in increasing fashion regarding the remaining arguments. For each tuple, it invokes the query machine for the m′ -th stratum with the goal (q d1 · · · dt dt+1 · · · dt′ ) in reusable memory. The bound on the representation formed is expk−1 (poly(n)) that follows from the order of E and Lemma A.5. Theorem 5.1 Let P be a (k + 1)-order Stratified Linear Datalog¬ program that defines a query. Then, there exists a deterministic Turing machine that takes as input an encoding of a database D that uses n individual constant symbols and a ground atom p(ā), where p is a predicate constant of P and ā is a tuple of those individual constants, and decides whether p(ā) ∈ QP (D), while using at most expk−1 (nd ) tape cells for some constant d. Proof Immediate from Lemma A.6.

B The Graph Recoloring Problem and its Transformation to QBF The theoretical alignment between the second-order fragment of Stratified Linear HigherOrder Datalog and PSPACE naturally motivates compiling these programs into Quantified Boolean Formulas (QBFs), allowing highly optimized modern solvers to serve as the execution backend. Rather than presenting a systematic treatment, this section serves as a proof of concept by walking through the Graph Recoloring program presented in Example 3. To intuitively illustrate the mechanics of this translation, we break the process down into three phases: grounding the first-order variables into boolean vectors, compiling the lower strata into a boolean formula, and utilizing universal quantification to compress the linear path search.

26

A. Charalambidis, B. Kostopoulos, and P. Rondogiannis B.1 Grounding the Configuration Space

In first-order Datalog, the active state of a computation is typically a single node or a tuple of domain elements. In second-order Datalog, the active state is an entire relation. Consider an input graph with N vertices (nodes) and a predefined set of K available colors. The configuration of the board at any given moment is fully captured by the existentially quantified first-order binary relation C, where C(X, Col) evaluates to true if vertex X is painted with color Col. Because the domain of vertices and colors is strictly finite, the total number of possible configurations is also finite. We can systematically flatten this first-order relation into a one-dimensional boolean vector ⃗c of length N × K. Each bit cx,col in this vector represents the truth value of the corresponding atom C(X, Col). Therefore, the dynamic evaluation of the 2nd-order Datalog program is mathematically equivalent to traversing a massive, albeit finite, graph of size 2N ×K , where each node is a specific boolean bit-vector representing a distinct coloring state. B.2 Compiling the Static Strata into Formulas The strict stratification of the language (Definition 3.1) guarantees that rules are evaluated in a feed-forward manner without negative cycles. Because they operate entirely on known, static structures (the graph edges E, the vertices V , the colors K, and the boolean vectors), they act purely as declarative constraints. A compiler can systematically map each of these rules directly into a static, quantifier-free boolean formula. First, we define the boolean formulas ensuring a vector ⃗c represents a valid graph coloring based on the logic: _ _ Tconflict (⃗c) = (cx,col ∧ cy,col ) (x,y)∈E col∈K _ _ Tmultiple colors (⃗c) = (cx,col1 ∧ cx,col2 ∧ col1 ̸= col2 ) x∈V

Tuncolored (⃗c) =

_

col1 ,col2 ∈K

^ x∈V

col∈K

¬cx,col

Tinvalid coloring (⃗c) = Tconf lict (⃗c) ∨ Tmultiple colors (⃗c) ∨ Tuncolored (⃗c) Tvalid coloring (⃗c) = ¬Tinvalid coloring (⃗c) Next, we define the formulas ensuring the transition from state ⃗c1 to state ⃗c2 modifies exactly one vertex. We first define a helper formula Tdiff (x, ⃗c1 , ⃗c2 ) which is true if vertex x loses a color it had in ⃗c1 (implying a change between the states): _ Tdiff (x, ⃗c1 , ⃗c2 ) = (c1,x,col ∧ ¬c2,x,col ) col∈K _ Thas diff (⃗c1 , ⃗c2 ) = Tdiff (x, ⃗c1 , ⃗c2 ) x∈V _ Tmultiple diffs (⃗c1 , ⃗c2 ) = (Tdiff (x, ⃗c1 , ⃗c2 ) ∧ Tdiff (y, ⃗c1 , ⃗c2 ) ∧ x ̸= y) x,y∈V

Tone diff (⃗c1 , ⃗c2 ) = Thas diff (⃗c1 , ⃗c2 ) ∧ ¬Tmultiple diffs (⃗c1 , ⃗c2 ) Finally, by conjoining these constraints, the compiler generates the formula Tvalid step (⃗c1 , ⃗c2 ) for the valid_step predicate: Tvalid step (⃗c1 , ⃗c2 ) = Tvalid coloring (⃗c1 ) ∧ Tvalid coloring (⃗c2 ) ∧ Tone diff (⃗c1 , ⃗c2 )

From Time to Space: The Impact of Linearity in Higher-Order Datalog

27

B.3 Compressing the Linear Path via Savitch’s Theorem The final stratum of our program introduces the predicate recolorable which is recursive. Because the rule contains at most one recursive call to itself, the evaluation does not branch into an exponentially expanding search tree. Given our configuration space, the maximum possible length of a non-looping path is bounded by 2N ×K . Naively asking a boolean solver to search for a path of this length would require unrolling the formula Tvalid step exponentially many times. For ⃗ ⃗v1 ) ∧ instance, testing a path of length m requires writing ∃⃗v1 . . . ∃⃗vm [Tvalid step (start, ⃗ · · · ∧ Tvalid step (⃗vm−1 , target)]. If m = 2N ×K , the resulting formula would be exponentially larger than the memory capacity of any physical machine, rendering the translation useless. To prevent this exponential blow-up, the compiler leverages the core principle of Savitch’s theorem, utilizing the universal quantifiers of QBF to act as a spatial compression i mechanism. We recursively define a bounded path formula Precolorable (⃗u, ⃗v ) which evaluates i to true if there is a valid path from ⃗u to ⃗v of length at most 2 . 0 For the base case: Precolorable (⃗u, ⃗v ) ≡ (⃗u ≈ ⃗v ) ∨ Tvalid step (⃗u, ⃗v ). For the recursive step: h  i i−1 i Precolorable (⃗u, ⃗v ) = ∃m∀⃗ ⃗ a∀⃗b (⃗a ≈ ⃗u ∧ ⃗b ≈ m) ⃗ ∨ (⃗a ≈ m ⃗ ∧ ⃗b ≈ ⃗v ) → Precolorable (⃗a, ⃗b) In this recursive definition, we posit the existence of an intermediate halfway state m. ⃗ i−1 Instead of explicitly writing the formula Precolorable twice (once for the left half ⃗u → m ⃗ and once for the right half m ⃗ → ⃗v ), the universal quantifiers ∀⃗a, ⃗b act as a structural umbrella. They force the solver to verify both halves of the journey using only a single, i−1 mathematically compressed copy of the Precolorable sub-formula.

Related documents

• String Diagrams for Process Mining#978502
• ZigZag Trie: A Novel Index for Contextual Queries#978503
• A Functional Pilot for Certified Freshness-Aware Semantic--Spatial Range Retrieval#978504
• Efficiently Linking Unstructured Data for Multi-step Reasoning#978505