6
$\begingroup$

Currently I read up on unifiers, however have some problem understanding its concept. Thus far I found an example of an equation:

add(suc(x); y) $\stackrel{.}{=}$ add(y; suc(z))

and unifiers to it:

$\omicron$ = [suc(x)/y; x/z],

$\omicron'$ = [suc(suc(z))/y; suc(z)/z; suc(z)/x] and

$\omicron'$ = $\omicron$[suc(z)=x]

However I do not understand how one generally derives these unifiers from the equation above. Any construcive comment/answer would be appreciated.

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
7
$\begingroup$

A unifier of a set of terms is just any substitution that, when applied to each of the terms, makes them all equal. There's also the concept of a "most general unifier" (MGU), which is a unifier $\sigma$ of the terms such that any other unifier can be written as $\sigma\circ\tau$ for some substitution $\tau$: in other words any other unifier can be written as "first do an MGU and then do some more substitutions, which were kinda unnecessary because you'd already made the terms equal."

As for finding unifiers, there are various algorithms; see the Wikipedia article for more details. In terms of what's required for undergraduate exercises, though, the most natural "algorithm" is the rather unhelpful "Look at the terms and see what works." Once you understand the definition and you're comfortable with it, a unifier is usually pretty immediate.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Ok, but what does [suc(x)/y; x/z] mean, how is substituted? Is any other property of function taken as granted, like commutativity of addition? $\endgroup$
    – Imago
    Commented Nov 6, 2016 at 15:17
  • 2
    $\begingroup$ $[a/b]$ means "replace every instance of $a$ with $b$". Whether or not commutativity of addition and so on are taken into account depends on whether you're looking for a syntactic unifier (one that makes the strings literally the same, without trying to assign any meaning to them) or a semantic unifier (one that makes the strings evaluate to the same thing). $\endgroup$
    – David Richerby
    Commented Nov 6, 2016 at 15:23
  • 1
    $\begingroup$ @DavidRicherby You meant "replace every instance of $b$ with $a$". $\endgroup$
    – Derek Elkins left SE
    Commented Nov 7, 2016 at 5:08
  • 1
    $\begingroup$ @DerekElkins Sorry, you're right. I hate that notation. The way to remember which way it goes is that, just like fractions, $b[a/b]=a$, but that didn't help me. $\endgroup$
    – David Richerby
    Commented Nov 7, 2016 at 8:17
  • $\begingroup$ Agreed. I usually use the less common $[b \mapsto a]$, so the original example would be $[y \mapsto \text{suc}(x), z \mapsto x]$. It's less compact, but I feel (I haven't verified this in any way) that it is more self-explanatory. It's certainly less amenable to mixing things up. I actually hadn't made the connection to fractions. Mentally, I usually keep track by visualizing $[a/b]$ as $a/$ looming over $b$ like a wave about to crash. 'still easy to flip things around though. $\endgroup$
    – Derek Elkins left SE
    Commented Nov 7, 2016 at 10:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.