On Wednesday, July 26, 2017 at 1:31:04 AM UTC+2, William Byrd wrote: > There is much, much more I could talk about on this topic...
Please do :-) > the running time might change from 1 millisecond to a million years > depending on the disjunct ordering. How does this happen? Is there some way of tracing the steps done by mK? Is "sequential execution of con-/disjuncts with backtracking on unification failure" an accurate model of what mK does? I figure this would describe a DFS(ish) search, but you've said "interleaving" here and "BFS(ish)" elsewhere (some talk/hangout), so I guess no. Can you describe the steps in similar high-level terms, such that I could compute a trace by hand? (I guess a 'trace' might be something like a list of [call stack, set of logical variables, what unification we're trying now]) Reordering disjuncts/conde clauses can affect running time [...] Reordering > conjuncts/fresh goals/goals within a single conde clause is more subtle [...] the running time may differ wildly. I guess the generic explanation for this is "some orderings look at every last corner of a large and solution-free subset of the search space, and others don't". How can I shine light on the way my search space is being explored? How can I make reasonable predictions about performance? > However, if no answer exists, reordering conjuncts can be the difference > between finite failure and divergence > Yes, I recall seeing what I'll slightly misquote as "(run 1 (q) (infinite-loop-of success) failure)" which diverges, but terminates immediately if you put failure before the infinite loop. I think that code was by you. The latest version of Barliman uses optimizations Greg Rosenblatt added I'll give that a look some time. Loose thoughts: I figure the way to quickly find a proof of some theorem t is for t to be an axiom, or (using modus ponens) to prove some formula such that t occurs positively on the right hand side of [the right hand side of]* an implication. As it happens, axiom 2 is the best axiom in this particular system to introduce such a formula. If I'm right, then a better optimized proof search is one that makes use of this insight, for instance by finding all the ways t can be matched against the right implication spine of each of the axioms, then recursively proving the path down one such spine. More generally, if t is not an axiom, constrain the search space as much as possible by applying the bit of information that t must occur as the right hand side of some inference rule and/or guide the search to the subset of the search space where the necessary thing occurs. Maybe what I'm trying to get at is "instead of generating and testing lots of proofs, do a top-down goal-directed search". Maybe, I dunno. Because I'm not all that familiar (yet) with how mK searches. -- 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.
