3 ms·

What would be some advantages of this design over the µKanren design [0] which uses a search monad [1] and expresses unification and relations directly as plain

What would be some advantages of this design over the µKanren design [0] which uses a search monad [1] and expresses unification and relations directly as plain values and functions? [0] http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf [1] http://homes.soic.indiana.edu/ccshan/logicprog/LogicT-icfp2005.pdf http://homes.soic.indiana.edu/ccshan/logicprog/LogicT-icfp20...

tom_mellior 8y ago
Those papers and systems deal with Prolog-like languages, not Datalog-like ones. These are different languages, even though there is a common set of similar-looking programs with similar-ish declarative semantics but completely different procedural semantics. In particular, it's easy to write programs that easily compute the desired results when run on a Datalog system, but that run into an infinite loop when run on a Prolog system. Also, the solver here is special-cased to treat only a certain subset of Datalog that is much simpler than the full language.
- convolvatron 8y ago
  it looks like it doesn't handle negation. one of those unfortunate but interesting features of the space of recursive declarative languages. if you allow something to be true only if something else is not true, your solution space is no longer monotonic. meaning that a result you thought was part of the solution can later be retracted. if there is a cycle (trivially "a if not a"), then you may not ever arrive at an answer. that might seem simple to detect, but that cycle can exist through an arbitrary number of rules and data dependencies, so in the limit is undecidable. ideally, as in this solver, you could keep adding terms you could show to be correct from the data and rules at hand until they and all their consequences have been found, and which point you can stop (fixed point). but negation screws up this plan. there are various restrictions on negation, solver heuristics, and partial conservative proofs of termination that can be applied. but this is where your beautiful simple declarative world starts getting sad and messy. [edit: I'd like to leave this because I wish I understood the problem with negation earlier, but I just skimmed and missed stratification, Frank thoughtfully explains below]
  - frankmcsherry 8y ago
    I'm drinking at the moment, so maybe messy but not sad. The engine supports negation in the standard way: stratification. You can call 'from_antijoin' with a static relation for its second argument but not a variable. It is not discussed in the post because it is a bit of a diversion from the intended message (and because antijoin is computationally not much different from a filter). If you would like a more general compute model with non-monotonic iteration, I recommend differential dataflow!

tom_mellior 8y ago

Those papers and systems deal with Prolog-like languages, not Datalog-like ones. These are different languages, even though there is a common set of similar-looking programs with similar-ish declarative semantics but completely different procedural semantics. In particular, it's easy to write programs that easily compute the desired results when run on a Datalog system, but that run into an infinite loop when run on a Prolog system. Also, the solver here is special-cased to treat only a certain subset of Datalog that is much simpler than the full language.

convolvatron 8y ago
it looks like it doesn't handle negation. one of those unfortunate but interesting features of the space of recursive declarative languages. if you allow something to be true only if something else is not true, your solution space is no longer monotonic. meaning that a result you thought was part of the solution can later be retracted. if there is a cycle (trivially "a if not a"), then you may not ever arrive at an answer. that might seem simple to detect, but that cycle can exist through an arbitrary number of rules and data dependencies, so in the limit is undecidable. ideally, as in this solver, you could keep adding terms you could show to be correct from the data and rules at hand until they and all their consequences have been found, and which point you can stop (fixed point). but negation screws up this plan. there are various restrictions on negation, solver heuristics, and partial conservative proofs of termination that can be applied. but this is where your beautiful simple declarative world starts getting sad and messy. [edit: I'd like to leave this because I wish I understood the problem with negation earlier, but I just skimmed and missed stratification, Frank thoughtfully explains below]
- frankmcsherry 8y ago
  I'm drinking at the moment, so maybe messy but not sad. The engine supports negation in the standard way: stratification. You can call 'from_antijoin' with a static relation for its second argument but not a variable. It is not discussed in the post because it is a bit of a diversion from the intended message (and because antijoin is computationally not much different from a filter). If you would like a more general compute model with non-monotonic iteration, I recommend differential dataflow!