\documentstyle[jair,twoside,11pt,theapa]{article} 
%\input epsf

\newcommand{\yy}[1]{{\it [#1]}}
\newcommand{\zz}[1]{}
\newcommand{\ct}[1]{[cite:#1]}
\newcommand{\shortct}[1]{[year:#1]}
\newcommand{\cut}[1]{}
\newcommand{\cd}[1]{{\it #1}}
\newcommand{\trm}[1]{{\em #1\/}}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{observation}[theorem]{Observation}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newenvironment{proof}{\noindent {\bf Proof:}}{\qed}
\newenvironment{lemmaproof}{\noindent {\bf Proof of lemma:}}{\qed}
%\newenvironment{example}{\begin{center}~\\%
%			 \begin{minipage}{0.9\textwidth}%
%			  \noindent {\bf Example.}}%
% 			{\end{minipage}~\\%
%			\end{center}}
%\newenvironment{example}{\noindent {\bf Example.}}{}
\newenvironment{example}{\begin{quote}{\bf Example.}}{\end{quote}}
\newenvironment{proofsketch}{\noindent {\bf Proof (sketch):}}{\qed}
\newcommand{\qed}{\hfill\rule{0.6em}{0.6em}\vspace{\baselineskip}}
\newenvironment{code}{\begin{tabbing}1234\=\kill}{\end{tabbing}}
\newenvironment{alg}{\begin{tabbing}1234\=1234\=1234\=1234\=1234\=\kill}{\end{tabbing}}
\newcommand{\predict}{\mbox{\sc PacPredict\/}}
\newcommand{\learn}{\mbox{\sc PacLearn\/}}
\newcommand{\ident}{\mbox{\sc Identify\/}}
\newcommand{\size}[1]{\mbox{$|\!|#1|\!|$}} % 
\newcommand{\ext}[2]{{\it ext}(#1,#2)}
\newcommand{\poly}{{\it poly}}
\newcommand{\llang}{\mbox{\sc Lang}}% 
\newcommand{\subcl}{\mbox{\sc Subclause}}% 
\newcommand{\dbset}{\mbox{${\cal DB}$}}
\newcommand{\dbj}[1]{\mbox{$#1$-${\cal DB}$}} % 
\newcommand{\decj}[1]{\mbox{$#1$-${\cal DEC}$}} % 
\newcommand{\db}{{\it DB}} % 
\newcommand{\dec}{{\it Dec}} % 
\newcommand{\decset}{\mbox{${\cal DEC}$}}
\newcommand{\detdec}{\mbox{${\cal D}$\it et${\cal DEC}$}}
\newcommand{\detdecj}[1]{\mbox{$#1$-${\cal D}$\it et${\cal DEC}$}} % 
\newcommand{\decsetj}[1]{\mbox{$#1$-${\cal DEC}$}} % 
\newcommand{\inp}{{\rm in}}
\newcommand{\outp}{{\rm out}}
\newcommand{\maxt}{{n_t}} % size of target
\newcommand{\maxi}{{n_e}} % size of instances
\newcommand{\maxb}{{n_b}} % size of background theory
\newcommand{\maxv}{{n_r}} % size of vocabulary
\newcommand{\deepen}{{\it DEEPEN}} 
\newcommand{\determ}[1]{\mbox{$#1$-{\sc Determinate}}}
\newcommand{\nrdepth}[1]{\mbox{$#1$-{\sc DepthNonRec}}}
\newcommand{\nrlocal}[1]{\mbox{$#1$-{\sc LocalNonRec}}}
\newcommand{\lrlocal}[1]{\mbox{$#1$-{\sc LocalLinRec}}}
\newcommand{\localprog}[3]%
    {\mbox{$#1$-{\sc Local}-$#2$-{\sc Rec}-$#3$-{\sc Clause}}}
\newcommand{\rdepth}[1]{\mbox{$#1$-{\sc DepthRec}}}
\newcommand{\lrdepthprog}[1]{\mbox{$#1$-{\sc DepthLinRecProg}}}
\newcommand{\lrdepth}[1]{\mbox{$#1$-{\sc DepthLinRec}}}
\newcommand{\krdepth}[2]{\mbox{$#1$-{\sc Depth}-$#2$-{\sc Rec}}}
\newcommand{\progtwodepth}[1]{\mbox{$#1$-{\sc Depth}-2-{\sc Clause}}}
\newcommand{\progdepth}[1]{\mbox{$#1$-{\sc Depth}-$n$-{\sc Clause}}}
\newcommand{\constrain}{{\it CONSTRAIN}} 
\newcommand{\clong}{{\it BOTTOM}^{*}}
\newcommand{\blong}{\hat{C}}
\newcommand{\maxlang}{\mbox{$kd$-\sc MaxRecLang}}
\newcommand{\clongd}[1]{{\it BOTTOM}_{#1}^{*}}

\newcommand{\finst}{{f_i}} % instance mapping
\newcommand{\fcon}{{f_c}} % concept mapping
\newcommand{\obar}[1]{\overline{#1}}  
\newcommand{\hcif}{\mbox{$\leftarrow$}}
\newcommand{\reduces}{\mbox{$\;\unlhd\;$}}
\newcommand{\resolves}{\mbox{$\;\sqcap\;$}}
\newcommand{\paramlang}[1]{\mbox{\sc #1}}
\newcommand{\dnf}{\paramlang{Dnf}}
\newcommand{\dfa}{\paramlang{Dfa}}
\newcommand{\monomial}{\paramlang{Monomial}}
\newcommand{\dlog}{\mbox{\sc DLog}}
\newcommand{\modes}[1]{{\it MODES}(#1)}
\newcommand{\act}{\mbox{\it active}}
\newcommand{\inact}{\mbox{\it inactive}}
\newcommand{\mesh}[4]{{\rm MESH}_{{#1},{#2}}({#3},{#4})}


\jairheading{2}{1995}{501-539}{9/94}{5/95}
\ShortHeadings{Pac-Learning Recursive Logic Programs: Efficient Algorithms}
{Cohen}
\firstpageno{501}

\begin{document}


\title{Pac-Learning Recursive Logic Programs: \\Efficient Algorithms}

\author{\name William W. Cohen	\email wcohen@research.att.com \\
	\addr 
	AT\&T Bell Laboratories\\
	600 Mountain Avenue, 
	Murray Hill, NJ 07974 USA}

\maketitle

\begin{abstract}
We present algorithms that learn certain classes of function-free
recursive logic programs in polynomial time from equivalence queries.
In particular, we show that a single $k$-ary recursive constant-depth
determinate clause is learnable. Two-clause programs consisting of one
learnable recursive clause and one constant-depth determinate
non-recursive clause are also learnable, if an additional ``basecase''
oracle is assumed.  These results immediately imply the
pac-learnability of these classes.  Although these classes of
learnable recursive programs are very constrained, it is shown in a
companion paper that they are maximally general, in that generalizing
either class in any natural way leads to a computationally difficult
learning problem.  Thus, taken together with its companion paper, this
paper establishes a boundary of efficient learnability for recursive
logic programs.

\end{abstract}

\section{Introduction}

One active area of research in machine learning is learning concepts
expressed in first-order logic. Since most researchers have used some
variant of Prolog to represent learned concepts, this subarea is
sometimes called \trm{inductive logic programming (ILP)} 
\cite{ILPBook92,MuggletonJLP94}.

Within ILP, researchers have considered two broad classes of learning
problems.  The first class of problems, which we will call here
\trm{logic based relational learning} problems, are first-order
variants of the sorts of classification problems typically considered
within AI machine learning community: prototypical examples include
Muggleton {\it et~al.}'s \citeyear{MuggletonPE92} formulation of
$\alpha$-helix prediction, King {\it et~al.}'s
\citeyear{KingPNAS92} formulation of predicting drug activity,
and Zelle and Mooney's \citeyear{ZelleAAAI94} use of ILP techniques
to learn control heuristics for deterministic parsers.  Logic-based
relational learning often involves noisy examples that reflect a
relatively complex underlying relationship; it is a natural extension
of propositional machine learning, and has already enjoyed a number of
experimental successes.

In the second class of problems studied by ILP researchers, the target
concept is a Prolog program that implements some common
list-processing or arithmetic function; prototypical problems from
this class might be learning to append two lists, or to multiply two
numbers.  These learning problems are similar in character to those
studied in the area of automatic programming from examples
\cite{SummersJACM77,BiermannSMC78}, and hence might be appropriately called
\trm{automatic logic programming} problems.  
Automatic logic programming problems are characterized by noise-free
training data and recursive target concepts. Thus a problem that is
central to the enterprise of automatic logic programming---but not,
perhaps, logic-based relational learning---is the problem of learning
{\em recursive\/} logic programs.

The goal of this paper is to formally analyze the learnability of
recursive logic programs in Valiant's \citeyear{ValiantCACM84} model
of pac-learnability, thus hopefully shedding some light on the task of
automatic logic programming.  To summarize our results, we will show
that some simple recursive programs are pac-learnable from examples
alone, or from examples plus a small number of additional ``hints''.
The largest learnable class we identify in a standard learning model
is the class of one-clause constant-depth determinate programs with at
most a constant number of ``closed'' recursive literals.  The largest
learnable class we identify that requires extra ``hints'' is the class
of constant-depth determinate programs consisting of a single
nonrecursive base clause and a single recursive clause from the class
described above.  All of our results are proved in the model of
\trm{identification from equivalence queries}
\cite{AngluinMLJ88,AngluinCOLT89}, which is somewhat stronger than
pac-learnability. Identification from equivalence queries requires
that the target concept be exactly identified, in polynomial time, and
using only a polynomial number of \trm{equivalence queries}.  An
equivalence query asks if a hypothesis program $H$ is equivalent to
the target program $C$; the answer to a query is either ``yes'' or an
adversarily chosen example on which $H$ and $C$ differ.  This model of
learnability is arguably more appropriate for automatic logic
programming tasks than the weaker model of pac-learnability, as it is
unclear how often an approximately correct recursive program 	will be
useful.

Interestingly, the learning algorithms analyzed are different from
most existing ILP learning methods; they all employ an unusual method
of generalizing examples called \trm{forced simulation}.  Forced
simulation is a simple and analytically tractable alternative to other
methods for generalizing recursive programs against examples, such as
$n$-th root finding \cite{MuggletonNthRoot}, sub-unification
\cite{AhaECML94} and recursive anti-unification
\cite{IdestamAlmquistIMLC92}, but it has been only rarely used in
experimental ILP systems \cite{LingTR91}.

The paper is organized as follows.  After presenting some preliminary
definitions, we begin by presenting (primarily for pedagogical
reasons) a procedure for identifying from equivalence queries a single
{\em non-recursive\/} constant-depth determinate clause.  Then, in
Section~\ref{learn one}, we extend this learning algorithm, and the
corresponding proof of correctness, to a simple class of recursive
clauses: the class of ``closed'' linear recursive constant-depth
determinate clauses.  In Section~\ref{learn one extensions}, we relax
some assumptions made to make the analysis easier, and present several
extensions to this algorithm: we extend the algorithm from linear
recursion to $k$-ary recursion, and also show how a $k$-ary recursive
clause and a non-recursive clause can be learned simultaneously given
an additional ``basecase'' oracle.  We then discuss related work and
conclude.

Although the learnable class of programs is large enough to include
some well-known automatic logic programming benchmarks, it is
extremely restricted. In a companion paper \cite{CohenJAIRNeg}, we
provide a number of negative results, showing that relaxing any of
these restrictions leads to difficult learning problems: in
particular, learning problems that are either as hard as learning DNF
(an open problem in computational learning theory), or as hard as
cracking certain presumably secure cryptographic schemes.  Thus, taken
together with the results of the companion paper, our results
delineate a boundary of learnability for recursive logic programs.

Although the two papers are independent, we suggest that readers
wishing to read both this paper and the companion paper read this
paper first.

\section{Background}

In this section we will present the technical background necessary to
state our results.  We will assume, however, that the reader is
familiar with the basic elements of logic programming; readers without
this background are referred to one of the standard texts, for example
\cite{Lloyd}.

\subsection{Logic Programs} \label{lp intro}

Our treatment of logic programs is standard, except that we will
usually consider the body of a clause to be an ordered set of
literals.

For most of this paper, we will consider logic programs without
function symbols---{\it i.e.}, programs written in Datalog.\footnote{This
assumption is made primarily for convenience. In Section~\ref{relax
datalog} we describe how this assumption can be relaxed.} The purpose
of such a logic program is to answer certain questions relative to a
\trm{database}, $\db$, which is a set of ground atomic facts.
(When convenient, we will also think of $\db$ as a conjunction of
ground unit clauses.)  The simplest use of a Datalog program is to
check the status of a \trm{simple instance}.  A \trm{simple instance}
(for a program $P$ and a database $\db$) is a fact $f$.  The pair
$(P,\db)$ is said to \trm{cover} $f$ iff $\db\wedge P\vdash f$.  The
set of simple instances covered by $(P,\db)$ is precisely the minimal
model of the logic program $P\wedge\db$.

In this paper, we will primarily consider \trm{extended instances}
which consist of two parts: an \trm{instance fact} $f$, which is
simply a ground fact, and a \trm{description} $D$, which is a finite
set of ground unit clauses.  An extended instance $e=(f,D)$ is covered
by $(P,\db)$ iff
\[ \db \wedge D \wedge P \vdash f
\]

If extended instances are allowed, then function-free programs are
expressive enough to encode surprisingly interesting programs.  In
particular, many programs that are usually written with function
symbols can be re-written as function-free programs, as the example
below illustrates.

\begin{example} Consider the usual program for appending two 
lists.
\begin{code}
append([$\/$],Ys,Ys).\\
append([X$|$Xs1],Ys,[X$|$Zs1]) $\hcif$ append(Xs1,Ys,Zs1).
\end{code}
One could use this program to classify atomic facts containing
function symbols such as
\cd{append([1,2],[3],[1,2,3])}. 
This program can be rewritten as a Datalog program that classifies
extended instances as follows:
\begin{code}
{\bf Program $P$:}\\
append(Xs,Ys,Ys) $\hcif$ \\
\>null(Xs).\\
append(Xs,Ys,Zs) $\hcif$ \\
\>components(Xs,X,Xs1) $\wedge$\\
\>components(Zs,X,Zs1) $\wedge$\\
\>append(Xs1,Ys,Zs1).\\
~\\
{\bf Database $\db$:}\\
null(nil).
\end{code}
The predicate \cd{components(A,B,C)} means that
\cd{A} is a list with head \cd{B} and tail \cd{C};
thus an extended instance equivalent to 
\cd{append([1,2],[3],[1,2,3])} 
would be
\begin{code}
{\bf Instance fact $f$:}\\
append(list12,list3,list123).\\
~\\
{\bf Description $D$:}\\
components(list12,1,list2).\\
components(list2,2,nil).\\
components(list123,1,list23).\\
components(list23,2,list3).\\
components(list3,3,nil).
\end{code}
\end{example}

We note that using extended instances as examples is closely related
to using ground clauses entailed by the target clause as examples:
specifically, the instance $e=(f,D)$ is covered by $P,\db$ iff
$P\wedge{}\db\vdash{}(f\hcif{}D)$.  As the example above shows, there
is also a close relationship between extended instances and literals
with function symbols that have been removed by ``flattening''
\cite{RouveirolMLJ94,DeRaedtILP94}.
We have elected to use Datalog programs and the model of extended
instances in this paper for several reasons.  Datalog is relatively
easy to analyze.  There is a close connection between Datalog
and the restrictions imposed by certain practical learning systems,
such {\sc FOIL}
\cite{QuinlanMLJ90,QuinlanECML93}, {\sc FOCL} \cite{PazzaniMLJ92}, and
{\sc GOLEM} \cite{MuggletonILP92}.

Finally, using extended instances addresses the following technical
problem.  The learning problems considered in this paper involve
restricted classes of logic programs. Often, the restrictions imply
that the number of simple instances is polynomial; we note that with
only a polynomial-size domain, questions about pac-learnability are
usually trivial.  Requiring learning algorithms to work over the
domain of extended instances precludes trivial learning techniques,
however, as the number of extended instances of size $n$ is
exponential in $n$ even for highly restricted programs.

\subsection{Restrictions on Logic Programs}

In this paper, we will consider the learnability of various restricted
classes of logic programs. Below we will define some of these
restrictions; however, we will first introduce some terminology.  

If $A\hcif B_1\wedge\ldots\wedge B_r$ is an (ordered) definite clause,
then the \trm{input variables} of the literal $B_i$ are those
variables appearing in $B_i$ which also appear in the clause $A\hcif
B_1\wedge\ldots\wedge B_{i-1}$; all other variables appearing in $B_i$
are called \trm{output variables}.  Also, if $A\hcif
B_1\wedge\ldots\wedge B_r$ is a definite clause, then $B_i$ is said to
be a \trm{recursive literal} if it has the same predicate symbol and
arity as $A$, the head of the clause.

\subsubsection{Types of Recursion}

The first set of restrictions concern the type of recursion that is
allowed in a program.  If every clause in a program has at most one recursive
literal, then the program is \trm{linear recursive}. If every clause
in a program has at most $k$ recursive literals, then the program is
\trm{$k$-ary recursive}.  Finally, if every recursive literal in a
program contains no output variables, then we will say that the
program is \trm{closed recursive.}

\subsubsection{Determinacy and Depth} \label{det-sect}

The second set of restrictions are variants of restrictions originally
introduced by Muggleton and Feng \citeyear{MuggletonILP92}.  If
$A\hcif B_1\wedge\ldots\wedge B_r$ is an (ordered) definite clause,
the literal $B_i$ is \trm{determinate} iff for every possible
substitution $\sigma$ that unifies $A$ with some fact $e$ such that
\[ \db\vdash B_1\sigma\wedge\ldots\wedge B_{i-1}\sigma
\]
there is at most one maximal substitution $\theta$ so that $\db\vdash
B_i\sigma\theta$.  A clause is \trm{determinate} if all of its
literals are determinate.  Informally, determinate clauses are those
that can be evaluated without backtracking by a Prolog interpreter.

We also define the \trm{depth} of a variable appearing in a clause
$A\hcif B_1\wedge\ldots\wedge B_r$ as follows.  Variables appearing in
the head of a clause have depth zero.  Otherwise, let $B_i$ be the
first literal containing the variable $V$, and let $d$ be the maximal
depth of the input variables of $B_i$; then the depth of $V$ is $d+1$.
The depth of a clause is the maximal depth of any variable in the
clause.

Muggleton and Feng define a logic program to be $ij$-determinate if it
is is determinate, of constant depth $i$, and contains literals of
arity $j$ or less.  In this paper we use the phrase ``constant-depth
determinate'' instead to denote this class of programs.  Below are
some examples of constant-depth determinate programs, taken from
D\u{z}eroski, Muggleton and Russell
\citeyear{DzeroskiCOLT92}.

\begin{example}
Assuming \cd{successor} is functional, the following program is
determinate. The maximum depth of a variable is one, for the variable
\cd{C} in the second clause, and hence the program is of depth one.
\begin{code}
less\_than(A,B) $\hcif$ successor(A,B).\\ less\_than(A,B) $\hcif$
successor(A,C) $\wedge$ less\_than(C,B).
\end{code}
The following program, which computes
$\left(\begin{array}{c}A\\C\end{array}\right)$, is determinate and of
depth two.
\begin{code}
choose(A,B,C) $\hcif$ \\
\>zero(B) $\wedge$ \\
\>one(C).\\
choose(A,B,C) $\hcif$ \\
\>decrement(B,D) $\wedge$ \\
\>decrement(A,E) $\wedge$ \\
\>multiply(B,C,G) $\wedge$ \\
\>divide(G,A,F) $\wedge$ \\
\>choose(E,D,F).
\end{code}
\end{example}

The program {\sc GOLEM} \cite{MuggletonILP92} learns constant-depth
determinate programs, and related restrictions have been adopted by
several other practical learning systems
\cite{QuinlanIMLW91,LavracAII92,CohenIJCAIWS93}.  The learnability of
constant-depth determinate clauses has also received some formal
study, which we will review in Section~\ref{previous}.

\subsubsection{Mode Constraints and Declarations}

We define the \trm{mode} of a literal $L$ appearing in a clause $C$ to
be a string $s$ such that the initial character of $s$ is the
predicate symbol of $L$, and for $j>1$ the $j$-th character of $s$ is
a ``+'' if the $(j-1)$-th argument of $L$ is an input variable and a
``$-$'' if the $(j-1)$-th argument of $L$ is an output variable.
(This definition coincides with the usual definition of Prolog modes
only when all arguments to the head of a clause are inputs. This
simplification is justified, however, as we are considering only how
clauses behave in classifying extended instances, which are ground.) A
\trm{mode constraint} is simply a set of mode
strings $R=\{s_1,\ldots,s_k\}$, and a clause $C$ is said to
\trm{satisfy} a mode constraint $R$ for $p$ if for every literal
$L$ in the body of $C$, the mode of $L$ is in $R$.

\begin{example} In the following \cd{append} program,
every literal has been annotated with its mode.
\begin{code}
append(Xs,Ys,Ys) $\hcif$ \\
\>null(Xs).  \hspace{1.5in}~\={\it \% mode: $null+$}\\
append(Xs,Ys,Zs) $\hcif$ \\
\>components(Xs,X,Xs1) $\wedge$ \>{\it \% mode: $components+--$}\\
\>components(Zs,X,Zs1) $\wedge$	\>{\it \% mode: $components++-$}\\
\>append(Xs1,Ys,Zs1).		\>{\it \% mode: $append+++$}
\end{code}
The clauses of this program satisfy the following mode
constraint:
\[ \begin{array}{llll}
    \{ & \cd{components}+--, & \cd{components}++-, & \cd{components}+-+, \\ 
       & \cd{components}-++, & \cd{components}+++, & \cd{null}+\\
       & \cd{append}++-,     & \cd{append}+-+, \\
       & \cd{append}-++,     & \cd{append}+++ & \}
   \end{array}
\]
\end{example}

Mode constraints are commonly used in analyzing Prolog code; for
instance, they are used in many Prolog compilers.  We will sometimes
use an alternative syntax for mode constraints that parallels the
syntax used in most Prolog systems: for instance, we may write the
mode constraint ``$\cd{components+--}$'' as
``$\cd{components(+,-,-)}$''.

We define a \trm{declaration} to be a tuple $(p,a',R)$ where $p$ is a
predicate symbol, $a'$ is an integer, and $R$ is a mode constraint.
We will say that a clause $C$ \trm{satisfies} a declaration if the
head of $C$ has arity $a'$ and predicate symbol $p$, and if for every
literal $L$ in the body of $C$ the mode of $L$ appears in $R$.

\subsection{A Model of Learnability}

In this section, we will present our model of learnability.  We will
first review the necessary definitions for a standard learning model,
the model of learning from equivalence queries
\cite{AngluinMLJ88,AngluinCOLT89}, and discuss its relationship to
other learning models.  We will then introduce an extension to this
model which is necessary for analyzing ILP problems.

\subsubsection{Identification From Equivalence Queries}

Let $X$ be a set. We will call $X$ the \trm{domain}, and call the
elements of $X$ \trm{instances}. Define a
\trm{concept} $C$ over $X$ to be a representation of some subset of
$X$, and define a {\em language} $\llang$ to be a set of concepts.  In
this paper, we will be rather casual about the distinction between a
concept and the set it represents; when there is a risk of confusion
we will refer to the set represented by a concept $C$ as the
\trm{extension of $C$}.  Two concepts $C_1$ and $C_2$ with the same
extension are said to be \trm{(semantically) equivalent}.

Associated with $X$ and $\llang$ are two \trm{size complexity
measures}, for which we will use the following notation:
\begin{itemize} 
\item The size complexity of a concept $C\in\llang$ is written $\size{C}$.
\item The size complexity of an instance $e\in X$ is written $\size{e}$. 
\item If $S$ is a set, $S_n$ stands for the set of all
elements of $S$ of size complexity no greater than $n$.
For instance, $X_n=\{e\in X:\size{e}\leq n\}$ and
$\llang_n=\{C\in\llang:\size{C}\leq n\}$.
\end{itemize} 
We will assume that all size measures are polynomially related to the
number of bits needed to represent $C$ or $e$.

The first learning model that we consider is the model of
\trm{identification with equivalence queries}. The
goal of the learner is to \trm{identify} some unknown
\trm{target concept} $C\in\llang$---that is, to
construct some hypothesis $H\in\llang$ such that $H\equiv C$.
Information about the target concept is gathered only through
\trm{equivalence queries}.  The input to an \trm{equivalence query for
$C$} is some hypothesis $H\in\llang$.  If $H\equiv C$, then the
response to the query is ``yes''. Otherwise, the response to the query
is an arbitrarily chosen \trm{counterexample}---an instance $e$ that
is in the symmetric difference of $C$ and $H$.

A deterministic algorithm \ident{} \trm{identifies \llang{}
>from equivalence queries} iff for every $C\in\llang$, whenever
\ident{} is run (with an oracle answering equivalence queries for $C$)
it eventually halts and outputs some $H\in\llang$ such that $H\equiv
C$. 
\ident{} \trm{polynomially identifies \llang{}
>from equivalence queries} iff there is a polynomial
$\poly(\maxt,\maxi)$ such that at any point in the execution of
\ident{} the total running time is bounded by $\poly(\maxt,\maxi)$,
where $\maxt=\size{C}$ and $\maxi$ is the size of the largest
counterexample seen so far, or $0$ if no equivalence queries have been
made.  

\subsubsection{Relation to Pac-Learnability}

The model of identification from equivalence queries has been
well-studied \cite{AngluinMLJ88,AngluinCOLT89}.  It is known that if a
language is learnable in this model, then it is also learnable in
Valiant's \citeyear{ValiantCACM84} model of pac-learnability.  (The
basic idea behind this result is that an equivalence query for the
hypothesis $H$ can be emulated by drawing a set of random examples of
a certain size.  If any of them is a counterexample to $H$, then one
returns the found counterexample as the answer to the equivalence
query. If no counterexamples are found, one can assume with high
confidence that $H$ is approximately equivalent to the target
concept.)  Thus identification from equivalence queries is a strictly
stronger model than pac-learnability.

Most existing positive results on the pac-learnability of logic
programs rely on showing that every concept in the target language can
be emulated by a boolean concept from some pac-learnable class
\cite{DzeroskiCOLT92,CohenAAAI94Local}.  While
such results can be illuminating, they are also disappointing, since
one of the motivations for considering first-order representations in
the first place is that they allow one to express concepts that cannot
be easily expressed in boolean logic.  One advantage of studying the
exact identification model and considering recursive programs is that
it essentially precludes use of this sort of proof technique: while
many recursive programs can be approximated by boolean functions over
a fixed set of attributes, few can be be exactly emulated by boolean
functions.

\subsubsection{Background Knowledge in Learning}

The framework described above is standard, and is one possible
formalization of the usual situation in inductive concept learning, in
which a user provides a set of examples (in this case counterexamples
to queries) and the learning system attempts to find a useful
hypothesis.  However, in a typical ILP system, the setting is slightly
different, as usually the user provides clues about the target concept
in addition to the examples. In most ILP systems the user provides a
database $\db$ of ``background knowledge'' in addition to a set of
examples; in this paper, we will assume that the user also provides a
{declaration}.  To account for these additional inputs it is necessary
to extend the framework described above to a setting where the learner
accepts inputs other than training examples.

To formalize this, we introduce the following notion of a ``language
family''.  If $\llang$ is a set of clauses, $\db$ is a database and
$\dec$ is a declaration, we will define $\llang[\db,\dec]$ to be the
set of all pairs $(C,\db)$ such that $C\in\llang$ and $C$ satisfies
$\dec$. Semantically, such a pair will denote the set of all extended
instances $(f,D)$ covered by $(C,\db)$.  Next, if $\dbset$ is a set of
databases and $\decset$ is a set of declarations, then define
\[ \llang[\dbset,\decset] = 
     \{ \llang[\db,\dec] : \db\in\dbset\mbox{~and~}\dec\in\decset \}
\]
This set of languages is called a \trm{language family}.

We will now extend the definition of identification from equivalence
queries to language families as follows.  A language family
$\llang[\dbset,\decset]$ is \trm{identifiable from equivalence
queries} iff every language in the set is identifiable from
equivalence queries.  A language family $\llang[\dbset,\decset]$ is
\trm{uniformly identifiable from equivalence queries} iff there is a
single algorithm $\ident(\db,\dec)$ that identifies any language
$\llang[\db,\dec]$ in the family given $\db$ and $\dec$.

\begin{sloppypar}
Uniform polynomial identifiability of a language family is defined
analogously: $\llang[\dbset,\decset]$ is
\trm{uniformly polynomially identifiable from equivalence queries} iff
there is a polynomial time algorithm $\ident(\db,\dec)$ that
identifies any language $\llang[\db,\dec]$ in the family given $\db$
and $\dec$.  Note that $\ident$ must run in time polynomial in the
size of the inputs $\dec$ and $\db$ as well as the target concept.  
\end{sloppypar}

\subsubsection{Restricted Types of Background Knowledge}

We will now describe a number of restricted classes of databases and
declarations.

One restriction which we will make throughout this paper is to assume
that all of the predicates of interest are of bounded arity.  We will
use the notation $\dbj{a}$ for the set of all databases that contain
only facts of arity $a$ or less, and the notation $\decj{a}$ for
the set of all declarations $(p,a',R)$ such that every string
$s\in{}R$ is of length $a+1$ or less.

For technical reasons, it will often be convenient to assume that a
database contains an \trm{equality predicate}---that is, a predicate
symbol {\it equal} such that ${\it equal}(t_i,t_i)\in\db$ for every
constant $t_i$ appearing in $\db$, and ${\it
equal}(t_i,t_j)\not\in\db$ for any $t_i\not=t_j$.  Similarly, we will
often wish to assume that a declaration allows literals of the form
\cd{equal(X,Y)}, where $X$ and $Y$ are input variables.  If $\dbset$
(respectively $\decset$) is any set of databases (declarations) we
will use $\dbset^=$ ($\decset^=$) to denote the corresponding set,
with the additional restriction that the database (declaration) must
contain an equality predicate (respectively the mode 
$\cd{equal(+,+)}$).

It will sometimes also be convenient to assume that a declaration $(p,a',R)$
allows only a single valid mode for each predicate: {\it i.e.}, that
for each predicate $q$ there is in $R$ only a single mode constraint
of the form $q\alpha$.  Such a declaration will be called a
\trm{unique-mode} declaration.  If $\decset$ is any set of
declarations we will use $\decset^1$ to denote the corresponding set
of declarations with the additional restriction that the declaration
is unique-mode.

Finally, we note that in a typical setting, the facts that appear in
a database $\db$ and descriptions $D$ of extended instances are not
arbitrary: instead, they are representative of some ``real'' predicate
({\it e.g.}, the relationship of a list to its \cd{components} in the
example above).  One way of formalizing this is assume that all facts
will be drawn from some restricted set ${\cal F}$; using this assumption
one can define the notion of a \trm{determinate mode}.  If
$f=p(t_1,\ldots,t_k)$ is a fact with predicate symbol $p$ and
$p\alpha$ is a mode, then define
\( {\it inputs}(f,p\alpha) 
\) 
to be the tuple $\langle t_{i_1},\ldots,t_{i_k}\rangle$,
where ${i_1}$, \ldots, $i_k$ are the indices of $\alpha$ containing a 
``$+$''. Also define
\( {\it outputs}(f,p\alpha) 
\) 
to be the tuple 
$\langle t_{j_1},\ldots,t_{j_l}\rangle$, where ${j_1}$, \ldots,
$j_l$ are the indices of $\alpha$ containing a ``$-$''. A mode string
$p\alpha$ for a predicate $p$ is
\trm{determinate for ${\cal F}$} iff the relation
\[ \{\langle {\it inputs}(f,p\alpha),{\it outputs}(f,p\alpha)\rangle : 
	f\in{}{\cal F} \}
\] 
is a function.  Informally, a mode is determinate if the input
positions of the facts in ${\cal F}$ functionally determine the output
positions.

The set of all declarations containing only modes determinate for
${\cal F}$ will be denoted $\detdec_{\cal F}$.  However, in this
paper, the set ${\cal F}$ will be assumed to be fixed, and thus we
will generally omit the subscript.

A program consistent with a determinate declaration $\dec\in\detdec$
must be determinate, as defined above; in other words, consistency
with a determinate declaration is a sufficient condition for semantic
determinacy.  It is also a condition that can be verified with a
simple syntactic test.

\subsubsection{Size Measures for Logic Programs}

Assuming that all predicates are arity $a$ or less for some constant
$a$ also allows very simple size measures to be used.  In this paper,
we will measure the size of a database $\db$ by its cardinality; the
size of an extended instance $(f,D)$ by the cardinality of $D$; the
size of a declaration $(p,a',R)$ by the cardinality of $R$; and the
size of a clause $A\hcif{}B_1\wedge\ldots\wedge{}B_r$ by the number of
literals in its body.

\section{Learning a Nonrecursive Clause} \label{learn nonrec}

The learning algorithms presented in this paper all use a
generalization technique which we call \trm{forced simulation.} By way
of an introduction to this technique, we will consider a learning
algorithm for non-recursive constant-depth clauses.  While this result
is presented primarily for pedagogical reasons, it may be of interest
on its own: it is independent of previous proofs of the
pac-learnability of this class \cite{DzeroskiCOLT92}, and it is also
somewhat more rigorous than previous proofs.

\begin{sloppypar}
Although the details and analysis of the algorithm for non-recursive
clauses are somewhat involved, the basic idea behind the algorithm is
quite simple.  First, a highly-specific ``bottom clause'' is
constructed, using two operations that we call $\deepen$ and
$\constrain$.  Second, this bottom clause is generalized by deleting
literals so that it covers the positive examples: the algorithm for
generalizing a clause to cover an example is (roughly) to simulate the
clause on the example, and delete any literals that would cause the
clause to fail.  In the remainder of this section we will describe and
analyze this learning algorithm in detail.
\end{sloppypar}

\subsection{Constructing a ``Bottom Clause''}

Let $\dec=(p,a',R)$ be a declaration and let $A\hcif
B_1\wedge\ldots\wedge B_r$ be a definite clause.  We define
\[ \deepen_{\dec}(A\hcif B_1\wedge\ldots\wedge B_r) \equiv
           A\hcif B_1\wedge\ldots\wedge B_r 
	          \wedge (\bigwedge_{L_i\in {\cal L}_D} L_i)
\]
where ${\cal L}_D$ is a maximal set of literals $L_i$ that satisfy the
following conditions:
\begin{itemize}
\item the clause $A\hcif B_1\wedge\ldots\wedge{}B_r\wedge{}L_i$
satisfies the mode constraints given in $R$; 

\item if $L_i\in{\cal L}_D$ has the same mode and predicate symbol as
some other $L_j\in{\cal L}_D$, then the input variables of $L_i$ are
different from the input variables of $L_j$;
\item every $L_i$ has at least one output variable, and 
the output variables of $L_i$ are all different from each other, and
are also difference from the output variables of any other
$L_j\in{\cal L}_D$.
\end{itemize}

As an extension of this notation, we define $\deepen_{\dec}^i(C)$ to
be the result of applying the function $\deepen_{\dec}$ repeatedly
$i$ times to $C$, {\it i.e.},
\[
  \deepen^i_{\dec}(C) \equiv 
  	\left\{  \begin{array}{ll}
		  C & \mbox{if $i=0$} \\
		  \deepen_{\dec}(\deepen^{i-1}_{\dec}(C)) & \mbox{otherwise}
		  \end{array}
	\right.
\]
We define the function $\constrain_{\dec}$ as 
\[ \constrain_{\dec}(A\hcif B_1\wedge\ldots\wedge B_r) \equiv
    A\hcif B_1\wedge\ldots\wedge B_r 
	   \wedge (\bigwedge_{L_i\in {\cal L}_C} L_i)
\]
where ${\cal L}_C$ is the set of all literals $L_i$ such that $A\hcif
B_1\wedge\ldots\wedge B_r\wedge{}L_i$ satisfies the mode constraints
given in $R$, and $L_i$ contains no output variables.

\begin{example}
Let $D0$ be the declaration $(p,2,R)$ where $R$ contains the mode
constraints $\cd{mother(+,-)}$, $\cd{father(+,-)}$, $\cd{male(+)}$,
$\cd{female(+)}$, and $\cd{equal(+,+)}$.  Then
\begin{tabbing}123\=123\=\kill
$\deepen_{D0}(\mbox{\small p(X,Y)$\hcif$}) \equiv$\\
\>{\small p(X,Y)$\hcif${mother(X,XM)}$\wedge${father(X,XF)}$\wedge$
               {mother(Y,YM)}$\wedge${father(Y,YF)} }\\
\ \\
$\deepen^2_{D0}(\mbox{\small p(X,Y)$\hcif$}) \equiv$ 
	$\deepen_{D0}(\deepen_{D0}(\mbox{\small p(X,Y)$\hcif$})) \equiv$ \\
\>{\small p(X,Y)$\hcif$}\\ 
\>\>{\small {mother(X,XM)}$\wedge${father(X,XF)}$\wedge$
	    {mother(Y,YM)}$\wedge${father(Y,YF)}$\wedge$}\\
\>\>{\small {mother(XM,XMM)}$\wedge${father(XM,XMF)}$\wedge$
	    {mother(XF,XFM)}$\wedge${father(XF,XFF)}$\wedge$}\\
\>\>{\small {mother(YM,YMM)}$\wedge${father(YM,YMF)}$\wedge$
	    {mother(YF,YFM)}$\wedge${father(YF,YFF)}}\\
\ \\
$\constrain_{D0}(\deepen_{D0}(\mbox{\small p(X,Y)$\hcif$})) \equiv$\\
\>{\small p(X,Y)$\hcif$}\\
\>\>{\small mother(X,XM)$\wedge${father(X,XF)}$\wedge$
            {mother(Y,YM)}$\wedge${father(Y,YF)}$\wedge$}\\
\>\>{\small male(X)$\wedge$female(X)$\wedge$male(Y)$\wedge$female(Y)$\wedge$}\\
\>\>{\small male(XM)$\wedge$female(XM)$\wedge$male(XF)$\wedge$female(XF)$\wedge$}\\
\>\>{\small male(YM)$\wedge$female(YM)$\wedge$male(YF)$\wedge$female(YF)$\wedge$}\\
\>\>{\small equal(X,X)$\wedge$equal(X,XM)$\wedge$equal(X,XF)$\wedge$}\\
\>\>{\small equal(X,Y)$\wedge$equal(X,YM)$\wedge$equal(X,YF)$\wedge$}\\
\>\>{\small equal(XM,X)$\wedge$equal(XM,XM)$\wedge$equal(XM,XF)$\wedge$}\\
\>\>{\small equal(XM,Y)$\wedge$equal(XM,YM)$\wedge$equal(XM,YF)$\wedge$}\\
\>\>{\small equal(XF,X)$\wedge$equal(XF,XM)$\wedge$equal(XF,XF)$\wedge$}\\
\>\>{\small equal(XF,Y)$\wedge$equal(XF,YM)$\wedge$equal(XF,YF)$\wedge$}\\
\>\>{\small equal(Y,X)$\wedge$equal(Y,XM)$\wedge$equal(Y,XF)$\wedge$}\\
\>\>{\small equal(Y,Y)$\wedge$equal(Y,YM)$\wedge$equal(Y,YF)$\wedge$}\\
\>\>{\small equal(YM,X)$\wedge$equal(YM,XM)$\wedge$equal(YM,XF)$\wedge$}\\
\>\>{\small equal(YM,Y)$\wedge$equal(YM,YM)$\wedge$equal(YM,YF)$\wedge$}\\
\>\>{\small equal(YF,X)$\wedge$equal(YF,XM)$\wedge$equal(YF,XF)$\wedge$}\\
\>\>{\small equal(YF,Y)$\wedge$equal(YF,YM)$\wedge$equal(YF,YF)}
\end{tabbing}
\end{example}

Let us say that clause $C_1$ is a \trm{subclause} of clause $C_2$ if
the heads of $C_1$ and $C_2$ are identical, if every literal in the
body of $C_1$ also appears in $C_2$, and if the literals in the body
of $C_1$ appear in the same order as they do in $C_2$.  The functions
$\deepen$ and $\constrain$ allow one to easily describe a clause with
an interesting property.

\begin{theorem} \label{clong res} 
Let $\dec=(p,a',R)$ be a declaration in $\detdecj{a}^{=}$, let
$X_1,\ldots,X_{a'}$ be distinct variables, and define the clause
$\clongd{d}$ as follows:
\[ \clongd{d}(\dec) \equiv \constrain_{\dec}(\deepen^d_{\dec}(p(X_1,\ldots,X_{a'})\hcif))
\]
For any constants $d$ and $a$, the following are true:
\begin{itemize}
\item the size of $\clongd{d}(\dec)$ is polynomial in $\size{\dec}$;
\item every depth-$d$ clause that satisfies $\dec$ (and hence, is 
determinate) is (semantically) equivalent to some subclause of
$\clongd{d}(\dec)$.
\end{itemize}
\end{theorem}

\begin{proof}
See Appendix~\ref{additional proofs}. A related result also
appears in Muggleton and Feng \citeyear{MuggletonILP92}. 
\end{proof}

\begin{example}
Below $C_1$ and $D_1$ are equivalent, as are $C_2$ and $D_2$.
Notice that $D_1$ and $D_2$ are subclauses of $\clongd{1}(D0)$.
\begin{tabbing}
$C_1:$ \= p(A,B)$\hcif$\=mother(A,C)$\wedge$father(A,D)$\wedge$
			mother(B,C)$\wedge$father(B,D)$\wedge$male(A)\\
$D_1:$ \> p(X,Y)$\hcif$\>mother(X,XM)$\wedge$father(X,XF)$\wedge$
				     mother(Y,YM)$\wedge$father(Y,YF)$\wedge$\\
      \>	      \>male(X)$\wedge$equal(XM,YM)$\wedge$equal(XF,YF)\\
$C_2:$ \> p(A,B)$\hcif$\>father(A,B)$\wedge$female(A)\\
$D_2:$ \> p(X,Y)$\hcif$\>father(X,XF)$\wedge$female(X)$\wedge$equal(XF,Y)
\end{tabbing}
For $C_1$ and $D_1$, \cd{p(X,Y)} is true when $X$ is $Y$'s brother.
For $C_2$ and $D_2$, \cd{p(X,Y)} is true when $X$ is $Y$'s daughter,
and $Y$ is $X$'s father.
\end{example}

\subsection{The Learning Algorithm}

\begin{figure}[t]
%\hrule
\begin{alg}
{\bf begin algorithm $\cd{Force1_{\it NR}(d,\dec,\db)}$:}\\
\> {\it \% below $\clongd{d}$ is the most specific possible clause}\\
\> {\bf let} $H \leftarrow \clongd{d}(\dec)$\\
\> {\bf repeat} \\
\> \> \cd{Ans} $\leftarrow$ answer to the query ``Is $H$ correct?'' \\
\> \> {\bf if } $\cd{Ans}=$``yes'' {\bf then} {\bf return $H$} \\
\> \> {\bf elseif} \cd{Ans} is a negative example {\bf then}\\
\> \> \> {\bf return} ``no consistent hypothesis''\\
\> \> {\bf elseif} \cd{Ans} is a positive example $e^+$ {\bf then}\\
\> \> \> {\it \% generalize $H$ minimally to cover $e^+$} \\
\> \> \> {\bf let} $(f,D)$ be the components of the extended instance $e^+$\\
\> \> \> $H\leftarrow\cd{ForceSim_{\it NR}(H,f,\dec,(\db\cup{}D))}$ \\
\> \> \> {\bf if} $H=\cd{FAILURE}$ {\bf then}\\
\> \> \> \> {\bf return} ``no consistent hypothesis''\\
\> \> \> {\bf endif}\\
\> \> {\bf endif}\\
\> {\bf endrepeat}\\
{\bf end}
\end{alg}
\caption{A learning algorithm for nonrecursive depth-$d$ determinate clauses}
\label{force1nr fig}
%\hrule
\end{figure}

\begin{figure}[t]
%\hrule
\begin{alg}
{\bf begin subroutine $\cd{ForceSim_{\it NR}(H,f,\dec,\db)}$:}\\
\> {\it \% ``forcibly simulate'' $H$ on fact $f$}\\
\> {\bf if} $f\in\db$ {\bf then return} $H$\\
\> {\bf elseif} the head of $H$ and $f$ cannot be unified {\bf then}\\
\> \> {\bf return} \cd{FAILURE}\\
\> {\bf else}\\
\> \> {\bf let} $H'\leftarrow H$\\
\> \> {\bf let} $\sigma$ be the mgu of $f$ and the head of $H'$\\
\> \> {\bf for} each literal $L$ in the body of $H'$ {\bf do}\\
\> \> \> {\bf if} there is a substitution $\sigma'$ 
 		such that $L\sigma\sigma'\in\db$ {\bf then}\\
\> \> \> \> $\sigma \leftarrow \sigma\circ\sigma'$, where
 	$\sigma'$ is the most general such substitution\\
\> \> \> {\bf else} \\
\> \> \> \> delete $L$ from the body of $H'$, together with\\
\> \> \> \> ~~all literals $L'$ supported (directly or indirectly) by $L$\\
\> \> \> {\bf endif}\\
\> \> {\bf endfor} \\
\> \> {\bf return} $H'$\\
\> {\bf endif}\\
{\bf end}  \\
\end{alg}
\caption{Forced simulation for nonrecursive depth-$d$ determinate clauses}
\label{forcesimnr fig}
%\hrule
\end{figure}

Theorem~\ref{clong res} suggests that it may be possible to learn
non-recursive constant-depth determinate clauses by searching the
space of subclauses of $\clongd{d}$ in some efficient manner.
Figures~\ref{force1nr fig} and \ref{forcesimnr fig} present an
algorithm called $\cd{Force1}_{\it NR}$ that does this when $\dec$ is
a unique-mode declaration.

\begin{sloppypar}
Figure~\ref{force1nr fig} presents the top-level learning algorithm,
$\cd{Force1}_{\it NR}$.  $\cd{Force1}_{\it NR}$ takes as input a
database $\db$ and a declaration $\dec$, and begins by hypothesizing
the clause $\clongd{d}(\dec)$.  After each positive counterexample
$e^+$, the current hypothesis is generalized as little as possible in
order to cover $e^+$.  This strategy means that the hypothesis is
always the least general hypothesis that covers the positive examples;
hence, if a negative counterexample $e^-$ is ever seen, the algorithm
will abort with a message that no consistent hypothesis exists.
\end{sloppypar}

To minimally generalize a hypothesis $H$, the function $ForceSim_{\it
NR}$ is used. This subroutine is shown in Figure~\ref{forcesimnr fig}.
In the figure, the following terminology is used. If some output
variable of $L$ is an input variable of $L'$, then we say that $L$
\trm{directly supports} $L'$.  We will say that $L$
\trm{supports} $L'$ iff $L$ directly supports $L'$, or if
$L$ directly supports some literal $L''$ that supports $L'$.  (Thus
``supports'' is the transitive closure of ``directly supports''.)
$\cd{ForceSim}_{\it NR}$ deletes from $H$ the minimal number of
literals necessary to let $H$ cover $e^+$.  To do this,
$\cd{ForceSim}_{\it NR}$ simulates the action of a Prolog interpreter
in evaluating $H$, except that whenever a literal $L$ in the body of
$H$ would fail, that literal is deleted, along with all literals $L'$
supported by $L$.

The idea of learning by repeated generalization is an old one; in
particular, previous methods exist for learning a definite clause by
generalizing a highly-specific one.  For example, {\sc CLINT}
\cite{DeRaedtMLJ92} generalizes a ``starting clause'' guided by
queries made to the user; {\sc PROGOL} \cite{MuggletonILP94} guides a
top-down generalization process with a known bottom clause; and
Rouveirol \citeyear{RouveirolMLJ94} describes a method for
generalizing bottom clauses created by saturation.  The
$\cd{Force1}_{\it NR}$ algorithm is thus of interest not for its
novelty, but because it is provably correct and efficient, as noted in
the theorem below.

In particular, let $\nrdepth{d}$ be the language of nonrecursive
clauses of depth $d$ or less (and hence
$\nrdepth{i}[\dbset,\detdecj{j}]$ is the language of nonrecursive
$ij$-determinate clauses).  We have the following result:

\begin{theorem} \label{nonrec learnable}
For any constants $a$ and $d$, the language family
\[ \nrdepth{d}[\dbset^=,\detdecj{a}^{=1}]
\] 
is uniformly identifiable from equivalence queries.
\end{theorem}

\begin{proof}
We will show that $\cd{Force1}_{\it NR}$ uniformly identifies this
language family with a polynomial number of queries.  We begin with
the following important lemma, which characterizes the behavior of
\cd{ForceSim$_{\it NR}$}.

\begin{lemma} \label{forcesim nr res}
Let $\dec$ declaration in $\detdec^{=1}$, let $\db$ be a database, let
$f$ be a fact, and let $H$ be a determinate nonrecursive clause that
satisfies $\dec$.  Then one of following conditions must hold:
\begin{itemize}
\item $\cd{ForceSim_{\it NR}(H,f,\dec,\db)}$ returns \cd{FAILURE}, 
and no subclause $H'$ of $H$ satisfies both $\dec$ and the constraint
\( H'\wedge\db\vdash f \); or,
\item $\cd{ForceSim_{\it NR}(H,f,\dec,\db)}$ returns a clause $H'$,
and $H'$ is the unique syntactically largest subclause of $H$ that
satisfies both $\dec$ and the constraint \( H'\wedge{}\db\vdash f \).
\end{itemize}
\end{lemma}

\begin{lemmaproof}
To avoid repetition, we will refer to the syntactically maximal
subclauses $H'$ of $H$ that satisfy both $\dec$ and the constraint
\( H'\wedge{}\db\vdash f\) as ``admissible subclauses'' in
the proof below.

Clearly the lemma is true if $H$ or \cd{FAILURE} is returned by
$\cd{ForceSim}_{\it NR}$.  In the remaining cases the {\bf for} loop
of the algorithm is executed, and we must establish these two claims
(under the assumptions that $A$ and $f$ unify, and that
$f\not\in\db$):
\begin{description}
\item[Claim 1.] If $L$ is retained, then every admissible subclause
contains $L$.
\item[Claim 2.] If $L$ is deleted, then no admissible subclause contains $L$.
\end{description}

First, however, observe that deleting a literal $L$ may cause the mode
of some other literals to violate the mode declarations of $\dec$.  It
is easy to see that if $L$ is deleted from a clause $C$, then the mode
of all literals $L'$ directly supported by $L$ will change.  Thus if
$C$ satisfies a unique-mode declaration prior to the deletion of $L$,
then after the deletion of $L$ all literals $L'$ that are directly
supported by $L$ will have invalid modes.

Now, to see that Claim~1 is true, suppose instead that it is false.
Then there must be some maximal subclause $C'$ of $H$ that satisfies
$\dec$, covers the fact $f$, and does not contain $L$.  By the
argument above, if $C'$ does not contain $L$ but satisfied $\dec$,
then $C'$ contains no literals $L'$ from $H$ that are supported by
$L$.  Hence the output variables of $L$ are disjoint from the
variables appearing in $C'$.  This means that if $L$ were to be added
to $C'$ the resulting clause would still satisfy $\dec$ and cover $f$,
which leads to a contradiction since $C'$ was assumed to be maximal.

To verify Claim~2, let us introduce the following terminology. If
$C=(A\hcif{}B_1\wedge\ldots\wedge{}B_r)$ is a clause and $\db$ is a
database, we will say that the substitution $\theta$ is a
\trm{$(\db,f)$-witness} for $C$ iff $\theta$ is associated with a
proof that $C\wedge\db\vdash{}f$ (or more precisely, iff $A\theta=f$
and $\forall i:1\leq{}i\leq{}r,B_i\theta\in\db$.)  We claim that the
following condition is an invariant of the {\bf for} loop of the
$\cd{ForceSim}_{\it NR}$ algorithm.
\begin{description}
\item[Invariant 1.] Let $C$ be any admissible subclause that
contains all the literals in $H'$ preceding $L$ ({\it i.e.}, that
contains all those literals of $H$ that were retained on previous
iterations of the algorithm).  Then every $(\db,f)$-witness for $C$ is
a superset of $\sigma$.
\end{description}
This can be easily established by induction on the number of
iterations of the {\it for} loop.  The condition is true when the loop
is first entered, since $\sigma$ is initially the most general unifier
of $A$ and $f$.  The condition remains true after an iteration in
which $L$ is deleted, since $\sigma$ is unchanged.  Finally, the
condition remains true after an iteration in which $L$ is retained:
because $\sigma'$ is maximally general, it may only assign values to
the output variables of $L$, and by determinacy only one assignment to
the output variables of $L$ can make $L$ true.  Hence every
$(\db,f)$-witness for $C$ must contain the bindings in $\sigma$.

Next, with an inductive argument and Claim~1 one can show that every
admissible subclause $C$ must contain all the literals that have been
retained in previous iterations of the loop, leading to the following
strengthening of Invariant~1:
\begin{description}
\item[Invariant $1'$.] Let $C$ be any admissible subclause.
Then every $(\db,f)$-witness for $C$ is a superset of $\sigma$.
\end{description}
Now, notice that only two types of literals are deleted:  (a) literals
$L$ such that no superset of $\sigma$ can make $L$ true, and (b)
literals $L'$ that are supported by a literal $L$ of the preceding
type.  In case (a), clearly $L$ cannot be part of any admissible
subclause, since no superset of $\sigma$ makes $L$ succeed, and only
such supersets can be witnesses of admissible clauses.  In case (b),
again $L'$ cannot be part of any admissible subclause, since its
declaration is invalid unless $L$ is present in the clause, and by the
argument above $L$ cannot be in the clause.

This concludes the proof of the lemma.
\end{lemmaproof}

To prove the theorem, we must now establish the following properties
of the identification algorithm.

\begin{sloppypar}
{\bf Correctness.} By Theorem~\ref{clong res}, if the target program
is in $\nrdepth{d}[\db,\dec]$, then there is some clause $C_T$ that is
equivalent to the target, and is a subclause of $\clongd{d}(\dec)$.
$H$ is initially $\clong{d}$ and hence a superclause of $C_T$.  Now
consider invoking $\cd{ForceSim}_{\it NR}$ on any positive
counterexample $e^+$.  By Lemma~\ref{forcesim nr res}, if this
invocation is successful, $H$ will be replaced by $H'$, the longest
subclause of $H$ that covers $e^+$. Since $C_T$ is a subclause of $H$
that covers $e^+$, this means that $H'$ will again be a superclause of
$C_T$.  Inductively, then, the hypothesis is always a superclause of
the target.
\end{sloppypar}

Further, since the counterexample $e^+$ is always an instance that is
not covered by the current hypothesis $H$, every time the hypothesis
is updated, the new hypothesis is a {\em proper\/} subclause of the
old.  This means that $\cd{Force1}_{\it NR}$ will eventually identify
the target clause.

{\bf Efficiency.} The number of queries made is polynomial in
$\size{\dec}$ and $\size{\db}$, since $H$ is initially of size
polynomial in $\size{\dec}$, and is reduced in size each time a
counterexample is provided.  To see that each counterexample is
processed in time polynomial in $\maxv$, $\maxi$, and $\maxt$, notice
that since the length of $H$ is polynomial, the number of repetitions
of the {\bf for} loop of $\cd{ForceSim}_{\it NR}$ is also polynomial;
further, since the arity of literals $L$ is bounded by $a$, only
$a\maxb+a\maxi$ constants exist in $\db\cup{}D$, and hence there are
at most $(a\maxb+a\maxi)^a$ substitutions $\sigma'$ to check inside
the {\bf for} loop, which is again polynomial.  Thus each execution of
$\cd{ForceSim}_{\it NR}$ requires only polynomial time.

This concludes the proof.
\end{proof}

\section{Learning a Linear Closed Recursive Clause} 
\label{learn one}

Recall that if a clause has only one recursive literal, then the
clause is \trm{linear recursive}, and that if no recursive literal
contains output variables, then the clause is \cd{closed linear
recursive}.  In this section, we will describe how the \cd{Force1}
algorithm can be extended to learn a single linear closed recursive
clause.\footnote{The reader may object that useful recursive programs
always have at least two clauses---a recursive clause and a
nonrecursive base case.  In posing the problem of learning a single
recursive clause, we are thus assuming the non-recursive ``base case''
of the target program is provided as background knowledge, either in
the background database $\db$, or in the description atoms $D$ of
extended instances.} Before presenting the extension, however, we
would first like to discuss a reasonable-sounding approach that, on
closer examination, turns out to be incorrect.

\subsection{A Remark on Recursive Clauses}

One plausible first step toward extending
\cd{Force1} to recursive clauses is to allow recursive
literals in hypotheses, and treat them the same way as other
literals---that is, to include recursive literals in the initial
clause $\clongd{d}$, and delete these literals gradually as positives
examples are received.  A problem with this approach is that there is
no simple way to check if a recursive literal in a clause succeeds or
fails on a particular example.  This makes it impossible to simply run
\cd{ForceSim$_{\it NR}$} on clauses containing recursive literals.

A straightforward (apparent) solution to this problem is to assume
that an oracle exists which can be queried as to the success or
failure of any recursive literal.  For closed recursive clauses, it is
sufficient to assume that there is an oracle MEMBER$_{C_t}(\db,f)$
that answers the question
\[ \mbox{Does~} \db \wedge P \vdash f ~?
\]
where $C_t$ is the unknown target concept, $f$ is a ground fact, and
$\db$ is a database.  Given such an oracle, one can determine if a
closed recursive literal $L_r$ should be retained by checking if
MEMBER$_{C_T}(\db,L_r\sigma)$ is true.  Such an oracle is very close
to the notion of a \trm{membership query} as used in computational
learning theory.

This is a natural extension of the $\cd{Force1_{\it NR}}$ learning
algorithm to recursive clauses---in fact an algorithm based on similar
ideas has been been previously conjectured to pac-learn closed
recursive constant-depth determinate clauses \cite{DzeroskiCOLT92}.
Unfortunately, this algorithm can fail to return a clause that is
consistent with a positive counterexample.  To illustrate this,
consider the following example.

\begin{example}
Consider using the extension of $\cd{Force1_{\it NR}}$ described above
to learn following target program:
\begin{code}
append(Xs,Ys,Zs) $\hcif$\\
\>components(Xs,X,Xs1),\\
\>components(Zs,Z,Zs1),\\
\>X1=Z1,\\
\>append(Xs1,Ys,Zs1).
\end{code}
This program is determinate, has depth 1, and satisfies the following
set of declarations:
\begin{code}
components(+,$-$,$-$).\\ null(+).\\ equal(+,+).\\ odd(+).\\ append(+,+,+).
\end{code}
We will assume also a database $\db$ that defines the predicate
\cd{null} to be true for empty lists, and \cd{odd} to be true for
the constants 1 and 3.

\newcommand{\todel}[1]{{\it #1}}

\begin{figure}[t]
%\hrule
\begin{center}
\begin{tabular}{|c|c|}
\hline
$\clongd{1}(\dec)$: & $\cd{ForceSim_{\it
NR}}(\clongd{1}(Dec),f,\dec,\db\cup{}D):$ \\
\hline
\begin{minipage}[t]{0.4\textwidth}
\begin{code}
append(Xs,Ys,Zs) $\hcif$ \\
\> components(Xs,X1,Xs1)$\wedge$\\
\> components(Ys,Y1,Ys1)$\wedge$\\
\> components(Zs,Z1,Zs1)$\wedge$\\
\> \todel{null(Xs)}$\wedge$\\
\> \todel{null(Ys)}$\wedge$\\
\> $\vdots$\\
\> null(Ys1)$\wedge$\\
\> \todel{null(Zs1),}\\
\> equal(Xs,Xs)$\wedge$\\
\> $\vdots$\\
\> equal(X1,Z1)$\wedge$\\
\> $\vdots$\\
\> \todel{equal(Zs1,Zs1)}$\wedge$\\
\> odd(Xs)$\wedge$\\
\> $\vdots$\\
\> odd(X1)$\wedge$\\
\> odd(Y1)$\wedge$\\
\> odd(Z1)$\wedge$\\
\> $\vdots$\\
\> \todel{odd(Zs1)}$\wedge$\\
\> \todel{append(Xs,Xs,Xs)}$\wedge$\\
\>$\vdots$\\
\> \todel{append(Zs1,Zs1,Zs1)}.
\end{code}
\end{minipage}
 &
\begin{minipage}[t]{0.4\textwidth}
\begin{code}
append(Xs,Ys,Zs) $\hcif$ \\
\> components(Xs,X1,Xs1)$\wedge$\\
\> components(Ys,Y1,Ys1)$\wedge$\\
\> components(Zs,Z1,Zs1)$\wedge$\\
\> null(Ys1)$\wedge$\\
\> equal(X1,Z1)$\wedge$\\
\> odd(X1)$\wedge$\\
\> odd(Y1)$\wedge$\\
\> odd(Z1)$\wedge$\\
\> append(Xs1,Ys,Zs1).\\
\end{code}
\end{minipage}
\\\hline
\end{tabular}
\end{center}
\caption{A recursive clause before and after generalization with \cd{ForceSim$_{\it NR}$}}
\label{bug fig}
%\hrule
\end{figure}

To see how the forced simulation can fail, consider the following
positive instance $e=(f,D)$:
\begin{tabbing}
$f=\cd{append(l12,l3,l123)}$\\ $D=\{$ 	\=\cd{cons(l123,1,l23)},
\=\cd{cons(l23,2,l3)}, \cd{cons(l3,3,nil)}, \\ 	\>\cd{cons(l12,1,l2)},
\>\cd{cons(l2,2,nil)}, \\ 	\>\cd{append(nil,l3,l3)} $\}$
\end{tabbing}
This is simply a ``flattened'' form of \cd{append([1,2],[3],[1,2,3])},
together with the appropriate base case \cd{append([],[3],[3])}.  Now
consider beginning with the clause $\clongd{1}$ and generalizing it
using $\cd{ForceSim_{\it NR}}$ to cover this positive instance.  This
process is illustrated in Figure~\ref{bug fig}.  The clause on the
left in the figure is $\clongd{d}(\dec)$; the clause on the right is
the output of forcibly simulating this clause on $f$ with
\cd{ForceSim}$_{\it NR}$. (For clarity we've assumed that only the
single correct recursive call remains after forced simulation.)

The resulting clause is incorrect, in that it does not cover the given
example $e$.  This can be easily seen by stepping through the actions
of a Prolog interpreter with the generalized clause of Figure~\ref{bug
fig}.  The nonrecursive literals will all succeed, leading to the
subgoal \cd{append(l2,l3,l23)} (or in the usual Prolog notation,
\cd{append([2],[3],[2,3])}).  This subgoal will fail at the literal
\cd{odd(X1)}, because \cd{X1} is bound to $2$ for this subgoal,
and the fact \cd{odd(2)} is not true in $\db\cup{}D$.
\end{example}

This example illustrates a pitfall in the policy of treating recursive
and non-recursive literals in a uniform manner (For more discussion,
see also \cite{BergadanoIJCAI93,DeRaedtILP93}.)  Unlike nonrecursive
literals, the truth of the fact $L_r\sigma$ (corresponding to the
recursive literal $L_r$) does not imply that a clause containing $L_r$
will succeed; it may be that while the first subgoal $L_r\sigma$
succeeds, deeper subgoals fail.

\begin{figure}
%\hrule
\begin{alg}
{\bf begin subroutine $\cd{ForceSim(H,f,\dec,\db,h)}$:}\\
\> {\it \% ``forcibly simulate'' recursive clause $H$ on $f$}\\
\> {\it \% 1. check for infinite loops}\\
\> {\bf if} $h<0$ {\bf then return} \cd{FAILURE}\\
\> {\it \% 2. check to see if $f$ is already covered}\\
\> {\bf elseif} $f\in\db$ {\bf then return} $H$ \\
\> {\it \% 3. check to see if $f$ cannot be covered}\\
\> {\bf elseif} the head of $H$ and $f$ cannot be unified {\bf then}\\
\> \> {\bf return} \cd{FAILURE}\\
\> {\bf else} \\
\> \> {\bf let} $L_r$ be the recursive literal of $H$\\
\> \> {\bf let} $H' \leftarrow H-\{L_r\}$\\
\> \> {\it \% 4. delete failing non-recursive literals as in ForceSim$_{NR}$}\\
\> \> {\bf let} $A$ be the head of $H'$ \\
\> \> {\bf let} $\sigma$ be the mgu of $A$ and $e$\\
\> \> {\bf for} each literal $L$ in the body of $H'$ {\bf do}\\
\> \> \> {\bf if} there is a substitution $\sigma'$ such that $L\sigma\sigma'\in\db$\\
\> \> \> {\bf then} $\sigma \leftarrow \sigma\circ\sigma'$, where
 	   	     $\sigma'$ is the most general such substitution\\
\> \> \> {\bf else} \\
\> \> \> \> delete $L$ from the body of $H'$, together with\\
\> \> \> \> ~~all literals $L'$ supported (directly or indirectly) by $L$\\
\> \> \> {\bf endif}\\
\> \> {\bf endfor} \\
\> \> {\it \% 5. generalize $H'$ on the recursive subgoal $L_r\sigma$}\\
\> \> {\bf if} $L_r\sigma$ is ground {\bf then}
	 {\bf return} ForceSim($H'\cup\{L_r\},L_r\sigma,\dec,\db,h-1$)\\
\> \> {\bf else return} \cd{FAILURE} \\
\> \> {\bf endif} \\
\> {\bf endif}\\
{\bf end}  \\
\end{alg}
\caption{Forced simulation for linear closed recursive clauses}
\label{forcesim fig}
%\hrule
\end{figure}

\subsection{Forced Simulation for Recursive Clauses} 

A solution to this problem is to replace the calls to the membership
oracle in the algorithm sketched above with a call to a routine that
forcibly simulates the actions of a top-down theorem-prover on a
recursive clause.  In particular, the following algorithm is
suggested.  First, build a nonrecursive ``bottom clause'', as was done
in $\cd{ForceSim}_{\it NR}$.  Second, find some recursive literal
$L_r$ such that appending $L_r$ to the bottom clause yields a
recursive clause that can be generalized to cover the positive
examples.

As in the nonrecursive case, a clause is generalized by deleting
literals, using a straightforward generalization of the procedure for
forced simulation of nonrecursive clauses.  During forced simulation,
any failing nonrecursive subgoals are simply deleted; however, when a
recursive literal $L_r$ is encountered, one forcibly simulates the
hypothesis clause recursively on the corresponding recursive subgoal.
An implementation of forced simulation for linear closed recursive
clauses is shown in Figure~\ref{forcesim fig}.  

The extended algorithm is similar to $\cd{ForceSim_{\it NR}}$, but
differs in that when the recursive literal $L_r$ is reached in the
simulation of $H$, the corresponding subgoal $L_r\sigma$ is created,
and the hypothesized clause is recursively forcibly simulated on this
subgoal.  This ensures that the generalized clause will also succeed
on the subgoal.  For reasons that will become clear shortly, we would
like this algorithm to terminate, even if the original clause $H$
enters an infinite loop when used in a top-down interpreter.  In order
to ensure termination, an extra argument $h$ is passed to
$\cd{ForceSim}$.  The argument $h$ represents a depth bound for the
forced simulation.

To summarize, the basic idea behind the algorithm of
Figure~\ref{forcesim fig} is to simulate the hypothesized clause $H$
on $f$, and generalize $H$ by deleting literals whenever $H$ would
fail on $f$ {or on any subgoal of $f$\/}.

\begin{example}
\begin{sloppypar}
Consider using \cd{ForceSim} to forcibly simulate the following
recursive clause $\clongd{1}(\dec)\cup{}L_r$
\begin{code}
append(Xs,Ys,Zs) $\hcif$ \\
\>components(Xs,X1,Xs1)$\wedge$components(Ys,Y1,Ys1)$\wedge$components(Zs,Z1,Zs1)$\wedge$\\
\>null(Xs)$\wedge$\ldots$\wedge$null(Zs1)$\wedge$\\
\>odd(Xs)$\wedge$\ldots$\wedge$odd(Zs1)$\wedge$\\
\>equal(Xs,Xs)$\wedge$\ldots$\wedge$equal(Zs1,Zs1)$\wedge$\\
\>append(Xs1,Ys,Zs1)
\end{code}
Here the recursive literal $L_r$ is \cd{append(Xs1,Ys,Zs1)}.  We will
also assume that $f$ is taken from the extended query $e=(f,D)$, which
is again the flattened version of the instance
\cd{append([1,2],[3],[1,2,3])} used in the previous example; that
$\dec$ is the set of declarations of in the previous example; and that
the database $\db$ is $D\cup\cd{null(nul)}$.

After executing steps 1-4 of \cd{ForceSim}, a number of failing
literals are deleted, leading to the substitution\footnote{Note that
for readability, we are using the term notation rather than the
flattened notation of $\cd{Xs}=l12$, $\cd{Ys}=l3$, etc.} $\sigma$ of
$\{\cd{Xs}=[1,2]$, $\cd{Ys}=[3]$, $\cd{Zs}=[1,2,3]$, $\cd{X1}=1$,
$\cd{Xs1}=[2]$, $\cd{Y1}=3$, $\cd{Ys1}=[]$, $\cd{Z1}=1$,
$\cd{Zs1}=[2,3]\}$ and the following reduced clause:
\begin{code}
append(Xs,Ys,Zs) $\hcif$ \\
\>components(Xs,X1,Xs1)$\wedge$components(Ys,Y1,Ys1)$\wedge$components(Zs,Z1,Zs1)$\wedge$\\
\>null(Ys1)$\wedge$odd(X1)$\wedge$odd(Y1)$\wedge$odd(Z1)$\wedge$equal(X1,Z1)$\wedge$\\
\>append(Xs1,Ys,Zs1)
\end{code}
Hence the recursive subgoal is 
\[ 
  L_r\sigma = \cd{append(Xs1,Ys,Zs1)}\sigma = \cd{append}([2],[3],[2,3])
\]
Recursively applying \cd{ForceSim} to this goal produces the substitution
$\{\cd{Xs}=[2]$,  $\cd{Ys}=[3]$, $\cd{Zs}=[2,3]$,  $\cd{X1}=2$,  $\cd{Xs1}=[]$, 
	$\cd{Y1}=3$,  $\cd{Ys1}=[]$, $\cd{Z1}=2$, $\cd{Zs1}=[3]\}$
and also results in deleting the additional literals \cd{odd(X1)} and
\cd{odd(Z1)}.  The next recursive subgoal is $L_r\sigma=\cd{append}([],[3],[3])$;
since this clause is included in the database $\db$, \cd{ForceSim}
will terminate.  The final clause returned by \cd{ForceSim}
in this case is the following:
\begin{code}
append(Xs,Ys,Zs) $\hcif$ \\
\>components(Xs,X1,Xs1)$\wedge$components(Ys,Y1,Ys1)$\wedge$components(Zs,Z1,Zs1)$\wedge$\\
\>null(Ys1)$\wedge$odd(Y1)$\wedge$equal(X1,Z1)$\wedge$\\
\>append(Xs1,Ys,Zs1)
\end{code}
Notice that this clause does cover $e$.
\end{sloppypar}
\end{example}

As in Section~\ref{learn nonrec} we begin our analysis by showing the
correctness of the forced simulation algorithm---{\it i.e.}, by
showing that forced simulation does indeed produce a unique maximally
specific generalization of the input clause that covers the example.

This proof of correctness uses induction on the depth of a proof.  Let
us introduce again some additional notation, and write
$P\wedge{}\db\vdash_h{}f$ if the Prolog program $(P,\db)$ can be used
to prove the fact $f$ in a proof of depth $h$ or less.  (The notion of
depth of a proof is the usual one; we will define looking up $f$ in
the database $\db$ to be a proof of depth zero.)  We have the
following result concerning the $\cd{ForceSim}$ algorithm.

\begin{theorem} \label{forcesim res}
Let $\dec$ be a declaration in $\detdec^{=1}$, let $\db$ be a
database, let $f$ be a fact, and let $H$ be a determinate closed
linear recursive clause that satisfies $\dec$.  Then one of the following
conditions must hold:
\begin{itemize}
\item $\cd{ForceSim}(H,f,\dec,\db,h)$ returns \cd{FAILURE}, and
no recursive subclause $H'$ of $H$ satisfies both $\dec$
and the constraint \( H'\wedge{}\db\vdash_h f \); or, 
\item $\cd{ForceSim}(H,f,\dec,\db,h)$ returns a clause $H'$, and 
$H'$ is the unique syntactically largest recursive subclause of $H$
that satisfies both $\dec$ and the constraint \(
H'\wedge{}\db\vdash_h f \).
\end{itemize}
\end{theorem}

\begin{proof}
Again to avoid repetition, we will refer to syntactically maximal
recursive (nonrecursive) subclauses $H'$ of $H$ that satisfy both
$\dec$ and the constraint \( H'\wedge{}\db\vdash_h f\) as
``admissible recursive (nonrecursive) subclauses'' respectively.  

The proof largely parallels the proof of Lemma~\ref{forcesim nr
res}---in particular, similar arguments show that the clause returned
by \cd{ForceSim} satisfies the conditions of the theorem whenever
\cd{FAILURE} is returned and whenever $H$ is returned.  Note that the 
correctness of \cd{ForceSim} when $H$ is returned establishes the base
case of the theorem for $h=0$.

For the case of depth $h>0$, let us assume the theorem holds for depth
$h-1$ and proceed using mathematical induction. The arguments of
Lemma~\ref{forcesim nr res} show that the following condition is true
after the {\bf for} loop terminates.
\begin{description}
\item[Invariant $1'$.] $H'$ is the unique maximal nonrecursive admissible
subclause of $H$, and every $(\db,f)$-witness for $H'$ is a superset
of $\sigma$.
\end{description}
Now, let us assume that there is some admissible recursive subclause
$H^*$.  Clearly $H^*$ must contain the recursive literal $L_r$ of $H$,
since $L_r$ is the only recursive literal of $H$.  Further, the
nonrecursive clause $\hat{H}=H^*-\{L_r\}$ must certainly satisfy
$\dec$ and also $\hat{H}\wedge\db\vdash{}f$, so it must (by the
maximality of $H'$) be a subclause of $H'$.  Hence $H^*$ must be a
subclause of $H'\cup\{L_r\}$.  Finally, if $L_r\sigma$ is ground ({\it
i.e.}, if $L_r$ is closed in the clause $H'\cup{}L_r$) then by
Invariant $1'$, the clause $H^*$ must also satisfy
$H^*\wedge\db\vdash{}L_r\sigma$ by a proof of depth $h-1$.  (This is
simply equivalent to saying that the recursive subgoal of $L_r\sigma$
generated in the proof must succeed.)

By the inductive hypothesis, then, the recursive call must return the
unique maximal admissible recursive subclause of $H'\cup{}L_r$, which
by the argument above must also be the unique maximal admissible
recursive subclause of $H$.

Thus by induction the theorem holds.  
\end{proof}

\begin{figure}
%\hrule
\begin{alg}
{\bf begin algorithm $\cd{Force1(d,\dec,\db)}$:}\\
\> {\it \% below $\clongd{d}$ is the most specific possible clause}\\
\> {\bf let} $L_{r_1},\ldots,L_{r_p}$ be all possible closed
     recursive literals for $\clongd{d}(\dec)$\\
\> choose an unmarked recursive literal $L_{r_i}$\\
\> {\bf let} $H \leftarrow \clongd{d}(\dec) \cup \{L_{r_i}\}$\\
\> {\bf repeat} \\
\> \> \cd{Ans} $\leftarrow$ answer to the query ``Is $H$ correct?'' \\
\> \> {\bf if } $\cd{Ans}=$``yes'' {\bf then} {\bf return $H$} \\
\> \> {\bf elseif} \cd{Ans} is a negative example $e^-$ {\bf then}\\
\> \> \> $H\leftarrow\cd{FAILURE}$ \\
\> \> {\bf elseif} \cd{Ans} is a positive example $e^+$ {\bf then}\\
\> \> \> {\it \% generalize $H$ minimally to cover $e^+$} \\
\> \> \> {\bf let} $(f,D)$ be the components of $e^+$\\
\> \> \> $H\leftarrow
    \cd{ForceSim(H,f,\dec,(\db\cup{}D),(a\size{D}+a\size{DB})^{a'})}$ \\
\> \> \> ~~where $a'$ is the arity of the clause head as given in $\dec$\\
\> \> {\bf endif}\\
\> \> {\bf if} $H=\cd{FAILURE}$ {\bf then}\\
\> \> \> {\bf if} all recursive literals are marked {\bf then}\\
\> \> \> \> {\bf return} ``no consistent hypothesis''\\
\> \> \> {\bf else} \\
\> \> \> \> mark $L_{r_i}$\\
\> \> \> \> choose an unmarked recursive literal $L_{r_j}$\\
\> \> \> \> {\bf let} $H \leftarrow \clongd{d}(\dec) \cup \{L_{r_j}\}$\\
\> \> \> {\bf endif}\\
\> \> {\bf endif}\\
\> {\bf endrepeat}\\
{\bf end}
\end{alg}
\caption{A learning algorithm for nonrecursive depth-$d$ determinate clauses}
\label{force1 fig}
%\hrule
\end{figure}

\subsection{A Learning Algorithm for Linear Recursive Clauses} 

Given this method for generalizing recursive clauses, one can
construct a learning algorithm for recursive clauses as follows.
First, guess a recursive literal $L_r$, and make
$H=\clongd{d}\cup{}L_r$ the initial hypothesis of the learner.  Then,
ask a series of equivalence queries. After a positive counterexample
$e^+$, use forced simulation to minimally generalize $H$ to cover
$e^+$.  After a negative example, choose another recursive literal
$L_r'$, and reset the hypothesis to $H=\clongd{d}\cup{}L_r'$.

Figure~\ref{force1 fig} presents an algorithm that operates along
these lines.  Let $\lrdepth{d}$ denote the language of linear closed
recursive clauses of depth $d$ or less. We have the following result:

\begin{theorem} \label{lr learnable}
For any constants $a$ and $d$, the language family
\[ \lrdepth{d}[\dbset^=,\detdecj{a}^{=1}]
\] 
is uniformly identifiable from equivalence queries.
\end{theorem}

\begin{proof}
We will show that $\cd{Force1}$ uniformly identifies this language
family with a polynomial number of queries.  

{\bf Correctness and query efficiency}. 
There are at most $a\size{D}+a\size{DB}$
constants in any set $\db\cup{}D$, at most
$(a\size{D}+a\size{DB})^{a'}$ $a'$-tuples of such constants, and hence
at most $(a\size{D}+a\size{DB})^{a'}$ distinct recursive subgoals
$L_r\sigma$ that might be produced in proving that a linear recursive
clause $C$ covers an extended instance $(f,D)$.  Thus every
terminating proof of a fact $f$ using a linear recursive clause $C$
must be of depth $(a\size{D}+a\size{DB})^{a'}$ or less; {\it i.e.},
for $h=(a\size{D}+a\size{DB})^{a'}$,
\[
	C\wedge\db\wedge{}D\vdash_h f \mbox{~~~iff~~~}
	C\wedge\db\wedge{}D\vdash f 
\]
Thus Theorem~\ref{forcesim res} can be strengthened: for the value of
$h$ used in \cd{Force1}, the subroutine \cd{ForceSim} returns the
syntactically largest subclause of $H$ that covers the example $(f,D)$
whenever any such a subclause exists, and returns \cd{FAILURE}
otherwise.

We now argue the correctness of the algorithm as follows.  Assume
that the hypothesized recursive literal is ``correct''---{\it i.e.},
that the target clause $C_T$ is some subclause of
$\clongd{d}\cup{}L_r$.  In this case it is easy to see that
\cd{Force1} will identify $C_T$, using an argument that parallels the
one made for $\cd{Force1}_{\it NR}$.  Again by analogy to
$\cd{Force1}_{\it NR}$, it is easy to see that only a polynomial
number of equivalence queries will be made involving the correct
recursive literal.

Next assume that $L_r$ is not the correct recursive literal.  Then
$C_T$ need not be a subclause of $\clongd{d}\cup{}L_r$, and the
response to an equivalence query may be either a positive or negative
counterexample.  If a positive counterexample $e^+$ is received and
\cd{ForceSim} is called, then the result may be
\cd{FAILURE}, or it may be a proper subclause of $H$ that
covers $e^+$.  Thus the result of choosing an incorrect $L_r$ will be
a (possibly empty) sequence of positive counterexamples followed by
either a negative counterexample or \cd{FAILURE}.  Since all
equivalence queries involving the correct recursive literal will be
answered by either a positive counterexample or
``yes''\footnote{Recall that an answer of ``yes'' to an equivalence
query means the hypothesis is correct.}, then if a negative
counterexample or \cd{FAILURE} is obtained, it must be that $L_r$ is
incorrect.

The number of variables in $\clongd{d}$ can be bounded by
$a\size{\clongd{d}(\dec)}$, and as each closed recursive literal is
completely defined by an $a'$-tuple of variables, the number of
possible closed recursive literals $L_r$ can be bounded by
\[ p = (a\size{\clongd{d}(\dec)})^{a'}
\]
Since $\size{\clongd{d}(\dec)}$ is polynomial in $\size{\dec}$, $p$ is
also polynomial in $\size{\dec}$.  This means that only a polynomial
number of incorrect $L_r$'s need to be discarded. Further since each
successive hypothesis using a single incorrect $L_r$ is a proper
subclause of the previous hypothesis, only a polynomial number of
equivalence queries are needed to discard an incorrect $L_r$.  Thus
only a polynomial number of equivalence queries can be made involving
incorrect recursive literals.

Thus \cd{Force1} needs only a polynomial number of queries to identify
$C_t$.

{\bf Efficiency.} 
\cd{ForceSim} runs in time polynomial in its
arguments $H^*$, $f$, $\dec$, $\db\cup{}D$ and $h$. When
\cd{ForceSim} is called from \cd{Force1}, $h$ is always polynomial in
$\maxi$ and $\size{DB}$, and $H$ is always no larger than
$\size{\clongd{d}(\dec)}+1$, which in turn is polynomial in the size
of $\dec$.  Hence every invocation of $\cd{ForceSim}$ requires time
polynomial in $\maxi$, $\dec$, and $\db$, and hence \cd{Force1}
processes each query in polynomial time.

This completes the proof.
\end{proof}

This result is somewhat surprising, as it shows that recursive clauses
can be learned even given an adversarial choice of training examples.
In contrast, most implemented ILP systems require well-choosen
examples to learn recursive clauses.

This formal result can also be strengthened in a number of technical
ways.  One of the more interesting strengthenings is to consider a
variant of \cd{Force1} that maintains a fixed set of positive and
negative examples, and constructs the set of all least general clauses
that are consistent with these examples: this could be done by taking
each of the clauses $\clongd{d}\cup{}L_{r_1}$, \ldots,
$\clongd{d}\cup{}L_{r_p}$, forcibly simulating them on each of the
positive examples in turn, and then discarding those clauses that
cover one of more negative examples.  This set of clauses could then
be used to tractably encode the version space of {\em all\/}
consistent programs, using the $[S,N]$ representation for version
spaces \cite{HirshAAAI92}.

\section{Extending the Learning Algorithm} \label{learn one extensions}

We will now consider a number of ways in which the result of
Theorem~\ref{lr learnable} can be extended.

\subsection{The Equality-Predicate and Unique-Mode Assumptions}
\label{relax unique-mode}

Theorem~\ref{lr learnable} shows that the language family
\[
\lrdepth{d}[\dbset^=,\detdecj{a}^{=1}]
\]
is identifiable from equivalence queries.  It is natural to ask if
this result can be extended by dropping the assumptions that an
equality predicate is present and that the declaration contains a
unique legal mode for each predicate: that is, if the result can be
extended to the language family
\[
\lrdepth{d}[\dbset,\detdecj{a}]
\]

This extension is in fact straightforward.  Given a database $\db$ and
a declaration $\dec=(p,a',R)$ that do not satisfy the equality-predicate
and unique-mode assumptions, one can modify them as follows.
\begin{enumerate}
\item \label{db xform 1}
For every constant $c$ appearing in $\db$, add the fact
$\cd{equal(c,c)}$ to $\db$.

\item For every predicate $q$ that has $k$ valid modes
$qs_1$, \ldots, $qs_k$ in $R$:
\begin{enumerate}
\item remove the mode declarations for $q$,
and replace them with $k$ mode strings for the $k$ new predicates
$q_{s_1}$, \ldots, $q_{s_k}$, letting $q_{s_i}s_i$ be the unique legal
mode for the predicate $q_{s_i}$;
\item \label{db xform 2}
remove every fact $q(t_1,\ldots,t_a)$ of the predicate $q$ from
$\db$, and replace it with the $k$ facts $q_{s_1}(t_1,\ldots,t_a)$,
\ldots, $q_{s_k}(t_1,\ldots,t_a)$.
\end{enumerate}
\end{enumerate}
Note that if the arity of predicates is bounded by a constant $a$,
then the number of modes $k$ for any predicate $q$ is bounded by the
constant $2^a$, and hence these transformations can be performed in
polynomial time, and with only a polynomial increase in the size of
$\dec$ and $\db$.

Clearly any target clause $C_t\in\lrdepth{d}[\db,\dec]$ is equivalent to
some clause $C_t'\in\lrdepth{d}[\db',\dec']$, where $\db'$ and $\dec'$ are
the modified versions of $\db$ and $\dec$ constructed above.  Using
\cd{Force1} it is possible to identify $C_t'$. (In learning $C_t'$,
one must also perform steps \ref{db xform 1} and \ref{db xform 2}
above on the description part $D$ of every counterexample $(f,D)$.)
Finally, one can convert $C_t'$ to an equivalent clause in
$\lrdepth{d}[\db,\dec]$ by repeatedly resolving against the clause
\cd{equal(X,X)$\hcif$}, and also replacing every predicate symbol $q_{s_i}$
with $q$.

This leads to the following strengthening of Theorem~\ref{lr
learnable}:

\begin{proposition} \label{no assumpts}
For any constants $a$ and $d$, the language family
\[ \lrdepth{d}[\dbset,\detdecj{a}]
\] 
is uniformly identifiable from equivalence queries.
\end{proposition}

\subsection{The Datalog Assumption}
\label{relax datalog}

So far we have assumed that the target program contains no function
symbols, and that the background knowledge provided by the user is a
database of ground facts.  While convenient for formal analysis, these
assumptions can be relaxed.

Examination of the learning algorithm shows that the database $\db$ 
is used in only two ways.
\begin{itemize}
\item In forcibly simulating a hypothesis on an extended instance
$(f,D)$, it is necessary to find a substitution $\sigma'$ that makes a
literal $L$ true in the database $\db\cup{}D$.  While this can be done
algorithmically if $\db$ and $D$ are sets of ground facts, it is also
plausible to assume that the user has provided an oracle that answers
in polynomial time any mode-correct query $L$ to the database $\db$.
Specifically, the answer of the oracle will be either
\begin{itemize}
\item the (unique) most-general substitution $\sigma'$ such that 
$\db\wedge{}D\vdash{}L\sigma'$ and $L\sigma'$ is ground; or 
\item ``no'' if no such $\sigma'$ exists.
\end{itemize}
Such an oracle would presumably take the form of an efficient
theorem-prover for $\db$.

\item When calling $\cd{ForceSim}$, the top-level learning
algorithm uses $\db$ and $D$ to determine a depth bound on the length
of a proof made using the hypothesis program.  Again, it is reasonable
to assume that the user can provide this information directly, in the
form of an oracle.  Specifically, this oracle would provide for any
fact $f$ a polynomial upper bound on the depth of the proof for $f$ in
the target program.
\end{itemize}
Finally we note that if efficient (but non-ground) background
knowledge is allowed, then function symbols always can be removed via
flattening \cite{RouveirolMLJ94}. This transformation also preserves
determinacy, although it may increase depth---in general, the depth of
a flattened clause depends also on term depth in the original clause.
Thus, the assumption that the target program is in Datalog can be
replaced by assumptions that the term depth is bounded by a constant,
and that two oracles are available: an oracle that answers queries to
the background knowledge, and a depth-bound oracle.  Both types of
oracles have been frequently assumed in the literature
\cite{ShapiroThesis,PageILP92,DzeroskiCOLT92}.

\subsection{Learning $k$-ary Recursive Clauses}

It is also natural to ask if Theorem~\ref{lr learnable} can be extended to
clauses that are not linear recursive.  One interesting case is the case of
closed $k$-ary recursive clauses for constant $k$. It is straightforward to
extend \cd{Force1} to guess a tuple of $k$ recursive literals $L_{r_1}$,
\ldots, $L_{r_k}$, and then to extend \cd{ForceSim} to recursively
generalize the hypothesis clause on each of the facts $L_{r_1}\sigma$,
\ldots, $L_{r_k}\sigma$.  The arguments of Theorems~\ref{forcesim res} and
\ref{lr learnable} can be modified to show that this extension will identify
the target clause after a polynomial number of equivalence queries.

Unfortunately, however, it is no longer the case that \cd{ForceSim}
runs in polynomial time.  This is easily seen if one considers a tree
of all the recursive calls made by \cd{ForceSim}; in general, this
tree will have branching factor $k$ and polynomial depth, and hence
exponential size.  This result is unsurprising, as the implementation
of \cd{ForceSim} described forcibly simulates a depth-bounded top-down
interpreter, and a $k$-ary recursive program can take exponential time
to interpret with such an interpreter.

There are at least two possible solutions to this problem.  One
possible solution is to retain the simple top-down forced simulation
procedure, and require the user to provide a depth bound tighter than
$(a\size{D}+a\size{DB})^{a'}$, the maximal possible depth of a tree.
For example, in learning a 2-ary recursive sort such as quicksort,
the user might specify a logarithmic depth bound, thus guaranteeing that
\cd{ForceSim} is polynomial-time.  This requires additional input
>from the user, but would be easy to implement. It also has the
advantage (not shared by the approach described below) that the
hypothesized program can be executed using a simple depth-bounded
Prolog interpreter, and will always have shallow proof trees.  This
seems to be a plausible bias to impose when learning $k$-ary recursive
Prolog programs, as many of these tend to have shallow proof trees.

A second solution to the possible high cost of forced simulation for
$k$-ary recursive programs is to forcibly simulate a ``smarter'' type
of interpreter---one which can execute $k$-ary recursive program in
polynomial time.\footnote{Note that it is plausible to believe that
such a theorem-prover exists, as there are only a polynomial number of
possible theorem-proving goals---namely, the
$(a\size{D}+a\size{DB})^{a'}$ possible recursive subgoals.} One sound
and complete theorem-prover for closed $k$-ary recursive programs can
be implemented as follows.

Construct a top-down proof tree in the usual fashion, {\it i.e.},
using a depth-first left-to-right strategy, but maintain a list
of the ancestors of the current subgoal, and also a list
\cd{VISITED} that records, for each previously visited node in the tree, the
subgoal associated with that node.  Now, suppose that in the course of
constructing the proof tree one generates a subgoal $f$ that is on the
\cd{VISITED} list.  Since the traversal of the tree is depth-first
left-to-right, the node associated with $f$ is either an ancestor of
the current node, or is a descendant of some left sibling of an
ancestor of the current node.  In the former case, the proof tree
contains a loop, and cannot produce a successful proof; in this case
the theorem-prover should exit with failure.  In the latter case, a
proof must already exist for $f'$, and hence nodes below the current
node in the tree need not be visited; instead the theorem prover can
simply assume that $f$ is true.

This top-down interpreter can be easily extended into a forced simulation
procedure: one simply traverses the tree in the same order, generalizing the
current hypothesis $H$ as needed to justify each inference step in the
tree.  The only additional point to note is that if one is performing forced
simulation and revisits a previously proved subgoal $f$ at a node $n$, the
current clause $H$ need not be further generalized in order to prove $f$,
and hence it is again permissible to simply skip the portion of the tree
below $n$.  We thus have the following result.

\begin{theorem} \label{kary rec learnable}
Let $\krdepth{d}{k}$ be the set of $k$-ary closed recursive clauses of
depth $d$.  For any constants $a$, $d$, and $k$ the language family
\[ \krdepth{d}{k}[\dbset,\detdecj{a}]
\] 
is uniformly identifiable from equivalence queries.
\end{theorem}

\begin{proof} Omitted, but following the informal argument
made above.
\end{proof}

Note that we give this result without the restrictions that the
database contains an equality relation and that the declaration is
unique-mode, since the tricks used to relax these restrictions in
Proposition~\ref{no assumpts} are still applicable.

\subsection{Learning Recursive and Base Cases Simultaneously}

So far, we have analyzed the problem of learning single clauses: first
a single nonrecursive clause, and then a single recursive clause.
However, every useful recursive program contains at least two clauses:
a recursive clause, and a nonrecursive base case.  It is natural to
ask if it is possible to learn a complete recursive program by
simultaneously learning both a recursive clause, and its associated
nonrecursive base case.

\begin{figure}
%\hrule
\begin{alg}
{\bf begin algorithm $\cd{Force2(d,\dec,\db)}$:}\\
\> {\bf let} $L_{r_1},\ldots,L_{r_p}$ be all possible 
		 recursive literals for $\clongd{d}(\dec)$\\
\> choose an unmarked recursive literal $L_{r_i}$\\
\> {\bf let} $H^*_R \leftarrow \clongd{d}(\dec) \cup \{L_{r_i}\}$\\
\> {\bf let} $H^*_B \leftarrow \clongd{d}(\dec)$\\
\> {\bf let} $P=(H_R,H_b)$\\
\> {\bf repeat} \\
\> \> \cd{Ans} $\leftarrow$ answer to query ``Is $H^*_R,H^*_B$ correct?'' \\
\> \> {\bf if } $\cd{Ans}=$``yes'' {\bf then} {\bf return $H^*_R,H^*_B$} \\
\> \> {\bf elseif} \cd{Ans} is a negative example $e^-$ {\bf then}\\
\> \> \> $P\leftarrow\cd{FAILURE}$ \\
\> \> {\bf elseif} \cd{Ans} is a positive example $e^+$ {\bf then}\\
\> \> \> {\bf let} $(f,D)$ be the components of $e^+$\\
\> \> \> $P \leftarrow
 \cd{ForceSim2(H^*_R,H^*_B,f,\dec,(\db\cup{}D),(a\size{D}+a\size{DB})^{a'})}$\\
\> \> {\bf endif}\\
\> \> {\bf if} $P=\cd{FAILURE}$ {\bf then}\\
\> \> \> {\bf if} all recursive literals $L_{r_j}$ are marked {\bf then}\\
\> \> \> \> {\bf return} ``no consistent hypothesis''\\
\> \> \> {\bf else} \\
\> \> \> \> mark $L_{r_i}$\\
\> \> \> \> choose an unmarked recursive literal $L_{r_j}$\\
\> \> \> \> {\bf let} $H^*_R \leftarrow \clongd{d}(\dec) \cup \{L_{r_j}\}$\\
\> \> \> \> {\bf let} $H^*_B \leftarrow \clongd{d}(\dec)$\\
\> \> \> \> {\bf let} $P=(H_R^*,H_B^*)$\\
\> \> \> {\bf endif}\\
\> \> {\bf endif}\\
\> {\bf endrepeat}\\
{\bf end}
\end{alg}
\caption{A learning algorithm for two-clause recursive programs}
\label{force2 fig}
%\hrule
\end{figure}


\begin{figure}
%\hrule
\begin{alg}
{\bf begin subroutine $\cd{ForceSim2(H_R,H_B,f,\dec,\db,h)}$:}\\
\> {\it \% ``forcibly simulate'' program $H_R,H_B$ on $f$}\\
\> {\bf if} $h<1$ {\bf then return} \cd{FAILURE}\\
\> {\it \% check to see if $f$ should be covered by $H_B$}\\
\> {\bf elseif} $\cd{BASECASE(f)}$ {\bf then}\\
\> \> {\it return current $H_r$ and generalized $H_B$}\\
\> \> {\bf return} $(H_R,\cd{ForceSim_{\it NR}(H_B,f,\dec,\db)})$\\
\> {\bf elseif} the head of $H_R$ and $f$ cannot be unified {\bf then}\\
\> \> {\bf return} \cd{FAILURE}\\
\> {\bf else} \\
\> \> {\bf let} $L_r$ be the recursive literal of $H_R$\\
\> \> {\bf let} $H' \leftarrow H-\{L_r\}$\\
\> \> {\bf let} $A$ be the head of $H'$ \\
\> \> {\bf let} $\sigma$ be the mgu of $A$ and $e$\\
\> \> {\bf for} each literal $L$ in the body of $H'$ {\bf do}\\
\> \> \> {\bf if} there is a substitution $\sigma'$ such that $L\sigma\sigma'\in\db$\\
\> \> \> {\bf then} $\sigma \leftarrow \sigma\circ\sigma'$, where
 	   	     $\sigma'$ is the most general such substitution\\
\> \> \> {\bf else} \\
\> \> \> \> delete $L$ from the body of $H'$, together with\\
\> \> \> \> ~~all literals $L'$ supported (directly or indirectly) by $L$\\
\> \> \> {\bf endif}\\
\> \> {\bf endfor} \\
\> \> {\it \% generalize $H',H_B$ on the recursive subgoal $L_r\sigma$}\\
\> \> {\bf if} $L_r\sigma$ is ground {\bf then}\\
\> \> \> {\it \% continue the simulation of the program}\\
\> \> \> {\bf return} 
	   \cd{ForceSim2}($H'\cup\{L_r\},H_B,L_r\sigma,\dec,\db,h-1$)\\
\> \> {\bf else return} \cd{FAILURE} \\
\> \> {\bf endif} \\
\> {\bf endif}\\
{\bf end}  \\
\end{alg}
\caption{Forced simulation for two-clause recursive programs}
\label{forcesim2 fig}
%\hrule
\end{figure}

In general, this is not possible, as is demonstrated elsewhere
\cite{CohenJAIRNeg}.  However,
there are several cases in which the positive result can be extended
to two-clause programs.  In this section, we will first discuss
learning a recursive clause and base clause simultaneously, assuming
that any determinate base clause is possible, but also assuming that
an additional ``hint'' is available, in the form of a special
``{basecase}'' oracle.  We will then discuss various alternative types
of ``hints''.

Let $P$ be a target program with base clause $C_B$ and recursive
clause $C_R$.  A \trm{basecase oracle} for $P$ takes as input an
extended instance $(f,D)$ and returns ``yes'' if
$C_B\wedge\db\wedge{}D\vdash{}f$, and ``no'' otherwise. In other
words, the oracle determines if $f$ is covered by the nonrecursive
base clause alone.  As an example, for the
\cd{append} program, the {basecase} oracle should return ``yes'' for
an instance \cd{append(Xs,Ys,Zs)} when \cd{Xs} is the empty list, and
``no'' otherwise.

Given the existence of a {basecase} oracle, the learning algorithm
can be extended as follows.  As before, all possible recursive
literals $L_{r_i}$ of the clause $\clongd{d}$ are generated; however,
in this case, the learner will test two clause hypotheses that are
initially of the form $(\clongd{d}\cup{}L_{r_i},\clongd{d})$.  To
forcibly simulate such a hypothesis on a fact $f$, the following
procedure is used.  After checking the usual termination conditions,
the forced simulator checks to see if \cd{BASECASE(f)} is true. If so,
it calls \cd{ForceSim$_{\it NR}$} (with appropriate arguments) to
generalize the current hypothesis for the base case.  If
\cd{BASECASE(f)} is false, then the recursive clause $H_r$ is forcibly
simulated on $f$, a subgoal $L_r\sigma$ is generated as in before, and
the generalized program is recursively forcibly simulated on the
subgoal.  Figures~\ref{force2 fig} and \ref{forcesim2 fig} present a
learning algorithm \cd{Force2} for two clause programs consisting of
one linear recursive clause $C_R$ and one nonrecursive clause $C_B$,
under the assumption that both equivalence and basecase oracles are
available.

It is straightforward to extend the arguments of Theorem~\ref{lr
learnable} to this case, leading to the following result.

\begin{theorem} \label{force2 res}
Let $\progtwodepth{d}$ be the set of 2-clause programs consisting of one
clause in $\lrdepth{d}$ and one clause in $\nrdepth{d}$.
For any constants $a$ and $d$ the language family
\[ \progtwodepth{d}[\dbset,\detdecj{a}]
\] 
is uniformly identifiable from equivalence and {basecase} queries.
\end{theorem}

\begin{proof} Omitted.
\end{proof}

A companion paper \cite{CohenJAIRNeg} shows that something like the
basecase oracle is necessary: in particular, without any ``hints''
about the base clause, learning a two-clause linear recursive program
is as hard as learning boolean DNF.  However, there are several
situations in which the basecase oracle can be dispensed with.
\begin{description}
\item[Case 1.] The basecase oracle can be replaced by a polynomial-sized
set of possible base clauses.  The learning algorithm in this case is
to enumerate pairs of base clauses $C_{B_i}$ and ``starting clauses''
$\clong\cup{}L_{r_j}$, generalize the starting clause with forced
simulation, and mark a pair as incorrect if overgeneralization is
detected.

\item[Case 2.] The basecase oracle can be replaced by a fixed rule that determines
when the base clause is applicable.  For example, consider the rule
that says that the base clause is applicable to any atom
$p(X_1,\ldots,X_a)$ such that no $X_i$ is a non-null list.  Adopting
such a rule leads immediately to a learning procedure that pac-learns
exactly those two-clause linear recursive programs for which the rule
is correct.

\item[Case 3.] 
The basecase oracle can be also be replaced by a polynomial-sized set
of rules for determining when a base clause is applicable.  The
learning algorithm in this case is pick a unmarked decision rule and
run \cd{Force2} using that rule as a basecase oracle.  If \cd{Force2}
returns ``no consistent hypothesis'' then the decision rule is marked
incorrect, and a new one is choosen.  This algorithm will learn those
two-clause linear recursive programs for which any of the given
decision rules is correct.
\end{description}
Even though the general problem of determining a basecase decision
rule for an arbitrary Datalog program may be difficult, it may be that
a small number of decision procedures apply to a large number of
common Prolog programs. For example, the recursion for most
list-manipulation programs halts when some argument is reduced to a
null list or to a singleton list.  Thus Case~3 above seems likely to
cover a large fraction of the automatic logic programming programs of
practical interest.

We also note that heuristics have been proposed for finding such
basecase decision rules automatically using typing restrictions
\cite{StahlECML93}.

\subsection{Combining the Results}

Finally, we note that all of the extensions described above are
compatible.  This means that if we let $\maxlang$ be the language of
two-clause programs consisting of one clause $C_R$ that is $k$-ary
closed recursive and depth-$d$ determinate, and one clause $C_B$ that
is nonrecursive and depth-$d$ determinate, then the following holds.

\begin{proposition} 
For any constants $a$, $k$ and $d$ the language family
\[ \maxlang[\dbset,\detdecj{a}]
\] 
is uniformly identifiable from equivalence and {basecase} queries.
\end{proposition}

\subsubsection{Further Extensions} \label{further}

The notation $\maxlang$ may seem at this point to be unjustified;
although it is the most expressive language of recursive clauses that
we have proven to be learnable, there are numerous extensions that 
may be efficiently learnable.  For example, one might generalize the
language to allow an arbitrary number of recursive clauses, or to
include clauses that are not determinate. These generalizations might
very well be pac-learnable---given the results that we have presented
so far.

However, a companion paper \cite{CohenJAIRNeg} presents a series of
negative results showing that most natural generalizations of
$\maxlang$ are not efficiently learnable, and further that $\maxlang$
itself is not efficiently learnable without the basecase oracle.
Specifically, the companion paper shows that eliminating the basecase
oracle leads to a problem that is as hard as learning boolean DNF, an
open problem in computational learning theory.  Similarly, learning
two linear recursive clauses simultaneously is as hard as
learning DNF, even if the base case is known.  Finally, the following
learning problems are all as hard as breaking certain (presumably)
secure cryptographic codes: learning $n$ linear recursive determinate
clauses, learning one $n$-ary recursive determinate clause, or
learning one linear recursive ``$k$-local'' clause.  All of these
negative results hold not only for the model of identification from
equivalence queries, but also for the weaker models of
pac-learnability and pac-predictability.

\section{Related Work} \label{previous}

In discussing related work we will concentrate on previous formal
analyses that employ a learning model similar to that considered here:
namely, models that (a) require all computation be polynomial in
natural parameters of the problem, and (b) assume either a neutral
source or adversarial source of examples, such as equivalence queries
or stochastically presented examples.  We note, however, that much
previous formal work exists that relies on different assumptions.  For
instance, there has been much work in which member or subset queries
are allowed \cite{ShapiroThesis,DeRaedtMLJ92}, or where examples are
choosen in some non-random manner that is helpful to the learner
\cite{LingILP92,DeRaedtILP94}.  There has also been some work in which
the efficiency requirements imposed by the pac-learnability model are
relaxed \cite{NienhuysChengECML94}.  If the requirement of efficiency
is relaxed far enough, very general positive results can be obtained
using very simple learning algorithms.  For example, in model of
learnability in the limit \cite{GoldIC67}, any language that is both
recursively enumerable and decidable (which includes all of Datalog)
can be learned by a simple enumeration procedure; in the model of
U-learnability
\cite{MuggletonPageILP94} any language that is polynomially enumerable and
polynomially decidable can be learned by enumeration.

The most similar previous work is that of Frazier and Page
\citeyear{FrazierAAAI93,FrazierILP93}. They analyze the learnability
>from equivalence queries of recursive programs with function symbols
but without background knowledge.  The positive results they provide
are for program classes that satisfy the following property: given a
set of positive examples $S^+$ that requires all clauses in the target
program to prove the instances in $S^+$, only a polynomial number of
recursive clauses are possible; further the base clause must have a
certain highly constrained form.  Thus the concept class is ``almost''
bounded in size by a polynomial.  The learning algorithm for such a
program class is to interleave a series of equivalence queries that
test every possible target program.  In contrast, our positive results
are for exponentially large classes of recursive clauses.  Frazier and
Page also present a series of negative results suggesting that the
learnable languages that they analyzed are difficult to generalize
without sacrificing efficient learnability.

Previous results also exist on the pac-learnability of nonrecursive
constant-depth determinate programs, and on the pac-learnability of
recursive constant-depth determinate programs in a model that also
allows membership and subset queries \cite{DzeroskiCOLT92}.

The basis for the intelligent search used in our learning algorithms
is the technique of \trm{forced simulation}. This method finds the
least implicant of a clause $C$ that covers an extended instance $e$.
Although when we developed this method we believed it to be original,
subsequently we discovered that this was not the case---an identical
technique had been previously proposed by Ling
\citeyear{LingTR91}.  Since an extended instance $e$ can be converted
(via saturation) to a ground Horn clause, there is also a close
connection between forced simulation and recent work on ``inverting
implication'' and ``recursive anti-unification''; for instance,
Muggleton \citeyear{MuggletonNthRoot} describes a nondeterministic
procedure for finding all clauses that imply a clause $C$, and
Idestam-Almquist \citeyear{IdestamAlmquistIMLC92} describes a means
of constraining such an implicant-generating procedure to produce the
least common implicant of two clauses.  However, while both of these
techniques have obvious applications in learning, both are extremely
expensive in the worst case.

The {\sc CRUSTACEAN} system \cite{AhaECML94} uses inverting implication in
constrained settings to learn certain restricted classes of recursive
programs.  The class of programs efficiently learned by this system is
not formally well-understood, but it appears to be similar to the
classes analyzed by Frazier and Page.  Experimental results show that
these systems perform well on inferring recursive programs that use
function symbols in certain restricted ways.  This system cannot,
however, make use of background knowledge.

Finally, we wish to direct the reader to several pieces of our own
research that are relevant.  As noted above, a companion paper exists
which presents negative learnability results for several natural
generalizations of the language $\maxlang$ \cite{CohenJAIRNeg}.
Another related paper investigates the learnability of non-recursive
Prolog programs \cite{CohenNonRecJnl93}; this paper also contains a
number of negative results which strongly motivate the restriction of
constant-depth determinacy.  A final prior paper which may be of
interest presents some experimental results with a Prolog
implementation of a variant of the \cd{Force2} algorithm
\cite{CohenAAAI93Force2}.  This paper shows that forced simulation can
be the basis of a learning program that outperforms state-of-the art
heuristic methods such as {\sc FOIL} \cite{QuinlanMLJ90,QuinlanECML93} in
learning from randomly chosen examples.

\section{Conclusions}

Just as it is often desirable to have guarantees of correctness for a
program, in many plausible contexts it would be highly desirable to
have an automatic programming system offer some formal guarantees of
correctness.  The topic of this paper is the learnability of recursive
logic programs using formally well-justified algorithms. More
specifically, we have been concerned with the development of
algorithms that are provably sound and efficient in learning
recursive logic programs from equivalence queries.  We showed that one
constant-depth determinate closed $k$-ary recursive clause is
identifiable from equivalent queries; this implies immediately that
this language is also learnable in Valiant's
\citeyear{ValiantCACM84} model of pac-learnability.  We also showed
that a program consisting of one such recursive clause and one
constant-depth determinate nonrecursive clause is identifiable from
equivalence queries given an additional ``basecase oracle'', which
determines if a positive example is covered by the non-recursive base
clause of the target program alone.

In obtaining these results, we have introduced several new formal
techniques for analyzing the learnability of recursive programs.  We
have also shown the soundness and efficiency of several instances of
\trm{generalization by forced simulation}. This method may have
applications in practical learning systems. The
\cd{Force2} algorithm compares quite well experimentally
with modern ILP systems on learning problems from the restricted class
that it can identify \cite{CohenAAAI93Force2}; thus sound learning
methods like \cd{Force2} might be useful as a filter before a more
general ILP system like {\sc FOIL} \cite{QuinlanMLJ90,QuinlanECML93}.
Alternatively, forced simulation could be used in heuristic programs.
For example, although forced simulation for programs with many
recursive clauses is nondeterministic and hence potentially
inefficient, one could introduce heuristics that would make the forced
simulation efficient, at the cost of completeness.

A companion paper \cite{CohenJAIRNeg} shows that the positive results
of this paper are not likely to be improved: either eliminating the
basecase oracle for the language above or learning two recursive
clauses simultaneously is as hard as learning DNF, and learning $n$
linear recursive determinate clauses, one $n$-ary recursive
determinate clause, or one linear recursive ``$k$-local'' clause is as
hard as breaking certain cryptographic codes.  With the positive
results of this paper, these negative results establish the boundaries
of learnability for recursive programs function-free in the
pac-learnability model. These results thus not only give a
prescription for building a formally justified system for learning
recursive programs; taken together, they also provide upper bounds on
what one can hope to achieve with an efficient, formally justified
system that learns recursive programs from random examples alone.

\appendix

\section{Additional Proofs} \label{additional proofs}

Theorem~\ref{clong res} states: Let $\dec=(p,a',R)$ be a declaration
in $\in\detdecj{a}^{=}$, let $\maxv=\size{R}$, let $X_1,\ldots,X_{a'}$
be distinct variables, and define the clause $\clongd{d}$ as follows:
\[ \clongd{d}(\dec) \equiv \constrain_{\dec}(\deepen^d_{\dec}(p(X_1,\ldots,X_{a'})\hcif))
\]
\begin{sloppypar}
For any constants $d$ and $a$, the following are true:
\begin{itemize}
\item the size of $\clongd{d}(\dec)$ is polynomial in $\maxv$;
\item every depth-$d$ clause that satisfies $\dec$
is equivalent to some subclause of $\clongd{d}(\dec)$.
\end{itemize}
\end{sloppypar}

\begin{proof}
Let us first establish the polynomial bound on the size of $\clongd{d}$.
Let $C$ be a clause of size $n$. As the number of variables in $C$ is
bounded by $an$, the size of the set ${\cal L}_D$ is bounded by
\[
	\underbrace{{\maxv}}_{\mbox{\footnotesize (\# modes)}}
\cdot 	\underbrace{{(an)^{a-1}}}_{\mbox{\footnotesize (\# tuples of input variables)}}
\]
Thus for any clause $C$ 
\begin{equation} \label{deepen bound}
 \size{\deepen_{\dec}(C)} \leq n+(an)^{a-1}\maxv
\end{equation}
By a similar argument
\begin{equation} \label{constrain bound}
 \size{\constrain_{\dec}(C)} \leq n+(an)^a\maxv
\end{equation}
Since both of the functions $\deepen_{\dec}$ and $\constrain_{\dec}$
give outputs that are polynomially larger in size than their inputs,
if follows that composing these functions a constant number of times,
as was done in computing $\clongd{d}$ for constant $d$, will also
produce only a polynomial increase in the size.

Next, we wish to show that every depth-$d$ determinate clause $C$ that
satisfies $\dec$ is equivalent to some subclause of $\clongd{d}$.  Let
$C$ be some depth-$d$ determinate clause, and without loss of
generality let us assume that no pair of literals $L_i$ and $L_j$ in
the body of $C$ have the same mode, predicate symbol, and sequence of
input variables.\footnote{This assumption can be made without loss of
generality since for a determinate clause $C$, the output variables of
$L_i$ and $L_j$ will necessarily be bound to the same values, and
hence $L_i$ or $L_j$ could be unified together and one of them deleted
without changing the semantics of $C$.}

Given $C$, let us now define the substitution $\theta_C$ as follows:
\begin{enumerate}
\item Initially set
\[ \theta_C \leftarrow \{X_1^* = X_1,\ldots,X_{a'}^*= X_{a'}\}
\]
where $X_1^*,\ldots,X_{a'}^*$ are the arguments to the head of
$\clongd{d}$ and $X_1,\ldots,X_{a'}$ are the arguments to the head of
$C$.

Notice that because the variables in the head of $\clongd{d}$ are
distinct, this mapping is well-defined.

\item Next, examine each of the literals in
the body of $C$ in left-to-right order.  For each literal $L$, let
variables $T_1,\ldots T_k$ be its input variables. For each literal
$L^*$ in the body $\clongd{d}$ with the same mode and predicate symbol
whose input variables $T^*_1,\ldots,T^*_k$ are such that 
$\forall i:1\leq{}i\leq{}r, T_j^*\theta_C=T_j$, modify $\theta_C$ as follows:
\[ \theta_C \leftarrow \theta_C \cup \{U_1^* = U_1,\ldots,U_l^*= U_l\}
\]
where $U_1,\ldots,U_l$ are the output variables of $L$ and
$U^*_1,\ldots,U^*_l$ are the output variables of $L^*$.

Notice that because we assume that $C$ contains only one literal $L$
with a given predicate symbol and sequence of input variables, and
because the output variables of literals $L^*$ in $\clongd{d}$ are
distinct, this mapping is again well-defined.  It is also easy to
verify (by induction on the length of $C$) that in executing this
procedure some variable in $\clongd{d}$ is always mapped to each input
variable $T_i$, and that at least one $L^*$ meeting the requirements
above exists. Thus the mapping $\theta_C$ is \trm{onto} the variables
appearing in $C$.\footnote{Recall that a function $f:X\leftarrow Y$ is
\trm{onto} its range $Y$ if $\forall y\in{}Y\exists x\in{}X : f(x)=y$.}
\end{enumerate}

Let $A^*$ be the head of $\clongd{d}$, and consider the clause $C'$
which is defined as follows:
\begin{itemize}
\item The head of $C'$ is $A^*$.
\item The body of $C'$ contains all literals $L^*$ from the body of 
$\clongd{d}$ such that either
\begin{itemize}
\item $L^*\theta_C$ is in the body of $C$
\item $L^*$ is the literal $\cd{equal(X^*_i,X^*_j)}$ and $X^*_i\theta_C=X^*_j\theta_C$.
\end{itemize}
\end{itemize}

We claim that $C'$ is a subclause of $\clongd{d}$ that is equivalent
to $C$.  Certainly $C'$ is a subclause of $\clongd{d}$.  One way to
see that it is equivalent to $C$ is to consider the clause $\hat{C}$
and the substitution $\hat{\theta_C}$ which are generated as follows.
Initially, let $\hat{C}=C'$ and let $\hat{\theta_C}=\theta_C$.  Then,
for every literal $L=\cd{equal}(X^*_i,X^*_j)$ in the body of
$\hat{C}$, delete $L$ from $\hat{C}$, and finally replace $\hat{C}$
with $\hat{C}\sigma_{ij}$ and replace $\hat\theta_C$ with
$(\hat\theta_C)\sigma_{ij}$, where $\sigma_{ij}$ is the substitution
$\{X^*_i=X^*_{ij},X^*_j=X^*_{ij}\}$ and $X_{ij}$ is some new variable
not previously appearing in $\hat{C}$.  (Note: by
$(\hat\theta_C)\sigma_{ij}$ we refer to the substitution formed by
replacing every occurrence of $X_i$ or $X_j$ appearing in
$\hat{\theta_C}$ with $X_{ij}$.)  $\hat{C}$ is semantically equivalent
to $C'$ because the operation described above is equivalent to simply
resolving each possible $L$ in the body of $C'$ against the clause
``\cd{equal(X,X)$\hcif$}''.

The following are now straightforward to verify:
\begin{itemize}
\item $\hat{\theta_C}$ is a one-to-one mapping.

To see that this is true, notice that for every pair of assignments
$X^*_i=Y$ and $X^*_j=Y$ in $\theta_C$ there must be a literal
$\cd{equal(X^*_i,X^*_j)}$ in $C'$.  Hence following the process
described above the assignments $X^*_i=Y$ and $X^*_j=Y$ in
$\hat\theta_C$ would eventually be replaced with $X^*_{ij}=Y$ and
$X^*_{ij}=Y$.

\item $\hat\theta_C$ is onto the variables in $C$.

Notice that $\theta_C$ was onto the variables in $C$, and for every
assignment $X_i^*=Y$ in $\theta_C$ there is some assignment in
$\hat\theta_C$ with a right-hand side of $Y$ (and this assignment is
either of the form $X_{i}^*=Y$ or $X_{ij}^*=Y$).  Thus $\hat\theta_C$
is also onto the variables in $C$.

\item A literal $\hat{L}$ is in the body of $\hat{C}$ iff $\hat{L}\hat\theta_C$
is in the body of $C$.

This follows from the definition of $C'$ and from the fact that for every
literal $L^*$ from $C'$ that is not of the form
$\cd{equal(X_i^*,X^*_j)}$ there is a corresponding literal in $\hat{C}$.
\end{itemize}
Thus $\hat{C}$ is an alphabetic variant of $C$, and hence is
equivalent to $C$.  Since $\hat{C}$ is also equivalent to $C'$, it
must be that $C'$ is equivalent to $C$, which proves our claim.
\end{proof}

\acks{The author wishes to thank three anonymous JAIR reviewers
for a number of useful suggestions on the presentation and technical
content.}

\vskip 0.2in
\bibliography{/home/wcohen/papers/bib/cohen,/home/wcohen/papers/bib/ml,/home/wcohen/papers/bib/se,/home/wcohen/papers/bib/books,/home/wcohen/papers/bib/colt,/home/wcohen/papers/bib/misc}
\bibliographystyle{theapa}

\end{document}



