Adderall: ≡ and consᵒ

My adventures at Hy seas continue and I’m still trying to chart the magical island of Adderall. This time I’m playing around with ≡ (also known as unifyo) and consᵒ (conso to buddies). The ≡ is used to unify two values (more or less saying these two things are same). For example:

(run* [q]
  (≡ 2 q))

This is equivalent of saying “lets say q and 2 are same, now give me all possible values of q”. The answer is of course 2. Not very interesting, but still, this is one of the building blocks.

We can make multiple unifies, like in:

(run 1 [q]
  (fresh (x y z) 
    (≡ x z) 
    (≡ 3 y)
    (≡ [x y z] q)))

fresh is used to introduce three variables x, y and z. After that, we specify that x and z have same value and y and 3 have same value. Last row specifies that [x y z] (a list made of them) and q have same value. Since we’re asking for all possible values of q, we get result as: [[<‘_.0’>, 3, <‘_.0’>]]. y equals three, while x and z can be any value, as long as they are the same value.

Of course, if we have contradicting specifications, results are not found:

(run* [q]
  (≡ 2 q))
  (≡ 3 q))

consᵒ is a bit more complex (but not by much). In lisp, cons is used to form a pair of values and have traditionally been used to make linked lists.

(run* [q]
  (consᵒ 2 3 q))

This is equivalent of saying: “pair made of 2 and 3 is same a q, find me q”. The result is [(2 . 3)]. This is where it gets interesting:

(run* [q]
  (consᵒ 2 q [2 3 4]))

This is same as “making a pair of 2 and q is same as [2 3 4], find me all possible values of q”. The result is [[3, 4]]. So if you take a pair of 3 and 4 and pair that with 2, you’ll get [2, 3, 4]. Pretty nifty?

We can even say:

(run* [q]
  (fresh (x y) 
    (consᵒ x y [2 3 4])
    (≡ [x y] q)))

Which is somewhat like “given we have x and y, and when they are paired together we get [2 3 4]. and [x y] has same value as q. find me all possible values of q”. The result for this is [[2, [3, 4]]] (essentially a list of 2 3 4).

I’m still playing around with very basic relations, but already I can see that there’s very promising possibilities with Adderall (and miniKanren in general). I can take bunch of values, perform an operation to them and get the result. Or, I can have an end goal, bunch of variables and an operation and Adderall tells me how to get there. Or, I can have everything and just have Adderall to check if the result is correct.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s