core.logic

A conde clause that beings with a fresh expression will initially fail

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Major Major
  • Resolution: Declined
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None
  • Environment:
    tested against HEAD (0.8.0-rc3-SNAPSHOT) and CLJ 1.5.0-RC15

Description

(ns test                                                                                                                                                                          
  (:refer-clojure :exclude [==])                                                                                                                                                  
  (:require                                                                                                                                                                       
   [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]                                                                                                                                                                      
     (conde                                                                                                                                                                       
       [(== q 1)]                                                                                                                                                                 
       [(== q 2)]))                                                                                                                                                               
   (run* [q]                                                                                                                                                                      
     (conde                                                                                                                                                                       
       [(fresh [a] (== q 1))]                                                                                                                                                     
       [(== q 2)])))

Activity

Hide
David Nolen added a comment -

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.

Show
David Nolen added a comment - 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.
Hide
Austin Haas added a comment -

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.

Show
Austin Haas added a comment - 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.
Hide
David Nolen added a comment - - edited

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.

Show
David Nolen added a comment - - edited 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.
Hide
David Nolen added a comment -

Not a bug.

Show
David Nolen added a comment - Not a bug.

People

Vote (0)
Watch (1)

Dates

  • Created:
    Updated:
    Resolved: