6.824 Artificial Intelligence, Fall 1993 Problem Set 5

Due: Beginning of class Wednesday, October 20

Problem 1. This problem involves writing a bottom-up logic program to compute the free variables in an expression. Variables are represented by expressions of the form (THE-VARIABLE x) where x is an expression representing the name of the variable. Constants are represented by expressions of the form (THE-CONSTANT x) where x is the name of the constant. An operator is an expression of the form (THE-OPERATOR f) where f is either the symbol + or the symbol *. An arithmetic expression is either a constant, a variable, of an expression of the form (apply f u v) where f is an operator and u and v are (recursively) arithmetic expressions. For example the following is an arithmetic expression.

(apply (the-operator +)
       (apply (the-operator *)
              (the-constant a)
              (the-variable x))
       (the-constant b))

part a. Write a set of inference rules for proving formulas of the form (ARITH-EXP y) where this assertion means that y is an expression as defined above. Your rule set R should have the property that ⊢_{R} (ARITH-EXP y) if and only if y is an arithmetic expression as defined above. (The notation ⊢_{R} Φ means that Φ can be derived from the inference rules without any premises). You will need to use inference rules which do not have any antecedents. You may want to use formulas of the form (OPERATOR f) so that new operators can be added easily.

part b. Write a set of inference rules for deriving assertions of the form (occurs-in x y) where this formula means that y is an arithmetic expression and x is a variable that occurs in y. Your rules set R should have the property that ⊢_{R} (occurs-in x y) if and only if y is an expression and x is a variable that occurs in y.

part c. Explain why bottom-up execution of the inference rules you wrote for parts a and b fails to terminate. (bottom-up execution computes C_{R}(Σ) = {Φ : Σ ⊢_{R} Φ}

part d. Modify the rules to use an input assertion of the form (INPUT! x) so that

• (INPUT! y) ⊢_{R} (ARITH-EXP y) if and only if y is an arithmetic expression.

• (INPUT! y) ⊢_{R} (OCCURS-IN x y) if and only if x is a variable, y is an arithmetic expression, and x occurs in y.

• For any finite set Σ, the set C_{R}(Σ) is finite.

part e. Give the order of running time for computing C_{R}(Σ) where Σ is a set of input assertions. Your running time should be a function of the number v of variables and the number n of arithmetic expressions that appear in input terms.

part f. Suppose we define the expression e_{n} by e_{0} = (THE-VARIABLE (X)) and e_{n+1} = (apply (the-operator +) e_{n} e_{n})). If we were to write the expression e_{n} as a string of characters what is the order of growth of the string length of e_{n} as a function of n? What is the order of growth of the time needed to compute C_{R}((INPUT! e_{n})) as a function of n? Explain your answer.

Problem 2. Suppose that we wish to perform a certain computation. It involves the computation of n quantities q_{1}, …, q_{n} such that for each quantity q_{i} we can have several alternative ways of computing it. We assume that each way of computing q_{i} is expressed as an assertion of the one of the following two forms.

                    (CAN-BE-COMPUTED q (APPLY0 f))
                  (CAN-BE-COMPUTED q (APPLY2 f s t))

Assertions of the first form provide a way of computing the quantity q by calling procedure f. Assertions of the first give a way of computing initial quantities — quantities that can be computed without requiring the precomputation of any other quantities. Assertions of the second form state that quantity q can be computed from the values of quantities s and t by calling procedure f on s and t. Each procedure has a cost of computation. The costs of procedures are represented by assertions of the following form.

                            (HAS-COST f c)

The problem is to find the cheapest way of computing a given quantity. For example, consider computing

part a. Let an assertion of the form (≤ q c) represent the statement that q can be computed with cost c or less. Write inference rules involving these bounds that can be used to derive the tightest possible upper bound for the cost of computing each quantity.

part b. Using the results of the paper (and assuming that each operator has nonnegative cost) give the order of running time need to compute C′_{R}(Σ) where this is defined (as in the notes) as the nonredundant assertions in C_{R}(Σ). Your answer should be given in terms of q, the number of quantities to be computed, and n, the number of CAN-BE-COMPUTED formulas in the initial data base.

Problem 3. This problem involves assertions that have semantics independent of any inference rules. This should make the notions of soundness and completeness clear. We consider the problem of data flow analysis and code optimization. Consider expressions generated by the following grammar.

S := (SETQ (THE-VARIABLE C) E) | (PROG S S) | (WHILE B S) | (IF B S
S)
B := (= E E) | (< E E)
E := (THE-VARIABLE C) | (THE-CONSTANT C) | (+ E E) | (* E E)
C := (ZERO) | (TWICE C) | (TWICE+1 C)

For example, the first line of the above grammar states that the set of expressions of type S consist of all assignments of the form (SETQ (THE-VARIABLE C) E) where C is an expression of type C variable and E is an expression of type E, plus all expressions of the form (PROG S S), i.e., an application of PROG to two (possibly different) expressions of type S, and so on. The expression type C is a way of representing all numerals in binary notation. For example (TWICE+1 (ZERO)) represents 1 and

(TWICE (TWICE+1 (TWICE+1 (ZERO)))) represents the number 6.

These expressions have the standard semantics. Each expression of type S is a program that can be executed in an environment. An environment is an assignment of numbers to variables. The result of executing an expression of type S in a given environment is a new environment. An expression of the form (THE-CONSTANT c) denotes the number represented by c. For example, consider the following.

(setq (the-variable (zero))
      (+ (the-variable (zero))
         (the-constant (twice-+ (zero)))))

This increments the given variable by 1. The program (PROG s_{1} s_{2}) first executes s_{1} then executes s_{2}. The program (WHILE b s) repeatedly executes s until b becomes false. If b is false initially then this program does nothing. The program (IF b s_{1} s_{2}) executes s_{1} in the case where b is true and s_{2} in the case where b is false.

We are interested in determining equivalences between programs written in this language. Note that any program is equivalent to an infinite variety of other programs. For example, the above program to increment a variable is equivalent to the following program.

(if (= (the-variable (zero))
       (the-variable (twice+1 (zero))))
     (setq (the-variable (zero))
           (+ (the-variable (zero))
           (the-constant (twice-+ (zero)))))
     (setq (the-variable (zero))
           (+ (the-variable (zero))
           (the-constant (twice-+ (zero))))))

Write a set of inference rules R with the following properties. Recall that ⊢_{R} Φ is an abbreviation for (GOAL! Φ) ⊢_{R} Φ.

• For any finite set Σ the set C_{R}(Σ) is finite and can be computed in polynomial time in the size of Σ.

• If ⊢_{R} (= s_{1} s_{2}) then s_{1} and s_{2} are equivalent programs.

• If ⊢_{R} (COMMUTES s_{1} s_{2}) then ⊢_{R} (= (PROG s_{1} s_{2}) (PROG s_{2} s_{1})). In other words, the programs can be run in either order and the result is the same.

• If v_{1} does not occur in e_{2} and v_{2} does not occur in e_{1} then

                  ⊢_{R} (COMMUTES (SETQ v_{1} e_{1}) (SETQ v_{2} e_{2}))

• If ⊢_{R} (COMMUTES s_{1} s_{2}) for every pair of SETQ expressions s_{1} and s_{2} such that s_{1} occurs in u_{1} and s_{2} occurs in u_{2} then ⊢_{R} (COMMUTES u_{1} u_{2})

You can assume you are given a rule set R′ such that ⊢_{R} (DIFFERENT-VARS v_{1} v_{2}) if and only if v_{1} and v_{2} are distinct variables. This is a rather easy program to write, but it is tedious.

Hint: The key inference rules derive COMMUTES assertions from COMMUTES assertions.

State whether the inference rules you gave are sound and/or complete relative to the intended meaning of equations of the form (= s_{1} s_{2}). Explain your answer. If your rules are not sound given an example of something that is provable but false. If your rules are not complete give an example of something that is true but not provable. If your rules are sound, given an example of an unsound rule under the intended semantics of the assertions.