\input psadobe
\documentstyle[12pt,epsf]{report}
\newcommand{\bigcenter}[1]{\begin{center} {\Large\bf #1} \end{center}}
\setlength{\oddsidemargin}{.25in}       
\setlength{\evensidemargin}{.25in}
\setlength{\textwidth}{6in}
\setlength{\topmargin}{-0.4in}          
\setlength{\textheight}{8.5in}

\parskip=2ex

\parindent=0ex

\newcommand{\necpos}[1]{[\langle #1 \rangle]}

\input nofill.tex
\input texcom.tex

\begin{document}
\centerline{\bf \large 6.824 Artificial Intelligence, Fall 1993}
\centerline{\bf \large Problem Set 5}
\medskip
\medskip

\centerline{Due:  Beginning of class Wednesday, October 20}


{\bf 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 {\tt (THE-VARIABLE $x$)} where $x$ is
an expression representing the name of the variable.
Constants are represented by expressions of the form {\tt (THE-CONSTANT $x$)} where
$x$ is the name of the constant.  An operator is an expression of the form
{\tt (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 {\tt (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.

\begin{code}
(apply (the-operator +)
       (apply (the-operator *)
              (the-constant a)
              (the-variable x))
       (the-constant b))
\end{code}

{\bf part a.} Write a set of inference rules for proving formulas of the form
{\tt (ARITH-EXP $y$)} where this assertion means that $y$ is an expression
as defined above.  Your rule set $R$ should have the property that $\subproves{R} \mbox{\tt (ARITH-EXP $y$)}$
if and only if $y$ is an arithmetic expression as defined above.
(The notation $\subproves{R} \Phi$ means that $\Phi$ 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 {\tt (OPERATOR $f$)}
so that new operators can be added easily.

{\bf part b.}  Write a set of inference rules for deriving assertions of the form
{\tt (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
$\subproves{R} \mbox{\tt (occurs-in $x$ $y$)}$ if and only if $y$ is an expression
and $x$ is a variable that occurs in $y$.

{\bf 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(\Sigma) = \{\Phi: \Sigma \subproves{R} \Phi\}$

{\bf part d.} Modify the rules to use an input assertion of the form {\tt (INPUT! $x$)}
so that
\begin{itemize}
\item $\mbox{\tt (INPUT! $y$)} \subproves{R} \mbox{\tt (ARITH-EXP $y$)}$
if and only if $y$ is an arithmetic expression.

\item $\mbox{\tt (INPUT! $y$)} \subproves{R} \mbox{\tt (OCCURS-IN $x$ $y$)}$
if and only if $x$ is a variable, $y$ is an arithmetic expression, and $x$ occurs
in $y$.

\item For any finite set $\Sigma$, the set $C_R(\Sigma)$ is finite.
\end{itemize}

{\bf part e.} Give the order of running time for computing $C_R(\Sigma)$
where $\Sigma$ 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.

{\bf part f.} Suppose we define the expression $e_n$ by $e_0 = \mbox{\tt (THE-VARIABLE (X))}$
and $e_{n+1} = \mbox{\tt (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(\mbox{\tt (INPUT! $e_n$)})$ as a function of $n$?  Explain your answer.

{\bf Problem 2.}  Suppose that we wish to perform a certain computation.  It involves
the computation of $n$ quantities $q_1$, $\ldots$, $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.

$$\mbox{\tt (CAN-BE-COMPUTED $q$ (APPLY0 $f$))}$$
$$\mbox{\tt (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.

$$\mbox{\tt (HAS-COST $f$ $c$)}$$

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

{\bf part a.} Let an assertion of the form {\tt ($\leq$ $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.

{\bf 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(\Sigma)$
where this is defined (as in the notes) as the nonredundant assertions in $C_R(\Sigma)$.
Your answer should be given in terms of $q$, the number of quantities to be computed,
and $n$, the number of {\tt CAN-BE-COMPUTED} formulas in the initial data base.

{\bf 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.

\begin{code}
$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$)
\end{code}

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 {\tt (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 {\tt (PROG $S$ $S$)}, i.e., an application of {\tt 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
{\tt (TWICE+1 (ZERO))} represents 1 and {\tt (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 {\tt (THE-CONSTANT $c$)} denotes
the number represented by $c$.  For example, consider the following.

\begin{code}
(setq (the-variable (zero))
      (+ (the-variable (zero))
         (the-constant (twice-+ (zero)))))
\end{code}

This increments the given variable by 1.
The program {\tt (PROG $s_1$ $s_2$)} first executes $s_1$ then executes $s_2$.
The program {\tt (WHILE $b$ $s$)} repeatedly executes $s$ until $b$ becomes false.
If $b$ is false initially then this program does nothing.  The program
{\tt (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.

\vfill

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.

\eject

\begin{code}
(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))))))
\end{code}

Write a set of inference rules $R$ with the following properties.
Recall that $\submcfproves{R} \Phi$ is an abbreviation for
$\mbox{\tt (GOAL! $\Phi$)} \subproves{R} \Phi$.

\begin{itemize}
\item For any finite set $\Sigma$ the set $C_R(\Sigma)$ is finite and can be computed in
polynomial time in the size of $\Sigma$.

\item If $\submcfproves{R} \mbox{\tt (= $s_1$ $s_2$)}$ then $s_1$
and $s_2$ are equivalent programs.

\item If $\submcfproves{R} \mbox{\tt (COMMUTES $s_1$ $s_2$)}$ then
$\submcfproves{R} \mbox{\tt (= (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.

\item If $v_1$ does not occur in $e_2$ and $v_2$ does not occur in $e_1$ then
$$\submcfproves{R} \mbox{\tt (COMMUTES (SETQ $v_1$ $e_1$) (SETQ $v_2$ $e_2$))}$$

\item If $\submcfproves{R} \mbox{\tt (COMMUTES $s_1$ $s_2$)}$ for every pair of
{\tt SETQ} expressions $s_1$ and $s_2$ such that $s_1$ occurs in $u_1$ and $s_2$
occurs in $u_2$ then $\submcfproves{R} \mbox{\tt (COMMUTES $u_1$ $u_2$)}$
\end{itemize}

You can assume you are given a rule set $R'$ such that
$\submcfproves{R} \mbox{\tt (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 {\tt COMMUTES} assertions from {\tt COMMUTES}
assertions.

State whether the inference rules you gave are sound and/or complete
relative to the intended meaning of equations of the form {\tt (= $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.

\end{document}