Add support for a form of "committed choice"

[tausbn]

Okay, this is probably a pretty "out there" suggestion, but bear with me.

Say I want to use Dusa to find a nonempty connected subgraph of some given graph (possibly subject to some other constraints). For simplicity, let's say the graph has only three vertices, arranged in a line:

vertex a. vertex b. vertex c.
adj a b. adj b c.

adj V1 V2 :- adj V2 V1.

Next, we select a subset of the vertices by means of a functional predicate selected:

selected V is {true, false} :- vertex V.

To enforce connectedness, we'll arbitrarily assign one of the selected vertices to be the "root", and demand that every other selected vertex is reachable from the root:

root is? V :- selected V is true.

reach root.
reach V2 :-
  reach V1,
  selected V2 is true,
  adj V1 V2.

Finally, we can enforce this globally by saying that every vertex is either not selected, or is reachable:

reach_or_unselected V :- reach V.
reach_or_unselected V :- selected V is false.

#demand reach_or_unselected a.
#demand reach_or_unselected b.
#demand reach_or_unselected c.
#demand selected V is true. # to enforce nonemptyness

Side note: I keep wanting to reach for a forall or not, but I can't seem to find either. In particular, I would much rather be able to write #demand forall V. reach_or_unselected V or #forbid not (reach_or_unselected V) (which is similar to what I would write in ASP). If there's a better way to represent this, do let me know! 🙂

Now, the above code (playground link) does the trick in that it only allows solutions where the selected vertices indeed induce a connected subgraph, but the solutions contain some unwanted duplicates that only differ in the choice of root.

Of course, I know that the choice of root doesn't really matter! If I have selected a connected subgraph, then every vertex is reachable from every other vertex.

What I would like, then, is some way to tell Dusa that I don't actually care about the choice of root, and that the evaluator can just use the first thing that fits.

In other words, I would like to be able to write something like

root is! V :- selected V is true.

where is! commits to any solution, and doesn't explore any alternatives. (So, it's kind of a mixture between is and is?.)

You can think of the ! as punning either "∃!" or the Prolog cut operator (though I feel like it's maybe a bit dangerous to suggest the latter 😉).

There are of course other options. I could project away the reach relation if there was some way to hide predicates (as I suggested in #96). I could break the symmetry by stating that the root vertex is the smallest of all the selected vertices (according to some total order).

However, both of these options might end up doing a lot of pointless computation when really all I want to say is "pick one; I don't care which one".

I haven't checked how this would interact with the semantics presented in the paper (I'm still working my way through it), but I figured it would be worth mentioning in case it could be made to fit in nicely.

[robsimmons]

Good stuff here! I believe your "side note" is handled by #17 — we haven't added it because, as far as I can figure, conditional demand doesn't desugar the way the existing #forbid and #demand do. However, post-POPL-paper-and-presentation I think I can confidently say "any way of declaring certain putative models invalid in a monotonic way is semantically reasonable," so this is totally a reasonable request.

[robsimmons]

I believe I needed what you describe in at least one of the Advent of Code examples. I handled it by wrapping in Javascript and writing two programs, grabbing one solution from the first program, and then asserting all facts from that program into the second program.

I see two issues at play: one of them is that mixing up the selected logic and the root logic can lead to wildly inefficient algorithms in certain cases, which could be solved by doing evaluation in a stratified way: fully evaluating the root relation before making choices about the selected relation. This is part of a "stratified evaluation" goal that's on Chris and my's private project tracker here, fwiw.

What would suffice in this example is a way to tell Dusa to commit, not in a rule-based way, but in a predicate based way: generate a solution up to the root relation but without making any decisions that (according to conclusion<-premise dependencies) are unnecessary for calculating the root relation, then commit to that part of the solution and proceed. I'm moderately opposed to adding a language-syntax-level feature to achieve this, and I think I'd describe @chrisamaphone as strongly opposed based on our initial conversations, BUT adding this as an API enhancement or command line option seems pretty reasonable.

[robsimmons]

asserting all facts from that program into the second program

hmm, could the command-line API be tweaked (or used in its current form?) to achieve this effect with Unix pipes?