\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 10}
\medskip
\medskip

\centerline{Due:  Beginning of class Friday, December 3}

{\bf Problem 1.} A {\em 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.

$$\mbox{\tt SUBREL}: (D \times D \rightarrow B) \times (D \times D \rightarrow B) \rightarrow B$$
The assertion {\tt (SUBREL R W)} should be true if {\tt R} is a subrelation of {\tt W},
i.e., if {\tt (W $x$ $y$)} is true for all $x$ and $y$ such that {\tt (R $x$ $y$)} is true.

$$\mbox{\tt REL-COMP}: (D \times D \rightarrow B) \times (D \times D \rightarrow B) \rightarrow (D \times D \rightarrow B)$$
The expression {\tt (REL-COMP R W)} is the relation that is the composition of {\tt R} and
{\tt W}.  More formally, {\tt ((REL-COMP R W) $x$ $y$)} should be true if there is some $z$
such that {\tt (R $x$ $z$)} is true and {\tt (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.

$$\mbox{\tt TRANS}: (D \times D \rightarrow B) \rightarrow B$$
The expression {\tt (TRANS R)} should be true if {\tt R} is transitive.
Your implementation should be of the form {\tt ($\lambda$ ($R$) $\Phi[R]$)}
where $\Phi[R]$ does not contain any $\lambda$-expressions (or quantifiers
which have implicit $\lambda$-expressions) other than the combinators
{\tt SUBREL} and {\tt REL-COMP}.

$$\mbox{\tt REL-UNION}: (D \times D \rightarrow B) \times (D \times D \rightarrow B) \rightarrow (D \times D \rightarrow B)$$
The expression {\tt (REL-UNION R W)} is the relation that is the relation union of {\tt R} and
{\tt W}.  More formally, {\tt ((REL-UNION R W) $x$ $y$)} should be true if either
{\tt (R $x$ $y$)} is true or {\tt (W $x$ $y$)} is true.

$$\mbox{\tt KLEENE-STAR}: (D \times D \rightarrow B) \rightarrow (D \times D \rightarrow B)$$
The expression {\tt (KLEENE-STAR R)} the infinite union of the identity relation and
any number of compositions of {\tt R} with itself.  This is equivalent to saying that
{\tt (KLEENE-STAR R)} is the least transitive relation containing the identity relation
and {\tt R}.  Hint:  The answer is a $\lambda$-expression of the form
$$\mbox{($\lambda$ ($r$) ($\lambda$ ($x$ $y$) $\exists$ $r'$ ``$r' = r^*$ and ($r'$ $x$ $y$)''))}$$

%\item $$\mbox{\tt CLOSED} : (D \rightarrow B) \times (D \rightarrow D) \rightarrow B$$
%The assertion {\tt (CLOSED S F)} should be true if the set represented
%by {\tt S} is closed under application of the function {\tt F}.  For example, the set
%if integers is closed under the square function (which takes the square of its input)
%but not under the square root function.  In higher order logic all sets are represented
%by ``characteristic functions'', i.e., by predicates that are true on the elements of
%those sets.  More formally, {\tt (CLOSED S F)} should be true if {\tt (S (F x))}
%is true for any x such that {\tt (S x)} is true.
%Give a term of higher order logic representing the combinator {\tt CLOSED}.
%
%\item $$\mbox{\tt CLOSURE}: (D \rightarrow B) \times (D \rightarrow D) \rightarrow (D \rightarrow B)$$
%The expression {\tt (CLOSURE S F)} should denote the closure of the set under tue function F.
%For example, the closure of the set $\{0\}$ under the successor function is the set of
%natural numbers.  More formally, the expression {\tt (CLOSURE S F)} should denote the
%least set {\tt W} shuch that {\tt W} contains {\tt S} and {\tt W} is closed under {\tt F}.
%Give a term of higher order logic representing the combinator {\tt CLOSURE}.
%

$$\mbox{\tt APPLY}: (D \times D \rightarrow B) \times (D \rightarrow B) \rightarrow (D \rightarrow B)$$
The expression {\tt (APPLY R S)} should denote the ``application'' of the relation {\tt R} to
the set {\tt S}.  More formally {\tt (APPLY R S)} should denote the set of individuals $y$
such that there exits an individual $x$ such that {\tt (S $x$)} and {\tt (R $x$ $y$)} are
both true.

$$\mbox{\tt EVERY}: (D \rightarrow B) \rightarrow (D \rightarrow B) \rightarrow B$$
The assertion {\tt ((EVERY P) Q)} should be true if {\tt P} is a subset of {\tt Q}.
More formally, {\tt ((EVERY P) Q)} should be true if {\tt (Q $x$)} is true for every $x$
such that {\tt (P $x$)} is true.

$$\mbox{\tt SOME}: (D \rightarrow B) \rightarrow (D \rightarrow B) \rightarrow B$$
The assertion {\tt ((SOME P) Q)} should be true if the set {\tt P} intersects the set {\tt Q}.
More formally, {\tt ((SOME P) Q)} should be true if there is some $x$ such that
{\tt (Q $x$)} and {\tt (P $x$)} are both true.

{\bf Problem 2.}  We define a ``quantifier'' to be an object of type
$(D \rightarrow B) \rightarrow B$.  For example, {\tt (EVERY BIRD)}
is a quantifier.  Modify the combinator {\tt APPLY} so that it takes
a quantifier as an argument and such that {\tt (APPLY R (SOME P))}
is the set of $y$ such that there exists an $x$ such that
{\tt (P $x$)} and {\tt (R $x$ $y$)} and {\tt (APPLY R (EVERY P))}
is the set of $y$ such that for all $x$ such that {\tt (P $x$)}
we have {\tt (R $x$ $y$)}.  Your solution should have the property
that {\tt ((SOME WOMAN) (APPLY LIKES (EVERY MAN)))} has a
meaning that is one of the intuitive meanings of the sentence
``some woman likes every man''.

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

{\bf 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 \rightarrow B$ or $D \times D \rightarrow
B$ and whose only quantifiers, i.e., expressions of the form $\forall_\tau$
or $\exists_\tau$, only quantify over $D$, i.e., are of the form $\forall_D$
or $\exists_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 type $D$ and that there are only finitely many elements of the set
denoted by $D$.  If $f$ is a constants of type $D \rightarrow B$ or $D \times D \rightarrow 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.

\begin{itemize}

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

\item $V[(f\;t)] = M(f)[V[t]]$ where $f$ is a constant of type $D \rightarrow B$ and
$t$ is a term of type $D$.

\item $V[(f\;t\;w)] = M(f)[V[t],\;V[w]]$ where $f$ is a constant of type $D \times D \rightarrow B$ and
$t$ is a term of type $D$.

\item $V[\mbox{($\lambda$ ($x_1$ $\ldots$ $x_n$) $b[x_1\;\ldots\;x_n]$)}]$ = ($\lambda$ ($x_1$ $\ldots$ $x_n$) $b[x_1\;\ldots\;x_n]$)

\item $V[\mbox{(($\lambda$ ($x_1$ $\ldots$ $x_n$) $b[x_1\;\ldots\;x_n]$) $u_1$ $\ldots$ $u_n$)}]$ = ?

\item $V[\mbox{($\forall_D$ ($\lambda$ ($x$) $\Phi[x]$))}]$ = ?

\item $V[\mbox{($\exists_D$ ($\lambda$ ($x$) $\Phi[x]$))}]$ = ?

\item $V[\mbox{(($s$ $w_1$ $\ldots$ $w_m$) $u_1$ $\ldots$ $u_n$)}]$ = ?
\end{itemize}

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

\begin{itemize}
\item  {\tt ((EVERY P) Q)}

\item  {\tt ((SOME P) Q)}

\item  {\tt ((EVERY P) (APPLY R (SOME Q)))}

\item  {\tt ((SOME P) (APPLY R (EVERY (APPLY W (SOME Q)))))}

\item  {\tt ((EVERY (APPLY R (SOME P))) Q)}
\end{itemize}

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

\eqruleii{a}{\mbox{\tt (SUBREL ?R ?W)}}
{\mbox {\tt (SUBREL ?W ?R)}}

\eqrulei{b}{{\mbox{\tt (SUBREL ?R ?R)}}}

\eqruleiii{c}{\mbox{\tt (SUBREL ?R ?W)}}
{\mbox{\tt (SUBREL ?W ?U)}}
{\mbox{\tt (SUBREL ?R ?U)}}

\eqrulei{d}{{\mbox{\tt (SUBREL ?R (REL-COMP ?R ?R))}}}

\eqrulei{e}{{\mbox{\tt (SUBREL ?R (REL-UNION ?R ?W))}}}

\eqrulei{e}{{\mbox{\tt (SUBREL ?R (KLEENE-STAR ?R))}}}

\eqruleii{f}{\mbox{\tt ((EVERY (APPLY ?R ?U)) ?U)}}
{\mbox{\tt ((EVERY (APPLY (KLEENE-STAR ?R) ?U)) ?U)}}

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

\end{document}