Hi Eugene! "Atleast one huge advantage Z3 impl will have will be scalarized and Pareto front multi-objective answer set optimization."
Can you elaborate on these a little bit? Also, do you think we could incorporate these optimizations into miniKanren? Thanks! --Will On Tue, Jul 25, 2017 at 5:03 PM, Eugene Grigoriev <[email protected]> wrote: > 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. -- 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.
