modus icon indicating copy to clipboard operation
modus copied to clipboard

SLD Resolution?

Open brurucy opened this issue 1 year ago • 2 comments

Hi,

What's the reason that lead you to use a prolog evaluation strategy (SLD resolution) for a datalog?

For instance, magic-sets is a relatively simple datalog-first strategy that would most certainly outperform SLD resolution by orders of magnitude.

The project is awesome though! Has there been a follow-up?

brurucy avatar Sep 17 '23 11:09 brurucy

Hi @brurucy,

We used SLD resolution to implement Prolog-style extensions. For example, Modus allows writing rules like

app(cflags) :-
  from("gcc:latest"),
  copy(".", "."),
  run(f"gcc ${cflags} test.c -o test").
  

where cflags is not a grounded variable in the sense that its value is not derived from the database, but from the user query. For example, if one wants to compile the project with debugging support, they may build app("-g"). Standard Datalog does not allow writing such rules. Please refer to this part of the documentation for more information. It would be nice to integrate optimisations like magic-sets, but we need more research to understand how to adapt it for our extensions.

Thank you! Yes, we are continuing working on Modus, but there have not been any concrete publications/releases yet. What is your opinion about this direction? Do you have any ideas or specific usecases?

mechtaev avatar Sep 21 '23 11:09 mechtaev

I think this could be solved in different ways.

we defer the evaluation of these predicates until all of their arguments are bound to constants

To my understanding, this means that by the time the head is evaluated, all "substitutions" that are applied to it will indeed yield a ground fact, hence not needing support for existential variables at all. I think "prolog-style" would be a "more correct" label if that variable could be propagated further than the current rule.

Why couldn't the rule be:

app(x) :-
  from("gcc:latest"),
  copy(".", "."),
  cflags(x),
  run(f"gcc ${x} test.c -o test").

I suppose that a "user query" could be modelled as an insertion to that "cflags" predicate.

It could also be done through skolemization, where cflags is a decidable UDF

app(cflags(runCmd)) :-
  from("gcc:latest"),
  copy(".", "."),
  runCmd := f"gcc <flags hardcoded in the rule definition> test.c -o test",
  run(runCmd).

Do you have any ideas or specific usecases? Yes. I believe this could be expanded in two ways:

  1. using bottom-up sideways information passing
  2. Being expanded to work with CI in general. A very interesting and practical take would be to make a Datalog of GitHub actions workflows.

We could chat more about this. My academic email is: [email protected]

brurucy avatar Sep 21 '23 12:09 brurucy