core.logic

disequality

Details

  • Type: Defect Defect
  • Status: Closed Closed
  • Priority: Blocker Blocker
  • Resolution: Completed
  • Affects Version/s: None
  • Fix Version/s: None
  • Component/s: None
  • Labels:
    None

Description

This snippet wrongly succeeds with the result:

(([foo _0] :- (!= (foo _0))))

(run* [q]
      (nom/fresh [a b]
        (fresh [x y]
          (!= x y)
          (== (nom/tie a (nom/tie b [b y])) (nom/tie b (nom/tie a [a x])))
          (== x 'foo)
          (== [x y] q))))

Moving the disequality anywhere further down makes the snippet rightly fail.

Activity

Hide
Nada Amin added a comment -

An insight: if I remove the -relevant-var? protocol from !=c in core.logic, then this works and all other tests pass. Of course, this probably has performance applications, so thinking of alternatives.

Show
Nada Amin added a comment - An insight: if I remove the -relevant-var? protocol from !=c in core.logic, then this works and all other tests pass. Of course, this probably has performance applications, so thinking of alternatives.
Hide
Nada Amin added a comment -

The problem is not specific to nominal disequality. Here is the same bug with only core.logic:

(run* [q]
    (fresh [x y w z]
      (!= x y)
      (!= w z)
      (== z y)
      (== x 'foo)
      (== y 'foo)))

This should fail, because x == y == 'foo, but instead we get:

(_0 :- (!= (_1 foo)) (!= (foo foo))))
.

The problem is that var-rands takes the substitution map into account, while -relevant-var doesn't.

Show
Nada Amin added a comment - The problem is not specific to nominal disequality. Here is the same bug with only core.logic:
(run* [q]
    (fresh [x y w z]
      (!= x y)
      (!= w z)
      (== z y)
      (== x 'foo)
      (== y 'foo)))
This should fail, because x == y == 'foo, but instead we get:
(_0 :- (!= (_1 foo)) (!= (foo foo))))
. The problem is that var-rands takes the substitution map into account, while -relevant-var doesn't.
Hide
Nada Amin added a comment -

Another way disequality is broken:

(run* [q]
  (fresh [x y w z]
    (!= x [y])
    (== x ['foo])
    (== y 'foo)))

This snippet should fail, but instead returns '(_0). This is because y is not returned by recover-vars.

Show
Nada Amin added a comment - Another way disequality is broken:
(run* [q]
  (fresh [x y w z]
    (!= x [y])
    (== x ['foo])
    (== y 'foo)))
This snippet should fail, but instead returns '(_0). This is because y is not returned by recover-vars.
Nada Amin made changes -
Field Original Value New Value
Summary nominal disequality disequality
David Nolen made changes -
Priority Major [ 3 ] Blocker [ 1 ]
Hide
Nada Amin added a comment -

diseq.diff contains detailed commit message explaining the issues, fixes, and tests.

Show
Nada Amin added a comment - diseq.diff contains detailed commit message explaining the issues, fixes, and tests.
Nada Amin made changes -
Attachment diseq.diff [ 11789 ]
David Nolen made changes -
Resolution Completed [ 1 ]
Status Open [ 1 ] Resolved [ 5 ]
David Nolen made changes -
Status Resolved [ 5 ] Closed [ 6 ]

People

Vote (0)
Watch (0)

Dates

  • Created:
    Updated:
    Resolved: