lookupo

I watched the minikanren uncourse hangout 4 from Will Byrd, video here. He is teaching people about the minikanren programming language, which I originally learned about from this book..

</img>

It’s a logic programming language like Prolog, but with some more modern ideas that make it very interesting. In particular you introduce fresh logic variables explicitly (the lack of this caused me a lot of bugs in prolog) and it has a fair search, unlike prolog.

In this episode he started by writing a lambda calculus interpreter in scheme (and every aspect of it was explained very very clearly! it would be a great thing to watch if you want to learn about interpreting lambda calculus). After that he transformed it into a kanren program.

One particularly interesting part was changing the lookup function into the lookupo relation:

(define lookup (lambda (x env) (pmatch env [((,y . ,v) . ,envˆ) (guard (eq? x y)) v] [((,y . ,_) . ,envˆ) (lookup x envˆ)])))

The lookup function is used to implement lexical scope, environments are lists of pairs and you just cons a new association on to shadow a variable.

This is something I had trouble with before when programming Prolog as well as in kanren. The naive way to translate it (which is wrong!) is this:

(define lookupo (lambda (x env out) (conde [(fresh (v env^) (== env `((,x . ,v) . ,envˆ)) (== v out))] [(fresh (y _ env^) (== env `((,y . ,_) . ,envˆ)) (lookup x envˆ out))])))

the problem with this is that it does not work correctly for implementing lexical scoping because it will give you all lookups. Shadowing in lexical scope requires that you only get the first lookup.. so what went wrong?

Will Byrd said (around 1:40:55) that in the definition of lookup there is an implicit ordering.

So when translating to kanren my plan is this: Imagine a demon would shuffle your pattern match clauses, what extra checks would you need to make the code still work? The answer in this case is (guard (not (eq? x y))). So to fix lookup you need to add a disequality constraint (=/= x y).

This is related to the idea of Guarded Command Language from Dijkstra.

… p.s.

I couldn’t resist but try running the interpreter backwards:

> (run 10 (q) (eval-expo q '() '(closure w w ()))) ((lambda (w) w) ((lambda (_.0) _.0) (lambda (w) w)) ((lambda (_.0) (_.0 _.0)) (lambda (w) w)) ((lambda (_.0) _.0) ((lambda (_.1) _.1) (lambda (w) w))) ((lambda (_.0) ((lambda (_.1) _.1) _.0)) (lambda (w) w)) (((lambda (_.0) _.0) (lambda (_.1) _.1)) (lambda (w) w)) ((lambda (_.0) (_.0 _.0)) ((lambda (_.1) _.1) (lambda (w) w))) ((lambda (_.0) ((lambda (_.1) _.0) _.0)) (lambda (w) w)) ((lambda (_.0) (_.0 _.0)) ((lambda (_.1) (lambda (_.2) _.1)) (lambda (w) w))) ((lambda (_.0) ((lambda (_.1) _.0) (lambda (_.2) _.3))) (lambda (w) w))) it found a whole bunch of programs that evaluate to the result I asked for!

fairness

I defined a relation to generate peano numbers in order:

(define peano (lambda (n) (conde [(== n `z)] [(fresh (m) (== n `(s ,m)) (peano m))])))

This lets you see how fair kanren is:

> (for-each print (run 15 (q) (fresh (x y) (peano x) (peano y) (== q `(,x ,y))))) (z z) (z (s z)) ((s z) z) (z (s (s z))) (z (s (s (s z)))) ((s z) (s z)) ((s (s z)) z) (z (s (s (s (s z))))) (z (s (s (s (s (s z)))))) ((s z) (s (s z))) (z (s (s (s (s (s (s z))))))) (z (s (s (s (s (s (s (s z)))))))) ((s z) (s (s (s z)))) ((s (s z)) (s z)) (z (s (s (s (s (s (s (s (s z)))))))))

the same query in prolog would only generate pairs with the first component always zero.