Bodil Stokke — Mukanren : Running the little things backwards

Bodil introduces uKamren: a simplified version of miniKanren. uKanren is an example of relational programming: using relations rather than using action or functions. The basic operations are:

2016-05-13 13.54.01

 

Now, Bodil is going to build a uKanren in a language called Pure. Pure is a term rewriting language, which is 1) nice, as there are no types and everything is easy but also 2) annoying as almost all things compile so you hardly ever get error messages.

We are going to use {} around logic variables, so:

var c = {c};

This really means a matrix, but probably we are not going to use matrices. Now, we want to get the value of a logic variable. For that we make a function walk that takes a key and a state (a mapping between logic variables and their values):

walk key state = if isvar key && member state key
                 then walk (state ! key) state
                 else key

Now, let’s make some relations! The first one is two variables that should be equal to each other. Unity is either going to return a new state or nil if the values cannot be made equal. The first option is added because we can call unify again with a nil state, resulting in nil again. Pattern matching works as in Haskell and F#: a _ matches everything.

unify _ _ nil = nil 

unify left right state = 
case (walk left state, walk right state) of 
   (l, r) = state if (isvar l) and (isvasr r) && (l == r); //the inputs are similar and (the same) variable
  
   (l, r) = update state l r if isvar l; 
   (l, r) = update state r l if isvar r;

   (l::ls, r::rs) = unify ls rs (unify l r state); //basically map the unify over the list

   (l, r) = state if l == r; //the inputs are similar and normal

   end;

And then, a real relationship operator:

infixl (==) ?==;
l ?== r = \(s,c) -> case unify l r s of //we try unification
     nil = nzero;
     state = unit (state, c)
end;

We now have to call this with the empty state all the time which is slightly annoying, so we add:

callgoal = goal emptystate;

Introducing variables goes as follows:

fresh f = \(s,c) -> (f var c)) (s, c + 1));

We no do not have to keep track of variables ourselves, when we introduce one, we just have the counter go up. 123

nplus [] stream2 = stream2 ;
nplus (head : tail) stream2 = head : nplus (tail stream2);
bind [] goal = nzero; <- monadic bind
bind (head : tail) goal = nplus (goal head) (bind tail goal));

Now, logical or is:

infixl (||) ?||;
goal1 ?|| goal2 \(s,c) -> nplus (goal1 (s,c)) (goal2) (s,c));

And, logical and is:

infixl (&&) ?||;
goal1 ?&&  goal2 \(s,c) -> bind (goal1 (s,c)) goal2);

This works! We can call callgoal on q = 6 or q = 5:

callgoal (callfresh (\q -> q ?== 5 ?|| q ?== 6));

and we get a matting with two options (I am too lazy to type it, it is long)

Similary,

callgoal (callfresh (\q -> q ?== 5  ?&& q ?== 6));

results in []

The highlight of course will be ….. appendo!!

appendo l r out =
       (l ?== [] ?&& r ? == out) //if  l = [] then r must be the output
       ?|| (fresh [head, tail, res] in 

           (head : tail ?== l ?&& head:res ?== out ?&& appendo (tail r res)) ; //otherwise, we want to match r with the tail of the result

Supercool stuff, although there was a bit too much content for the talk, and then end was a bit rushed.