On this page:
4.1 disj and conj goals
4.2 Streams
4.3 Syntactic Sugar
4.4 Updating Reification
4.5 Example
8.4

4 Implementing disjunction and conjunction

Now we add support for disjunction and conjunction. To do this, our state will remain the same, but we will make significant changes to our reifier.

4.1 disj and conj goals

disj and conj are used to express various combinations of other operators — not only the operators we have implemented so far such as == and fresh but also recursive combinations of disj and conj themselves. These goals take a state like == and fresh but instead of returning a single state like the latter, they return a stream (a list that has potentially infinite elements, from which we "pull" one element at a time). The streams themselves are implemented as a monad. Without any further ado, here are disj and conj:

(define (disj g1 g2)
  (lambda (s/c)
    (mplus (g1 s/c) (g2 s/c))))
 
(define (conj g1 g2)
  (lambda (s/c)
    (bind (g1 s/c) g2)))

Here, mplus and bind are operators on streams used to combine them. Intuitively, in a disjunction we want the results of independently applying both the goals to the state and in a conjunction we first apply the first goal, and then apply the second goal to the results of the first application. The stream operators will thus be implemented to achieve this.

4.2 Streams

For pedagogical convenience we first implement finite streams, then extend them to infinte streams. Finite streams are just lists. Thus, mplus is append and bind is applying a goal each element of the list:

(define (mplus $1 $2)
  (cond
    [(empty? $1) $2]
    [(cons? $1) (cons (car $1) (mplus (cdr $1) $2))]))
 
(define (bind $ g)
  (cond
    [(empty? $) mzero]
    [(cons? $) (mplus (g (car $)) (bind (cdr $) g))]))

where we define mzero as an empty stream (implemented as an empty list):

(define mzero empty)

Now consider, the following program:
(define (fives x)
   (disj
     (== x 5)
     (fives x)))
(run 1 (x) (fives x))
The problem with such a program is that it eagerly keeps on evaluating an infinite loop, when in reality only the first result is needed. This is where we use streams implemented as suspended lambdas, and instead write the program as:
(define-syntax snooze
  (syntax-rules ()
    [(_ g) (lambda (st) (lambda () (g st)))]))
 
(define (snoozed-fives x)
  (disj
    (== x 5)
    (snooze (fives x))))
(run 1 (x) (snoozed-fives x))
We also update our mplus and bind to handle suspended lambdas
(define (mplus $1 $2)
  (cond
    [(empty? $1) $2]
    [(procedure? $1) (lambda () (mplus $2 ($1)))]
    [(cons? $1) (cons (car $1) (mplus (cdr $1) $2))]))
 
(define (bind $ g)
  (cond
    [(empty? $) mzero]
    [(procedure? $) (lambda () (bind ($) g))]
    [(cons? $) (mplus (g (car $)) (bind (cdr $) g))]))

4.3 Syntactic Sugar

We next yet again define some syntactic sugar to make it convenient to write programs:
(define-syntax disj+
  (syntax-rules ()
    [(_ g) (snooze g)]
    [(_ g0 g ...) (disj (snooze g0) (disj+ g ...))]))
 
(define-syntax conj+
  (syntax-rules ()
    [(_ g) (snooze g)]
    [(_ g0 g ...) (conj (snooze g0) (conj+ g ...))]))
 
(define-syntax conde
  (syntax-rules ()
    [(_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...)]))

4.4 Updating Reification

Similarly, we update our reifier to deal with suspended lambdas
(define (pull $)
  (if (procedure? $) (pull ($)) $))
 
(define (take n $)
  (if (zero? n) empty
    (let ([$ (pull $)])
      (cond
        [(empty? $) $]
        [else (cons (car $) (take (- n 1) (cdr $)))]))))
 
(define (take-all $)
  (let ([$ (pull $)])
    (if (empty? $) $ (cons (car $) (take-all (cdr $))))))
 
(define-syntax run
  (syntax-rules ()
    [(_ n (x ...) g0 g ...)
     (mk-reify (take n (call/empty-state
                         (fresh (x ...) g0 g ...))))]))
 
(define-syntax run*
  (syntax-rules ()
    [(_ (x ...) g0 g ...)
     (mk-reify (take-all (call/empty-state
                           (fresh (x ...) g0 g ...))))]))

4.5 Example

An example that our current interpreter can handle is:
(define (snoozed-fives x)
  (disj
    (== x 5)
    (snooze (fives x))))
(run 1 (x) (snoozed-fives x))