minikanren notes.txt

four primitives: run*, ==, conde, fresh

(run* (q)
  (== q #t))

; for what values of q is q equal to true?

answer: q must also be #t, so
'(#t)    ; answer comes back in a list

(run* (q)
  (== q #t)
  (== q #f))

yields '(), since no q can be both true and false

(run* (q)
  (== #t q))

same as first example, order irrelevant

(run* (q)
  (== #f q)
  (== #t q))

again '(), order irrelevant in pure relational style.
Order never changes meaning of program

fresh introduces a new logic variable

logic vars can get linked:

(run* (q)
  (fresh (x)
    (== q x)
    (== x 1)))

yields '(1)

logic vars are assign once. You can only unify with one value

(run* (q)
  (fresh (x)
    (== q x)
    (== x 1)
    (== q 2)))  ; yields '()

but this works:

(run* (q)
  (fresh (x)
    (== q x)
    (== x 1)
    (== q 1)))  ; yields '(1)

fresh constructs a lexical scope, similar to let

unifying with a list:

> (run* (q)
    (fresh (x y)
      (== `(,x 2) `(1 ,y))
      (== q `(,x ,y))))
'((1 2))

` (backtick) is quasiquote operator - lets you use comma to splice in values
instead of '(x y) which would be literally '(x y)

Now let's do logical disjunction, or

> (run* (q)
    (conde
     [(== q 'tea)]
     [(== q 'coffee)]))
'(tea coffee)

conde is logical conjunction

it's OR-ing a series of ANDs

> (run* (q)
    (conde
     [(== q 'tea) (== q 'foo)]
     [(== q 'coffee)]))
'(coffee)

in this case q can't be tea AND foo, so that fails
but coffee still matches

> (run* (q)
    (fresh (x y)
      (conde
       [(== x 'tea) (== y 'biscuit)]
       [(== x 'coffee) (== y 'cake)])
      (== q `(,x ,y))))
'((tea biscuit) (coffee cake))

another way, composing relations, the same way we might compose functions:

(define menu
  (lambda (x y)
    (conde
     [(== x 'tea) (== y 'biscuit)]
     [(== x 'coffee) (== y 'cake)])))

> (run* (q)
    (fresh (x y)
      (menu x y)
      (== q `(,x ,y))))
'((tea biscuit) (coffee cake))

going further:

(define conso
  (lambda (x y o)  ; have to receive output as an argument
    (== `(,x . ,y) o)))

then:

> (run* (q)
    (conso 'a '(b c) q))
'((a b c))

also:

> (run* (q)
    (conso q '(b c) '(a b c)))
'(a)

> (run* (q)
    (conso 'a q '(a b c)))
'((b c))

so conso can do more than what cons can do. Inference based on parameters
Can go backwards from data structures to how they were constructed

> (run* (q)
    (fresh (x y)
      (conso x y q)))
'((_.0 . _.1))

nothing has a value, it's telling us that q can be any list.

> (run* (q)
    (fresh (x)
      (conso x '(b c) q)
      (== q '(dog b c))))
'((dog b c))
> (run* (q)
    (fresh (x)
      (conso x '(b c) q)
      (== q '(cat b c))))
'((cat b c))

here no value for head of list, but rest must be '(b c)

(define child
  (lambda (x y)
    (conde
     [(== 'Mary x) (== 'Richard y)]
     [(== 'Richard x) (== 'Leslie y)])))

> (run* (q)
    (child 'Mary q))
'(Richard)
> (run* (q)
    (child 'Richard q))
'(Leslie)

(define grandchild
  (lambda (x y)
    (fresh (z)
      (child x z)
      (child z y))))

> (run* (q)
    (grandchild 'Mary q))
'(Leslie)

primitive logical relation (child) can support more elaborate ones
(grandchild)

> (run* (q)
    (fresh (x y)
      (grandchild x y)
      (== q `(,x ,y))))
'((Mary Leslie))

; this returns every pair of people who satisfy the grandchild relation


(define child
  (lambda (x y)
    (conde
     [(== 'Mary x) (== 'Richard y)]
     [(== 'Richard x) (== 'Leslie y)]
     [(== 'Emma x) (== 'Helen y)]
     [(== 'Sophie x) (== 'Helen y)])))

(define male
  (lambda (x)
    (conde
     [(== 'Leslie x)]
     [(== 'Richard x)])))

(define female
  (lambda (x)
    (conde
     [(== 'Emma x)]
     [(== 'Sophie x)]
     [(== 'Mary x)]
     [(== 'Helen x)])))

> (run* (q)
    (fresh (y)
      (son q y)))
'(Richard)
> (run* (q)
    (fresh (x y)
      (son x y)
      (== `(,x ,y) q)))
'((Richard Leslie))

; define daughter similarly to son


more generally working with data structures:


(define right  ; determine if y is to the right of x in a list
  (lambda (x y l)
    (conde ; the e is for every; even if we succeed every clause is tried
     [(fresh (z)
        (== `(,x ,y . ,z) l))]
     [(fresh (a z)
        (== `(,a . ,z) l)
        (right x y z))])))

(define next
  (lambda (x y l)
    (conde
     [(right x y l)]
     [(right y x l)])))


> (run 5 (q)
    (fresh (x y l)
      (== q `(,x ,y ,l))
      (right x y l)))
'((_.0 _.1 (_.0 _.1 . _.2))
  (_.0 _.1 (_.2 _.0 _.1 . _.3))
  (_.0 _.1 (_.2 _.3 _.0 _.1 . _.4))
  (_.0 _.1 (_.2 _.3 _.4 _.0 _.1 . _.5))
  (_.0 _.1 (_.2 _.3 _.4 _.5 _.0 _.1 . _.6)))

"run 5" takes first 5 results
"run*" in above situation would never terminate
note that in above answers, _.1 is always to the right of _.0

The zebra problem took Peter Norvig 17sec in 1993
Now 8ms on an old MacBook Air in core.logic

Changing the order of constraints can affect pruning efficiency




going into the implementation... lambdag@ and lambdaf@ are just syntactic sugar

probing walk:

> (let ((y (var 'y))
        (x (var 'x)))
    (walk y `(,(cons y x) ,(cons x 1))))
1


when the input to walk is not a var, there's nothing to substitute in the
substitution map:

> (let ((y (var 'y))
        (x (var 'x)))
    (walk 5 `(,(cons y x) ,(cons x 1))))
5
> (let ((y (var 'y))
        (x (var 'x)))
    (walk 'foo `(,(cons y x) ,(cons x 1))))
'foo


(define ext-s
  (lambda (x v s)
    (cons `(,x . ,v) s)))

ext-s simply takes a logic var (x), some value (v), and adds it to the front
of the substitution (s)

e.g.
> (ext-s (var 'x) 1 empty-s)
'((#(x) . 1))


unify - lambda (u v s)

example:
> (unify `(,(var 'x) 1) `(2 ,(var 'y)) empty-s)
'((#(y) . 1) (#(x) . 2))

just descends both lists, extending the substitution based on what's
in the list

takes x and 2 off the front, unifies x with 2, extending substitution
then takes cdrs, 2 and var y, and extends subst with that

same but lift off x:
> (let ((x (var 'x)))
    (unify `(,x 1) `(2 ,(var 'y)) empty-s))
'((#(y) . 1) (#(x) . 2))

now we can bind x to something else:
> (let ((x (var 'x)))
    (unify `(,x 1) `(2 ,(var 'y)) `((,x . 5))))
#f

doesn't work because it looks up x as 5
the moment we see it won't work, we bomb out
we fall through all the cases in unify:
  not eq?
  u not a var
  v not a var
  cars don't unify
  not equal?

equal? is a deep compare, whereas eq? is comparing memory locations
There's some specific case where you want to catch something with that

(equal? '(1 2) '(1 2))
=> #t

(eq? '(1 2) '(1 2))
=> #f

ext-s-check does what ext-s does, but makes sure the term doesn't exist
inside of itself first - preventing self-reference


walk* is recursive case - takes a term, if there are any logic vars it will
replace all of them

> (let ((x (var 'x))
        (y (var 'y))
        (z (var 'z)))
    (walk x `((,x . ,(list y z)))))
'(#(y) #(z))

this is ok because y and z aren't bound to anything, BUT:

> (let ((x (var 'x))
        (y (var 'y))
        (z (var 'z)))
    (walk x `((,x . ,(list y z)) (,y . 1) (,z . 2))))
'(#(y) #(z))

we don't want this, we want actual values!!!

thus, walk star:

> (let ((x (var 'x))
        (y (var 'y))
        (z (var 'z)))
    (walk* x `((,x . ,(list y z)) (,y . 1) (,z . 2))))
'(1 2)

one thing though, we're not used to seeing this:

> (let ((x (var 'x))
        (y (var 'y))
        (z (var 'z)))
    (walk* x `((,x . ,(list y z)) (,y . 1))))
'(1 #(z))

we're used to seeing _.0 type stuff, reify-s does that.

> (let ((x (var 'x))
        (y (var 'y))
        (z (var 'z)))
    (reify x `((,x . ,(list y z)) (,y . 1))))
'(1 _.0)





THE HARD PART



The search part. Done in a monadic way.

A MiniKanren program produces a potentially infinite stream.
There may be infinitely many answers.
Obvious example: next, above, with no bound values
So clearly run* must potentially produce an infinite stream

Four possibilities inside that stream.
It's not actually just one stream.
The search is a tree, and each branch of the tree might itself be infinite
It's a bit like weaving. We have all these branches going down,
  we want to unify them into one thread of answers.

mzero means we do not succeed. It's the failed value.

Weird thing called inc. Will discuss later.

unit means we have something. We found a substitution that works.

choice is the stream, where we have multiple answers.
If we never use conde, we will only ever produce mzero if we succeed and
unit if we fail. Only conde allows choice to appear: we might have something,
or we might have something else. And when we add recursion, e.g. with next,
we can get infinite possibilities, all hiding behind thunks which may produce
more possibilities.

So the 4 possibilities are:

Nothing (mzero), Something (unit), some weird thing we don't discuss yet
(inc), or Many Somethings (choice).

Scheme doesn't really support datatypes so we have case-inf to deal with
the 4 possibilities.

(define-syntax case-inf
  (syntax-rules ()
    ((_ e (() e0) ((f^) e1) ((a^) e2) ((a f) e3))
     (let ((a-inf e))
       (cond
         ((not a-inf) e0)
         ((procedure? a-inf)  (let ((f^ a-inf)) e1))
         ((not (and (pair? a-inf)
                    (procedure? (cdr a-inf))))
          (let ((a^ a-inf)) e2))
         (else (let ((a (car a-inf)) (f (cdr a-inf))) 
                 e3)))))))

A choice always looks like this:

> (choice empty-s (lambda () empty-s))
'(() . #<procedure>)

It's a substitution form, cons'd onto a function that produces more
substitution forms - like a lazy stream.

You can go deep with recursion, choices with more choices, like:

> (choice (choice empty-s (lambda () empty-s)) (lambda () empty-s))
'((() . #<procedure>) . #<procedure>)




We need a scheduler to prevent a bad goal from taking all the computation
time.

e.g. define nevero, which never returns an answer, then:

(run* (q)
  (conde
   [(nevero)]
   [(== q #t)]))

will loop forever! BUT if you run 1:

(run 1 (q)
  (conde
   [(nevero)]
   [(== q #t)]))
=> '(#t)

If you get a function back, they count that as a "tick", switch to a diff
branch. Prolog can't do this. MiniKanren can, and Dan Friedman calls it a
"distributed trampoline" - if there is an answer, it will find it in finite
time, and that's a guarantee.

It's a tradeoff b/t depth-first and breadth-first, kinda like a diagonal.

Because we have to do thunking, if we get a function in 'take',
we simply force it, leaving n the same.

(define take
  ...
    ..
     ..
      ..
    (case-inf (f)
      ..
    ((f) (take n f))



The way == is defined is, it returns a goal which does a unification.

> ((== (var 'x) 1) empty-s)
'((#(x) . 1))

we usually don't write it that way, but we're dealing with functions
that return substitutions.

fresh, again, just expands into a function.
It does an inc - this weird thing.

The inc is a scheduling thing - it says we can stop here if we need to.


fresh is binding, like so:

 (fresh ()
   (== x 1)
   (== y 2))

is like:

 (bind (bind empty-s (== x 1))
       (== y 2))


this part of bind is a lazy map:

      ((a f) (mplus (g a) (lambdaf@ () (bind (f) g)))))))

we do some computation, but delay the rest


mplus is a filter. When we have failures, it filters them all out,
so we never see failures. When mplus gets a failure, it just invokes the
remainder — the tail.

If we get a function, some crazy scheduling: flips it:

(case-inf a-inf
  (() (f))  ; discard failures
  ((f^) (inc (mplus (f) f^)))  ; flip the order of the stream
  ((a) (choice a f))  ; converts unit directly into a choice
  ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))))))  ; basically mapcat

mapcat takes the things inside many lists, and concatenates them all together
so this is weaving the many streams into one stream
again, we flip the order of functions

what happens with nevero? because it's fresh, fresh expressions wrapped in a
thunk. So nevero returns a thunk, inc

We're inside of a conde, so it tries the other branch first, does a
unification. You only wanted one result? Ok, we're done.
So once we did "run 1", and got one answer, we stop. nevero keeps returning
thunks. This allows us to schedule nevero so it doesn't steal all the time.

In Clojure, DN thought, "Oh, I can do this with lazy streams!"
But they don't work, b/c when you ask for something they automatically force.
You don't want that. You just want to get the inc so you can schedule.
So what's nice about this design is, even if there's nothing ultimately,
it always pauses at the incs.





Now onto core.logic / cKanren, not in minikanren.

(run* [q]
  (fresh [x y z]
    (== x 1)
    (== y 2)
    (== z (+ x y))
    (== q [x y z])))

x and y are logic variables, so this won't work in minikanren.
They don't have a value at the point where you do == (unification).

You get ClassCastException, LVar cannot be converted to Number

Prolog does, and we used to do, project:

(run* [q]
  (fresh [x y z]
    (== x 1)
    (== y 2)
    (project [x y]
      (== z (+ x y)))
    (== q [x y z])))

=> ([1 2 3])

Problem, you can't reorder these. You won't have the right values bound.
This fails:

(run* [q]
  (fresh [x y z]
    (project [x y]
      (== z (+ x y)))
    (== x 1)
    (== y 2)
    (== q [x y z])))

same ClassCastException, they're not numbers yet.

You don't have much control over which way your clauses are computed,
so you can get to a situation where it looks like the numbers SHOULD be
bound, but they're not.

We now do stuff like this:

(run* [q]
  (fresh [x y z]
    (fd/in x y z (fd/interval 0 9))
    (== x 1)
    (== y 2)
    (fd/+ x y z)
    (== q [x y z])))

=> ([1 2 3])

can also efficiently produce all solutions:

(run* [q]
  (fresh [x y z]
    (fd/+ x y z)
    (== q [x y z])
    (fd/in x y z (fd/interval 0 9))))

produces all triples x, y, z such that x+y=z for all numbers on [0,9]

can add more conditions like
  (fd/< x y)

Sudoku is fun
t