msv-lab / modus

A language for building Docker/OCI container images
GNU Affero General Public License v3.0
279 stars 9 forks source link

SLD Resolution? #209

Open brurucy opened 1 year ago

brurucy commented 1 year ago

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?

mechtaev commented 1 year ago

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?

brurucy commented 1 year ago

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: bruno.rucy.carneiro.alves.de.lima@ut.ee