Making conjunction fair is the reason why I messed up with core.logic, and this post document the approach I explore in the fair-conj2 branch.

In The Reasoned Scheduler I said that conjunction is easy: you wait for the first stream to provide a answer that you pass to the next goal. It looks easy but it suffers from being ordered: when the first goal diverges (produces an infinite stream of results or never halts) and the next goal is known to fail, the conjuction diverges too! This is unfair conjunction.

Changing the order of the goals would fix this particular example but like noted by William Byrd in Relational Programming in miniKanren: Techniques, Applications, and Implementations (page 53 and 54):

However, reordering goals has its disadvantages. For many programs, no ordering of goals will result in finite failure (see the remaining example in this chapter). Also, by committing to a certain goal ordering we are giving up on the declarative nature of relational programming: we are specifying how the program computes, rather than only what it computes. For these reasons, we should consider alternative solutions.

[T]he goal ordering we picked might diverge when we ask for a second answer, while the other ordering may fail finitely after producing a single answer.

So, to make conjunction fair (commutative), one has to not commit to an ordering of goal, which means that both goals must be executed in parallel (interleaved execution or even true parallelism). As soon as one of the goal produces an answer, this substitution has to be communicated to the other threadgoal so as to narrow its search space.

As a consequence of the disappearance of ordering, the distinction between a goal and a stream disappears too. I introduced a Search abstraction. A Search may yield a substitution (or nil)
and progress with step. It sounds awfully familiar with first and next.

Let’s name plus, join and narrow respectively the disjunction, conjunction and narrowing operators. Conjunction is distributive over disjunction as usual and narrowing is distributive over both.

Here is how the key expression is derived:

(join a b)
(join (plus (yield a) (step a)) b) ; decompose a 
(plus (join (yield a) b) (join (step a) b)) ; distribute join
(plus (narrow b (yield a)) (join (step a) b)) ; joining with a substitution (or nil) is narrowing
(plus (narrow b (yield a)) (join b (step a))) ; commute the operands of join for interleaving

This expression can be found nearly as-is in the code.

Narrowing is performed lazily: when one steps a suspended narrowing (a Narrow instance), the narrowing is propagated (thanks to its distributivity) to the children searches of its argument.

To make narrowing efficient, I introduced the min-yield function which, given a Search, returns the minimal substitution yielded by this search. That is: if this Search ever yield results they will be extensions of the min-yield substitution. This allows to discard a Search in its entirety when the narrowing substitution and the min-yield substitutions are not compatible!

To compute min-yield substitutions, the narrowing process leaves nodes (Scope instances) in the computation tree labeled with the narrowing substitution. By default min-yield returns empty-s the empty substitution.

This is the gist of my approach to fair conjunction. In a subsequent post, I’ll cover heuristics I use to prioritize execution of Searches.

Practically, what does it mean? It means that logic programs are easier to write, it also means that, at the moment, a program written with unfair conjunction in mind run slower with fair conjunction. Interestingly, under fair conjunction, naive pluso (p. 63) seems refutationally complete.

I intend to explore how constraints can be added to this branch and how it will impact (positively) performance.

If you feel like dabbling with this branch, I’ll be more than happy to hear your feedback. Thanks!