Assuming correct Kanren implementation, order has no effect on correctness.
Execution order of disjunctions has everything to do with performance. Reordering of conjunctions can have performance effect if atleast two conjuncts have disjunctions. Depending on what Kanren optimizations are used, different source orders matter for performance. Some implementations attempt to do automatic cuts, which mitigates some combinatoral explosion. None that I know off attempt to reorder neither dynamically based on some runtime stats, nor based on static analysis of predicate complexity. I plan to implement minikanren-like interface to Z3 and see how that will perform againts different kanren imps over a range of problems. Atleast one huge advantage Z3 impl will have will be scalarized and Pareto front multi-objective answer set optimization. On Jul 25, 2017 3:34 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.
