\documentstyle[12pt, epsf]{article}
\pagestyle{empty}
\input nofill.tex
\input texcom.tex
\headsep=.5in
\parindent=0ex
\textwidth=7.0in
\oddsidemargin=-.5in

\pagestyle{empty}
\newcommand{\determined}[1]{\mbox{\tt (at-most-one $#1$)}}
\newcommand{\is}[2]{\mbox{\tt (every $#1$ $#2$)}}
\newcommand{\ist}[2]{\mbox{\tt (every #1 #2)}}
\newcommand{\exsts}[1]{\mbox{\tt (exists-a $#1$)}}
\newcommand{\inter}[2]{\mbox{\tt (some $#1$ $#2$)}}
\newcommand{\preserves}[2]{\mbox{\tt (preserves $#1$ $#2$)}}

%the following are different from those in texcom (larger font)

\def\eqruleiv#1#2#3#4#5{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
                 \> $#3$ \\
                 \> $#4$ \\
                 \> \parbox{1.5in}{\noindent \hrule \mbox{~}} \\
                 \> $#5$
\end{tabbing}}}

\def\eqruleiii#1#2#3#4{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
                 \> $#3$ \\
                 \> \parbox{1.5in}{\noindent \hrule \mbox{~}} \\
                 \> $#4$
\end{tabbing}}}

\def\eqruleii#1#2#3{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
                 \> \parbox{1.5in}{\noindent \hrule \mbox{}} \\
                 \> $#3$
\end{tabbing}}}

\def\eqrulei#1#2{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ 
\end{tabbing}}}

\newcommand{\slide}[1]{\vfill
\eject
\centerline{\bf #1}
\vfill}




\begin{document}

{\Large

\centerline{\bf DESCRIPTIVE COMPLEXITY THEORY}
\centerline{and}
\centerline{\bf PROGRAMMING LANGUAGE DESIGN}

\vfill

\centerline{David McAllester}
\centerline{MIT Artificial Intelligence Laboratory}

\vfill
\vfill

\slide{\bf Bottom-Up Logic Programming}

We define an {\em expression} by the following grammar:

\vfill

$$e ::= x \;\;| \;\; f(e_1, \ldots, e_n) \;\;\mbox{where f has arity $n$}$$

\vfill
\vfill

An {\em inference rule} consists of a set of antecedent expressions and a conclusion expression.

\vfill
\eqruleiv{}{A_1}{\vdots}{A_2}{C}

\vfill
\vfill

$\Sigma\subproves{R}\Phi$ means $\Phi$ is provable from $\Sigma$ using rules $R$.

\slide{\bf Transitive Closure}

\eqruleii{}{\mbox{\tt ARC(?X, ?Y)}}
{\mbox{\tt PATH(?X, ?Y)}}

\vfill

\eqruleiii{}{\mbox{\tt ARC(?X, ?Y)}}
{\mbox{\tt PATH(?Y, ?Z)}}
{\mbox{\tt PATH(?X, ?Z)}}

\vfill
$G \subproves{R} \mbox{\tt PATH(A, B)}$ iff there is a path from A to B in the graph $G$.

\vfill
A general rule compiler can convert the above rules to an $O(en)$ algorithm
for an $e$ edge $n$ node graph.
 
\slide{\bf Context Free Parsing I}

Assume a Chomsky normal form grammar with productions of the form

\vfill
$$A \rightarrow BC$$
$$A \rightarrow c$$

\vfill
Assume these productions are represented by assertions in the data base of
the form

\vfill
$$\mbox{\tt PRODUCTION(A, B, C)}$$
$$\mbox{\tt TERMINAL-PRODUCTION(A, c)}$$

\vfill
For nonterminal {\tt A} and strings $x$ and $y$, the assertion {\tt REMOVE(A, $x$, $y$)} means that
removing a prefix of type $A$ from $x$ results in $y$.

\slide{\bf Context Free Parsing II}

\vspace{-.3in}

\sidebyside{
\eqruleiii{}
{\mbox{\tt TERMINAL-PRODUCTION(?A, ?T)}}
{\mbox{\tt INPUT!(CONS(?T, ?X))}}
{\mbox{\tt REMOVE(?A, CONS(?T, ?X), ?X)}}

\vspace{.5in}

\eqruleii{}{\mbox{{\tt INPUT!}(CONS(?X, ?Y))}}
{\mbox{\tt INPUT!(?Y)}}
}{
\eqruleiv{}
{\mbox{\tt PRODUCTION(?A, ?B, ?C)}}
{\mbox{\tt REMOVE(?B, ?X, ?Y)}}
{\mbox{\tt REMOVE(?C, ?Y, ?Z)}}
{\mbox{\tt REMOVE(?A, ?X, ?Z)}}

\vspace{.25in}

\eqruleii{}
{\mbox{\tt REMOVE(?A, ?X, (NIL))}}
{\mbox{\tt PARSES-AS(?X, ?A)}}
}

\vfill
$G,\mbox{\tt INPUT!(?X)}\subproves{R}\mbox{\tt PARSES-AS(?X, ?A)}$ iff the string {\tt ?X}
parses as nonterminal {\tt ?A} under the grammar $G$.

\vfill
A general purpose rule compiler converts these rules to an $O(gn^3)$ algorithm
where $g$ is the number of productions in the grammar and $n$ is the length
of the input string.

\slide{\bf The Order Theorem I}

Let $\Sigma$ be a data base of premises and let $R$ be a set of rules.

\bigskip
$C_R(\Sigma)\;\; = \;\; \{\Phi:\; \Sigma\subproves{R}\Phi\}$

\vfill
A {\em prefix firing} of a rule
\eqruleiv{}{A_1}{\vdots}{A_2}{C}
in the set $\Gamma$ is a ground instance $A'_1$, $\ldots$ $A'_j$ of the antecedents
$A_1$, $\ldots$, $A_j$ where $j \leq n$ such that each $A_i'$ is a member of $\Gamma$.
Typically $\Gamma$ is $C_R(\Sigma)$.

\slide{\bf Order theorem II}

For example, consider the following rule.

\vfill
\eqruleiv{}
{\mbox{\tt (PRODUCTION ?A ?B ?C)}}
{\mbox{\tt (REMOVE ?B ?X ?Y)}}
{\mbox{\tt (REMOVE ?C ?Y ?Z)}}
{\mbox{\tt (REMOVE ?A ?X ?Z)}}

\vfill
The pair of assertions
\begin{code}
(PRODUCTION S NP VP)
\medskip
(REMOVE NP
        (CONS JOHN (CONS RAN NIL))
        (CONS RAN NIL))
\end{code}

\vfill
is a prefix firing of this rule in the set $C_R(\Sigma)$ provided these two
assertions are both members of $C_R(\Sigma)$.

\slide{\bf Order Theorem III}

{\bf Theorem:} Assuming that hash table operations take unit time
one can compute $C_R(\Sigma)$ in time
proportional to the number of prefix firings of rules in $R$ in
the set $C_R(\Sigma)$.

\vfill
There are $O(en)$ prefix firings in computing transitive closure
of a graph with $e$ edges and $n$ nodes.  Consider

\vfill
\eqruleiii{}{\mbox{\tt (ARC ?X ?Y)}}
{\mbox{\tt (PATH ?Y ?Z)}}
{\mbox{\tt (PATH ?X ?Z)}}

\vfill
There are $e$ prefix firings involving just the first antecedent.
There are at most $en$ firings involving both antecedents. 

\vfill
There are $O(gn^3)$ prefix firings involved in parsing
a string of $n$ symbols using a grammar with $g$ productions.

\slide{\bf Capturing P}

A rule is {\em local} if every proper subexpression of
the conclusion is a proper subexpression of some antecedent.

\vfill
Local rules:

\vfill
\eqruleiii{}{\mbox{\tt (SMALLER ?X ?Y)}}
{\mbox{\tt (SMALLER ?Y ?Z)}}
{\mbox{\tt (SMALLER ?X ?Z)}}

\vfill
\eqruleii{}{\mbox{\tt (= (CONS ?X ?Y) (CONS ?Z ?W))}}
{\mbox{\tt (= ?X ?Z)}}

\vfill
Nonlocal rules:

\vfill
\eqruleii{}{\mbox{\tt (NATNUM ?X)}}
{\mbox{\tt (NATNUM (SUCCESSOR ?X))}}

\vfill
\eqruleii{}{\mbox{\tt (= ?X ?Y)}}
{\mbox{\tt (= (F ?X) (F ?Y))}}

\slide{Capturing P II}

{\bf Definition:} $R \;\; \mbox{\em accepts} \;\;t\;\;\;\mbox{ if}\;\;\;\;\;\mbox{\tt INPUT!}(t)\subproves{R} \mbox{\tt Accept}(t)$.

\vfill
{\bf Theorem:} An expression language over a finite signature is polynomial
time recognizable if and only if it is the language accepted by a syntactically
local rule set.

\slide{\bf Dijkstra Shortest Path}

We introduce a special relation symbol $\leq$ whose second argument
is always a number.

\vfill

We now write Dijkstra Shortest path as follows.

\vfill
\eqruleiii{}{\mbox{\tt SOURCE!(?X)}}
{\mbox{\tt ARC(?X, ?Z, ?D)}}
{\mbox{\tt $\leq$(DISTANCE(?X, ?Z), ?D)}}

\vfill
\eqruleiv{}
{\mbox{\tt SOURCE!(?X)}}
{\mbox{\tt $\leq$(DISTANCE(?X, ?Y), ?D1)}}
{\mbox{\tt ARC(?Y, ?Z, ?D2)}}
{\mbox{\tt $\leq$(DISTANCE(?X, ?Z), +(?D1, ?D2))}}

\vfill
A general rule compiler can convert these rules to an $e \log n$ algorithm where $e$ is
the number of arcs and $n$ is the number of nodes (assuming that we are only
given one source).

\slide{\bf MAP Parsing}

Consider a stochastic grammar.

\hspace{-.5in}\sidebyside{
\eqruleiii{}
{\mbox{\tt TERMINAL-PRODUCTION(?A, ?T, ?W)}}
{\mbox{\tt INPUT!(CONS(?T, ?X))}}
{\mbox{\tt $\leq$(REMOVE(?A, CONS(?T, ?X), ?X), ?W)}}
}{

\eqruleii{}
{\mbox{\tt $\leq$(REMOVE(?A, ?X, NIL), $W$)}}
{\mbox{\tt ($\leq$ PARSES-AS(?X, ?A), $W$)}}
}


\eqruleiv{}{\mbox{\tt PRODUCTION(?A, ?B, ?C, ?W1)}}
{\mbox{\tt $\leq$(REMOVE(?B, ?X, ?Y), ?W1)}}
{\mbox{\tt $\leq$(REMOVE(?C, ?Y, ?Z), ?W2)}}
{\mbox{\tt $\leq$(REMOVE(?A, ?X, ?Z), +(?W1, ?W2, ?W3))}}


\vfill
$G,\mbox{\tt INPUT!(X)}\subproves{R}\mbox{\tt $\leq$(PARSES-AS(X, A), W)}$ iff A generates
the string {\tt X} with finite probability weight {\tt W}.

\vfill
A general purpose rule compiler converts these rules to an
$O(gn^3\log(gn))$ algorithm
where $g$ is the number of productions in the grammar and $n$ is the length
of the input string.

\slide{\bf Order Theorem for Bounds}

{\bf Definition:} A {\em bound assertion} is a formula of the form
{\tt ($\leq$ $e$ $b$)}.

\vfill
{\bf Definition:} A bound assertion {\tt ($\leq$ $s$ $b$)} will be called
{\em redundant} in $C_R(\Sigma)$ if $C_R(\Sigma)$ contains
a bound formula {\tt ($\leq$ $s$ $b'$)} where $b' < b$.

\vfill
{\bf Definition:} $C'_R(\Sigma)$ is the set of nonredundant elements of
$C_R(\Sigma)$ .

\vfill
{\bf Theorem:} Assuming that hash table operations take unit time,
that no conclusion bound is smaller than
any antecedent bound in any given rule firing, and
that any rule with a bound formula antecedent has a bound formula conclusion,
we can compute $C'_R(\Sigma)$ in $c + b \log b$ time
where $c$ is the number of prefix firings of $R$ in $C_r'(\Sigma)$
and $b$ is the number of bound assertions in $C'_R(\Sigma)$.

\vfill

\end{document}