Created
March 29, 2012 11:18
-
-
Save jonase/2236019 to your computer and use it in GitHub Desktop.
Why doesn't the expression terminate?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(defn segmento [left middle right all] | |
(fresh [xs] | |
(appendo left middle xs) | |
(appendo xs right all))) | |
user> (run* [q] | |
(segmento [1 2] [3 4] [5 6] [1 2 3 4 5 6])) | |
(_.0) | |
user> (run* [q] | |
(segmento [1 2] [3 4] [5 6] q)) | |
((1 2 3 4 5 6)) | |
user> (run* [q] | |
(segmento [1 2] [3 4] q [1 2 3 4 5 6])) | |
((5 6)) | |
user> (run* [q] | |
(segmento [1 2] q [5 6] [1 2 3 4 5 6])) | |
((3 4)) | |
user> (run* [q] | |
(fresh [xs ys] | |
(segmento [1 2] xs ys [1 2 3 4 5 6]) | |
(== q [xs ys]))) | |
([() (3 4 5 6)] | |
[(3) (4 5 6)] | |
[(3 4) (5 6)] | |
[(3 4 5) (6)] | |
[(3 4 5 6) ()]) | |
;; Does not terminate. | |
;; user> (run* [q] (segmento q [3 4] [5 6] [1 2 3 4 5 6])) | |
; Evaluation aborted. | |
;; Changing the order of the clauses yields "expected" results: | |
(defn segmento [left middle right all] | |
(fresh [xs] | |
(appendo xs right all) | |
(appendo left middle xs))) | |
user> (run* [q] | |
(fresh [a b c] | |
(segmento a b c [1 2 3 4 5 6]) | |
(== q [a b c]))) | |
([() () [1 2 3 4 5 6]] | |
[() (1) (2 3 4 5 6)] | |
[(1) () (2 3 4 5 6)] | |
[() (1 2) (3 4 5 6)] | |
[(1) (2) (3 4 5 6)] | |
[() (1 2 3) (4 5 6)] | |
[(1 2) () (3 4 5 6)] | |
[(1) (2 3) (4 5 6)] | |
[() (1 2 3 4) (5 6)] | |
[(1 2) (3) (4 5 6)] | |
[(1 2 3) () (4 5 6)] | |
[(1) (2 3 4) (5 6)] | |
[() (1 2 3 4 5) (6)] | |
[(1 2) (3 4) (5 6)] | |
[(1 2 3) (4) (5 6)] | |
[(1) (2 3 4 5) (6)] | |
[(1 2 3 4) () (5 6)] | |
[() (1 2 3 4 5 6) ()] | |
[(1 2) (3 4 5) (6)] | |
[(1) (2 3 4 5 6) ()] | |
[(1 2 3) (4 5) (6)] | |
[(1 2) (3 4 5 6) ()] | |
[(1 2 3 4) (5) (6)] | |
[(1 2 3) (4 5 6) ()] | |
[(1 2 3 4 5) () (6)] | |
[(1 2 3 4) (5 6) ()] | |
[(1 2 3 4 5) (6) ()] | |
[(1 2 3 4 5 6) () ()]) |
I'll understand what that means when I get my version of TRS :) (it's on its way!)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
It's important to consider which one receives ground vars and which one does not