Evaluation order and nontermination in query languages

# Evaluation order and nontermination in query languages Source: [https://www.rntz.net/post/2026-06-11-datalog-nontermination.html](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html) June 2026 Last month I gave a talk at[FLOPS](https://functional-logic.org/events/flops/2026/)about[finite functional programming](https://arxiv.org/abs/2604.26161)or ‘λFS’, my latest attempt \(previously:[Datafun](https://www.rntz.net/datafun)\) to combine functional programming with relational programming à la Datalog or SQL – and tensor algebra too, because why not? In λFS, a relation R is treated as a function: we let R\(*x*\) = true iff*x*is in R, false otherwise\. This function is*finite*in thatR\(*x*\) = truefor only finitely many inputs*x*: these are its*support\.*[The paper](https://arxiv.org/abs/2604.26161)gives a type system for ensuring functions have finite support\. At runtime, we represent a finite boolean function by tabulating its support in a hash table or a balanced tree \(like a table in a database\)\. This generalizes beyond booleans to any codomain with a ‘default’ value\. A function’s support are those inputs whose output is non\-default; for instance, the booleans with false as default, or the integers with 0 as default\. A finite function can then be represented as a key\-value table whose keys are the function’s support; any other key implicitly maps to the default value\. Non\-boolean finite maps arise naturally as the result of aggregations, while tensor algebra is essentially relational algebra over non\-boolean \(usually real\-valued\) finite maps\. ## Nontermination and evaluation order In the talk, I mentioned that recursion was future work for λFS\. Naturally, someone – I think it was Atsushi Igarashi – asked what the difficulty was\. The primary difficulty is that recursion allows nontermination\. Semantics for nontermination usually use domain theory, which has fallen out of fashion in recent decades, and which consequently I’ve never deeply studied and find a bit intimidating\.[1](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-1) Moreover, as soon as nontermination or any effect is involved, there is a question of evaluation order\. Even in the untyped lambda calculus, where evaluation is confluent, call\-by\-name and call\-by\-value evaluation terminate on different programs\. What’s worse, in relational languages ‘evaluation order’ has a more expansive meaning than in functional languages\. Consider this example: Given`R,S : nat =\> bool`input tablesand`test : nat \-\> bool`a black\-box predicatelet`Q\(x\) := R\(x\) and test\(x\) and S\(x\)`the queryHere,`=\>`denotes a finite function, represented as a table, while`\-\>`denotes an arbitrary function, represented by a procedure or closure\. Thinking relationally, our query`Q`is the intersection of the tables`R`and`S`, filtered by the black\-box predicate`test`\. The central question is:*in what order do we evaluate this query?*We could go left\-to\-right: for each`x`in`R`, if`test\(x\)`passes, check if`x`is in`S`\. In Python: ``` [x for x in R if test(x) if x in S] ``` Or, noting that`test`may be expensive but looking up an entry in a table is cheap, we could check if`x`is in`S`before calling`test`: ``` [x for x in R if x in S if test(x)] ``` And if we happen to know`S`is much smaller than`R`, we can save a lot of time by iterating over`S`instead of`R`: ``` [x for x in S if x in R if test(x)] ``` The standard relational philosophy regards evaluation order as an implementation detail, decided by the query planner\. However, this ordering may affect whether`Q`terminates, because different orders call`test`on different arguments\. A contrived example: ``` R := {"hello", "world"} S := {"hello", "alice"} test(x) := x == "hello" or loop-forever() Q(x) := R(x) and test(x) and S(x) ``` Left\-to\-right execution calls`test\("hello"\)`, which succeeds, followed by`test\("world"\)`, which loops forever\. But if we intersect`R`and`S`*before*calling`test`, we only test`"hello"`and so terminate\. I have expressed this problem in λFS, but it arises in any SQL or Datalog engine supporting user\-defined functions, and exposes a tension between typical DB and PL assumptions: DB*The query engine may choose the execution strategy to optimize performance\.* PL*We can reason compositionally about program behavior – in particular, about termination or execution time\.* λFS tries to bridge DB and PL, and gets stuck in the awkward middle: I must either favor one perspective over another, or find a way to thread the needle’s eye\. I do not yet know how best to do this\. Instead, here are three directions forward – three sketches of possible semantics for λFS with recursion \(or Datalog with nonterminating functions\)\. ## 1Left to right evaluation has a simple cost model The simplest strategy to implement also has the most straightforward semantics: evaluate from left to right\. This is the most typical PL approach: it avoids query planning and puts the job squarely in the hands of the programmer\. This makes the execution time of a query easy to predict and reason about, as my friend[Rob Simmons](https://typesafety.net/rob/about/)pointed out to me while working on[Finite Choice Logic Programming](https://dl.acm.org/doi/10.1145/3704849); this is more or less the cost model of[Dusa](https://dusa.rocks/docs), an implementation of FCLP\. In this approach, a conjunction of*n*terms turns into at most*n*nested loops\. For instance,`R\(x\) and S\(y\)`becomes 2 loops: ``` for x in R: for y in S: yield (x,y) ``` In a query like`R\(x\) and S\(x\)`, where the variables of`S\(x\)`are already entirely grounded, we generate a test rather than a loop: ``` for x in R: if x not in S: continue yield x ``` If some but not all variables of a conjunct are grounded, we need an index; for example, to run`R\(x,y\) and S\(y,z\)`, we want to index`S`by`y`: ``` for x,y in R: for z in S_index[y]: -- assuming an appropriate S_index yield (x,y,z) ``` If we have these indexes and all our conjuncts are applications of finite maps, the cost model is simple: count the prefix firings\. That is, for every prefix of the conjunction,count how many assignments of its free variables satisfy it\. So for`R\(x,y\) and S\(y,z\)`, we add together: 1. The number of`x,y`tuples satisfying`R\(x,y\)`\. 2. The number of`x,y,z`tuples satisfying`R\(x,y\) and S\(y,z\)`\. What about black\-box predicates like`test\(x\)`? For such a conjunct: 1. All its arguments must be grounded by the preceding conjuncts, so that when we reach it we have concrete values for them\. 2. We add the cost of evaluating`test\(x\)`for each firing of our preceding conjuncts\. This may exceed the number of total`x`values; for instance,`R\(x\) and S\(y\) and test\(x\)`will call`test\(x\)`once for each`x,y`pair\. This straightforwardly answers our original question about termination: we run predicates on exactly the values which satisfy their preceding conjuncts\. By complete coincidence, the left\-to\-right grounding requirement exactly matches the[type system in the finite functional programming paper](https://arxiv.org/abs/2604.26161); I originally regarded this as a weakness of the type system, but with a left\-to\-right execution strategy it makes perfect sense\. I like the simplicity and predictability of this approach, and appreciate how it ‘bites the bullet’, making the programmer responsible for performance \(though this is plainly also a downside\)\. Unfortunately, for some queries \(the*cyclic*queries\) this makes it impossible to achieve acceptable performance – for instance, the triangle query`edge\(x,y\) and edge\(y,z\) and edge\(x,z\)`\.[2](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-2) ## 2Nondeterministic evaluation order allows declarative optimizations We’ve seen three plausible evaluation orders for`R\(x\) and test\(x\) and S\(x\)`\. Why commit ourselves unnecessarily? The typical DB approach is to give the query planner/optimizer as much leeway as possible by leaving the order of evaluation unspecified\. This means we cannot say exactly which values we will call`test`on, but we can*bound*this set above and below\. Similarly, program termination goes from a yes/no question to yes/no/maybe\. Returning to our running example,`R\(x\) and test\(x\) and S\(x\)`, we can’t call`test`without some`x`value\. The only sources we have are`R`and`S`; so any query execution will call`test`on*at most*the values in either`R`or`S`, and*at least*the values that are in both\. If`test\(x\)`terminates for all`x ∈ R ∪ S`, our query terminates; if it diverges for some`x ∈ R ∩ S`, our query diverges; otherwise, it may go either way\. But all terminating executions should give the same result\. Unfortunately, I don’t know how to specify this nondeterminism in a compositional way\. There are two typical approaches to semantics: operational and denotational\. Operationally, I’m not sure how to give semantics that correspond to bottom\-up logic programming at all, let alone which capture variation in evaluation order\. In particular, in λFS, how do finite λs evaluate? Normal procedural λs wait until they’re applied to an argument to reduce, but the entire point of finite functions is that they don’t do that; they’re tabled eagerly like database queries\. But it’s not obvious how to capture this behavior in a small\-step operational semantics\. \(Datafun does have an operational semantics, but only because it uses monad comprehensions, which commit to left\-to\-right evaluation – exactly what I want to get away from\!\) Denotationally, the natural way forward would be to augment the denotational semantics outlined in[the Finite Functional Programming paper](https://arxiv.org/abs/2604.26161)with domain theory and some form of nondeterminism\. Unfortunately, I’m not yet familiar enough with the domain theory of nondeterminism \(powerdomains\) to know how to make this work\. If you think you know an appropriate approach here, or would like to work on this together, please email me \(*qnrxunery@tznvy\.pbz*,[rot13](http://www.rot13.com/)\)\. ## 3‘Parallel and’ has the most declarative behavior What if we could have our cake and eat it too? So far I’ve assumed that if we execute`test\(x\)`and it diverges, then our query diverges\. This is why evaluation order matters: it affects which`x`we call`test`on\. We can drop this assumption if we allow ourselves to think a little less*sequentially\.* Let ⊥ represent divergence\. The typical implementation of`and`is sequential, examining its left argument first and short\-circuiting if it yields`false`: ``` false and x = false -- short circuit; don't evaluate x true and x = x ⊥ and x = ⊥ -- we never get around to evaluating x. ``` This is ugly: logical conjunction is symmetric, but this`and`is left\-biased\. Let’s restore symmetry while preserving continuity: ``` false and x = false -- no need to evaluate x further true and x = x x and false = false -- no need to evaluate x further x and true = x ``` I call this ‘parallel and’ by analogy with Plotkin’s parallel or\.[3](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-3)Sequential ‘and’ always fully evaluates its left argument, but parallel ‘and’ evaluates both arguments concurrently, terminating when either yields`false`or both yield`true`\. This miraculously restores determinism to λFS\.Consider our previous example: ``` R := {"hello", "world"} S := {"hello", "alice"} test x := (x == "hello") or loop-forever() Q(x) := R(x) and test(x) and S(x) ``` Left\-to\-right execution evaluates`test\("world"\) and S\("world"\) = ⊥ and false`\. With sequential ‘and’ this diverges, but with parallel ‘and’ it is simply`false`\. No matter whether we iterate over`R`first,`S`first, or their intersection, we get the same intuitively correct answer:`Q = \{"hello"\}`\. Unfortunately it is not clear how to implement parallel`and`efficiently\. It is not inconceivable, however:[miniKanren](https://minikanren.org/)’s search strategy, for instance, resembles an implementation of parallel\-or, and I have heard from[Will Byrd](http://webyrd.net/)that Andorra Prolog supported a form of conjunction analogous to parallel and\. I myself[had a paper at miniKanren 2025](https://arxiv.org/abs/2510.26016)about fair conjunction using an iterator interface for the implementation of worst\-case optimal joins\. So I suspect this problem is crackable\. But is it worth it?[4](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fn-4) ## Footnotes 1. Complicating things further, there are two distinct varieties of recursion: \(a\) recursive*functions,*which are computed lazily – the function body is not evaluated until required by a function application — and \(b\) recursive*relations*\(in λFS, finite functions\), which in bottom\-up relational programming are computed eagerly by iteration to a fixed point \(we start with the empty relation and repeatedly apply the definition until it stabilizes\)\. But the second can probably be defined in terms of the first: recursion suffices to define iteration\.[↩](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-1) 2. Concretely, let*edge*= \{\(1,*x*\) :*x*∈ \[1\.\.*n*\]\} ∪ \{\(*x*, 1\) :*x*∈ \[1\.\.*n*\]\} for some large*n*\. Then the triangles \(the answers to our query\) are those triples*x*,*y*,*z*in which at least two of*x*,*y*,*z*are 1 and the other is any of \[1\.\.*n*\]; so there are3*n*− 2 ∈ Θ\(*n*\)of them\. But there areΘ\(*n*2\)triples satisfying the prefix`edge\(x,y\) and edge\(y,z\)`\. So left\-to\-right evaluation does quadratic work to find linear results\. More generally, left\-to\-right evaluation corresponds to a left\-deep binary join plan, and for cyclic queries it is known that binary join plans can be asymptotically inefficient: cyclic queries require[worst\-case optimal joins\.](https://dl.acm.org/doi/10.1145/3180143)[↩](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-2) 3. I believe ‘parallel or’ originated in Gordon Plotkin’s[LCF Considered as a Programming Language](https://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf)\(1977\), but I find[these lecture notes](https://www.cl.cam.ac.uk/teaching/2526/DenotSem/DenSem-Notes.pdf)a more approachable introduction; see p64, §8\.1, “Failure of full abstraction\.”[↩](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-3) 4. See also[this mastodon discussion](https://lipn.info/@mevenlennonbertrand/116658145724067149)with Meven Lennon\-Bertrand, who quite reasonably questions the validity of my analogy between parallel or/and on booleans and fair logic programming disjunction/conjunction\.[↩](https://www.rntz.net/post/2026-06-11-datalog-nontermination.html#fnref-4)