Section 10.4 Notes

6.034 Notes: Section 10.4 Slide 10.4.1 We introduced first-order resolution and said there were two issues to resolve before we could do it. First was conversion to clausal form, which we've done. Now we have to figure out how to instantiate the variables in the universal statements. In this problem, it was clear that A was the relevant individual. But it is not necessarily clear at all how to do that automatically. Slide 10.4.2 In order to derive an algorithmic way of finding the right instantiations for the universal variables, we need something called substitutions. Slide 10.4.3 Here's an example of what we called an atomic sentence before: a predicate applied to some terms. There are two variables here: x and y. We can think of many different ways to substitute terms into this expression. Those are called substitution instances of the expression. Slide 10.4.4 A substitution is a set of variable-term pairs, written this way. It says that whenever you see variable vi, you should substitute in term ti. There should not be more than one entry for a single variable. Slide 10.4.5 So here's one substitution instance. P(z,f(w),B). It's not particularly interesting. It's called an alphabetic variant, because we've just substituted some different variables in for x and y. In particular, we've put z in for x and w in for y, as shown in the substitution. Slide 10.4.6 Here's another substitution instance of our sentence: P(x, f(A), B), We've put the constant A in for the variable y. Slide 10.4.7 To get P(g(z), f(A), B), we substitute the term g(z) in for x and the constant A for y. Slide 10.4.8 Here's one more -- P(C, f(A), B). It's sort of interesting, because it doesn't have any variables in it. We'll call an atomic sentence with no variables a ground instance. Ground means it doesn't have any variables. Slide 10.4.9 You can think about substitution instances, in general, as being more specific than the original sentence. A constant is more specific than a variable. There are fewer interpretations under which a sentence with a constant is true. And even f(x) is more specific than y, because the range of f might be smaller than U. You're not allowed to substitute anything in for a constant, or for a compound term (the application of a function symbol to some terms). You are allowed to substitute for a variable inside a compound term, though, as we have done with f in this example. Slide 10.4.10 We'll use the notation of an expression followed by a substitution to mean the expression that we get by applying the substitution to the expression. To apply a substitution to an expression, we look to see if any of the variables in the expression have entries in the substitution. If they do, we substitute in the appropriate new expression for the variable, and continue to look for possible substitutions until no more opportunities exist. So, in this second example, we substitute A in for y, then y in for x, and then we keep going and substitute A in for y again. Slide 10.4.11 Now we'll look at the process of unification, which is finding a substitution that makes two expressions match each other exactly. Slide 10.4.12 So, expressions omega1 and omega2 are unifiable if and only if there exists a substitution S such that we get the same thing when we apply S to omega1 as we do when we apply S to omega2. That substitution, S, is called a unifier of omega1 and omega2. Slide 10.4.13 So, let's look at some unifiers of the expressions x and y. Since x and y are both variables, there are lots of things you can do to make them match. Slide 10.4.14 If you substitute x in for y, then both expressions come out to be x. Slide 10.4.15 If you put in y for x, then they both come out to be y. Slide 10.4.16 But you could also substitute something else, like f(f(A)) for x and for y, and you'd get matching expressions. Slide 10.4.17 Or, you could substitute some constant, like A, in for both x and y. Some of these unifiers seem a bit arbitrary. Binding both x and y to A, or to f(f(A)) is a kind of over­ commitment. Slide 10.4.18 So, in fact, what we're really going to be looking for is not just any unifier of two expressions, but a most general unifier, or MGU. Slide 10.4.19 G is a most general unifier of omega1 and omega2 if and only if for all unifiers S, there exists an Sprime such that the result of applying G followed by S-prime to omega1 is the same as the result of applying S to omega1; and the result of applying G followed by S-prime to omega2 is the same as the result of applying S to omega2. A unifier is most general if every single one of the other unifiers can be expressed as an extra substitution added onto the most general one. An MGU is a substitution that you can make that makes the fewest commitments, and can still make these two expressions equal. Slide 10.4.20 So, let's do a few examples together. What's a most general unifier of P(x) and P(A)? A for x. Slide 10.4.21 What about these two expressions? We can make them match up either by substituting x for y, or y for x. It doesn't matter which one we do. They're both "most general". Slide 10.4.22 Okay. What about this one? It's a bit tricky. You can kind of see that, ultimately, all of the variables are going to have to be the same. Matching the arguments to g forces y and x to be the same, And since z and y have to be the same as well (to make the middle argument match), they all have to be the same variable. Might as well make it x (though it could be any other variable). Slide 10.4.23 What about P(x, B, B) and P(A, y, z)? It seems pretty clear that we're going to have to substitute A for x, B for y, and B for z. Slide 10.4.24 Here's a tricky one. It looks like x is going to have to simultaneously be g(f(v)) and g(u). How can we make that work? By substituting f(v) in for u. Slide 10.4.25 Now, let's try unifying P(x, f(x)) with P(x,x). The temptation is to say x has to be f(x), but then that x has to be f(x), etc. The answer is that these expressions are not unifiable. The last time I explained this to a class, someone asked me what would happen if f were the identity function. Then, couldn't we unify these two expressions? That's a great question, and it illustrates a point I should have made before. In unification, we are interested in ways of making expressions equivalent, in every interpretation of the constant and function symbols. So, although it might be possible for the constants A and B to be equal because they both denote the same object in some interpretation, we can't unify them, because they aren't required to be the same in every interpretation. Slide 10.4.26 An MGU can be computed recursively, given two expressions x and y, to be unified, and a substitution that contains substitutions that must already be made. The argument s will be empty in a top-level call to unify two expressions. Slide 10.4.27 The algorithm returns a substitution if x and y are unifiable in the context of s, and fail otherwise. If s is already a failure, we return failure. Slide 10.4.28 If x is equal to y, then we don't have to do any work and we return s, the substitution we were given. Slide 10.4.29 If either x or y is a variable, then we go to a special subroutine that's shown in upcoming slides. Slide 10.4.30 If x is a predicate or a function application, then y must be one also, with the same predicate or function. Slide 10.4.31 If so, we'll unify the lists of arguments from x and y in the context of s. Slide 10.4.32 If not, that is, if x and y have different predicate or function symbols, we simply fail. Slide 10.4.33 Finally, (if we get to this case, then x and y are either lists of predicate or function arguments, or something malformed), we go down the lists, unifying the first elements, then the second elements, and so on. Each time we unify a pair of elements, we get a new substitution that records the commitments we had to make to get that pair of expressions to unify. Each further unification must take place in the context of the commitments generated by the previous elements of the lists. Because, at each stage, we find the most general unifier, we make as few commitments as possible as we go along, and therefore we never have to back up and try a different substitution. Slide 10.4.34 Given a variable var, an expression x, and a substitution s, we need to return a substitution that unifies var and x in the context of s. What makes this tricky is that we have to first keep applying the existing substitutions in s to var, and to x, if it is a variable, before we're down to a new concrete problem to solve. Slide 10.4.35 So, if var is bound to val in s, then we unify that value with x, in the context of s (because we're already committed that val has to be substituted for var). Slide 10.4.36 Similarly, if x is a variable, and it is bound to val in s, then we have to unify var with val in s. (We call unify-var directly, because we know that var is still a var). Slide 10.4.37 If var occurs anywhere in x, with substitution s applied to it, then fail. This is the "occurs" check, which keeps us from circularities, like binding x to f(x). Slide 10.4.38 Finally, we know var is a variable that doesn't already have a substitution, so we add the substitution of x for var to s, and return it. Slide 10.4.39 Here are a few more examples of unifications, just so you can practice. If you don't see the answer immediately, try simulating the algorithm.