Binding sets for infinite predicates?

[turbo]

In my queries, I often have shared conjunct conditions between many rules that would be useful to extract, but this always leads to the error

Atom contains unbound variable, or rule contains no variable at all

Which is expected for infinite predicates. I'm looking for a mechanism similar to CodeQL's Binding Sets to enable infinite predicate calls from constrained contexts.

Other prior art includes Logica's automatic infinite predicates, which are analyzed at compile time and only error when not used in a finite context. See “Infinite Predicates” here.

Here's a simple example that works, finding unique disjoint lists:

candidates[l] <- [
  [[1, 2, 3]],
  [[1, 4, 5]],
  [[7, 54, 23]]
]

?[rset] :=
  rset = sorted([l, r]),
  candidates[l],
  candidates[r],
  length(intersection(l, r)) == 0

gives

 rset
--------------------------
 [[1, 2, 3], [7, 54, 23]]
 [[1, 4, 5], [7, 54, 23]]

If I now create a predicate, I get the error mentioned above, since disjoint has no inherent binding. I'd like to be able to declare the "real" binding from the query predicate, though.

candidates[l] <- [
  [[1, 2, 3]],
  [[1, 4, 5]],
  [[7, 54, 23]]
]

disjoint[left, right] :=
  length(intersection(left, right)) == 0

?[rset] :=
  rset = sorted([l, r]),
  candidates[l],
  candidates[r],
  disjoint[l, r]

This is of course a trivial example, where the disjoint predicate could be grounded directly to the input relation. But in my uses, I sometimes have multiple rule bodies which all in themselves re-use the same conditions. Here's an example of a Countdown Number Problem solver, which could really benefit from a reusable operand-selection predicate:

# define numbers
numbers[n] <- [[1], [3], [7], [10], [25], [50]]

# constant expressions
mexpr[value, choice(used), choice(expr), min(cost)] := 
  numbers[value],
  used = [value],
  expr = to_string(value),
  cost = 0.0

# addition
mexpr[value, choice(used), choice(expr), min(cost)] := 
  mexpr[vl, ul, el, cl],
  mexpr[vr, ur, er, cr],
  length(intersection(ul, ur)) == 0,
  used = sorted(union(ul, ur)),
  length(used) <= 6,
  opcost = cl + cr + length(used),
  cost <= 15,

  value = vl + vr,
  expr = concat("(", el, " + ", er, ")"),
  cost = opcost + 1.0

# subtraction (positive intermediate only)
mexpr[value, choice(used), choice(expr), min(cost)] := 
  mexpr[vl, ul, el, cl],
  mexpr[vr, ur, er, cr],
  length(intersection(ul, ur)) == 0,
  used = sorted(union(ul, ur)),
  length(used) <= 6,
  opcost = cl + cr + length(used),
  cost <= 15,

  value = vl - vr,
  value > 0,
  expr = concat("(", el, " - ", er, ")"),
  cost = opcost + 1.05

# multiplication
mexpr[value, choice(used), choice(expr), min(cost)] := 
  mexpr[vl, ul, el, cl],
  mexpr[vr, ur, er, cr],
  length(intersection(ul, ur)) == 0,
  used = sorted(union(ul, ur)),
  length(used) <= 6,
  opcost = cl + cr + length(used),
  cost <= 15,

  value = vl * vr,
  expr = concat("(", el, " * ", er, ")"),
  cost = opcost + 1.2,
  vl != 1,
  vr != 1

# division
mexpr[value, choice(used), choice(expr), min(cost)] := 
  mexpr[vl, ul, el, cl],
  mexpr[vr, ur, er, cr],
  length(intersection(ul, ur)) == 0,
  used = sorted(union(ul, ur)),
  length(used) <= 6,
  opcost = cl + cr + length(used),
  cost <= 15,

  vr != 0,
  vl % vr == 0,
  value = vl / vr,
  expr = concat("(", el, " / ", er, ")"),
  cost = opcost + 1.3

?[result, cost] := 
  total = 765,
  mexpr[total, _, expr, cost],
  result = concat(expr, " = ", to_string(total))

:order cost
:limit 1

[CharlesTyrrell]

When I saw this question I realized it was what I was looking for as well. I'm trying to find an embedded database for user scripted read only analysis of their own data, and cozodb looks absolutely amazing for this use case, and being able to create abstractions/functions within the scripting language itself would be pretty important for extensibility / maintainability of a scripting code base.

[CharlesTyrrell]

The other option that I'm looking at is sqlite, but much of the time user's personal data might be more heirarchical than tabular, and it seems much easier to limit the side effects of a datalog query than one from sql.

[turbo]

Logica might be what you're looking for.

[CharlesTyrrell]

Omg this is what I'm looking for, thank you

[ConstantinVasilev]

@CharlesTyrrell @turbo can you give simplified example of the workflow that you are needing? Im a big fan of Logica an want to understand your use cases.