Hi Jonas! miniKanren uses a complete, interleaving search algorithm that (in theory) is guaranteed to find a answer, *if* an answer exists.
Reordering disjuncts/conde clauses can affect running time, but never the semantics. If an answer exists, it will be found regardless of ordering of disjuncts, but the running time might change from 1 millisecond to a million years depending on the disjunct ordering. Reordering conjuncts/fresh goals/goals within a single conde clause is more subtle. Once again, if an answer exists, in theory it will be found regardless of conjunct ordering, but the running time may differ wildly. However, if no answer exists, reordering conjuncts can be the difference between "finite failure" (the query terminates in finite time) and "divergence" (an infinite loop). As a general rule, place recursive goals last within conjunctions and disjunctions. Obviously this is not always possible, since many times there are multiple recursive goals in a conjunction. The latest version of Barliman uses optimizations Greg Rosenblatt added that "delay" certain goals until their arguments become more instantiated, a form of dynamic goal reordering. Alas, this can't always help. There is much, much more I could talk about on this topic... Cheers, --Will On Tue, Jul 25, 2017 at 4:33 PM, 'Jonas Kölker' via minikanren <[email protected]> wrote: > Hello all :-) > > I've attached a fragment of my learning-some-miniKanren project, which is a > theorem prover. > > Running the file Chez Scheme, it spits out two proofs after about ~77 ms and > ~34 ms, respectively. (It takes about ~10s in total using Chicken Scheme.) > > As far as I have been able to tell, if I re-order either the two calls from > modus-ponens to proof-treeo or any of the calls from proof-treeo to axiomN, > the program takes forever. > > My questions which I hope all of you lovely folks will help me answer: > > Should "forever" be taken literally or figuratively? That is, do the > reorderings cause divergence or merely a massive slow-down? > In either case, why? What are the steps performed by the miniKanren system, > and why is that order-dependent? > How does one tell (at least some of the time) whether one's program is > divergent? > > All of this order-dependence raises a scary question: are there some > theorems which a prover like mine will find a proof of if the con- and > disjuncts are ordered one way, but won't find a proof of if they're ordered > some other way? How does one tell that a concrete proof search algorithm is > complete (finds >=1 proof of all valid theorems)? > > (The axioms in my prover are Łukasiewicz's third systems, see > https://en.wikipedia.org/wiki/List_of_logic_systems. IIRC my textbook listed > that one as its single example of a complete and minimal system of axioms, > FWIW.) > > -- > You received this message because you are subscribed to the Google Groups > "minikanren" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/minikanren. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/minikanren. For more options, visit https://groups.google.com/d/optout.
