Assignment 10: Logic Programming

Revisions and Clarifications

Complete both parts of this assignment, and submit your results to Vincent in a file named a10.scm.

Make sure you have the most recent versions of mk.scm and mkdefs.scm:

Part I

Write the answer to the following problems using your knowledge of the miniKanren logic programming system. For each problem, explain how miniKanren arrived at the answer. You will be graded on the quality and completeness of your explanation; a full explanation will require several sentences.

Assume the following definitions for alwayso, nevero, succeed, and fail.

(define anyo
  (lambda (g)
    (conde
      [g]
      [(anyo g)])))

(define alwayso (anyo succeed))
(define nevero (anyo fail))

(define succeed (== #f #f))
(define fail (== #f #t))

Make sure to verify your answers by running the programs in miniKanren. You will need to load mk.scm and the definitions above before evaluating the run expressions.

What is the value of

(run 2 (q)
  (== 5 q)
  (conde
    [(conde
       [(== 5 q) (== 6 q)]) (== 5 q)]
    [(== q 5)]))

What is the value of

(run* (q)
  (exist (x y)
    (== `(,x ,y) q)
    (conde
      [fail succeed]
      [(conde
         [(== 5 x) (== y x)]
         [(== `(,x) y)]
         [(== x y)])]
      [succeed])))

What is the value of
```
(run 1 (q)
  alwayso
  fail)
```
What is the value of
```
(run 1 (q)
  fail
  alwayso)
```

What is the value of

(run 2 (q)
  (conde
    [succeed]
    [nevero]))

What is the value of

(run* (q)
  (exist (a b c d)
    (== `(,a ,b) `(,c (,a . ,d)))
    (== `(,b ,c) `((,a) ,d))
    (== `(,a ,b ,c ,d) q)))

Part II

Translate each of Scheme function into an equivalent miniKanren relation. Your relations must pass all of the provided tests. Remember that you may need to rearrange some of the goals in your relations to ensure termination (and therefore to pass the tests). In general, recursive calls should come at the end of a sequence of goals, while explicit or implicit calls to == should come at the beginning.

(define one-item
  (lambda (x s)
    (cond
      [(null? s) '()]
      [else (cons (cons x (car s))
              (one-item x (cdr s)))])))

(define assq
  (lambda (x ls)
    (cond
      [(null? ls) #f]
      [(eq? (car (car ls)) x) (car ls)]
      [else (assq x (cdr ls))])))

Here are the tests.

(define-syntax test
  (syntax-rules ()
    ((_ title tested-expression expected-result)
     (let* ((expected expected-result)
            (produced tested-expression))
       (if (equal? expected produced)
           (printf "~s works!\n" title)
           (error
            'test
            "Failed ~s: ~a\nExpected: ~a\nComputed: ~a"
            title 'tested-expression expected produced))))))

(define-syntax multi-test
  (syntax-rules ()
    ((_ title tested-expression expected-result* ...)
     (let* ((expected* expected-result*)
            ...
            (produced tested-expression))
       (cond
         [(equal? produced expected-result*) (printf "~s works!\n" title)]
         ...
         [else (error
                'test
                "Failed ~s: ~a\nComputed: ~a"
                title 'tested-expression produced)])))))

(test "one-itemo-1"
  (run* (q)
    (one-itemo 'a '(b c d) q))
  '(((a . b) (a . c) (a . d))))

(test "one-itemo-2"
  (run* (q)
    (one-itemo q '(b c d) '((a . b) (a . c) (a . d))))
  '(a))

(test "one-itemo-3"
  (run* (q)
    (one-itemo 'a q '((a . b) (a . c) (a . d))))
  '((b c d)))

(test "one-itemo-4"
  (run* (q)
    (one-itemo 'a '(b c d) `((a . b) . ,q)))
  '(((a . c) (a . d))))

(test "one-itemo-5"
  (run* (q)
    (one-itemo 'a '(b c d) '((a . b) (a . c) (a . d))))
  '(_.0))

(test "one-itemo-6"
  (run* (q)
    (one-itemo 'a `(b ,q d) '((a . b) (a . c) (a . d))))
  '(c))

(test "one-itemo-7"
  (run* (q)
    (exist (x y)
      (one-itemo x y '((a . b) (a . c) (a . d)))
      (== `(,x ,y) q)))
  '((a (b c d))))

(test "one-itemo-8"
  (run 6 (q)
    (exist (x y z)
      (one-itemo x y z)
      (== `(,x ,y ,z) q)))
  '((_.0 () ()) (_.0 (_.1) ((_.0 . _.1)))
    (_.0 (_.1 _.2) ((_.0 . _.1) (_.0 . _.2)))
    (_.0 (_.1 _.2 _.3) ((_.0 . _.1) (_.0 . _.2) (_.0 . _.3)))
    (_.0 (_.1 _.2 _.3 _.4) ((_.0 . _.1) (_.0 . _.2) (_.0 . _.3) (_.0 . _.4)))
    (_.0 (_.1 _.2 _.3 _.4 _.5) ((_.0 . _.1) (_.0 . _.2) (_.0 . _.3) (_.0 . _.4) (_.0 . _.5)))))



(test "assqo-1"
  (run* (q)
    (assqo 'x '() q))
  '())

(test "assqo-2"
  (run* (q)
    (assqo 'x '((x . 5)) q))
  '((x . 5)))

(test "assqo-3"
  (run* (q)
    (assqo 'x '((y . 6) (x . 5)) q))
  '((x . 5)))

(test "assqo-4"
  (run* (q)
    (assqo 'x '((x . 6) (x . 5)) q))
  '((x . 6) (x . 5)))

(test "assqo-5"
  (run* (q)
    (assqo 'x '((x . 5)) '(x . 5)))
  '(_.0))

(test "assqo-6"
  (run* (q)
    (assqo 'x '((x . 6) (x . 5)) '(x . 6)))
  '(_.0))

(test "assqo-7"
  (run* (q)
    (assqo 'x '((x . 6) (x . 5)) '(x . 5)))
  '(_.0))

(test "assqo-8"
  (run* (q)
    (assqo q '((x . 6) (x . 5)) '(x . 5)))
  '(x))

(test "assqo-9"
  (run* (q)
    (assqo 'x '((x . 6) . ,q) '(x . 6)))
  '(_.0))

(multi-test "assqo-10"
  (run 10 (q)
    (assqo 'x q '(x . 5)))
  '(((x . 5) . _.0)
    (_.0 (x . 5) . _.1)
    (_.0 _.1 (x . 5) . _.2)
    (_.0 _.1 _.2 (x . 5) . _.3)
    (_.0 _.1 _.2 _.3 (x . 5) . _.4)
    (_.0 _.1 _.2 _.3 _.4 (x . 5) . _.5)
    (_.0 _.1 _.2 _.3 _.4 _.5 (x . 5) . _.6)
    (_.0 _.1 _.2 _.3 _.4 _.5 _.6 (x . 5) . _.7)
    (_.0 _.1 _.2 _.3 _.4 _.5 _.6 _.7 (x . 5) . _.8)
    (_.0 _.1 _.2 _.3 _.4 _.5 _.6 _.7 _.8 (x . 5) . _.9))
  '(((x . 5) . _.0)
    ((_.0 . _.1) (x . 5) . _.2)
    ((_.0 . _.1) (_.2 . _.3) (x . 5) . _.4)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (x . 5) . _.6)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (x . 5) . _.8)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (_.8 . _.9) (x . 5) . _.10)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (_.8 . _.9) (_.10 . _.11) (x . 5) . _.12)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (_.8 . _.9) (_.10 . _.11) (_.12 . _.13) (x . 5) . _.14)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (_.8 . _.9) (_.10 . _.11) (_.12 . _.13) (_.14 . _.15) (x . 5) . _.16)
    ((_.0 . _.1) (_.2 . _.3) (_.4 . _.5) (_.6 . _.7) (_.8 . _.9) (_.10 . _.11) (_.12 . _.13) (_.14 . _.15) (_.16 . _.17) (x . 5) . _.18)))

(multi-test "assqo-11"
  (run 10 (q)
    (exist (x y z)
      (assqo x y z)
      (== `(,x ,y ,z) q)))
  '((_.0 ((_.0 . _.1) . _.2) (_.0 . _.1))
    (_.0 (_.1 (_.0 . _.2) . _.3) (_.0 . _.2))
    (_.0 (_.1 _.2 (_.0 . _.3) . _.4) (_.0 . _.3))
    (_.0 (_.1 _.2 _.3 (_.0 . _.4) . _.5) (_.0 . _.4))
    (_.0 (_.1 _.2 _.3 _.4 (_.0 . _.5) . _.6) (_.0 . _.5))
    (_.0 (_.1 _.2 _.3 _.4 _.5 (_.0 . _.6) . _.7) (_.0 . _.6))
    (_.0 (_.1 _.2 _.3 _.4 _.5 _.6 (_.0 . _.7) . _.8) (_.0 . _.7))
    (_.0 (_.1 _.2 _.3 _.4 _.5 _.6 _.7 (_.0 . _.8) . _.9) (_.0 . _.8))
    (_.0 (_.1 _.2 _.3 _.4 _.5 _.6 _.7 _.8 (_.0 . _.9) . _.10) (_.0 . _.9))
    (_.0 (_.1 _.2 _.3 _.4 _.5 _.6 _.7 _.8 _.9 (_.0 . _.10) . _.11) (_.0 . _.10)))
  '((_.0
     ((_.0 . _.1) . _.2)
     (_.0 . _.1))
    (_.0
     ((_.1 . _.2) (_.0 . _.3) . _.4)
     (_.0 . _.3))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.0 . _.5) . _.6)
     (_.0 . _.5))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.0 . _.7) . _.8)
     (_.0 . _.7))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.0 . _.9) . _.10)
     (_.0 . _.9))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.9 . _.10) (_.0 . _.11) . _.12)
     (_.0 . _.11))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8)
      (_.9 . _.10) (_.11 . _.12) (_.0 . _.13) . _.14)
     (_.0 . _.13))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.9 . _.10) (_.11 . _.12) (_.13 . _.14) (_.0 . _.15) . _.16)
     (_.0 . _.15))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.9 . _.10) (_.11 . _.12) (_.13 . _.14) (_.15 . _.16) (_.0 . _.17) . _.18)
     (_.0 . _.17))
    (_.0
     ((_.1 . _.2) (_.3 . _.4) (_.5 . _.6) (_.7 . _.8) (_.9 . _.10) (_.11 . _.12) (_.13 . _.14) (_.15 . _.16) (_.17 . _.18) (_.0 . _.19) . _.20)
     (_.0 . _.19))))