1 00:00:04,240 --> 00:00:08,650 Unification is the process of determining whether two expressions can be unified, 2 00:00:08,650 --> 00:00:13,920 that is made identical, by appropriate substitutions for the variables. 3 00:00:13,920 --> 00:00:17,880 As we'll see shortly, making this determination is an essential part of 4 00:00:17,880 --> 00:00:24,500 resolution. A substitution is a finite mapping of 5 00:00:24,500 --> 00:00:29,40 variables to terms. What follows will right substitution as 6 00:00:29,40 --> 00:00:33,0 sets of replacement rules like the one shown here. 7 00:00:33,0 --> 00:00:36,348 In each rule the variable to which the arrow is pointing is to be replaced by 8 00:00:36,348 --> 00:00:39,535 the term from which the arrow is pointing. 9 00:00:39,535 --> 00:00:45,199 In this case, x is to be replaced by a, y is to be replaced by f of b and v is to 10 00:00:45,199 --> 00:00:51,650 be replaced by w. The result of applying a substitution, is 11 00:00:51,650 --> 00:00:57,464 called sigma, to an expression phi is the expression written phi sigma. 12 00:00:57,464 --> 00:01:02,19 Obtained from phi by replacing every occurrence of every variable in sigma. 13 00:01:03,450 --> 00:01:09,889 By the term with which it is associated. For example applying our substitution to 14 00:01:09,889 --> 00:01:17,218 the expression p of x, x y z, yields p of a, a f of b and z. 15 00:01:23,140 --> 00:01:26,691 Given two or more substitutions, it's possible to define a single substitution 16 00:01:26,691 --> 00:01:31,26 that has the same effect as applying those substitutions in sequence. 17 00:01:31,26 --> 00:01:38,292 For example, the substitutions x gets a, y gets f of u, z gets v. 18 00:01:38,292 --> 00:01:44,892 And, u gets d, v gets e and z gets g, can be combined to form the single 19 00:01:44,892 --> 00:01:55,649 substitution, x gets a, y gets f of d, z gets e, u gets d and v gets e. 20 00:01:56,800 --> 00:02:02,740 And the single substitution has the same effect as the first two substitutions 21 00:02:02,740 --> 00:02:07,730 when applied to any expression whatsoever. 22 00:02:07,730 --> 00:02:11,140 Computing the composition of a substitution sigma, the cup substitution 23 00:02:11,140 --> 00:02:14,470 toa is easy. Okay, there are three steps. 24 00:02:14,470 --> 00:02:22,830 First we take too and apply it to the replacement in sigma. 25 00:02:22,830 --> 00:02:27,510 Having done that, we join to sigma or[UNKNOWN] which are different variables 26 00:02:27,510 --> 00:02:32,58 than those in sigma. Notice that in this case we did not 27 00:02:32,58 --> 00:02:36,770 inlcude the binding of z to g from toa because we already had a binding of z to 28 00:02:36,770 --> 00:02:42,620 e in sigma. Finally in the third step we delete any 29 00:02:42,620 --> 00:02:48,92 assignments of variables to themselves. No examples of that in this case. 30 00:02:48,92 --> 00:02:52,970 Okay now why do we care about substitutions? 31 00:02:52,970 --> 00:02:57,724 Well it's the first step in unification. Say a substitution sigma is a unifier for 32 00:02:57,724 --> 00:03:05,110 an expression phi and expression psi. If and only if phi sigma is the same as 33 00:03:05,110 --> 00:03:09,334 psi sigma. Now, does sigma apply to psi, does sigma 34 00:03:09,334 --> 00:03:12,670 psi apply to psi, produce the same expression? 35 00:03:12,670 --> 00:03:17,390 If two expressions have a unifier, they're said to be unifiable. 36 00:03:17,390 --> 00:03:22,910 And otherwise they're nonunifiable. So an example of nonunifiable expressions 37 00:03:22,910 --> 00:03:26,810 is shown here. would be p of x,x on the one hand and p 38 00:03:26,810 --> 00:03:33,110 of a,b on the other. There's no way to bind x so that, it's 39 00:03:33,110 --> 00:03:40,120 the same as a and at the same time the same as b. 40 00:03:40,120 --> 00:03:41,380 Okay now, although the substitution unifies two expressions, it may not be 41 00:03:41,380 --> 00:03:43,30 the only unifier. We don't have to substitute b for y and v 42 00:03:43,30 --> 00:03:46,699 to unify two expressions. We can equally well substitute c, or d, 43 00:03:46,699 --> 00:03:53,478 or f of c, or f of w. In fact, you can unify these expressions 44 00:03:53,478 --> 00:04:01,440 without changing v at all by simply replacing y by v. 45 00:04:03,730 --> 00:04:07,939 Now in considering these alternatives it should be clear that some substitutions 46 00:04:07,939 --> 00:04:11,796 are more general than others. In fact we're going to enshrine that with 47 00:04:11,796 --> 00:04:15,56 a definition. We say that a substition sigma is as 48 00:04:15,56 --> 00:04:20,880 general as, or more general than, a substititon tao. 49 00:04:20,880 --> 00:04:24,302 If and only if there's another substitution delta such that tao is the 50 00:04:24,302 --> 00:04:28,947 composition of sigma and delta. For example, the substitution at the 51 00:04:28,947 --> 00:04:33,172 bottom here is more general, as are more general than the other two, since each 52 00:04:33,172 --> 00:04:37,332 can, of the first two can be contained by composing unifier at the bottom with 53 00:04:37,332 --> 00:04:44,290 another substitution. And in fact, the substitution at the 54 00:04:44,290 --> 00:04:48,20 bottom is more general than the other two in that the reverse does not hold. 55 00:04:48,20 --> 00:04:52,244 There's no way to convert either one of the first two into the third unifier by 56 00:04:52,244 --> 00:04:58,918 applying an additional substitution. Now, in resolution we're interested only 57 00:04:58,918 --> 00:05:05,602 in unifiers with maximum generality. It's called a most general unifier, or 58 00:05:05,602 --> 00:05:10,256 mgu, and it's defined as follows. An mgu sigma of two expressions has the 59 00:05:10,256 --> 00:05:15,566 property that is as general as or more general than any other unifier. 60 00:05:15,566 --> 00:05:20,222 Now, it's possible for two expressions to have more than one most general unifier. 61 00:05:20,222 --> 00:05:23,918 However, even this, as though this is the case, all of the most general unifiers 62 00:05:23,918 --> 00:05:28,58 are structurally the same. And, in otherwords, they're unique up to 63 00:05:28,58 --> 00:05:31,700 variable renaming. For example, p of x and p of y can be 64 00:05:31,700 --> 00:05:40,0 unified by either the substitution x gets y or by the substitution y gets x. 65 00:05:40,0 --> 00:05:43,575 And either of these substitutions can be obtained from the other by applying a 66 00:05:43,575 --> 00:05:47,776 third substitution. It's not true of those unifiers we saw 67 00:05:47,776 --> 00:05:51,122 earlier. Okay, one good thing about our language 68 00:05:51,122 --> 00:05:55,154 is that there is a simple and quite inexpensive procedure for computing the 69 00:05:55,154 --> 00:06:01,49 most general unifier of any two expressions provided that there is one. 70 00:06:03,150 --> 00:06:07,56 the procedure assumes a representation of expressions as sequences of 71 00:06:07,56 --> 00:06:10,980 subexpressions. For example, the expression p of a, f of 72 00:06:10,980 --> 00:06:15,460 b and z can be thought of as a sequence with four elements, namely the relation 73 00:06:15,460 --> 00:06:20,920 constant p, the object constant a, the term f of b. 74 00:06:20,920 --> 00:06:24,208 I'm sorry f of b, c. And the variable z. 75 00:06:24,208 --> 00:06:30,608 The term f of b, c can in turn be thought of as sequence of three elements namely 76 00:06:30,608 --> 00:06:39,845 the function constant f, the object constant b and the object constant c. 77 00:06:39,845 --> 00:06:45,765 Okay, given that representation, we can describe the procedure. 78 00:06:45,765 --> 00:06:49,853 in detail. You start with two express, 79 00:06:49,853 --> 00:06:55,210 subexpressions, and a sub, and an empty, a substitution, which is initially empty. 80 00:06:55,210 --> 00:06:59,630 We then recursively process the two expressions, comparing the subexpressions 81 00:06:59,630 --> 00:07:04,875 of the, those expressions at each point. Along the way, we expand the substitution 82 00:07:04,875 --> 00:07:09,744 with variable assignments, as we'll see. If we fail to unify any pair of 83 00:07:09,744 --> 00:07:13,570 subexpressions at any point in the process the procedure as a whole fails. 84 00:07:13,570 --> 00:07:17,854 If we finish the recursive comparison of the expressions, the procedure as whole 85 00:07:17,854 --> 00:07:21,508 succeeds, and the accumulated substitution at that point is our most 86 00:07:21,508 --> 00:07:25,960 generally unifier. Okay the rules are these. 87 00:07:25,960 --> 00:07:29,740 If two expressions being compared into sub expressions being compared are 88 00:07:29,740 --> 00:07:36,15 identical, we succeed on that step. If neither one is a variable and at least 89 00:07:36,15 --> 00:07:41,861 one is a constant, then we fail. If at least one of the expressions is a 90 00:07:41,861 --> 00:07:46,70 variable, we proceed as described in just a moment. 91 00:07:46,70 --> 00:07:49,975 However, both expressions are sequences, neither variables nor constants, then we 92 00:07:49,975 --> 00:07:54,45 iterate across the expressions, comparing sub-expression to sub-expression, as just 93 00:07:54,45 --> 00:07:57,890 described, in the same manners just described. 94 00:07:57,890 --> 00:08:02,160 Okay, now what about the case where we have at least one of the expressions 95 00:08:02,160 --> 00:08:06,242 being a variable? Alright, in this case we first check 96 00:08:06,242 --> 00:08:10,370 whether the variable has a binding in the current substitution. 97 00:08:10,370 --> 00:08:15,590 If so, we try to unify that binding with the other expression. 98 00:08:15,590 --> 00:08:18,790 If there's no binding, we can give it a binding, but first we check whether the 99 00:08:18,790 --> 00:08:23,810 second expression contains the variable that, to which we are binding it. 100 00:08:23,810 --> 00:08:26,340 That the variable occurs within the expression, we fail. 101 00:08:26,340 --> 00:08:29,721 Otherwise we set the substitution to com, the composition of the old substitution 102 00:08:29,721 --> 00:08:34,124 and a new substitution which we bind the variable to that second expression. 103 00:08:34,124 --> 00:08:38,604 This will all become a lot clearer when you look through some examples, right 104 00:08:38,604 --> 00:08:41,52 now. So here's our first example. 105 00:08:41,52 --> 00:08:45,540 Instead of the computation of the most general unifier for the expressions p of 106 00:08:45,540 --> 00:08:50,42 xb and p of ay, with the initial substitution empty. 107 00:08:50,42 --> 00:08:54,394 The trace of the execution or procedure for this case is shown here. 108 00:08:54,394 --> 00:08:58,879 we show the beginning of a comparison, with a line labeled, call. 109 00:08:58,879 --> 00:09:03,433 Together with the expressions being compared, and the input substitution. 110 00:09:04,460 --> 00:09:07,670 And we show the result of that comparison with the line label x. 111 00:09:07,670 --> 00:09:13,522 At each point here, the indentation shows the depth of incursion of the procedure. 112 00:09:13,522 --> 00:09:18,214 Okay, so here on the first[UNKNOWN] step, we compare the first element of the first 113 00:09:18,214 --> 00:09:22,498 expression with the first element of the second expression, since they're 114 00:09:22,498 --> 00:09:29,310 identical in this case, we succeed with no changes to our substitution. 115 00:09:29,310 --> 00:09:33,824 We then compare the variable x to the constant a, in this case, leading to a 116 00:09:33,824 --> 00:09:42,720 binding of x to a. And finally we compare b to y. 117 00:09:42,720 --> 00:09:47,27 In this case we compose the current variable assigment x gets a with the 118 00:09:47,27 --> 00:09:53,370 assignment y to b which produces the joint assignment x gets a y gets b. 119 00:09:53,370 --> 00:10:03,690 At this point having reached the ends of both expressions, we're done. 120 00:10:03,690 --> 00:10:08,490 Okay here's another example, consider unifying the expressions p of x, x and 121 00:10:08,490 --> 00:10:14,870 the expression p of a, y. Here's our trace, main interest in this 122 00:10:14,870 --> 00:10:21,903 case is in the step involving x and y. So at this point x has a binding to a, 123 00:10:21,903 --> 00:10:26,600 and so we recursively compare that binding of y replacement, which is a in 124 00:10:26,600 --> 00:10:32,109 this case, to y. In this case, we can bind y to a, we 125 00:10:32,109 --> 00:10:37,464 could pose that substitution with the original substitution to reduce the 126 00:10:37,464 --> 00:10:44,268 resulting a composite substitution, x gets a and y gets a. 127 00:10:44,268 --> 00:10:50,316 And again since we're done processing all the sub expressions the substitution at 128 00:10:50,316 --> 00:10:58,4 this point is the most generally unifier. Okay, using example where two expressions 129 00:10:58,4 --> 00:11:02,120 do not unify. Start same as before. 130 00:11:02,120 --> 00:11:06,838 This time when we compare the second x to b, get a different result. 131 00:11:06,838 --> 00:11:16,520 As before we retrieve that binding of x namely a and try to unify a with b. 132 00:11:16,520 --> 00:11:21,359 Since its two different constants we fail and unification as a whole fails. 133 00:11:28,430 --> 00:11:32,375 Okay here's one more example. This one's similar to that last one 134 00:11:32,375 --> 00:11:36,60 except that the second term in the second expression is the functional term that 135 00:11:36,60 --> 00:11:39,808 contains y. After unifying the first two arguments, 136 00:11:39,808 --> 00:11:43,900 we find ourselves trying to unify. x and f of y. 137 00:11:43,900 --> 00:11:48,240 With a substitution where x is bound to y. 138 00:11:48,240 --> 00:11:51,820 Now in order for this to work we would have to unify y and f of y. 139 00:11:51,820 --> 00:11:56,212 We would have to bind y to f of y. But now remember back to the condition 140 00:11:56,212 --> 00:12:00,362 that I mentioned on variable assignments. We must not ever bind a variable to a 141 00:12:00,362 --> 00:12:05,465 term which contains itself. Since f of y contains y, the 142 00:12:05,465 --> 00:12:12,352 substitution, unification process in this case fails, and the unification process 143 00:12:12,352 --> 00:12:17,856 as a whole fails. Okay now you might be wondering why 144 00:12:17,856 --> 00:12:23,290 exactly we have this condition, that a variable may not be bound to itself. 145 00:12:24,410 --> 00:12:27,230 Okay well one reason is this, if we were to allow bindings of variables to 146 00:12:27,230 --> 00:12:31,700 expressions that contain those variables, it would lead to circular bindings. 147 00:12:31,700 --> 00:12:34,750 Now this in itself is not a problem, though it does raise the question, how 148 00:12:34,750 --> 00:12:37,922 many times the substitution needs to be applied. 149 00:12:37,922 --> 00:12:41,791 more importantly though, it can create a situation where the substitution does not 150 00:12:41,791 --> 00:12:46,698 actually unify the input expressions, no matter how many times it's applied. 151 00:12:46,698 --> 00:12:49,772 Okay, as we see here, applying a substitution does not lead to the same 152 00:12:49,772 --> 00:12:52,700 result. And, it fails no matter how many more 153 00:12:52,700 --> 00:12:56,192 times we apply it. The second argument in the second case 154 00:12:56,192 --> 00:12:59,210 always has one additional applicational f. 155 00:12:59,210 --> 00:13:01,354 And so these expressions will never look alike. 156 00:13:01,354 --> 00:13:05,189 it's the reason why we check, whether variables contained in an expression 157 00:13:05,189 --> 00:13:10,880 before creating a binding, and it has a name, it's so important this condition. 158 00:13:10,880 --> 00:13:13,627 It's called the occur check for obvious reasons. 159 00:13:13,627 --> 00:13:17,799 interestingly though, not all logical systems do this occur check. 160 00:13:17,799 --> 00:13:20,904 Prolog, the programming language Prolog, is notable for not performing the occur 161 00:13:20,904 --> 00:13:23,708 check, or at least not by default in most systems. 162 00:13:23,708 --> 00:13:30,568 programatically it's useful as a way of generating circular data structure, or 163 00:13:30,568 --> 00:13:36,840 logically it can lead to errors and so in logic we always do the occur checking 164 00:13:36,840 --> 00:13:40,793 resolution.