12 Assignment 12: Functionalized miniKanren
Preliminaries
This week we discussed how to implement miniKanren with only functions. Before you start the assignment, make sure you download mk-func.rkt.
(require "mk-func.rkt")
Assignment
In assignment 10, we miniKanrenized functions reverse and stutter. Your task here is to miniKanrenize these two functions again, using the functional version of miniKanren we showed in class. Here is an example:
(defrel (appendo l1 s2 o) (disj (conj (== '() l1) (== s2 o)) (call/fresh 'a (λ (a) (call/fresh 'd (λ (d) (call/fresh 'res (λ (res) (conj (== `(,a . ,d) l1) (== `(,a . ,res) o) (appendo d s2 res)))))))))) (run* (λ (q) (call/fresh 'r (λ (r) (call/fresh 's (λ (s) (conj (== `(,r ,s) q) (appendo r s '(a b c d e)))))))))
Here are the Racket procedures reverse and stutter:
(define reverse (lambda (ls) (cond ((equal? '() ls) '()) (else (match-let* ((`(,a . ,d) ls) (res (reverse d))) (append res `(,a))))))) (define stutter (lambda (ls) (cond ((equal? '() ls) '()) (else (match-let* ((`(,a . ,d) ls) (res (stutter d))) `(,a ,a . ,res))))))
Take reverse and stutter, and translate them into the equivalent miniKanren relations (reverseo and stuttero) and put them at the end of your a12.rkt file. Your can copy the definition of appendo from above.
The tests from assignment 10 have been adapted to use the new run and run*. For run, we provide a function simple-printer for you to print the results.
Here are the tests.
> (require "a12.rkt") > (run 1 (λ (q) (stuttero q '(1 1 2 2 3 3))) simple-print) '((1 2 3)) #<procedure> > (run* (λ (q) (stuttero q '(1 1 2 2 3 3)))) '((1 2 3)) > (run 1 (λ (q) (call/fresh 'a (λ (a) (call/fresh 'b (b) (call/fresh 'c (λ (c) (call/fresh 'd (λ (d) (conj (== q `(,a ,b ,c ,d)) (stuttero a `(1 ,b ,c 2 3 ,d))))))))))) simple-print) '(((1 2 3) 1 2 3)) #<procedure> > (run 1 (λ (q) (call/fresh 'a (λ (a) (call/fresh 'b (λ (b) (call/fresh 'c (λ (c) (call/fresh 'd (λ (d) (conj (== q `(,a ,b ,c ,d)) (stuttero `(,b 1) `(,c . ,d)))))))))))) simple-print) '((_0 _1 _1 (_1 1 1))) #<procedure> > (run 1 (λ (q) (call/fresh 'e (λ (e) (call/fresh 'f (λ (f) (call/fresh 'g (λ (g) (conj (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g))))))))) simple-print) '((_0 () (_0 _0))) #<procedure> > (run 2 (λ (q) (call/fresh 'e (λ (e) (call/fresh 'f (λ (f) (call/fresh 'g (λ (g) (conj (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g))))))))) simple-print) '((_0 () (_0 _0)) (_0 (_1) (_0 _0 _1 _1))) #<procedure> > (run* (λ (q) (reverseo '() q))) '(()) > (run* (λ (q) (reverseo '(a) q))) '((a)) > (run* (λ (q) (reverseo '(a b c d) q))) '((d c b a)) > (run* (λ (q) (call/fresh 'x (λ (x) (reverseo `(a b ,x c d) q))))) '((d c _0 b a)) > (run* (λ (x) (reverseo `(a b ,x d) '(d c b a)))) '(c) > (run* (λ (x) (reverseo `(a b c d) `(d . ,x)))) '((c b a)) > (run* (λ (q) (call/fresh 'x (λ (x) (reverseo '(a b c d) `(d ,q . ,x)))))) '(c) > (run 10 (λ (q) (call/fresh 'x (λ (x) (call/fresh 'y (λ (y) (conj (== `(,x ,y) q) (reverseo x y))))))) simple-print) '(((_0 _1 _2 _3 _4 _5 _6 _7 _8) (_8 _7 _6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5 _6 _7) (_7 _6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5 _6) (_6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5) (_5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4) (_4 _3 _2 _1 _0)) ((_0 _1 _2 _3) (_3 _2 _1 _0)) ((_0 _1 _2) (_2 _1 _0)) ((_0 _1) (_1 _0)) ((_0) (_0)) (() ())) #<procedure>
Brainteaser
In class, we learned an alternative implementation of run. Using the functions provided in mk-func.rkt, implement rung that behaves similarly to the run we’ve been using in the previous lectures. rung is a function taking three arguments: a natural number n, a symbol q, and a function f. The function f should take a logic variable and return a goal, similar to the function argument to call/fresh. rung should return a list of reified results. For example,
> (rung 1 'q (λ (q) (call/fresh 'a (λ (a) (call/fresh 'b (λ (b) (call/fresh 'c (λ (c) (call/fresh 'd (λ (d) (conj (== q `(,a ,b ,c ,d)) (stuttero a `(1 ,b ,c 2 3 ,d))))))))))))) '(((1 2 3) 1 2 3)) > (rung 1 'q (λ (q) (call/fresh 'a (λ (a) (call/fresh 'b (λ (b) (call/fresh 'c (λ (c) (call/fresh 'd (λ (d) (conj (== q `(,a ,b ,c ,d)) (stuttero `(,b 1) `(,c . ,d))))))))))))) '((_0 _1 _1 (_1 1 1))) > (rung 1 'q (λ (q) (call/fresh 'e (λ (e) (call/fresh 'f (λ (f) (call/fresh 'g (λ (g) (conj (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g)))))))))) '((_0 () (_0 _0))) > (rung 2 'q (λ (q) (call/fresh 'e (λ (e) (call/fresh 'f (λ (f) (call/fresh 'g (λ (g) (conj (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g)))))))))) '((_0 () (_0 _0)) (_0 (_1) (_0 _0 _1 _1))) > (rung 10 'q (λ (q) (call/fresh 'x (λ (x) (call/fresh 'y (λ (y) (conj (== `(,x ,y) q) (reverseo x y)))))))) '(((_0 _1 _2 _3 _4 _5 _6 _7 _8) (_8 _7 _6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5 _6 _7) (_7 _6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5 _6) (_6 _5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4 _5) (_5 _4 _3 _2 _1 _0)) ((_0 _1 _2 _3 _4) (_4 _3 _2 _1 _0)) ((_0 _1 _2 _3) (_3 _2 _1 _0)) ((_0 _1 _2) (_2 _1 _0)) ((_0 _1) (_1 _0)) ((_0) (_0)) (() ()))
Just Dessert
No dessert either ;)