# Tiny Rule Engine and Unification Woes

Work continues with tiny rule engine and I have encountered rather interesting design decision relating to unification, namely uniqueness of values.

Remember following example?

```=> (rule tre (?x is parent of ?y)
...  (rule tre (?x is parent of ?z)
...    (assert! tre (?y is sibling of ?z))))

=> (assert! tre (Alice is parent of Bob))
=> (assert! tre (Alice is parent of Charlie))
```

If ?y and ?z aren’t forced to be unique, we end up into a situation where Bob is sibling of both Bob and Charlie. Which clearly doesn’t make sense at all. When I first encountered this, I decided to force values be unique and had a feeling that I had introduced a subtle bug.

Fast forward to next example that I came up while playing around with 8 queens puzzle:

```=> (rule tre (queen ?x is placed on row ?r)
...  (rule tre (queen ?y is placed on row ?r)
...    (assert! (queen ?x can take queen ?y))))

=> (assert! tre (queen 1 is placed on row 2))
=> (assert! tre (queen 2 is placed on row 2))
```

Here rule should trigger, as both queen 1 and 2 are both on row 2. But because this would require both ?y and ?r have the same value, it doesn’t trigger. And if I undo the fix that forces values to be unique, we end in situation where queen 1 can take queen 1. Which again doesn’t make any sense at all.

After some tinkering and experimenting, I came up with a solution, where values can be marked being unique and thus have to have different values for unification to succeed:

```=> (rule tre (?x is parent of ?y)
...  (rule tre (?x is parent of ?z)
...    (unique ?y ?z)
...    (assert! tre (?y is sibling of ?z))))
```

Behind the hood this works in a way that each rule has a list of tuples. Each tuple has symbols that are required to be unique in respect to each other. This list is then carried through the system all the way up to the unification, where it can be checked. If unified symbol isn’t in the list, no further checks are needed. If it’s in the list, then value of each symbol that is required to be unique is checked. If values are different than the value that is being unified, unification succeeds.