Assignment 10: Introduction to Logic Programming
Show pagesource
Log In
(require “mk.rkt”)
(require “numbers.rkt”)
how miniKanren arrived at the answer.
assoc reverse stutter
For each problem, explain
(define assoc
(lambda (x ls)
(match-let* ((`(,a . ,d) ls)
(`(,aa . ,da) a))
(cond
((equal? aa x) a)
((not (equal? aa x)) (assoc x d))))))
(define reverse
(lambda (ls)
(cond
((equal? ‘() ls) ‘())
(else
(match-let* ((`(,a . ,d) ls)
(res (reverse d)))
: , dna , serudecorp tekcaR eht era ereH II traP
.secnetnes lareves eriuqer lliw noitanalpxe lluf a ;noitanalpxe ruoy fo ssenetelpmoc dna ytilauq eht no dedarg eb lliw uoY
.uoy ot dedivorp elfi tkr.01a eht ni dnuof snoitseuq eht ot srewsna eht etirW I traP
.noitacfiinu nosetonesehtro,gnimmargorpcigolno]fdp.polinim/113c/sessalc/www/l/ude.anaidni.sc.www//:ptth[ setonfo]fdp.porinim/113c/sessalc/www/l/ude.anaidni.sc.www//:ptth[ecneuqes ]fdp.poainim/113c/sessalc/www/l/ude.anaidni.sc.www//:ptth[ gniwollof eht ni detseretni eb osla thgim uoY
.]92%92%A2%tel-hctam_.92%tkr..hctamF2%tekcar_.bil82%82%_.mrof82%#tel-hctam=q ?lmth.hctam/ecnerefer/gro.gnal-tekcar.scod//:ptth[ *tel-hctam no noitatnemucod eht tlusnoc ot tnaw osla thgim uoY .lufesu eb ot nernaKinim ot smargorp tekcaR gnimrofsnart no seton gniwollof eht dnfi yam uoY
.resaetniarb a sulp ,strap owt fo desopmoc si tnemngissa sihT tnemngissA
.ssalc morf seton nwo ruoy dna remehcS denosaeR ehT tlusnoc dluohs uoy ,nernaKinim htiw flesruoy ezirailimaf rehtruf oT
.tkr.srebmun dna tkr.km evah uoy erus ekam ,tnemngissa eht trats uoy erofeB .nernaKinim gnisu gnimmargorp lanoitaler fo noissucsid ruo nugeb ev’ew keew sihT
seiranimilerP .msaisuhtne fo ssol on htiw rehtona ot eruliaf eno morf og ot ytiliba eht si sseccuS
setoN
assoc reverse stutter assoco reverseo stuttero
==
numbers.rkt
appendo
(append res `(,a)))))))
(define stutter
(lambda (ls)
(cond
((equal? ‘() ls) ‘())
(else
(match-let* ((`(,a . ,d) ls)
(res (stutter d)))
`(,a ,a . ,res))))))
> (require “a10.rkt”)
> (run 1 q (stuttero q ‘(1 1 2 2 3 3)))
((1 2 3))
> (run* q (stuttero q ‘(1 1 2 2 3 3)))
((1 2 3))
> (run 1 q (fresh (a b c d) (== q `(,a ,b ,c ,d)) (stuttero a `(1 ,b ,c 2 3 ,d))))
(((1 2 3) 1 2 3))
> (run 1 q (fresh (a b c d) (== q `(,a ,b ,c ,d)) (stuttero `(,b 1) `(,c . ,d))))
((_0 _1 _1 (_1 1 1)))
> (run 1 q (fresh (e f g) (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g)))
((_0 () (_0 _0)))
> (run 2 q (fresh (e f g) (== q `(,e ,f ,g)) (stuttero `(,e . ,f) g)))
((_0 () (_0 _0)) (_0 (_1) (_0 _0 _1 _1)))
> (run* q (assoco ‘x ‘() q))
()
> (run* q (assoco ‘x ‘((x . 5)) q))
((x . 5))
> (run* q (assoco ‘x ‘((y . 6) (x . 5)) q))
((x . 5))
> (run* q (assoco ‘x ‘((x . 6) (x . 5)) q))
((x . 6))
> (run* q (assoco ‘x ‘((x . 5)) ‘(x . 5)))
(_0)
> (run* q (assoco ‘x ‘((x . 6) (x . 5)) ‘(x . 6)))
(_0)
> (run* q (assoco ‘x ‘((x . 6) (x . 5)) ‘(x . 5)))
()
> (run* q (assoco q ‘((x . 6) (x . 5)) ‘(x . 5)))
()
> (run* q (assoco ‘x ‘((x . 6) . ,q) ‘(x . 6)))
(_0)
.gninnigeb eht ta emoc dluohs ot sllac ticilpmi ro ticilpxe elihw ,slaog fo ecneuqes a fo dne eht ta emoc dluohs sllac evisrucer ,lareneg nI .)stset eht ssap ot erofereht dna( noitanimret erusne ot snoitaler ruoy ni slaog eht fo emos egnarraer ot deen yam uoy taht rebmemeR
.liaf stset eht hguoht tcerroc si edoc ruoy taht elbissop si ti oS .redro tnereffid a ni stluser nruter ot maerts eht esuac yam redro tnereffid a ni slaog gnitnemelpmi sa ,stset eseht ssap ton thgim snoitaler ruoY .ediug a era stset woleb ehT
. fo noitatnemelpmi na sniatnoc ydaerla elfi ruoY .elfi tkr.01a ruoy fo dne eht ta meht tup dna ) , dna , ( snoitaler nernaKinim tnelaviuqe eht otni meht etalsnart dna , dna , , ekaT
.stset eht era ereH
numbers
lengtho
> (run 5 q (assoco ‘x q ‘(x . 5)))
(((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))
> (run 5 q (fresh (x y z)
(assoco x y z)
(== `(,x ,y ,z) q)))
((_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)))
> (run* q (reverseo ‘() q))
(())
> (run* q (reverseo ‘(a) q))
((a))
> (run* q (reverseo ‘(a b c d) q))
((d c b a))
> (run* q (fresh (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 (fresh (x) (reverseo `(a b c d) `(d . (,q . ,x)))))
(c)
> (run 10 q (fresh (x y) (reverseo x y) (== `(,x ,y) q)))
((() ())
((_0) (_0))
((_0 _1) (_1 _0))
((_0 _1 _2) (_2 _1 _0))
((_0 _1 _2 _3) (_3 _2 _1 _0))
((_0 _1 _2 _3 _4) (_4 _3 _2 _1 _0))
((_0 _1 _2 _3 _4 _5) (_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 _6 _7) (_7 _6 _5 _4 _3 _2 _1 _0))
((_0 _1 _2 _3 _4 _5 _6 _7 _8) (_8 _7 _6 _5 _4 _3 _2 _1 _0)))
> (require “a10.rkt”)
> (run 1 q (lengtho ‘() q))
(())
> (run 1 q (lengtho ‘(a b) q))
((0 1))
> (run 1 q (lengtho ‘(a b c) q))
((1 1))
> (run 1 q (lengtho ‘(a b c d e f g) q))
((1 1 1))
:stset emos era ereH .)srebmun fo noitatneserper lamron eht si siht ,srepleh dedivorp eht esu uoy fi( redro esrever ni rebmun yranib a sa tsil a fo htgnel eht htiw tuptuo sti setaicossa hcihw , etirW
.etius eht ni dedivorp era esehT .gnimmargorp lanoitaler ni sregetni eldnah ot yaw a secudortni remehcS denosaeR ehT fo 7 retpahC
resaetniarB
==
=/=
> (run 1 q (lengtho q (build-num 0)))
(())
> (run 1 q (lengtho q (build-num 5)))
((_0 _1 _2 _3 _4))
> (run 10 q (fresh (x y) (lengtho x y) (== `(,x ,y) q)))
((() ())
((_0) (1))
((_0 _1) (0 1))
((_0 _1 _2) (1 1))
((_0 _1 _2 _3) (0 0 1))
((_0 _1 _2 _3 _4) (1 0 1))
((_0 _1 _2 _3 _4 _5) (0 1 1))
((_0 _1 _2 _3 _4 _5 _6) (1 1 1))
((_0 _1 _2 _3 _4 _5 _6 _7) (0 0 0 1))
((_0 _1 _2 _3 _4 _5 _6 _7 _8) (1 0 0 1)))
cvm yb 02:01 13/30/0202 :defiidom tsaL ¡¤ txt.2a-pl
.krow ot hcihw morf egaugnal level-rehgih a ekil dluow uoy fi tkr.inim sorcam repleh fo elfi eht fo esu ekam nac uoY .noitatnemelpmi nernaKorcim eht ot dda tkr.qesid-rof-orcim elfi eht neviG .stniartsnoc rehto eht dedda t’nevah ew tuB .taht fo pot no nernaKinim na dliub ot woh bal ni was ew dna , htiw nernaKorcim a tnemelpmi ot woh was eW
tresseD tsuJ