Witch of Git - web/blog/blob - posts/2020/syntactic-unification.md

   1 ---
   2 title: "Syntactic Unification Is Easy!"
   3 date: 2020-02-19
   4 tags:
   5 - unification
   6 - logic programming
   7 - algorithms
   8 summary: "Last year I tried implementing syntactic unification and got completely stuck on the algorithms. Last week I read the MicroKanren paper and discovered that unification could be very simple. Let me show you how!"
   9 next: posts/2020/logic-programming
  10 ---
  11
  12 Syntactic unification is the process of trying to find an assignment of variables that makes two terms the same.
  13 For example, attempting to unify the terms in the equation `(X, Y) = (1, 2)` would give the substitution `{X: 1, Y: 2}`, but if we tried to unify `(X, X) = (1, 2)` it would fail since one variable can't be equal to two different values.
  14 Unification is used to implement two things I'm very interested in: type systems, and logic programming languages.
  15
  16 Earlier last year I tried implementing unification in order to make a toy Prolog, and I got completely stuck on the algorithms.
  17 I eventually puzzled throught it by reading lots of papers and articles, but I don't recall understanding it fully.
  18 You can take a look at [the equations that the Wikipedia article uses][wiki] to see what I was dealing with---it's certainly intimidating!
  19
  20 Cut to last week, I happened to read [the MicroKanren paper] (which is very readable) and discovered that unification could be very simple!
  21 Let me show you how!
  22
  23 [wiki]: https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm
  24 [the microkanren paper]: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
  25
  26 ### The Terms To Unify
  27
  28 We have to define what kinds of things we're going to unify.
  29 There are a few basic things we *need* to have.
  30
  31 - Variables, because otherwise unification is just equality comparison.
  32 - Terms with multiple subterms, because otherwise unification is just.
  33 - Other atomic "base" terms are good to have, because they let you write more interesting terms that are easily understandable.
  34
  35 I'm going to write my examples in Python, so the types I'm going to work with are:
  36
  37 - Variables: A `Var` class defined for this purpose.
  38 - Composite terms: Tuples and lists of terms.
  39 - Atomic terms: Any Python type that can be compared for equality.
  40
  41 The scheme example they demonstrate in the MicroKanren article uses variables, pairs, and arbitrary objects.
  42 The Rust version I wrote just has variables, pairs, and integers.
  43 Exactly what you want to work with is completely up to you: hopefully at the end of this, you'll be able to figure out how to do it for some custom type.
  44
  45 My `Var` type is very simple, with only one custom method to make the printing more compact:
  46
  47 ```python
  48 from dataclasses import dataclass
  49
  50 @dataclass(frozen=True)
  51 class Var:
  52     name: str
  53
  54     def __repr__(self):
  55         return self.name
  56 ```
  57
  58 And everything else is base Python types, so we're done with this part.
  59
  60 ### Unifying Terms
  61
  62 Let's work through unifying things.
  63 We want to unify two terms, and return a substitution that makes them equal, which I'll call the "environment."
  64 If they can't possibly be equal, we'll return `None`.
  65 Let's start out simple: two things can be unified if they're already equal.
  66
  67 ```python
  68 def unify(a, b):
  69     if a == b:
  70         return {}
  71     # ... other cases ...
  72     return None
  73 ```
  74
  75 The variable cases can also be solved very easily.
  76 Trying to unify a variable with another term, we can just substitute that for the variable.
  77 When unifying `x = 1`, we get back `{ x: 1 }`.
  78
  79 ```python
  80     if isinstance(a, Var):
  81         return {a: b}
  82     if isinstance(b, Var):
  83         return {b: a}
  84 ```
  85
  86 Finally, let's handle tuples.
  87 For this, we want to unify each individual component of the tuple.
  88 We want the union of each of these unifications, so we'll update the dictionary each time.
  89 We have to check if the sub-unification returned None and pass that along.
  90
  91 ```python
  92     if isinstance(a, tuple) and isinstance(b, tuple):
  93         if len(a) != len(b):
  94             return None
  95         env = {}
  96         for (ax, bx) in zip(a, b):
  97             res = unify(ax, bx)
  98             if res is None:
  99                 return None
 100             env.update(res)
 101         return env
 102 ```
 103
 104 Now you might see where this could go wrong, and we'll get to that in a moment with an example.
 105 Repeating that function all in one piece:
 106
 107 ```python
 108 def unify(a, b):
 109     if a == b:
 110         return {}
 111     if isinstance(a, Var):
 112         return {a: b}
 113     if isinstance(b, Var):
 114         return {b: a}
 115     if isinstance(a, tuple) and isinstance(b, tuple):
 116         if len(a) != len(b):
 117             return None
 118         env = {}
 119         for (ax, bx) in zip(a, b):
 120             res = unify(ax, bx)
 121             if res is None:
 122                 return None
 123             env.update(res)
 124         return env
 125     return None
 126 ```
 127
 128 Now we can unify stuff:
 129
 130 ```python
 131 >>> x, y = Var("x"), Var("y")
 132 >>> unify(1, 1)
 133 {}
 134 >>> unify(x, 1)
 135 { x: 1 }
 136 >>> unify((x, 2), (1, 2))
 137 { x: 1 }
 138 >>> unify((x, y), (1, 2))
 139 { x: 1, y: 2 }
 140 >>> unify((x, x), (1, 2))
 141 { x: 2 }
 142 ```
 143
 144 Oops!
 145 That last one is wrong!
 146 So what can we do to fix that?
 147
 148 Well, we need to take into account context.
 149 Let's change our `unify` function to accept an environment to work inside.
 150 I'm gonna make this a pure function, so we don't update the environment, we just make a new version of it.
 151 Some things are changed a bit when doing this.
 152 We include `env` in all of our outputs, instead of starting from nothing.
 153 We'll also include
 154
 155 ```python
 156 def unify(a, b, env={}):
 157     if a == b:
 158         return env
 159     if isinstance(a, Var):
 160         return {**env, a: b}
 161     if isinstance(b, Var):
 162         return {**env, b: a}
 163     if isinstance(a, tuple) and isinstance(b, tuple):
 164         if len(a) != len(b):
 165             return None
 166         for (ax, bx) in zip(a, b):
 167             env = unify(a, b, env)
 168             if env is None:
 169                 return None
 170         return env
 171     return None
 172 ```
 173
 174 This still doesn't do the right thing though, because we're not actually looking in the environment.
 175 We need to look stuff up, so let's write a function to do that.
 176 We'll just always call it, and if the term isn't a key for the environment, we'll just return it unchanged.
 177
 178 ```python
 179 def walk(env, term):
 180     if term in env:
 181         term = term[env]
 182     return term
 183 ```
 184
 185 Now we can add these two lines at the beginning.
 186
 187 ```python
 188     a = walk(env, a)
 189     b = walk(env, b)
 190 ```
 191
 192 With these modifications, we correctly handle the case we were stuck on earlier.
 193
 194 ```python
 195 >>> unify((x, x), (1, 2))
 196 >>> # look ma no solution!
 197 ```
 198
 199 It's still not perfect though.
 200 It doesn't properly reject this case where the conflict is two steps away:
 201
 202 ```python
 203 >>> unify((x, y, x), (y, 8, 9))
 204 { x: y, y: 9 }
 205 ```
 206
 207 Here the problem is that we have two facts around, that `x = y`, and that `y = 8`.
 208 Even so, it doesn't see that that means `x = 8` when it gets to the assertion of `x = 9`.
 209 Luckily this is another simple fix.
 210 We just keep walking through the environment as long as we have a binding.
 211 Just change the `if` to a `while`!
 212
 213 ```python
 214 def walk(env, term):
 215     while term in env:
 216         term = term[env]
 217     return term
 218 ```
 219
 220 And now this unifier should be able to handle any [(finite)](#postscript-unifying-infinity) hard cases you throw at it!
 221
 222 ### The Whole Unifier
 223
 224 Here's the whole program we wrote in one piece, in just 30 lines.
 225
 226 ```python
 227 from dataclasses import dataclass
 228
 229 @dataclass(frozen=True)
 230 class Var:
 231     name: str
 232     def __repr__(self):
 233         return self.name
 234
 235 def walk(env, term):
 236     while term in env:
 237         term = env[term]
 238     return term
 239
 240 def unify(a, b, env={}):
 241     a = walk(env, a)
 242     b = walk(env, b)
 243     if a == b:
 244         return env
 245     if isinstance(a, Var):
 246         return { **env, a: b }
 247     if isinstance(b, Var):
 248         return { **env, b: a }
 249     if isinstance(a, tuple) and isinstance(b, tuple):
 250         if len(a) != len(b):
 251             return None
 252         for (a, b) in zip(a, b):
 253             env = unify(a, b, env)
 254             if env is None:
 255                 return None
 256         return env
 257     return None
 258 ```
 259
 260 Consider writing your own in your language of choice, or adding support for new datatypes.
 261 It would be nice to be able to unify namedtuples and dictionaries and things, or do unification in the web browser.
 262 Try it out for yourself, because next time I'll be talking about how you can go from here and use unification to build logic programs.
 263
 264 ### Postscript: Unifying Infinity
 265
 266 What was that earlier?
 267 About only the finite cases?
 268 Well, it turns out this unifier is good enough for implementing well-behaved logic programs, but it leaves out one complexity: the "Occurs Check."
 269 This checks that a variable does not "occur" inside a term you unify it with, to avoid infinite solutions and non-termination.
 270 Many old Prolog implementations left out the occurs check for efficiency reasons, and we can leave it out for simplicity reasons if we want to trust our programmers to only write finite terms.
 271
 272 But let's go look at the problem specifically.
 273 We can write a unification like:
 274
 275 ```python
 276 >>> unify(a, (1, a))
 277 { a: (1, a) }
 278 ```
 279
 280 If you think through this, you can see that `a = (1, (1, (1, (1, ...))))`, going on infinitely deep.
 281 There are languages that work with logic on infinite terms like this, but applied naively it can end up giving us incorrect results or non-termination.
 282 For instance, with proper support for infinite terms, the following should unify:
 283
 284 ```python
 285 >>> env = unify(a, (1, a))
 286 >>> env = unify(b, (1, b), env)
 287 >>> env = unify(a, b)
 288 ```
 289
 290 But instead, it gets stuck on the last step, descending forever.
 291 There are two ways to solve this.
 292 One is to embrace infinite terms and include fixpoints in your logic, giving you terms like `a = fix x. (1, x)` and `b = fix x. (1, x)`.
 293 I don't know how to do this, though.
 294
 295 The other way is to detect unifications that would lead to infinite terms, and reject them.
 296 We take our code that adds variables to the substitution, and add the occurs check there:
 297
 298 ```python
 299     if isinstance(a, Var):
 300         if occurs(a, b, env): return None
 301         return { **env, a: b }
 302 ```
 303
 304 If we're using the occurs-check here, then we know a few things:
 305
 306 - `a` is a variable that's already been `walk()`-ed.
 307 - `a` and `b` aren't equal to each other, because earlier in the unify checked that.
 308
 309 This means that we can check if the literal variable `a` occurs literally in walked terms and subterms of `b`.
 310 If there's a variable in `b` that's a synonym of `a`, then it will walk to `a` because it was the result of walking.
 311 Then, the implementation looks like this:
 312
 313 ```python
 314 def occurs(a, b, env={}):
 315     b = walk(env, b)
 316     if a == b:
 317         return True
 318     if isinstance(b, tuple):
 319         return any(occurs(a, x) for x in b)
 320     return False
 321 ```
 322
 323 Now if we try...
 324
 325 ```python
 326 >>> unify(a, (1, a))
 327 >>>
 328 ```
 329
 330 We correctly don't unify this.
 331 We've got sound unification over finite terms.
 332 This is useful to clean the situtation up, but I'm still a bit sad to see infinite terms go...