<< Back to previous view

[LOGIC-113] A conde clause that beings with a fresh expression will initially fail Created: 13/Feb/13  Updated: 28/Jul/13  Resolved: 15/Feb/13

Status: Closed
Project: core.logic
Component/s: None
Affects Version/s: None
Fix Version/s: None

Type: Defect Priority: Major
Reporter: Austin Haas Assignee: David Nolen
Resolution: Declined Votes: 0
Labels: None

tested against HEAD (0.8.0-rc3-SNAPSHOT) and CLJ 1.5.0-RC15

(ns test                                                                                                                                                                          
  (:refer-clojure :exclude [==])                                                                                                                                                  
   [clojure.core.logic :refer :all]))                                                                                                                                             

;; This expression should evaluate to true, but it does not, 
;; because the second run* returns (2 1) instead of (1 2).
(= (run* [q]                                                                                                                                                                      
       [(== q 1)]                                                                                                                                                                 
       [(== q 2)]))                                                                                                                                                               
   (run* [q]                                                                                                                                                                      
       [(fresh [a] (== q 1))]                                                                                                                                                     
       [(== q 2)])))

Comment by David Nolen [ 14/Feb/13 12:13 AM ]

This is not an error. No promises are made about the order of results. If you want need to verify that two runs are the same it's best to put the results into a set - we actually do this in the tests now.

Comment by Austin Haas [ 14/Feb/13 1:14 AM ]

Shouldn't the programmer be able to reason about the order that the clauses will be tried? That's one way to direct the search and I know at least one example in TRS highlights that aspect--in Ch. 5, unwrapo is re-written to push the recursive call down, otherwise it diverges. How could you know that goal will terminate if you can't reason about the order of the clauses? I assume it is much more difficult to write exclusively non-overlapping clauses.

Likewise, shouldn't the programmer be able to design a logic program so that it produces a predictable first result?

This is all very new to me, so please forgive me if I'm way off.

Comment by David Nolen [ 14/Feb/13 8:57 AM ]

miniKanren makes no promises about order anymore, Will actually talks about this in his dissertation. It's part of the design and leaves the door wide open for concurrent search when we get there.

Even so, I do understand there are cases where the programmer might want more control than is provided by the default behavior. Customizable search is on the roadmap.

But the current default behavior is expected and unlikely to change.

Comment by David Nolen [ 15/Feb/13 12:49 PM ]

Not a bug.

Generated at Tue Jan 16 21:43:24 CST 2018 using JIRA 4.4#649-r158309.