(define evalo
(lambda (expr env val)
(conde
[(numbero expr) (== expr val)]
[(== #f expr) (== expr val)]
[(== #t expr) (== expr val)]
[(fresh (datum)
(== `(quote ,datum) expr)
(not-in-envo 'quote env)
(absento 'closure datum)
(== datum val))]
[(fresh (head-e tail-e head-v tail-v)
(== `(cons ,head-e ,tail-e) expr)
(== `(,head-v . ,tail-v) val)
(not-in-envo 'cons env)
(evalo head-e env head-v)
(evalo tail-e env tail-v))]
[(fresh (e tail)
(== `(car ,e) expr)
(not-in-envo 'car env)
(evalo e env `(,val . ,tail)))]
[(fresh (e head)
(== `(cdr ,e) expr)
(not-in-envo 'cdr env)
(evalo e env `(,head . ,val)))]
[(symbolo expr)
(lookupo expr env val)]
[(fresh (x body)
(== `(lambda (,x) ,body) expr)
(== `(closure ,x ,body ,env) val)
(not-in-envo 'lambda env))]
[(fresh (e1 e2 x body env^ arg)
(== `(,e1 ,e2) expr)
(evalo e1 env
`(closure ,x ,body ,env^))
(evalo e2 env arg)
(evalo body
`((,x . ,arg) . ,env^) val))])))
(define lookupo
(lambda (x env val)
(fresh (y v rest)
(== `((,y . ,v) . ,rest) env)
(conde
[(== x y) (== v val)]
[(=/= x y)
(lookupo x rest val)]))))
(define not-in-envo
(lambda (x env)
(conde
[(== '() env)]
[(fresh (y v rest)
(== `((,y . ,v) . ,rest) env)
(=/= x y)
(not-in-envo x rest))])))
(define eval-expr
(lambda (expr env)
(match expr
[(? number?) expr]
[(? string?) expr]
['null '()]
[#f #f]
[#t #t]
[`(quote ,datum) datum]
[`(null? ,e) (null? (eval-expr e env))]
[`(not ,e) (not (eval-expr e env))]
[`(* ,e1 ,e2) (* (eval-expr e1 env) (eval-expr e2 env))]
[`(sub1 ,e) (sub1 (eval-expr e env))]
[`(zero? ,e) (zero? (eval-expr e env))]
[`(if ,e1 ,e2 ,e3) (if (eval-expr e1 env)
(eval-expr e2 env)
(eval-expr e3 env))]
[(? symbol?) (lookup expr env)] ; var
[`(lambda (,x) ,body)
`(closure ,x ,body ,env)]
[`(,e1 ,e2)
(let ((proc (eval-expr e1 env))
(arg (eval-expr e2 env)))
(match proc
[`(closure ,x ,body ,env^)
(eval-expr body `((,x . ,arg) . ,env^))]))])))
(define lookup
(lambda (x env)
(match env
['() (error "unbound variable")]
[`((,y . ,v) . ,rest)
(if (equal? x y)
v
(lookup x rest))])))
(define Z
(lambda (f)
((lambda (x) (f (lambda (n) ((x x) n))))
(lambda (x) (f (lambda (n) ((x x) n)))))))
(eval-expr
'(((lambda (f)
((lambda (x) (f (lambda (n) ((x x) n))))
(lambda (x) (f (lambda (n) ((x x) n))))))
(lambda (!)
(lambda (n)
(if (zero? n)
1
(* (! (sub1 n)) n)))))
5)
'())
(define eval-exp
(lambda (expr env)
(match expr
[(? symbol?) (env expr)]
[`(lambda (,x) ,body)
(lambda (arg)
(eval-exp body (lambda (y)
(if (equal? x y)
arg
(env y)))))]
[`(,e1 ,e2)
((eval-exp e1 env) (eval-exp e2 env))])))
(eval-exp '((lambda (x) x) (lambda (y) y)) (lambda (y) (error "unbound variable")))
#f and #t)
numbero)
'())
sub1
zero?
*
if
null?
cons (hint: you will want to introduce a pair type, which is a tagged list of the types of the car and the cdr of the pair)
car
cdr
(f f) or (lambda (x) (x x)). We therefore cannot typecheck any functions that might go into an inifinite loop, or functions that can handle arbitrarily large numbers or lists. To avoid this problem we will introduce into our language a fix-point operator, fix.
Please add the following definition of fix to your type inferencer:
(define !-fixo
(lambda (gamma expr type)
(fresh (rand)
(== `(fix ,rand) expr)
(!- gamma rand `(,type -> ,type)))))
fix to your type inferencer, please use your !-o relation to typecheck these expressions, which calculate factorial and list concatenation:
((fix (lambda (!)
(lambda (n)
(if (zero? n)
1
(* (! (sub1 n)) n)))))
5)
(((fix (lambda (append)
(lambda (l)
(lambda (s)
(if (null? l)
s
(cons (car l) ((append (cdr l)) s)))))))
'(a b c))
'(d e))
If you want to evaluate these expressions in Racket (rather than typechecking the expressions in miniKanren), you can use this definition of fix:
(define fix
(lambda (f)
(letrec ([g (lambda (x) ((f g) x))])
g)))
(run* (q) (reverseo '(a b c) q)) => '((c b a))Define a relation palindromeo that succeeds when its argument is a list that is a palindrome (a list whose elements are the same forward and backwards):
(run* (q) (palindromeo '())) => '(_.0) (run* (q) (palindromeo '(a b c))) => '() (run* (q) (palindromeo '(a b c b a))) => '(_.0)
(cons 3 4)
(car (cons 3 4))
(cdr (cons 3 4))
(list 3 4)
(car (list 3 4))
(cdr (list 3 4))
'(3 4)
(car '(3 4))
(cdr '(3 4))
'(3 . 4)
(car '(3 . 4))
(cdr '(3 . 4))
`(3 4)
(car `(3 4))
(cdr `(3 4))
`(3 (+ 4 5) 6)
`(3 ,(+ 4 5) 6)
(let ((x (+ 2 3)))
`(3 ,x 4))
(let ((x (+ 2 3)))
`(3 x 4))
(cons 4 '())
(cons 3 (cons 4 5))
(cons 3 (cons 4 '()))
(cons (cons 3 4) (cons 5 '()))
(cons (cons 3 '()) (cons 5 '()))
For students who want more practice with Racket/Scheme, please define as many of the following recursive functions as you need to feel comfortable with Racket:
append that takes two lists, ls1 and ls2, and appends ls2 to ls1.
(append '(a b c) '(1 2 3)) => (a b c 1 2 3)
fact that takes a single integer and computes the factorial of that number. The factorial of a number is computed by multiplying it by every positive integer less than it.
(fact 5) => 120
increment that takes a list of numbers and returns a new list whose elements are equal to the elements of the original list incremented by one.
(increment '(1 2 3 4 5)) => '(2 3 4 5 6)
insertl that takes as input two symbols and a list, and inserts the second symbol before each occurrence in the list of the first symbol.
(insertl 'x 'y '(x z z x y x)) => '(y x z z y x y y x)
last-eq? that takes a symbol and a non-empty list and returns the result of the comparison between the symbol and the last element of that list.
(remove 'x '(z x y x y z)) => '(z y y z)
count-between that takes two integers m and n where m < n and returns a list counting up from m to n, including m but not including n.
(filter even? '(1 2 3 4 5 6)) => '(2 4 6)
zip that takes two lists of equal length and forms a new list, each element of which is the two-element list formed by combining the corresponding elements of the two input lists.
(zip '(1 2 3) '(a b c)) => '((1 a) (2 b) (3 c))
function sum-to that takes an integer and sums the integers from one to the input number.
(sum-to 4) => 10
map that takes a procedure p of one argument and a list ls, and returns a new list containing the results of applying p to the elements of ls. Do not use Scheme's built-in map in your definition.
(map add1 '(1 2 3 4)) => (2 3 4 5)
reverse that takes a list and returns the reverse of that list.
(reverse '(a 3 x)) => (x 3 a)
count-symbols that takes a (potentially deep) list of symbols, and returns the number of symbols in the list.
(count-symbols '(a b c)) => 3
(count-symbols '((a ((b)) ((c) d c)))) => 5
fib that takes a single integer n as input and computes the nth number, starting from zero, in the Fibonacci sequence (0, 1, 1, 2, 3, 5, 8, 13, 21, ...). Each number in the sequence is computed by adding the two previous numbers.
(fib 0) => 0
(fib 1) => 1
(fib 7) => 13
even-layers? and odd-layers? that take an onion of the form (((...))). even-layers? should return #t if the onion has an even number of layers and #f otherwise, and odd-layers? should return #t if the input has odd number of layers and #f otherwise. The onion () has zero layers.
(even-layers? '()) => #t
(even-layers? '(())) => #f
(odd-layers? '(((((((((((())))))))))))) => #t
(even-layers? '(((((((((((((((((((((((((((((((((((((((((((((((((())))))))))))))))))))))))))))))))))))))))))))))))))) => #f
Some of the problems use definitions for alwayso and nevero.
(define anyo
(lambda (g)
(conde
[g]
[(anyo g)])))
(define alwayso (anyo succeed))
(define nevero (anyo fail))
succeed and fail are already defined in miniKanren; succeed is equivalent to
(== #f #f) while fail is equivalent to
(== #f #t).
Make sure to verify your answers by running the programs in miniKanren. You will need to load
mk.rkt and enter the definitions of anyo, alwayso, and nevero above before evaluating the run expressions.
Some of these run expressions may result in infinite loops--in this case, please press the Stop button in DrRacket.
(run* (q) (== 5 q))
(run* (q) (== 5 5))
(run* (q) (== 5 6))
(run* (q) (== '(a b c) '(a b c)))
(run* (q) (== (list 'a 'b 'c) (list 'a 'b 'c)))
(run* (q) (== (list 'a 'b 'c) (list 'a q 'c)))
(run* (q) (== (list 'a 'b 'c) (list 'a q q)))
(run* (q)
(fresh (x)
(== 5 x)
(== x q)))
(run* (q)
(fresh (x)
(== 5 x)))
(run* (q)
(conde
[(== 5 q)]
[(== q 5)]))
(run* (q)
(conde
[(== 5 5)]
[(== q q)]))
(run* (q)
(conde
[(conde
[(== q 5)]
[(== q 6)])]
[(== q 7)]))
(run* (q) succeed)
(run* (q) fail)
(run 2 (q)
(== 5 q)
(conde
[(conde
[(== 5 q) (== 6 q)]) (== 5 q)]
[(== q 5)]))
(run* (q)
(fresh (x y)
(== `(,x ,y) q)
(conde
[fail succeed]
[(conde
[(== 5 x) (== y x)]
[(== `(,x) y)]
[(== x y)])]
[succeed])))
alwayso, nevero, and infinite loops)(run 1 (q) alwayso)
(run 1 (q) nevero)
(run 5 (q) alwayso)
(run 5 (q) nevero)
(run 1 (q) alwayso fail)
(run 1 (q) fail alwayso)
(run 2 (q)
(conde
[succeed]
[nevero]))
(run* (q)
(fresh (a b c d)
(== `(,a ,b) `(,c (,a . ,d)))
(== `(,b ,c) `((,a) ,d))
(== `(,a ,b ,c ,d) q)))
== 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))])))
(define multi-rember
(lambda (e l)
(cond
[(null? l) '()]
[(equal? (car l) e) (multi-rember e (cdr l))]
[else (cons (car l) (multi-rember e (cdr l)))])))
Here are a few test cases to help ensure your definitions are correct:
(run* (q)
(one-itemo 'a '(b c d) q))
=>
'(((a . b) (a . c) (a . d)))
(run* (q)
(one-itemo q '(b c d) '((a . b) (a . c) (a . d))))
=>
'(a)
(run* (q)
(one-itemo 'a q '((a . b) (a . c) (a . d))))
=>
'((b c d))
(run* (q)
(one-itemo 'a '(b c d) `((a . b) . ,q)))
=>
'(((a . c) (a . d)))
(run* (q)
(one-itemo 'a '(b c d) '((a . b) (a . c) (a . d))))
=>
'(_.0)
(run* (q)
(one-itemo 'a `(b ,q d) '((a . b) (a . c) (a . d))))
=>
'(c)
(run* (q)
(fresh (x y)
(one-itemo x y '((a . b) (a . c) (a . d)))
(== `(,x ,y) q)))
=>
'((a (b c d)))
(run 6 (q)
(fresh (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))))
(run* (q)
(assqo 'x '() q))
=>
'()
(run* (q)
(assqo 'x '((x . 5)) q))
=>
'((x . 5))
(run* (q)
(assqo 'x '((y . 6) (x . 5)) q))
=>
'((x . 5))
(run* (q)
(assqo 'x '((x . 6) (x . 5)) q))
=>
'((x . 6) (x . 5))
(run* (q)
(assqo 'x '((x . 5)) '(x . 5)))
=>
'(_.0)
(run* (q)
(assqo 'x '((x . 6) (x . 5)) '(x . 6)))
=>
'(_.0)
(run* (q)
(assqo 'x '((x . 6) (x . 5)) '(x . 5)))
=>
'(_.0)
(run* (q)
(assqo q '((x . 6) (x . 5)) '(x . 5)))
=>
'(x)
(run* (q)
(assqo 'x '((x . 6) . ,q) '(x . 6)))
=>
'(_.0)
(run* (q)
(multi-rembero 'x '() q))
=>
'(())
(run* (q)
(multi-rembero 'x '(y x z x) q))
=>
'((y z))
(run* (q)
(multi-rembero 'x '(y w z v) q))
=>
'((y w z v))
(run* (q)
(multi-rembero q '(y x z x) '(y z)))
=>
'(x)