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

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