On this page:
5.1 Introduction to Disequality Constraints
5.2 Updating ==
5.3 Implementing =/  =
5.4 Optimizations
5.5 Updating Reification
5.6 Examples
8.4

5 Implementing Disequality

The final constraint that we will implement in this tutorial is disequality.

5.1 Introduction to Disequality Constraints

To implement disequality we must once again extend our state. Now our state also holds a disequality store that captures all the disequality constraints present in a program. The store is a list of association lists, where each association list corresponds to a use of the disequality constraint in a program. To understand how an association list is built, consider the following disequality constraint:

(fresh (x y) (=/= (x y) (1 2)))

The association list built for this would be

((x . 1) (y . 2))

The way to interpret this association list is that both x being 1 and y being 2 cannot happen simultaneously.

As our state is extended, we define a new helper:

(define (d-of st)
  (caddr st))

5.2 Updating ==

After each unification, we now need to check if any of the disequality constraints are violated:

(define (== u v)
  (lambdag (st)
    (==-verify (unify u v (s-of st)) st)))
 
(define ==-verify
  (lambda (s st)
    (cond
      [(not s) mzero]
      [(eq? (s-of st) s) (unit st)]
      [(verify-d (d-of st) '() s)
       => (lambda (d) (unit `(,s ,(c-of st) ,d)))]
      [else mzero])))

If the unification failed, then nothing needs to be checked. If it succeeded without extending the substitution, then again nothing needs to be checked. If it succeeded by extending the substitution, we use the helper verify-d to verify that no disequality constraints are violated:

(define verify-d
  (lambda (d* d*^ s)
    (cond
      [(empty? d*) d*^]
      [(unify* (car d*) s)
       => (lambda (s^)
            (cond
              [(eq? s s^) #f]
              [else (let ([d (prefix-s s^ s)])
                      (verify-d (cdr d*) (cons d d*^) s))]))]
      [else (verify-d (cdr d*) d*^ s)])))
 
(define unify*
  (lambda (d s)
    (cond
      [(empty? d) s]
      [(unify (caar d) (cdar d) s)
       => (lambda (s)
            (unify* (cdr d) s))]
      [else #f])))

5.3 Implementing =/=

Now we define the disequality operator:
(define =/=
  (lambda (u v)
    (lambdag (st : s c d)
       (cond
         [(unify u v s) => (post-unify-=/= s c d)]
         [else (unit st)]))))
 
(define post-unify-=/=
  (lambda (s c d)
    (lambda (s^)
      (cond
        [(eq? s^ s) mzero]
        [else (let ([d+ (prefix-s s^ s)])
                (unit `(,s ,c ,(cons d+ d))))]))))
 
(define prefix-s
  (lambda (s^ s)
    (cond
      [(eq? s^ s) '()]
      [else (cons (car s^) (prefix-s (cdr s^) s))])))

This makes use of unification to add new constraints to the disequality store — if unification already succeeds without extending the substitution, then the disequality should fail. If it succeeds by extending the substitution, this new extension will be the constraint to be added to the disequality store.

5.4 Optimizations

Now we implement two optimizations. Firstly, we can remove constraints that are irrelevant to the final answer. For example, in the following program:

(run 1 (x) (fresh (y) (=/= y 6)) (=/= x 'elephant))

the constraint on y may be discarded. This is implemented as follows:

(define purify
  (lambda (d* r)
    (cond
      [(null? d*) '()]
      [(anyvar? (car d*) r)
       (purify (cdr d*) r)]
      [else (cons (car d*)
                  (purify (cdr d*) r))])))
 
(define anyvar?
  (lambda (v r)
    (cond
      [(var? v) (var? (walk v r))]
      [(pair? v) (or (anyvar? (car v) r) (anyvar? (cdr v) r))]
      [else #f])))

Next, we may also discard constraints that are subsumed by other constraints. For example, in the following program:

(run 1 (x) (fresh (y) (=/= `(,x ,y) '(5 6)) (=/= x 5)))

if the first constraint is violated, then the second constraint is also definitely violated. Thus, the second constraint is subsumed by the first constraint and may be discarded. This is implemented as follows:

(define subsumed?
  (lambda (d d*)
    (and (not (null? d*))
         (or (eq? (unify* (car d*) d) d)
             (subsumed? d (cdr d*))))))
 
(define rem-subsumed
  (lambda (d* d*^)
    (cond
      [(null? d*) d*^]
      [(or (subsumed? (car d*) d*^) (subsumed? (car d*) (cdr d*)))
       (rem-subsumed (cdr d*) d*^)]
      [else (rem-subsumed (cdr d*) (cons (car d*) d*^))])))

5.5 Updating Reification

Finally, we make minor changes to our reifier to take care of the disequality store:

(define subsumed?
  (lambda (d d*)
    (and (not (null? d*))
         (or (eq? (unify* (car d*) d) d)
             (subsumed? d (cdr d*))))))
 
(define rem-subsumed
  (lambda (d* d*^)
    (cond
      [(null? d*) d*^]
      [(or (subsumed? (car d*) d*^) (subsumed? (car d*) (cdr d*)))
       (rem-subsumed (cdr d*) d*^)]
      [else (rem-subsumed (cdr d*) (cons (car d*) d*^))])))

5.6 Examples

Some example programs we can now run are:

(run* (p) (=/= p 1))
(run* (p) (=/= 1 p) (== 1 p))
(run* (q)
  (fresh (p r)
    (=/= '(1 2) `(,p ,r))
    (== `(,p ,r) q)))
(run* (q)
  (fresh (p r)
    (=/= '((1) (2)) `((,p) (,r)))
    (== `(,p ,r) q)))
(run* (q)
  (fresh (p r)
    (=/= '(1 2) `(,p ,r))
    (== 1 p)
    (== 2 r)
    (== `(,p ,r) q)))
(run* (q)
  (fresh (p r)
    (=/= `((1) (,r)) `((,p) (2)))
    (== `(,p ,r) q)))