Non-determinism? · Elpi users & devs

I meant "non-deterministic" in the Prolog meaning, as in a predicate that may (fail or) succeed more than once (aka have more than one "solution"). Here is a very simple one, and what I get is not a new goal for each solution, just the first solution:

Elpi Tactic isel.
Elpi Accumulate lp:{{

  pred isel o:term.

  isel {{ 0 }}.
  isel {{ 1 }}.

  solve (goal _ _ _ _ [] as G) GL :-
    isel P,
    refine P G GL.

}}.
Elpi Typecheck.

Definition sel: nat.
Proof.
  elpi isel.
  Show Proof.  (* 0 *)
Qed.

(I'd have also tried an "inat" predicate, to try a recursive one, but couldn't get around converting from int to term... Anyway, I have seen there are examples with recursive predicates so I assume this is not a problem per se.)

Could you please confirm that indeed (talking of non-deterministic predicates) the first solution is the one that counts and the rest of the Prolog search space gets simply dropped (as the example above seems to tell)? Otherwise, if that's not the case, could you provide a minimal example that shows how to get multiple solutions/sub-goals/how to use a non-deterministic predicate? (Indeed, I am not sure what you mean exactly by "result".)

Julio Di Egidio (Oct 12 2023 at 09:30):

(I am not sure I am asking a sensible question, given this is about tactics, so having a proof is enough. Might make more sense with commands? But I have not yet explored that part at all. Overall, I am essentially interested in to which point I can actually leverage (lambda-)Prolog in my Coq coding...)

Enrico Tassi (Oct 12 2023 at 09:48):

Elpi can compute multiple solutions, but Coq's term can only contain one, so you have to look at the multiple solution in Elpi, not in Coq.
Try

std.findall (isel P) Solutions,
coq.say "solutions:" Solutions,
Solutions = [isel X|_],
refine X G GL

Julio Di Egidio (Oct 12 2023 at 10:05):

Thanks, Enrico. OK, which means (if I get you correctly) that only ever a finite set of solutions (out of the infinitely many that a predicate might have, e.g. an inat) is ultimately usable by/relevant to the Coq side [directly: I guess one can concoct a pair solution-continuation, anyway this is beside the point of what one can do at each step]... which FWIW is fine by me, please just correct me if I am still missing something (otherwise feel free to close the question).

Enrico Tassi (Oct 12 2023 at 11:23):

Well, ATM, Elpi is SLD, which may not be the best strategy to enumerate all solutions (eg, no loop detection, no duplicate pruning, no cache).
So std.findall is very dumb, and if the solutions are not finite (but reachable by SLD) then it will diverge.

In some sense the execution model of Elpi and Coq are orthogonal, so when you cross the boundary you have to live in the intersection of the two.

Julio Di Egidio (Oct 12 2023 at 11:28):

Allowing for different and even custom resolution strategies would make it into a "super-Prolog": findall over infinitely many solutions diverges in plain Prolog, too... As it is, I think it's fine: that we have to "bound the solution space" to get out to Coq's realm I find also totally reasonable... Anyway, my 2c. For now, thanks for the great work!

Enrico Tassi (Oct 12 2023 at 11:45):

Well, I think one day we might have an SLG engine baked in. Making the resolution engine pluggable would be too hard, IMO.

Julio Di Egidio (Oct 12 2023 at 13:06):

If one could code it in Coq, over I'd expect a very simple API... but then the problem would be performances. There are also other features that are super-cool in any Prolog, e.g. user-controllable (by meta-predicate) argument indexing, or solution tabling (assuming we have 'cut', I still know very little about Elpi :)). The point is reasonable performances: and if that's indeed a problem, unless there is a clever compilation scheme (leveraging 'coqc' only, not 'make' or we get into platform availability issues) such that we can really open Elpi to any custom (meta-)extensions (from a custom resolution strategy to, and more generally, custom meta-predicates) simply written in Coq itself, I'd really say it's fine as it is: meaning (from a user's perspective) the bulk of the logic stays in Coq and that's what we will compile or extract...

Stream: Elpi users & devs

Topic: Non-determinism?

Notification Bot (Oct 12 2023 at 09:13):