6.824 Artificial Intelligence, Fall 1993 Problem Set 10

Due: Beginning of class Friday, December 3

Problem 1. A combinator is a closed term of higher order logic. Intuitively, a combinator is a term whose meaning is fixed — the meaning of a combinator does not depend on the meaning of free variables. Below is a list of specifications for higher order combinators. For each specification give a term of higher order logic satisfying the specification, i.e., implement the desired function in higher order logic.

SUBREL : (D × D → B) × (D × D → B) → B

The assertion (SUBREL R W) should be true if R is a subrelation of W, i.e., if (W x y) is true for all x and y such that (R x y) is true.

REL-COMP : (D × D → B) × (D × D → B) → (D × D → B)

The expression (REL-COMP R W) is the relation that is the composition of R and W. More formally, ((REL-COMP R W) x y) should be true if there is some z such that (R x z) is true and (W z y) is true. For example, the composition of the parent relation with itself is the grandparent relation and the composition of the parent relation with the gradparent relation is the great-grandparent relation.

TRANS : (D × D → B) → B

The expression (TRANS R) should be true if R is transitive. Your implementation should be of the form (λ (R) Φ[R]) where Φ[R] does not contain any λ-expressions (or quantifiers which have implicit λ-expressions) other than the combinators SUBREL

and REL-COMP.

REL-UNION : (D × D → B) × (D × D → B) → (D × D → B)

The expression (REL-UNION R W) is the relation that is the relation union of R and W. More formally, ((REL-UNION R W) x y) should be true if either (R x y) is true or (W x y) is true.

KLEENE-STAR : (D × D → B) → (D × D → B)

The expression (KLEENE-STAR R) the infinite union of the identity relation and any number of compositions of R with itself. This is equivalent to saying that (KLEENE-STAR R) is the least transitive relation containing the identity relation and R. Hint: The answer is a λ-expression of the form

(λ (r) (λ (x y) ∃ r′ “r′ = r^{∗} and (r′ x y)”))

APPLY : (D × D → B) × (D → B) → (D → B)

The expression (APPLY R S) should denote the “application” of the relation R to the set S. More formally (APPLY R S) should denote the set of individuals y such that there exits an individual x such that (S x) and (R x y) are both true.

EVERY : (D → B) → (D → B) → B

The assertion ((EVERY P) Q) should be true if P is a subset of Q. More formally, ((EVERY P) Q) should be true if (Q x) is true for every x such that (P x) is true.

SOME : (D → B) → (D → B) → B

The assertion ((SOME P) Q) should be true if the set P intersects the set Q. More formally, ((SOME P) Q) should be true if there is some x such that (Q x) and (P x) are both true.

Problem 2. We define a “quantifier” to be an object of type (D → B) → B. For example, (EVERY BIRD) is a quantifier. Modify the combinator APPLY so that it takes a quantifier as an argument and such that (APPLY R (SOME P)) is the set of y such that there exists an x such that (P x) and (R x y) and (APPLY R (EVERY P)) is the set of y such that for all x such that (P x) we have (R x y). Your solution

should have the property that ((SOME WOMAN) (APPLY LIKES (EVERY MAN))) has

a meaning that is one of the intuitive meanings of the sentence “some woman likes every man”.

Problem 3. In this problem we consider computing (as opposed to defining) the values of expressions in higher order logic.

Part a. Consider the following definition of a function V which computes a “value” for an expression in higher order logic. Fill in the missing parts of the definition. We will only be concerned with expressions that have no free variables and all of whose constants are of types D, D → B or D × D → B and whose only quantifiers, i.e., expressions of the form ∀_{τ} or ∃_{τ}, only quantify over D, i.e., are of the form ∀_{D} and ∃_{D}. We assume that each constant c has an interpretation denoted by M(c). We also assume that each element of D is named by some constant of thype D and that there are only finitely many elements of the set denoted by D. If f is a constants of type D → B and D × D → B then M(f) is an array of Boolean values indexed by the elements of D. Your completion of the following definition should have the property that if P is an expression of type B satisfying these conditions then the equations provide a way of computing V [P] as a truth value.

• V [c] = M(c) where c is a variable of type D.

• V [(f t)] = M(f)[V [t]] where f is a constant of type D → B and t is a term of type D.

• V [(f t w)] = M(f)[V [t], V [w]] where f is a constant of type D × D → B and t is a term of type D.

• V [(λ (x_{1} … x_{n}) b[x_{1} … x_{n}])] = (λ (x_{1} … x_{n}) b[x_{1} … x_{n}])

• V [((λ (x_{1} … x_{n}) b[x_{1} … x_{n}]) u_{1} … u_{n})] = ?

• V [(∀_{D} (λ (x) Φ[x]))] = ?

• V [(∃_{D} (λ (x) Φ[x]))] = ?

• V [((s w_{1} … w_{m}) u_{1} … u_{n})] = ?

Part b. Give the order of running time as a function of n (the number of elements in the interpretation of D) used to compute the value of the following expressions using the recursive evaluator defined in part a. Remember that each combinator is just an abbreviation for a closed expression of higher order logic. Explain your answers.

   • ((EVERY P) Q)
   • ((SOME P) Q)
   • ((EVERY P) (APPLY R (SOME Q)))
   • ((SOME P) (APPLY R (EVERY (APPLY W (SOME Q)))))
   • ((EVERY (APPLY R (SOME P))) Q)

Problem 4. Direct evaluation of the sort described in problem 2 is not possible for infinite or unbounded domains. In this problem we consider inference rules stated directly in terms of the combinators defined in problem 1. For each of the inference rules given below state whether or not that inference rule is sound relative to the semantics of higher order logic. Briefly explain each answer.

a (SUBREL ?R ?W)
    (SUBREL ?W ?R)
b (SUBREL ?R ?R)
c (SUBREL ?R ?W)
    (SUBREL ?W ?U)
    (SUBREL ?R ?U)
d (SUBREL ?R (REL-COMP ?R ?R))
e (SUBREL ?R (REL-UNION ?R ?W))
e (SUBREL ?R (KLEENE-STAR ?R))
f ((EVERY (APPLY ?R ?U)) ?U)
    ((EVERY (APPLY (KLEENE-STAR ?R) ?U)) ?U)

Problem 5. Consider a dungeon with all exits locked. In other words, any open door connects two rooms inside the dungeon. We can infer that a person who can not get through locked doors can not get out of the dungeon. Formalize this inference in higher order logic in such a way that it can be seen as a special case of of inference rule f given in the previous problem.