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 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 Here we return an empty environment because they're already equal, and nothing needs to be substituted.
  76
  77 The variable cases can also be solved very easily.
  78 Trying to unify a variable with another term, we can just substitute that for the variable.
  79 When unifying `x = 1`, we get back `{ x: 1 }`.
  80
  81 ```python
  82     if isinstance(a, Var):
  83         return {a: b}
  84     if isinstance(b, Var):
  85         return {b: a}
  86 ```
  87
  88 Finally, let's handle tuples.
  89 For this, we want to unify each individual component of the tuple.
  90 We want the union of each of these unifications, so we'll update the dictionary each time.
  91 We have to check if the sub-unification returned None and pass that along.
  92
  93 ```python
  94     if isinstance(a, tuple) and isinstance(b, tuple):
  95         if len(a) != len(b):
  96             return None
  97         env = {}
  98         for (ax, bx) in zip(a, b):
  99             res = unify(ax, bx)
 100             if res is None:
 101                 return None
 102             env.update(res)
 103         return env
 104 ```
 105
 106 Now you might see where this could go wrong, and we'll get to that in a moment with an example.
 107 Repeating that function all in one piece:
 108
 109 ```python
 110 def unify(a, b):
 111     if a == b:
 112         return {}
 113     if isinstance(a, Var):
 114         return {a: b}
 115     if isinstance(b, Var):
 116         return {b: a}
 117     if isinstance(a, tuple) and isinstance(b, tuple):
 118         if len(a) != len(b):
 119             return None
 120         env = {}
 121         for (ax, bx) in zip(a, b):
 122             res = unify(ax, bx)
 123             if res is None:
 124                 return None
 125             env.update(res)
 126         return env
 127     return None
 128 ```
 129
 130 Now we can unify stuff:
 131
 132 ```python
 133 >>> x, y = Var("x"), Var("y")
 134 >>> unify(1, 1)
 135 {}
 136 >>> unify(x, 1)
 137 { x: 1 }
 138 >>> unify((x, 2), (1, 2))
 139 { x: 1 }
 140 >>> unify((x, y), (1, 2))
 141 { x: 1, y: 2 }
 142 >>> unify((x, x), (1, 2))
 143 { x: 2 }
 144 ```
 145
 146 Oops!
 147 That last one is wrong!
 148 So what can we do to fix that?
 149
 150 Well, we need to take into account context.
 151 Let's change our `unify` function to accept an environment to work inside.
 152 I'm gonna make this a pure function, so we don't update the environment, we just make a new version of it.
 153 Some things are changed a bit when doing this.
 154 We include `env` in all of our outputs, instead of starting from nothing.
 155 We'll also include
 156
 157 ```python
 158 def unify(a, b, env={}):
 159     if a == b:
 160         return env
 161     if isinstance(a, Var):
 162         return {**env, a: b}
 163     if isinstance(b, Var):
 164         return {**env, b: a}
 165     if isinstance(a, tuple) and isinstance(b, tuple):
 166         if len(a) != len(b):
 167             return None
 168         for (ax, bx) in zip(a, b):
 169             env = unify(a, b, env)
 170             if env is None:
 171                 return None
 172         return env
 173     return None
 174 ```
 175
 176 This still doesn't do the right thing though, because we're not actually looking in the environment.
 177 We need to look stuff up, so let's write a function to do that.
 178 We'll just always call it, and if the term isn't a key for the environment, we'll just return it unchanged.
 179
 180 ```python
 181 def walk(env, term):
 182     if term in env:
 183         term = env[term]
 184     return term
 185 ```
 186
 187 Now we can add these two lines at the beginning.
 188
 189 ```python
 190     a = walk(env, a)
 191     b = walk(env, b)
 192 ```
 193
 194 With these modifications, we correctly handle the case we were stuck on earlier.
 195
 196 ```python
 197 >>> unify((x, x), (1, 2))
 198 >>> # look ma no solution!
 199 ```
 200
 201 It's still not perfect though.
 202 It doesn't properly reject this case where the conflict is two steps away:
 203
 204 ```python
 205 >>> unify((x, y, x), (y, 8, 9))
 206 { x: y, y: 9 }
 207 ```
 208
 209 Here the problem is that we have two facts around, that `x = y`, and that `y = 8`.
 210 Even so, it doesn't see that that means `x = 8` when it gets to the assertion of `x = 9`.
 211 Luckily this is another simple fix.
 212 We just keep walking through the environment as long as we have a binding.
 213 Just change the `if` to a `while`!
 214
 215 ```python
 216 def walk(env, term):
 217     while term in env:
 218         term = env[term]
 219     return term
 220 ```
 221
 222 And now this unifier should be able to handle any [(finite)](#postscript-unifying-infinity) hard cases you throw at it!
 223
 224 ### The Whole Unifier
 225
 226 Here's the whole program we wrote in one piece, in just 30 lines.
 227
 228 ```python
 229 from dataclasses import dataclass
 230
 231 @dataclass(frozen=True)
 232 class Var:
 233     name: str
 234     def __repr__(self):
 235         return self.name
 236
 237 def walk(env, term):
 238     while term in env:
 239         term = env[term]
 240     return term
 241
 242 def unify(a, b, env={}):
 243     a = walk(env, a)
 244     b = walk(env, b)
 245     if a == b:
 246         return env
 247     if isinstance(a, Var):
 248         return { **env, a: b }
 249     if isinstance(b, Var):
 250         return { **env, b: a }
 251     if isinstance(a, tuple) and isinstance(b, tuple):
 252         if len(a) != len(b):
 253             return None
 254         for (a, b) in zip(a, b):
 255             env = unify(a, b, env)
 256             if env is None:
 257                 return None
 258         return env
 259     return None
 260 ```
 261
 262 Consider writing your own in your language of choice, or adding support for new datatypes.
 263 It would be nice to be able to unify namedtuples and dictionaries and things, or do unification in the web browser.
 264 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.
 265
 266 ### Postscript: Unifying Infinity
 267
 268 What was that earlier?
 269 About only the finite cases?
 270 Well, it turns out this unifier is good enough for implementing well-behaved logic programs, but it leaves out one complexity: the "Occurs Check."
 271 This checks that a variable does not "occur" inside a term you unify it with, to avoid infinite solutions and non-termination.
 272 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.
 273
 274 But let's go look at the problem specifically.
 275 We can write a unification like:
 276
 277 ```python
 278 >>> unify(a, (1, a))
 279 { a: (1, a) }
 280 ```
 281
 282 If you think through this, you can see that `a = (1, (1, (1, (1, ...))))`, going on infinitely deep.
 283 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.
 284 For instance, with proper support for infinite terms, the following should unify:
 285
 286 ```python
 287 >>> env = unify(a, (1, a))
 288 >>> env = unify(b, (1, b), env)
 289 >>> env = unify(a, b)
 290 ```
 291
 292 But instead, it gets stuck on the last step, descending forever.
 293 There are two ways to solve this.
 294 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)`.
 295 I don't know how to do this, though.
 296
 297 The other way is to detect unifications that would lead to infinite terms, and reject them.
 298 We take our code that adds variables to the substitution, and add the occurs check there:
 299
 300 ```python
 301     if isinstance(a, Var):
 302         if occurs(a, b, env): return None
 303         return { **env, a: b }
 304     if isinstance(b, Var):
 305         if occurs(b, a, env): return None
 306         return { **env, b: a }
 307 ```
 308
 309 If we're using the occurs-check here, then we know a few things:
 310
 311 - `a` is a variable that's already been `walk()`-ed.
 312 - `a` and `b` aren't equal to each other, because earlier in the unify checked that.
 313
 314 This means that we can check if the literal variable `a` occurs literally in walked terms and subterms of `b`.
 315 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.
 316 While it's safe to assume to that `a` has already been walked, note that we can't assume that `b` has already been walked since we're recursing over it.
 317 Then, the implementation looks like this:
 318
 319 ```python
 320 def occurs(a, b, env={}):
 321     b = walk(env, b)
 322     if a == b:
 323         return True
 324     if isinstance(b, tuple):
 325         return any(occurs(a, x) for x in b)
 326     return False
 327 ```
 328
 329 Now if we try...
 330
 331 ```python
 332 >>> unify(a, (1, a))
 333 >>>
 334 ```
 335
 336 We correctly don't unify this.
 337 We've got sound unification over finite terms.
 338 This is useful to clean the situtation up, but I'm still a bit sad to see infinite terms go...
 339
 340 ----
 341
 342 *Edit November 26, 2020.*
 343 Thanks to Onel Harrison for giving some clarity feedback and pointing out some typos.