\documentstyle [11pt]{article}

\setlength {\textwidth}{16.0cm}
\setlength {\textheight}{22.0cm}
\setlength {\evensidemargin}{0cm}
\setlength {\oddsidemargin}{0cm}
\setlength {\topmargin}{0.0cm}

%\pagestyle{headings}
%\pagestyle{myheadings}
%\markright{\hfill {\bf DRAFT: ~IN PREPARATION} \hfill}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%      ENVIRONMENTS        %%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%% theorems

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{property}{Property}
%\newcommand{\Proof}{{\it Proof.} (Sketch) }
%\newcommand{\Proof}{{\it Proof.\ }}
%\def\endproof{\nolinebreak$\Box$\par\addvspace{\bigskipamount}}

%%%%%% environments

\newenvironment{Proof}{{\noindent\it Proof:}}{\hfill $\Box$ \bigskip}

\newtheorem{dummylemma}{BLA}[section]
\newtheorem{ExamplE}[dummylemma]{\em Example}%[section]
\newenvironment{example}{\begin{ExamplE} \rm}{\hfill $\Box$ \end{ExamplE}}
\newenvironment{mathlines}[1]{\medskip\begin{center}\begin{math}\begin{array}{#1}}{\end{array}\end{math}\end{center}\medskip}

%\newtheorem{ex}{Example}
%\newenvironment{example}{\begin{ex} \rm}{\end{ex}}
%\def\endexampl{\nolinebreak$\Box$\par\addvspace{\bigskipamount}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%        MACROS         %%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%% ``strange names''

\newcommand{\lfp}{{\it lfp}}
\newcommand{\union}{\bigcup}
\newcommand{\blank}{\sqcup}
\newcommand{\name}{Sequence Datalog}
\newcommand{\Tname}{Transducer Datalog}
\newcommand{\pnrc}{nonrecursive wrt constructions}
\newcommand{\pnr}{nonrecursive}
\newcommand{\nrc}{pseudorecursive wrt constructions}
\newcommand{\nr}{pseudorecursive}
\newcommand{\wrc}{domain bounded}
\newcommand{\wrec}{domain bounded}
\newcommand{\rlr}{simple linear recursive}
\newcommand{\rl}{simple linear}
\newcommand{\lpc}{length preserving wrt constructions}
\newcommand{\lp}{length preserving}
\newcommand{\lpt}{length preserving transducer}
\newcommand{\td}{weakly safe}
\newcommand{\linear}{linear}
\newcommand{\nonlinear}{nonlinear}
%\newcommand{\ssafe}{safe}
\newcommand{\Ssafe}{Strongly Safe}
%\newcommand{\ssafety}{safety}
\newcommand{\ssafe}{strongly safe}
\newcommand{\ssafety}{strong safety}
\newcommand{\guarded}{guarded}
\newcommand{\unguarded}{unguarded}

%%%%%% alphabet and sequences

\newcommand{\alp}[2]{\Sigma_{#1}^{#2}}
\newcommand{\seq}[1]{\sigma_{#1}}
\newcommand{\length}{\mbox{\sc len}}
\newcommand{\subseq}{\mbox{\sc subseq}}
\newcommand{\e}{\epsilon}
\newcommand{\conc}{\bullet}
\newcommand{\nat}{\mathbin{\mbox{I}\mkern-3mu\mbox{N}}}

%%%%%% database

\newcommand{\rel}[1]{r_{#1}}
\newcommand{\Rel}[1]{R_{#1}}
\newcommand{\relations}{{\cal R}}
\newcommand{\Sscheme}{scheme}
\newcommand{\Sinst}{instance}
\newcommand{\scheme}{{\bf R}}
\newcommand{\instances}[1]{\mbox{\sc inst}({#1})}
\newcommand{\inst}{\mbox{\sc db}}
%\newcommand{\inst}{{\bf r}}
\newcommand{\dom}[1]{dom_{#1}}
\newcommand{\sdom}[1]{S_{#1}}
\newcommand{\idom}[1]{N_{#1}}
\newcommand{\domact}[2]{{\cal D}^{#1}_{#2}}
\newcommand{\query}{Q}
\newcommand{\Squery}{sequence query}
\newcommand{\Squeries}{sequence queries}
\newcommand{\Sfunction}{sequence function}
\newcommand{\Scomp}{computable}
\newcommand{\Qcompl}{query complete}
\newcommand{\Fcompl}{function complete}
\newcommand{\perm}{\rho}
\newcommand{\Cperm}{C--permutation}
\newcommand{\Cgeneric}{C--generic}
\newcommand{\C}{{\cal S}_C}
\newcommand{\enum}{\rho}

%%%%%% language

\newcommand{\lang}[1]{\mbox{\sc {#1}SDat}}
\newcommand{\svar}{V_{\alp{}{}}}
\newcommand{\ivar}{V_I}
\newcommand{\x}[1]{X_{#1}}
\newcommand{\n}[1]{N_{#1}}
\newcommand{\s}[1]{S_{#1}}
\newcommand{\sterm}[1]{s_{#1}}
\newcommand{\iterm}[1]{n_{#1}}
\newcommand{\sdue}[2]{[{#1}\mbox{:}{#2}]}
\newcommand{\suno}[1]{[{#1}]}
\newcommand{\tr}[1]{t_{#1}}
\newcommand{\eos}{end}
\newcommand{\pred}{{\cal P}}
\newcommand{\p}[1]{p_{#1}}
\newcommand{\arity}{\mbox{\sc arity}}
\newcommand{\atom}[1]{A_{#1}}
\newcommand{\cl}[1]{\gamma_{#1}}
\newcommand{\prog}{P}
\newcommand{\head}{\mbox{\sc head}}
\newcommand{\body}{\mbox{\sc body}}
\newcommand{\subs}[1]{\theta_{#1}}
\newcommand{\huniv}{\cal U}
\newcommand{\hbase}[2]{\mbox{{\sc hb}}_{{#1},{#2}}}
\newcommand{\interp}{I}
\newcommand{\uni}{\Delta}
\newcommand{\trasf}[1]{{T}_{\prog_{#1},\inst_{#1}}}
\newcommand{\trasfi}[2]{\trasf{#1}\uparrow{#2}}
\newcommand{\fpsem}[1]{\mbox{{\sc fp--sem}}(\prog_{#1},\inst_{#1})}
\newcommand{\dsem}[1]{\mbox{{\sc d--sem}}(\prog_{#1},\inst_{#1})}
\newcommand{\md}[1]{{\cal M}_{#1}}
\newcommand{\model}[1]{\md{#1}}
\newcommand{\modelsd}{\models_{\domact{}{}}}
\newcommand{\rew}[2]{\mbox{\sc rew}^{#1}({#2})}

%%%%%% lattice

\newcommand{\lattice}{\cal C}
\newcommand{\LEQ}{\preceq}
\newcommand{\lattleq}{(\lattice,\LEQ)}
\newcommand{\elem}[1]{(\interp_{#1},\uni_{#1})}
\newcommand{\lub}{\mbox{\sc lub}}
\newcommand{\glb}{\mbox{\sc glb}}

%%%%%% finiteness

\newcommand{\pdgp}{\mbox{{\sc pdg}}_\prog}
\newcommand{\adgp}{\mbox{{\sc adg}}_\prog}
\newcommand{\tdgp}{\mbox{{\sc tdg}}_\prog}
\newcommand{\nodi}{{\cal N}}
\newcommand{\archi}{{\cal A}}
\newcommand{\nodo}[2]{({#1},{#2})}
\newcommand{\slength}[1]{L({#1})}
\newcommand{\ls}[1]{L_{#1}}
\newcommand{\sint}[2]{I_{#2}({#1})}

%%%%%% transducers

\newcommand{\transducers}{{\cal T}}
\newcommand{\biotrans}{biological transducer}
\newcommand{\tmap}[1]{f_{#1}}
\newcommand{\tmapz}[1]{f^0_{#1}}
\newcommand{\MM}{\mbox{MM}}
\newcommand{\ST}{T}
\newcommand{\reach}{\vdash_c}
\newcommand{\stay}{-}
\newcommand{\move}{\rightarrow}
\newcommand{\inizio}{\lhd}
\newcommand{\out}{\mbox{\sc out}}
\newcommand{\op}{\mbox{\sc op}}
\newcommand{\goc}{\mbox{\sc gc}}
\newcommand{\outputsize}[2]{|out_{#1}^{#2}|}
\newcommand{\inputsize}[2]{|in_{#1}^{#2}|}

%%%%%% complexity

\newcommand{\Omicron}{{\cal O}}
\newcommand{\enc}{\mbox{\sc enc}}
\newcommand{\dtime}{\mbox{\sc dtime}}
\newcommand{\tm}{M}
\newcommand{\size}{\mbox{\sc size}}

%%%%%% other definitions

\newcommand{\powset}[1]{\mbox{2}^{#1}}
\newcommand{\eset}{\emptyset}
\newcommand{\IF}{\leftarrow}
\newcommand{\IFT}{\Leftarrow}
\newcommand{\hyp}{hyp}
\newcommand{\DNA}{\mbox{DNA}}
\newcommand{\RNA}{\mbox{RNA}}
\newcommand{\MRNA}{\mbox{MRNA}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%        DOCUMENT        %%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\title{\Large \bf Sequences, Datalog and Transducers}

\author{
\begin{tabular}{c}
{\bf Anthony Bonner} \smallskip\\
%
{\small Department of Computer Science} \\
{\small University of Toronto --- Canada M5S 1A1}
%\\ {\small tel: +416 978-7441,~~ fax: +416 978-4765}
\smallskip\\
%{\tt www.cs.toronto.edu/$\tilde{~}$bonner} \\
{\tt bonner@db.toronto.edu}
\end{tabular}
%
\and
%
\begin{tabular}{c}
{\bf Giansalvatore Mecca} \smallskip\\
%
{\small D.I.F.A. --- Universit\`a della Basilicata}
\\ {\small Via della Tecnica, 3 --- 85100 Potenza, Italy}
%\\ {\small tel: +39  971 474-638,~~ fax: +39 971 56537}
\smallskip\\
%{\tt http://poincare.inf.uniroma3.it:8080/$\tilde{~}$mecca/} \\
{\tt mecca@dis.uniroma1.it}
\end{tabular}
}

\date{}
%\date{\today}



%%%%%%%%%%%%%%%%%%%%%%%%  BEGIN DOCUMENT  %%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\maketitle
%\thispagestyle{empty}


%%%%%%%%%%%     ABSTRACT    %%%%%%%%%%%%%%%%%%%%%%%

\begin{abstract}
%\normalsize
\noindent
This paper develops a query language for sequence databases, such as
genome databases and text databases.  The language, called {\em
{\name}}, extends classical Datalog with interpreted function symbols
for manipulating sequences.  It has both a clear operational and
declarative semantics, based on a new notion called the\/ {\em
extended active domain}\/ of a database.  The extended domain contains
all the sequences in the database and all their subsequences. This
idea leads to a clear distinction between safe and unsafe recursion
over sequences: safe recursion stays inside the extended active
domain, while unsafe recursion does not.  By carefully limiting the
amount of unsafe recursion, the paper develops a safe and expressive
subset of {\name}.  As part of the development, a new type of
transducer is introduced, called a\/ {\em generalized sequence
transducer}.  Unsafe recursion is allowed only within these
generalized transducers.  Generalized transducers extend ordinary
transducers by allowing them to invoke other transducers as
``subroutines.''  Generalized transducers can be implemented in
{\name} in a straightforward way.  Moreover, their introduction into
the language leads to simple conditions that guarantee safety and
finiteness.  This paper develops two such conditions.  The first
condition expresses exactly the class of {\sc ptime} sequence
functions; and the second expresses exactly the class of elementary
sequence functions.
\end{abstract}
%\vspace{8mm}


%\begin{center}
%\framebox{
%\begin{minipage}{5.5in}
%Submitted to the {\it Journal of Computer and System Sciences
%(JCSS)\/}, special issue on the {\it Fourteenth ACM International
%Symposium on Principles of Database Systems (PODS'95)\/}.
%\end{minipage}
%}
%\end{center}



%%%%%%%%%%% TABLE OF CONTENTS %%%%%%%%%%%%%%%%%%%%

%\newpage
%\pagenumbering{roman}
%\setcounter{page}{1}
%{\setlength{\baselineskip}{1.5\baselineskip}  \tableofcontents}


%%%%%%%%%%%     INTRODUCTION   %%%%%%%%%%%%%%%%%%%%

%\newpage
%\pagenumbering{arabic}
%\setcounter{page}{1}

\section{Introduction}

Sequences represent an important feature of {\em Next Generation
Database Systems}~\cite{Atk+89,Comm90}.  In recent years, new
applications have arisen in which the storage and manipulation of
sequences of unbounded length is a crucial feature.  A prominent
example is {\em genome databases}, in which long sequences
representing genetic information are stored, and sophisticated pattern
matching and restructuring facilities are needed~\cite{CACM91}.  These
new applications have led to the introduction of sequence types in
recent data models and query languages
($e.g.$~\cite{AlCO85,LOGIDATA,BaCD89,VaDW91,Catt94}).  In many cases,
however, queries over sequences are described only by means of a set
of pre-defined, {\em ad hoc}\/ operators, and are not investigated in
a theoretical framework.  In other cases,
($e.g.$~\cite{HeSi93,Sear93}) query languages concentrate on {\em
pattern extraction\/} capabilities and do not consider\/ {\em sequence
restructurings}.  Although pattern recognition is a fundamental
feature of any language for querying sequences, sequence
restructurings are equally important.  For example, in genome
databases, one frequently needs to concatenate sequences together, to
splice out selected subsequences, and to compute the reverse of a
sequence.  In addition, because genome-technology is rapidly evolving,
new sequence operations are constantly needed, operations that cannot
be anticipated in advance. Genome databases thus need to combine a
declarative query language with arbitrary procedures for efficiently
executing sequence operations~\cite{Good95}.

Sequence data presents interesting challenges in the development of
query languages.  For instance, the query language should be {\em
expressive}\/ both in terms of pattern matching and sequence
restructurings.  At the same time, it should have a natural syntax and
a clear semantics.  Finally, it should be {\em safe}.  Safety and
finiteness of computations is a major concern when dealing with
sequences, since by growing in length, sequences can easily become
unbounded, even when the underlying alphabet---or domain---is finite.
This means that, unlike traditional query languages, sequence queries
can end up in nonterminating computations.

%To achieve expressiveness, database researchers have developed sequence
%query languages based on abstract machines, such as {\it transducers\/}
%(finite automata that can generate strings as well as read them).
%Unfortunately, to achieve safety, they have had to impose restrictions
%that severely limit expressiveness ($e.g.$,
%\cite{GiWa92,Wang92,GrNU94}).

To address this problem, we propose a new logic called {\em \name}\/ for
reasoning about sequences.  {\name} has both a clear declarative
semantics and an operational semantics.  The semantics are based on
fixpoint theory, as in classical Logic Programming~\cite{Lloy87}.

%Thus, each {\name} program, $P$, has an associated operator, $T_P$, that
%maps databases to databases.  Each application of $T_P$ may create new
%atoms, which may contain new sequences.  $T_P$ is monotonic and
%continuous and has a least fixpoint.  If the least fixpoint is finite,
%then we say that the program has a {\em finite}\/ semantics; otherwise,
%it has an {\em infinite}\/ semantics.

We show that {\name} can express all computable sequence functions. To
achieve safety and finiteness, we introduce two devices.  $(i)$ We
distinguish between structural recursion (which is safe) and
constructive recursion (which is unsafe).  We also develop a semantic
counterpart to structural recursion, which we call the {\it extended
active domain}.  $(ii)$ We allow the use of constructive recursion in
a controlled fashion.  In effect, we allow constructive recursion to
simulate a new kind of machine that we call a {\it generalized
transducer}.  Ordinary transducers are finite automata that read input
sequences and generate output sequences.  A generalized transducer is
a transducer that can invoke other transducers as subroutines.  Like
transducers, generalized transducers always terminate.  We can
therefore use them as the basis for a safe variant of \name, which we
call {\it \ssafe} {\it \Tname}.  However, because generalized
transducers are more powerful than ordinary transducers, this safe
language retains considerable expressive power.  For instance, with
one level of transducer subroutine calls, it can express any mapping
from sequences to sequences computable in {\sc ptime}.  With two
levels of subroutine calls, it can express any mapping from sequences
to sequences in the elementary functions~\cite{Papa94}.

The rest of this section describes related work, and provides an
introduction to {\name} and generalized transducers.
Section~\ref{sec:preliminary} then defines preliminary notions, such
as sequence database and sequence query, that are used throughout this
paper.  Section~\ref{sec:language} defines the syntax of {\name}, and
develops its fixpoint semantics.  (Appendix~\ref{app:model} develops
an equivalent model-theoretic semantics.)  Section~\ref{sec:express}
shows that {\name} expresses exactly the class of computable sequence
functions.  Section~\ref{sec:finite} addresses issues of finiteness
and safety, and shows that determining whether a {\name} program has a
finite semantics is a fully undecidable problem ($i.e.$, is outside of
RE).  Section~\ref{sec:seqtrans} develops the notion of generalized
sequence transducer, and of transducer network, and characterizes the
expressibility of two classes of networks based on the depth of
subtransducer calls.  Section~\ref{sec:td} integrates generalized
transducers into {\name}, to form a new language called {\Tname}, and
shows that the two languages are expressively equivalent.  Finally,
Section~\ref{sec:safetd} develops simple syntactic restrictions for
{\Tname}, shows that they guarantee {\it both\/} a finite semantics
{\it and\/} high expressibility, and characterizes the expressibility
of the restricted language.  Appendix~\ref{app:guarded} establishes
results on a class of ``guarded'' programs, results used in a number
of expressibility proofs in the paper.




%%%%%%%%%%  OTHER LANGUAGES FOR SEQUENCES  %%%%%%%%%%%

\subsection{Background}
\label{sec:background}

Sequence query languages have been recently investigated in the
context of functional and algebraic programming~\cite{CRSV94,GrMi95},
and some sophisticated and expressive languages have been proposed.
Great care has been devoted to the development of {\em tractable\/}
languages, that is, languages whose complexity is in {\sc ptime}.

In~\cite{CRSV94}, for example, a functional query language for nested
lists is obtained by introducing a new form of structural recursion
called {\em list traversal}, in which two different lists are used.
One list is used to control the number of iterative steps, while the
other list can be modified at each iteration.  This mechanism ensures
that query answers are finite.  The language is then restricted to
express exactly the class of {\sc ptime} mappings over nested lists.

A similar result is reported in~\cite{GrMi95}, in which an algebra for
{\em partially ordered multi-sets\/} ({\sc pomsets\/}) is defined.
The algebra is obtained by extending the {\em bag algebra\/} of
\cite{GrMi93} with new operators to handle arbitrary {\sc pomsets},
plus an iterator for performing structural recursion~\cite{BTBN91}.
The authors define a tractable fragment of the language by restricting
the class of structures allowed and introducing a form of {\em bounded
iterator\/} to prevent exponential growth of query answers.  When
restricted to relational structures, the tractable language is shown
to be equivalent to first-order logic augmented with operators for
counting and computing least fixpoints~\cite{GrOt93}.  When restricted
to lists, that is, to totally ordered structures, the language
expresses exactly the class of {\sc ptime\/} mappings over lists.

%The characterizations of {\sc ptime} reported in~\cite{CRSV94,GrMi95}
%represent fundamental contributions to the manipulation of lists in
%databases. However, in our opinion, these languages lack the elegance
%and simplicity of relational algebra, especially when applied to
%lists.  For this reason, we explore a different approach to the
%problem, an approach based on {\it logic\/} programming, instead of
%{\it functional\/} programming.

In this paper, we explore a different approach to the problem, an
approach based on {\it logic\/} programming, instead of {\it
functional\/} programming. In particular, we develop an extension of
Datalog that is a simple yet powerful tool for manipulating sequences
in databases. We first propose a simple intuitive syntax for the
language, and develop a clear logical semantics.  We then establish
its data complexity, expressive power, and finiteness properties.

The trade-off between {\em expressiveness}, {\em finiteness\/} and
effective {\em computability\/} is typically a hard one.  In many
cases, powerful logics for expressing sequence transformations have
been proposed, but a great part of the expressive power was sacrificed
to achieve finiteness and safety.  In other cases, both expressiveness
and finiteness were achieved, but at the expense of an effective
procedure for evaluating queries, $i.e.$, at the expense of an
operational semantics.

In~\cite{GiWa92,Wang92}, for example, an {\em extended relational
model\/} is defined, where each relation is a set of tuples of
sequences over a fixed alphabet.  A {\em sequence logic}~\cite{GiWa92}
is then developed based on the notion of {\em rs-operations}.  Each
{\em rs-operation\/} is either a {\em merger\/} or an {\em extractor}.
Intuitively, given a set of patterns, an associated {\em merger\/}
uses the patterns to ``merge'' a set of sequences.  An {\em
extractor\/} ``retrieves'' subsequences of a given sequence.  The
authors introduce the notion of a {\em generic a-transducer\/} as the
computational counterpart of {\rm rs-operations}.  Based on their
sequence logic, two languages for the extended relational model are
defined, called the {\em s-calculus\/} and the {\em s-algebra}.  The
s-calculus allows for {\em unsafe\/} queries, that is, queries whose
semantics is not computable.  A {\em safe\/} subset of the language is
then defined and proven equivalent to the s-algebra.  Unfortunately,
this safe sublanguage cannot express many queries for which the length
of the result depends on the database.  These include natural queries
such as the {\em reverse\/} and the {\em complement\/} of a sequence.

%Intuitively, the {\em safe} version of the s-calculus is restricted to
%queries for which it is possible to bound, independently of the
%database, the length of sequences in the final result and in
%intermediate results~\cite{Wang92}.

This problem is partially solved by the {\em alignment logic\/}
of~\cite{GrNU94}, an elegant and expressive first-order logic for a
relational model with sequences.  The computational counterpart of the
logic is the class of {\em multi-tape, nondeterministic, two-way,
finite-state automata}, which are used to accept or reject tuples of
sequences.  In its full version, {\em alignment logic} has the power
of {\em recursively enumerable sets}~\cite{Papa94}.  A subset of the
language called {\em right restricted formulas\/} is then developed.
For this sublanguage, the safety problem is shown to be decidable, and
complexity results related to the polynomial-time hierarchy are
presented.  Unfortunately, the nondeterministic nature of the
computational model makes the evaluation of queries problematic.
Because existential quantification over the infinite universe of
sequences, $\alp{}{*}$, is allowed, it is not easy to determine the
maximum length of the sequences in a query answer, even when the query
is known to be safe.

Another interesting proposal for the use of logic in querying
sequences is~\cite{Rich92}.  In this case, {\em temporal logic\/} is
used as the basis of a list query language.  Conceptually, each
successive position in a list is interpreted as a successive instance
in time.  This yields a query language in which temporal predicates
are used to investigate the properties of lists.  However, temporal
logic cannot be used to express some simple properties of sequences,
such as whether a certain predicate is true at every even position of
a list, or whether a sequence contains one or more copies of another
sequence~\cite{Wolp83}.


%%%%%%%%%%%  OVERVIEW  %%%%%%%%%%%%%%

\subsection{Overview of the Language}

This paper builds on the works of~\cite{GiWa92,GrNU94,Rich92} to
propose a query language that is safe, expressive and has a clear
declarative and operational semantics.  This language, called {\em
\name}, is a Horn-like logic with special, interpreted function
symbols that allow for {\em structural recursion\/} over sequences.

The goal of this paper is to develop and investigate different forms
of structural recursion over sequences, especially forms that
guarantee terminating computations.  At the same time, we wish to
construct new sequences and restructure old ones.  To meet these two
goals, {\em \name}\/ has two interpreted function terms: {\em indexed
terms}\/ to extract subsequences, and {\em constructive terms}\/ to
concatenate sequences.  A constructive term has the form
$\sterm{1}\conc\sterm{2}$, and is interpreted as the concatenation of
sequences $\sterm{1}$ and $\sterm{2}$.  An indexed term has the form
$\sterm{}\sdue{\iterm{1}}{\iterm{2}}$, and is interpreted as the
subsequence of $\sterm{}$ extending from position $\iterm{1}$ to
position $\iterm{2}$.


%\begin{example} ~{\bf [Extracting Subsequences]}~
%\\
%The following rule extracts all prefixes of all sequences in relation
%$r$:
%%
%\[
%        {\it prefix}(X\sdue{1}{N}) ~\IF~ r(X)
%\]
%%
%For each sequence, $X$, in $r$, this rules says that a prefix of $X$
%is any subsequence starting with the first element and ending with the
%$N$-th element, so long as $N \geq 0$ and no longer than the length of
%$X$.
%\end{example}

\begin{example} ~{\bf [Extracting Subsequences]}~
The following rule extracts all suffixes of all sequences in relation
$r$:
%
\begin{center}
\begin{tabular}{lcl}
        ${\it suffix}(X\sdue{N}{\eos})$ & $\IF$ & $r(X).$
\end{tabular}
\end{center}
%
This rule says that for each sequence $X$ in relation $r$, and for
each integer $N$, the subsequence of $X$ extending from the $N^{th}$
element to the last element is a suffix of $X$.  By convention, we
interpret the keyword $\eos$ as the last position in a sequence.
\end{example}

The universe of sequences over an alphabet, $\alp{}{}$, is infinite.
Thus, to keep the semantics of programs finite, we do not evaluate
rules over the entire universe, $\alp{}{*}$, but on a specific active
domain.  We define the {\em active domain\/} of a database to be the
set of sequences occurring in the database.  We then define the {\em
extended active domain\/} to include both the sequences in the active
domain and all their {\em subsequences}.  The semantics of Sequence
Datalog is defined with respect to the extended active domain.  In
particular, substitutions range over this domain when rules are
evaluated.

The extended active domain is not fixed during query evaluation.
Instead, whenever a new sequence is created (by the concatenation
operator, $\conc$), the new sequence---and its subsequences---are
added to the extended active domain.  The fixpoint theory of {\name}
provides a declarative semantics for this apparently procedural
notion.  In the fixpoint theory, the extended active domain of the
least fixpoint may be larger than the extended active domain of the
database.  In the database, it consists of the sequences in the
database and all their subsequences.  In the least fixpoint, it
consists of the sequences in the database and any new sequences
created during rule evaluation, and all their subsequences.

\begin{example} ~{\bf [Concatenating Sequences]}~
The following rule constructs all possible concatenations of sequences
in relation $r$:
%
\begin{center}
\begin{tabular}{lcl}
        $answer(X\conc Y)$ & $\IF$ & $r(X),~r(Y).$ \\
\end{tabular}
\end{center}
%
This rule takes any pair of sequences, $X$ and $Y$, in relation $r$,
concatenates them, and puts the result in relation $answer$, thereby
adding new sequences to the extended active domain.
%The concatenated
%sequences (and their subsequences) form the extended active domain of
%the least fixpoint.
\end{example}


By combining subsequence extraction and sequence concatenation, a user
can express complex pattern matching and restructuring operations, as
the next two examples show.


\begin{example} ~{\bf [Pattern Matching]}~
\label{es:abcn}
Suppose we are interested in sequences of the form $a^nb^nc^n$ in
relation $r$.  The query $answer(X)$ retrieves all such sequences,
where the predicate $answer$ is defined by the following clauses, and
$\e$ is the empty sequence:
%
\begin{center}
%\small
\begin{tabular}{lll}
$answer(X)$ & $\IF$
      & $r(X),~abc_n(X\sdue{1}{N_1},X\sdue{N_1+1}{N_2},X\sdue{N_2+1}{\eos}).$
      \medskip\\
$abc_n(\e,\e,\e)$ & $\IF$ & $true$. \\
$abc_n(X,Y,Z)$    & $\IF$ & $X\suno{1}=a,~ Y\suno{1}=b,~ Z\suno{1}=c,~
                    abc_n(X\sdue{2}{\eos},Y\sdue{2}{\eos},Z\sdue{2}{\eos})$.
\end{tabular}
\end{center}
%
For each sequence $X$ in $r$, the formula $answer(X)$ is true if it is
possible to split $X$ into three parts such that $abc_n$ is true.  The
predicate $abc_n$ is true for every triple of sequences of the form
$(a^n,b^n,c^n)$ in the extended active domain of the database.
\end{example}


\begin{example} ~{\bf [Sequence Restructuring]}~
\label{es:reverse}
Suppose $r$ is a unary relation containing a set of binary sequences.
We want to generate the reverse of every sequence in $r$.  $e.g.$, The
reverse of $110000$ is $000011$.  The query $answer(Y)$ generates
these sequences, where the predicate $answer$ is defined by the
following clauses:
%
\begin{center}
%\small
\begin{tabular}{lll}
$answer(Y)$ & $\IF$ & $r(X),~reverse(X,Y).$ \medskip\\
$reverse(\e,\e)$
            & $\IF$ & $true$. \\
$reverse(X\sdue{1}{N+1}, X\suno{N+1}\conc Y)$
            & $\IF$ & $r(X),~reverse(X\sdue{1}{N},Y).$
\end{tabular}
\end{center}
%
In this program, the sequences in $r$ act as input for the predicate
$reverse(X,Y)$.  The third clause recursively scans each input
sequence, $X$, while constructing an output sequence, $Y$.  Each bit
in the input sequence is appended to the other end of the output
sequence.  The clause generates the reverse of each prefix of each
sequence in $r$.  The first clause then retrieves the reverse of each
sequence in $r$.
\end{example}


Compared to Datalog with function symbols, or Prolog, two differences
are apparent.  The first is that {\name} has no uninterpreted function
symbols, so it is not possible to build arbitrarily nested structures.
On the other hand, {\name} has a richer syntax than the $[Head|Tail]$
list constructor of Prolog.  This richer syntax is motivated by a
natural distinction between two types of recursion, one safe and the
other unsafe.  Recursion through construction of new sequences is {\em
inherently unsafe}, since it can create longer sequences, which can
make the active domain grow indefinitely.  On the other hand,
recursion through subsequence extraction is {\em inherently safe},
since it only creates shorter sequences, so that growth in the active
domain is bounded.  We refer to these two types of recursion as {\it
constructive recursion\/} and {\it structural recursion},
respectively.  Languages for list manipulation do not typically make
this distinction.  {\name} does: constructive recursion is performed
using constructive terms, of the form $X\conc Y$, while structural
recursion is performed using indexed terms, of the form
$X\sdue{\iterm{1}}{\iterm{2}}$.  The next example illustrates both
types of recursion.


\begin{example} ~{\bf [Multiple Repeats]}~
\label{es:multrep}
Suppose we are interested in sequences of the form $Y^n$.  The
sequence $abcdabcdabcd$ has this form, where $Y = abcd$ and
$n=3$.\footnote{Repetitive patterns are of great importance in
Molecular Biology~\cite{Sear93}.} Here are two straightforward ways of
expressing this idea in {\em \name}:
%
\begin{center}
\begin{small}
\begin{tabular}{lcl}
$rep_1(X,X)$ & $\IF$ & $true.$ \\
$rep_1(X,X\sdue{1}{N}))$ & $\IF$ & $rep_1(X\sdue{N+1}{\eos},X\sdue{1}{N}).$ \\
~\\
$rep_2(X,X)$ & $\IF$ & $true.$ \\
$rep_2(X\conc Y,Y)$ & $\IF$ & $rep_2(X,Y).$
\end{tabular}
\end{small}
\end{center}
%
The formulas $rep_1(X,Y)$ and $rep_2(X,Y)$ both mean that $X$ has the
form $Y^n$ for some $n$.  However, $rep_2$ has an infinite semantics,
while $rep_1$ has a finite semantics.  The rules for $rep_1$ do {\em
not}\/ create new sequences, since they do not use the concatenation
operator, $\conc$.  Instead, these rules retrieve all sequences in the
extended active domain that fit the pattern $Y^n$.  They try to
recursively ``chop'' an existing sequence into identical pieces.  We
call this {\em structural recursion}.  In contrast, the rules for
$rep_2$ {\em do}\/ create new sequences.  They produce sequences of
the form $Y^n$ by recursively concatenating each sequence in the
domain with itself.  We call this {\em constructive recursion}.
\end{example}


Structural recursion is always safe, since it stays within the
extended active domain of the database, thus leading to a finite least
fixpoint.  However, as Example~\ref{es:multrep} shows, constructive
recursion can be unsafe, since by generating more-and-more new
sequences, it can expand the active domain indefinitely, thus leading
to an infinite least fixpoint.  The next example provides another
illustration of unsafe recursion.


\begin{example} {\bf [Infinite Semantics]}~
\label{es:echo1}
Suppose $R$ is a unary relation containing a set of sequences.  For
each sequence, $X$, in $R$, we want the sequence obtained by repeating
each symbol in $X$ twice.  For example, given the sequence $abcd$, we
want the sequence $aabbccdd$.  We call these sequences {\em echo\/}
sequences.  The easiest way to define echo sequences is with the
following program:
%
\begin{center}
\begin{tabular}{rcl}
$answer(X,Y)$ & $\IF$ & $R(X),echo(X,Y).$  \medskip\\
$echo(\e,\e)$      & $\IF$ & $true$. \\
$echo(X, X\suno{1}\conc X\suno{1}\conc Z)$ & $\IF$ &
                           $echo(X\sdue{2}{\eos},Z)$.
\end{tabular}
\end{center}
%
The first rule retrieves every sequence in relation $R$ and its echo,
by invoking the predicate $echo(X,Y)$.  The last two rules specify
what an echo sequence is.  For every sequence, $X$, in the extended
active domain, these rules generate its echo sequence, $Y$.  Starting
with $X = \e$ and $Y = \e$, they recursively concatenate single
characters onto $X$ while concatenating two copies of the same
character onto $Y$.  As new sequences are generated, they are added to
the active domain, which expands indefinitely.  Thus, even though the
answer to the query is finite, the least fixpoint is infinite.
\end{example}



\subsection{Safety and Transducers}

We say that a program has a finite semantics if it has a finite least
fixpoint for every database.  Given a {\name} program, we show that
determining whether it has a finite semantics is an undecidable
problem.  The challenge, then, is to develop subsets of the logic that
are both finite and expressive.  As shown in Examples~\ref{es:multrep}
and~\ref{es:echo1}, constructive recursion is the basic source of
non-finiteness; so some way must be found to limit its effects.

There are a number of simple ways to do this, but unfortunately, they
all lead to drastic reductions in the expressiveness of the language,
especially in its ability to restructure sequences.  For instance, we
could simply forbid constructive recursion, but this would eliminate
many basic restructurings, such as computing the reverse or the
complement of a sequence.  Alternatively, we could arbitrarily limit
the size of new sequences.  For instance, we could decree that all new
sequences must be no longer than the longest sequence in the database;
but this would also eliminate many basic restructurings, such as
appending two sequences from the database.  To avoid such drastic
reductions in expressibility, this paper develops a more subtle way of
limiting and controlling constructive recursion.  Specifically, we
allow constructive recursion only in the context of a precise (and
novel) computational model.

The model we develop is called {\em generalized sequence transducers}
(or {\em generalized transducers}, for short), which are a simple
extension of ordinary transducers.
Typically~\cite{GiWa92,SPSV92,Gonn94}, a {\em transducer\/} is defined
as a machine with multiple input lines, one output line, and an
internal state.  The machine sequentially ``reads'' the input strings,
and progressively ``computes'' the output.  At each step of the
computation, the transducer reads the left-most symbol on each input
tape, and ``consumes'' one of them.  The transducer then changes state
and appends a symbol to the output.  The computation stops when all
the input sequences have been consumed.  Termination is therefore
guaranteed for finite-length inputs.  Unfortunately, ordinary
transducers have very low complexity, essentially linear time.  This
means that they cannot perform complex operations, such as detecting
context-free or context-sensitive languages, as it is often needed in
genome databases~\cite{Sear93}.

We generalize this machine model by allowing one transducer to call
other transducers, in the style of (non-recursive) subroutines.  At
each step, a generalized transducer can {\em append}\/ a symbol to its
output or it can {\em transform}\/ its output by invoking a
sub-transducer.  Like transducers, generalized transducers consume one
input symbol at each step, and are thus guaranteed to terminate on
finite inputs.  In this way, we increase expressibility while
preserving termination.  We shall see that the depth of subroutine
calls within a generalized transducer dramatically affects their
computational complexity.

{\em \name} provides a natural framework for implementing generalized
transducers.  The consumption of input symbols is easily implemented
as structural recursion; appending symbols to output tapes is easily
implemented as constructive recursion; and sub-transducers are easily
implemented as subroutines, in the logic-programming sense.  Moreover,
by introducing transducers into the logic, we can develop simple
syntactic restrictions that guarantee finiteness.  These restrictions
allow constructive recursion only ``inside'' transducers.  Using this
idea, we develop safe and finite subsets of {\em \name}, and establish
their complexity and expressibility.



%%%%%%%%%%%    PRELIMINARY DEFINITIONS   %%%%%%%%%%%

\section{Preliminary Definitions}
\label{sec:preliminary}

This section provides technical definitions used in the rest of the
paper, including {\em sequence database}, {\em sequence query} and
{\em sequence function}.


\subsubsection*{Sequences and Subsequences:}

Let $\alp{}{}$ be a countable set of symbols, called the {\em
alphabet}.  $\alp{}{*}$ denotes the set of all possible sequences over
$\alp{}{}$, including the {\em empty sequence}, $\e$. $\seq{1}\seq{2}$
denotes the concatenation of two sequences, $\seq{1},\seq{2} \in
\alp{}{*}$.  $\length(\seq{})$ denotes the length of sequence
$\seq{}$, and $\seq{}(i)$ denotes its $i$-th element. With an abuse of
notation, we blur the distinction between elements of the alphabet and
sequences of length 1.  We say that a sequence, $\seq{}'$, of length
$k$ is a {\em contiguous subsequence}\/ (or simply a {\it
subsequence\/}) of sequence $\seq{}$ if for some integer, $i\geq 0$,
~$\seq{}'(j)=\seq{}(i+j)$~ for $j=1,\ldots,k$.  Note that for each
sequence of length $k$ over $\alp{}{}$, there are at most \,${k(k+1)
\over 2} + 1$\, different contiguous subsequences (including the empty
sequence).  For example, the contiguous subsequences of the sequence
$abc$ are: $\e,a,b,c,ab,bc,abc$.


\subsubsection*{Databases, Queries and Functions:}

As in~\cite{GiWa92,GrNU94}, we extend the relational model so that
tuples can contain sequences of symbols, instead of just single
symbols.  Formally, a {\em relation\/} of arity $k$ over $\alp{}{}$ is
a finite subset of the $k$-fold cartesian product of $\alp{}{*}$ with
itself.  A {\em database\/} over $\alp{}{}$ is a tuple of relations
over $\alp{}{}$.  We assign a distinct predicate symbol of appropriate
arity to each relation in a database.  These predicate symbols are
called {\it base predicates}, and together they form the database {\it
schema}.  Using predicates, we can represent relations and databases
as sets of ground atomic formulas in the usual way.  A set of ground
atomic formulas made from base predicate symbols is called an {\it
instance\/} of the database schema.

A {\em \Squery} is a partial mapping from the databases over
$\alp{}{}$ to the relations over $\alp{}{}$.  Given a {\Squery}, $Q$,
and a database, $\inst{}$, $Q(\inst{})$ is the result of evaluating
$Q$ over $\inst{}$.%
%
\footnote{Database queries are often required to be {\it
generic\/}~\cite{ChHa80}.  Although this notion can be extended to
sequence databases in a straightforward way, genericity is not an
issue in this paper.}
%
%Usually, a notion of {\em genericity}~\cite{ChHa80} is introduced for
%queries to formalize the idea that the constant symbols in a database
%are uninterpreted.  This notion can be extended to sequence queries in
%a natural way.  To do this, we consider permutations of the alphabet
%$\alp{}{}$, that is, one-to-one mappings $\rho : \alp{}{} \rightarrow
%\alp{}{}$ of $\alp{}{}$ onto itself.  Permutations can be extended in
%a natural way to strings in $\alp{}{*}$, tuples of strings, relations
%and databases.  We say that a sequence query $Q$ is {\em generic\/} if
%it commutes with every permutation, that is, if
%\[
%       Q(\rho(\inst{}))=\rho(Q(\inst{}))
%\]
%for every permutation $\rho$ of $\alp{}{}$, and every database
%$\inst{}$ on which $Q$ is defined.  Finally, we say that a {\Squery}
%is {\em computable}~\cite{ChHa80} if it is both generic and partial
%recursive.
%
A {\em \Sfunction} is a partial mapping from $\alp{}{*}$ to itself. We
say that the function is {\em {\Scomp}} if it is partial recursive. If
$f$ is a {\Sfunction}, we define the {\em query corresponding to
$f$\/} to be a query whose domain is the set of databases of the form
\mbox{$\{input(\seq{})\}$}, where \mbox{$\seq{} \in \Sigma^*$}.  If
$\seq{}$ is in the domain of $f$, then the output of this query is the
relation \mbox{$\{output(f(\seq{}))\}$}; otherwise, the output is the
empty relation.  Observe that this query takes a single tuple as
input, and returns either a single tuple or no tuples as output.  When
we say that a query language expresses a sequence function, we shall
mean that it expresses the query corresponding to the function.  This
paper focuses on sequence functions for which the alphabet, $\Sigma$,
is finite.  Of course, the domain of such functions may still be
infinite; $e.g.$, it may be all of $\Sigma^*$.


\subsubsection*{Complexity and Expressibility:}

Given a {\Sfunction}, $f$, the {\em complexity} of $f$ is defined in
the usual way as the complexity of computing $f(\seq{})$, measured
with respect to the length of the input sequence, $\seq{}$.  Given a
{\Squery} $Q$, a database $\inst{}$, and a suitable encoding of
$\inst{}$ as a Turing machine tape, the {\em data complexity} of $Q$
is the complexity of computing an encoding of $Q(\inst{})$, measured
with respect to the size of $\inst{}$~\cite{Vard82}.

In relational databases, a query language is a set of formulas
representing relational queries.  This leads to the notions of data
complexity and expressibility of query languages~\cite{AbHV95}. These
ideas can be extended to sequence databases in a natural way.  A
sequence query language is a set of formulas representing sequence
queries.\footnote{Definition~\ref{def:express} in
Section~\ref{sec:express} describes how formulas of Sequence Datalog
represent sequence queries.}  A sequence query is expressible in a
language if some formula in the language represents it.  A sequence
query language, $L$, is {\em complete\/} for complexity class {\sc c}
if $(i)$ each query expressible in $L$ is in {\sc c}, and $(ii)$ some
query expressible in $L$ is a complete problem for {\sc c}.  Observe
that being complete for a complexity class {\sc c} does not imply that
a language expresses all the queries in {\sc c}; it implies only that
the language expresses {\it some\/} complete problem in {\sc c}.  This
motivates a stronger notion.  A query language $L$ {\em expresses\/} a
class {\sc qc} of sequence queries if $(i)$ each query expressible in
$L$ is in {\sc qc}, and conversely, $(ii)$ each query in {\sc qc} is
expressible in $L$.  Finally, a query language expresses a class of
sequence {\it functions\/} if it expresses the class of corresponding
sequence queries.

Observe that expressibility results formulated in terms of sequence
functions are especially meaningful for sequence query languages,
since they provide a clear characterization of the power of the
language to manipulate sequences: a sequence query language cannot
express complex queries over sequence databases if it cannot express
complex sequence functions.  In short, function expressibility is
necessary for query expressibility.



%%%%%%%%%%%%   THE LANGUAGE  %%%%%%%%%%%%%%%

\section{{\name}}
\label{sec:language}

{\em {\name}} is a query language for the extended relational model
defined in the previous section.  This section develops its syntax and
semantics.


%%%%%%%%%%%%  SYNTAX %%%%%%%%%%%%

\subsection{Syntax}
\label{sec:syntax}

Like most first-order logics, {\name} includes both {\it terms\/} and
{\it formulas}.

The language of terms has four countable, disjoint sets: the set of
non-negative integers, $0,1,2,...$; a set of constant symbols,
$a,b,c,...$, called the {\em alphabet} and denoted $\alp{}{}$; a set
of variables, $R,S,T,...$, called {\em sequence variables} and denoted
$\svar$; and another set of variables, $I,J,K,...$, called {\em index
variables} and denoted $\ivar$.  A constant sequence (or {\em
sequence}, for short) is an element of $\alp{}{*}$.  From these sets,
we construct two kinds of term as follows:
%
\begin{itemize}
\item
{\em index terms} are built from integers, index variables, and the
special symbol $\eos$, by combining them recursively using the binary
connectives $+$ and $-$;

\item
{\em sequence terms} are built from constant sequences, sequence
variables and index terms, by combining them recursively into {\em
indexed terms} and {\em constructive terms}, as follows:
%
\begin{itemize}
\item
If $\sterm{}$ is a sequence variable or a constant sequence, and
$\iterm{1},\iterm{2}$ are {\em index terms}, then
$\sterm{}\sdue{\iterm{1}}{\iterm{2}}$ is an {\em indexed sequence
term}.  $\iterm{1}$ and $\iterm{2}$ are called the {\em indexes} of
$\sterm{}$.  As a shorthand, each sequence term of the form
$\sterm{}\sdue{\iterm{i}}{\iterm{i}}$ is written
$\sterm{}\suno{\iterm{i}}$.

\item
If $\sterm{1},\sterm{2}$ are {\em sequence terms}, then
$\sterm{1}\conc\sterm{2}$ is a {\em constructive sequence term}.
\end{itemize}

\end{itemize}
%
For example, if $N$ and $M$ are index variables, then ~$3$, ~$N+3$,
~$N-M$, ~$\eos-5$ ~and ~$\eos-5+M$ are all index terms.  Similarly, if
$\s{1}$ and $\s{2}$ are sequence variables, and $N$ is an index
variable, then ~$\s{1}\suno{4}$, ~$\s{1}\sdue{1}{N}$ ~and
~$ccgt\conc\s{1}\sdue{1}{\eos-3}\conc\s{2}$ are all sequence terms.
Note that ~$(\s{1}\conc\s{2})\sdue{1}{N}$ ~and
~$\s{}\sdue{1}{N}\sdue{M}{end}$ are {\it not\/} terms.  By excluding
such terms, we obtain a clear distiction between index terms and
constructive terms.  This then leads to clear distinction between the
extraction of subsequences and the creation of new sequences, and to a
parallel distinction between structural recursion and constructive
recursion.

The language of formulas has a countable set of predicate symbols,
$p,q,r,...$, where each predicate symbol has an associated arity.  If
$p$ is a predicate symbol of arity $n$, and $s_1,...,s_n$ are sequence
terms, then $p(s_1,...,s_n)$ is an atom.  Moreover, if $s_1$ and $s_2$
are sequence terms, then $s_1=s_2$ and $s_1 \neq s_2$ are also atoms.
From atoms, we build {\em facts\/} and {\em clauses\/} in the usual
way~\cite{Lloy87}.  Clauses are also referred to as {\em rules}.  The
head and body of a clause, $\cl{}$, are denoted \(\head(\cl{})\) and
\(\body(\cl{})\), respectively.  A clause that contains a constructive
term in its head is called a {\em constructive clause}.  A {\name}
{\em program}\/ is a set of {\name} clauses.

We impose the restriction that constructive terms may appear only in
the head of a clause, and not in the body.  Allowing them in the body
would not complicate the semantics, but it is only in the head that
constructive terms are interesting: in the head, they create new
sequences and expand the data domain, while in the body, they would
simply decompose existing sequences.  (The same is true of function
terms in classical logic programming.)  Since index terms already
decompose sequences, constructive terms are not needed in rule bodies.
Moreover, we shall see in Section~\ref{sec:td} that this restriction
allows us to generalize the idea of ``constructive term'' in a novel
way, one that guarantees both finite semantics and high
expressibility.

Another restriction that we shall find useful is {\em guardedness}.
We say that a variable, $X$, is {\em \guarded} in a clause if $X$
occurs in the body of the clause as an argument of some predicate.
Otherwise, we say that $X$ is {\em \unguarded}.  For example, $X$ is
{\guarded} in \,\mbox{$p(X\suno{1}) \IF q(X)$},\, but it is
{\unguarded} in \,\mbox{$p(X) \IF q(X\suno{1})$}.\, Because of the
active domain semantics, variables in {\name} clauses are {\em not\/}
required to be {\guarded}.  However, the concept of guardedness will
be useful in some proofs.

Finally, we assume familiarity with basic notions of logic
programming, such as {\em ground} terms and {\em Herbrand universe}.
Note that the Herbrand universe associated with $\alp{}{}$ contains
$\alp{}{*}$ and is thus an infinite set.

%A finite set of predicate symbols are identified as {\it base
%predicates}.  A {\it database\/} is a finite set of atoms made from
%base predicates.  The semantics of {\name} does not depend on the
%notion of base predicates, but some results on query expressibility
%do.


%%%%%%%%%%%%  SEMANTICS %%%%%%%%%%%%

\subsection{Substitutions}

The semantics of {\name} relies on the notion of {\it substitution},
defined as follows:


\begin{definition} ~{\bf (Substitutions Based on a Domain)}~
Let $\domact{}{}$ be a set of sequences and integers.  A {\em
substitution based on} $\domact{}{}$ is a mapping that associates a
sequence in $\domact{}{}$ to every sequence variable, and an integer
in $\domact{}{}$ to every index variable.
\end{definition}


As defined above, substitutions are total mappings on variables.  We
can extend them to partial mappings on terms in a natural way.
Because these terms are interpreted, the result of a substitution is
either a sequence or an integer.  For instance, if $\sterm{}$ is a
sequence and $\iterm{1}$ and $\iterm{2}$ are integers, then
$\subs{}(\sterm{}\sdue{\iterm{1}}{\iterm{2}})$ is the contiguous
subsequence of $\sterm{}$ extending from position $\iterm{1}$ to
position $\iterm{2}$.  Here, terms such as $\sterm{}\sdue{n+1}{n}$ are
conveniently interpreted as the empty sequence, $\e$.  For example,
%
\begin{center}
\begin{tabular}{|c|c|}
\hline
$\sterm{}$ & $\subs{}(\sterm{})$ \\
\hline
$uvwxy[3:6]$ & undefined \\
$uvwxy[3:5]$ & $wxy$         \\
$uvwxy[3:4]$ & $wx$          \\
$uvwxy[3:3]$ & $w$           \\
$uvwxy[3:2]$ & $\e$          \\
$uvwxy[3:1]$ & undefined \\
\hline
\end{tabular}
\end{center}


%For example, if $\iterm{1}$ and $\iterm{2}$ are index terms, then
%$\subs{}(\iterm{1} \pm \iterm{2}) = \subs{}(\iterm{1}) \pm
%\subs{}(\iterm{2})$.  Similarly, if
%$\sterm{}\sdue{\iterm{1}}{\iterm{2}}$ is a sequence term, then
%$\subs{}(\sterm{}\sdue{\iterm{1}}{\iterm{2}})$ is defined iff
%~\mbox{$1 \,\leq\, \subs{}(\iterm{1}) \,\leq\, \subs{}(\iterm{2})+1
%\,\leq\, \length(\subs{}(\sterm{}))+1$}.~

To formalize this idea, let $\subs{}$ be a substitution based on a
domain.  We extend $\subs{}$ to terms as follows:
%
\begin{itemize}
  \item
    if \(\sterm{}\) is a sequence in $\alp{}{*}$ or an integer,
    then \(\subs{}(\sterm{})=\sterm{}\);

  \item
    in the context of the sequence term $\s{}\sdue{\iterm{}}{\eos}$,
    we define $\subs{}(\eos)=\length(\subs{}(\s{}))$;


  \item if $\iterm{1}$ and $\iterm{2}$ are index terms, then
$\subs{}(\iterm{1}+\iterm{2}) = \subs{}(\iterm{1})+\subs{}(\iterm{2})$
\\ ~and~
$\subs{}(\iterm{1}-\iterm{2}) = \subs{}(\iterm{1})-\subs{}(\iterm{2})$;

  \item if $\sterm{}$ is a sequence term of the form
    $\s{}\sdue{\iterm{1}}{\iterm{2}}$,
    then $\subs{}(\sterm{})$ is defined iff \\
    ~\mbox{$1 \,\leq\, \subs{}(\iterm{1}) \,\leq\, \subs{}(\iterm{2})+1
    \,\leq\, \length(\subs{}(\s{}))+1$},~
    in which case
%
  \begin{itemize}

    \item
    $\subs{}(\sterm{})$ is the contiguous subsequence of
    $\subs{}(\s{})$ extending from position $\subs{}(\iterm{1})$ to
    $\subs{}(\iterm{2})$
    ~if~ \,$\subs{}(\iterm{1}) \leq \subs{}(\iterm{2})$

    \item
    $\subs{}(\sterm{})=\e$ (the empty sequence)
    ~if~ $\subs{}(\iterm{1}) = \subs{}(\iterm{2})+1$
  \end{itemize}

  \item if $\sterm{1}$ and $\sterm{2}$ are sequence terms, then
$\subs{}(\sterm{1}\conc\sterm{2}) =
    \subs{}(\sterm{1})\subs{}(\sterm{2})$\, if both $\subs{}(\sterm{1})$
    and $\subs{}(\sterm{2})$ are defined; otherwise,
    $\subs{}(\sterm{1}\conc\sterm{2})$ is {\em undefined}.

\end{itemize}
%
Substitutions can be extended to atoms, literals and clauses in the
usual way.  We need only add that $\subs{}(p(X_1,\ldots,X_n))$ is
defined if and only if each $\subs{}(X_i)$ is defined.  Likewise,
$\subs{}(q_0 \leftarrow q_1,\ldots,q_k)$ is defined if and only if
each $\subs{}(q_i)$ is defined, for $0 \leq i \leq k$.



\subsection{Fixpoint Semantics}
\label{sec:fix}

The semantics of clauses is defined in terms of a least fixpoint
theory.  As in classical logic programming~\cite{Lloy87}, each {\name}
program, $P$, and database, $\inst$, has an associated ``T-operator,''
$\trasf{}$, that maps Herbrand interpretations to Herbrand
interpretations.  Each application of $\trasf{}$ may create new atoms,
which may contain new sequences.  As shown below, $\trasf{}$ is
monotonic and continuous, and thus has a least fixpoint that can be
computed in a bottom-up, iterative fashion.

To develop the fixpoint semantics formally, we define the {\em
Herbrand base\/} to be the set of all ground atomic formulas built
from predicate symbols in the language and sequences in $\alp{}{*}$.
A {\em database\/} is a finite subset of the Herbrand base.  An {\em
interpretation\/} of a program is any subset of the Herbrand base.
%In the rest of this section, the program, $\prog$, is fixed.

\begin{definition}[Extensions]
Given a set of sequences, $dom$, the {\em extension\/} of $dom$,
written $dom^{ext}$, is the set of sequences and integers containing
the following elements:
%
\begin{enumerate}
  \item
    each element in $dom$;
  \item
    for each sequence in $dom$, all its contiguous
    subsequences;
  \item
    the set of integers \,$\{0,1,2,\ldots,l_{max}+1\}$,\, where $l_{max}$ is
    the maximum length of a sequence in $dom$.
\end{enumerate}
\end{definition}

\begin{definition}[Extended Active Domain] \label{def:domain}
The {\em active domain} of an interpretation, $\interp$, denoted
$\domact{}{\interp}$, is the set of sequences occurring in $\interp$.
The {\em extended active domain} of $\interp$, denoted
$\domact{ext}{\interp}$, is the extension of $\domact{}{\interp}$.
\end{definition}

Note that active domains contain only sequences, while extended active
domains contain integers as well.  The following lemma states some
basic results about extended active domains.

\begin{lemma} \label{lem-domains}
If \,$\interp_1 \subseteq \interp_2$\, are two interpretations, then
\,$\domact{ext}{\interp_1} \,\subseteq\, \domact{ext}{\interp_2}$.  If
$\cal I$ is a set of interpretations, then their union, $\union\cal
I$, is also an interpretation, and \,$\domact{ext}{\union\cal I} =
\union_{\interp \in {\cal I}} \domact{ext}{\interp}$.
\end{lemma}

Like any power set, the set of interpretations forms a complete
lattice under subset, union and intersection.  We define a T-operator
on this lattice, and show that it is monotonic and continuous.  In
defining the T-operator, each database atom is treated as a clause
with an empty body.

\begin{definition}[T-Operator] \label{def-T}
The operator $\trasf{}$ associated with program $\prog$ and database
$\inst$ maps interpretations to interpretations.  In particular, if
$\interp$ is an interpretation, then $\trasf{}(\interp)$ is the
following interpretation:
\begin{mathlines}{llll}
        \{\subs{}(\head(\cl{}))
            & \mid & \subs{}(\body(\cl{})) \subseteq \interp
                   ~~\mbox{\it for some clause}~ \gamma\in\prog\cup\inst \\
        & & \mbox{\it and some substitution}~ \subs{} ~\mbox{\it based on}~
            \domact{ext}{\interp} ~\mbox{and defined at}~ \cl{} \}
\end{mathlines}
\end{definition}


\begin{lemma}[Monotonicity] \label{lem:monotonicity}
The operator $\trasf{}$ is {\em \/monotonic}; $i.e.$, if \,$\interp_1
\subseteq \interp_2$\, are two interpretations, then
\,$\trasf{}(\interp_1) \,\subseteq\, \trasf{}(\interp_2)$.
\end{lemma}
%
\begin{Proof}
Follows immediately from Definition~\ref{def-T} and
Lemma~\ref{lem-domains}.
\end{Proof}


Because $\trasf{}$ is a monotonic operator on a complete lattice, it
has a least fixpoint, by the Knaster-Tarski Fixpoint
Theorem~\cite{Tars55}.  That is, there is a unique minimal
interpretation $\interp$ such that \,\mbox{$\interp =
\trasf{}(\interp)$}.  Let $\lfp(\trasf{})$ denote this minimal
interpretation.  We say that $\lfp(\trasf{})$ is the {\em fixpoint
semantics\/} of program $\prog$ over database $\inst$.  We also say
that $\lfp(\trasf{})$ is the set of facts implied by program $\prog$
and database $\inst$.  We now show that the least fixpoint can be
computed by a bottom-up iterative procedure, as in classical logic
programming~\cite{Lloy87}.  The first step is to show that $\trasf{}$
is a continuous operator.


\begin{lemma}[Continuity]
\label{lem:continuity}
The operator $\trasf{}$ is {\em \/continuous}; $i.e.$, if
\,\mbox{$\interp_1 \subseteq \interp_2 \subseteq \interp_3 \ldots$}\,
is a (possibly infinite) increasing sequence of interpretations, then
~$\trasf{}(\union_i \interp_i) \,\subseteq\, \union_i\,
\trasf{}(\interp_i)$.
\end{lemma}
%
\begin{Proof}
Let \,$\interp = \union_i \interp_i$\, and let $\alpha$ be an atom in
$\trasf{}(\interp)$.  We must show that $\alpha$ is also in
$\union_i\,\trasf{}(\interp_i)$.  By Definition~\ref{def-T}, \,$\alpha
= \subs{}(\head(\cl{}))$\, and \,$\subs{}(\body(\cl{})) \subseteq
\interp$\, for some clause $\gamma$ in $\prog\cup\inst$, and some
substitution $\subs{}$ based on $\domact{ext}{\interp}$.  In addition,
since the interpretations, $\interp_i$, are increasing, their extended
active domains, $\domact{ext}{\interp_i}$, are also increasing, by
Lemma \ref{lem-domains}.  With this in mind, we proceed in three
steps.
%
\begin{itemize}

\item
$\subs{}(\body(\cl{}))$ is a finite set of ground atomic formulas, and
\,$\subs{}(\body(\cl{})) \subseteq \union_i \interp_i$.  ~Thus
\,$\subs{}(\body(\cl{})) \subseteq \interp_{j_1}$\, for some $j_1$,
since the $\interp_i$ are increasing.

\item
Let $\cal V$ be the set of variables in clause $\gamma$, and let
$\subs{}({\cal V})$ be the result of applying $\subs{}$ to each
variable.  Thus $\subs{}({\cal V})$ is a finite subset of
$\domact{ext}{\interp}$, since $\subs{}$ is based on
$\domact{ext}{\interp}$.  Thus \,$\subs{}({\cal V}) \subseteq \union_i
\domact{ext}{\interp_i}$\, by Lemma \ref{lem-domains}.  Thus
\,$\subs{}({\cal V}) \subseteq \domact{ext}{\interp_{j_2}}$\, for some
$j_2$, since $\subs{}({\cal V})$ is finite and the
$\domact{ext}{\interp_i}$ are increasing.

\item
Let $j$ be the larger of $j_1$ and $j_2$.  Then \,$\subs{}(\body(\cl{}))
\subseteq \interp_{j}$\, and \,$\subs{}({\cal V}) \subseteq
\domact{ext}{\interp_{j}}$.\, Let $\subs{}'$ be any substitution based
on $\domact{ext}{\interp_{j}}$ that agrees with $\subs{}$ on the
variables in $\cal V$.  Then \mbox{$\subs{}'(\cl{}) =
\subs{}(\cl{})$}.  Thus, \,$\subs{}'(\body(\cl{})) \subseteq
\interp_{j}$.\, Thus \,$\subs{}'(\head(\cl{})) \in
\trasf{}(\interp_{j})$\, by Definition~\ref{def-T}.  Thus
\,\mbox{$\alpha \in \trasf{}(\interp_{j})$}.\, Thus \,$\alpha \in
\union_i\,\trasf{}(\interp_i)$.
\end{itemize}
~\end{Proof}


Starting with the empty interpretation and applying $\trasf{}$
repeatedly, we define the following sequence of interpretations, in
the usual way~\cite{Lloy87}:


\begin{eqnarray*}
\trasfi{}{0}      & = & \{\,\} \smallskip\\
\trasfi{}{(i+1)}  & = & \trasf{}(\trasfi{}{i}) ~~~\mbox{\it  for}~ i \geq 0 \smallskip\\
\trasfi{}{\omega} & = & \union_{i \geq 0}~\trasfi{}{i}
\end{eqnarray*}

Intuitively, \mbox{$\trasfi{}{\omega}$} is the set of atoms that can
be derived by applying the operator $\trasf{}$ some finite number of
times (though some atoms may require more applications than others).
Because the operator is continuous, this process is complete, $i.e.$,
any atom in the least fixpoint will eventually be derived.  Formally,
by the Knaster-Tarski Fixpoint Theorem~\cite{Tars55},
\[
        \lfp(\trasf{}) ~=~ \trasfi{}{\omega}
\]

This completes the fixpoint semantics of {\name}.  An equivalent model
theory is developed in Appendix~\ref{app:model}.



%%%%%%%%%%%%%%% EXPRESSIVE POWER %%%%%%%%%%%%%%%%%%%%

\section{Expressive Power of {\name}}
\label{sec:express}

This section studies the expressive power of {\name} programs.  The
language has considerable power for manipulating sequences, and can
express any computable {\Sfunction}, as shown in
Theorem~\ref{th:complexitysd} below.  First, we define precisely what
it means for a {\name} program to {\it express\/} a sequence query and
a sequence function.


\begin{definition}[Expressibility] \label{def:express}
Let $P$ be a program in Sequence Datalog.
%
\begin{itemize}
\item
$\prog$ expresses a sequence query, $Q$, if for some predicate symbol,
$output$,
\[
        Q(\inst) ~=~ \{\, \overline{y}~|~
                        output(\overline{y}) \,\in\, \trasfi{}{\omega} \,\}
\]
for all databases $\inst$ in the domain of $Q$.

\item
$P$ expresses a sequence function, $f$, if it expresses the query
corresponding to $f$.

\end{itemize}
\end{definition}
%
To clarify the second point, suppose that program $P$ expresses
sequence function $f$, and the database is the singleton set \,$\inst
= \{input(x)\}$.  Then \,\mbox{$\trasfi{}{\omega}$}\, contains the
atom $output(y)$ if and only if $f$ is defined at $x$ and $y = f(x)$.


\begin{theorem} \label{th:complexitysd}
{\bf (Expressive power)}
{\name} expresses exactly the class of computable sequence functions,
{\em i.e.} the class of partial recursive sequence functions.
\end{theorem}
%
\begin{Proof}
%
Using the fixpoint semantics developed in Section~\ref{sec:fix}, it is
easy to show that each {\Sfunction} expressible in {\name} is partial
recursive.  To see this, suppose that $P$ is a {\name} program
expressing sequence function $f$.  The comment after
Definition~\ref{def:express} shows that to compute $f(x)$ it is enough
to construct the database \,$\inst = \{input(x)\}$\, and then test
whether the set \,\mbox{$\trasfi{}{\omega}$}\, contains an atom of the
form $output(y)$, in which case $y = f(x)$.  To carry out this test,
we can generate the sets \,\mbox{$\trasfi{}{k}$}\, for $k=1,2,3...$,
stopping when the atom $output(y)$ appears in one of them.  This is
possible because each \,\mbox{$\trasfi{}{k}$}\, is finite, even though
\,\mbox{$\trasfi{}{\omega}$}\, may be infinite.  If $f$ is defined at
$x$, then $output(y)$ is in at least one of the
\,\mbox{$\trasfi{}{k}$},\, so the test terminates in finite time.  The
test fails to terminate only if $f$ is undefined at $x$.  This shows
that $f$ is partial recursive.

We now show the converse, that {\name} expresses every partial
recursive {\Sfunction}.  Specifically, given a fixed finite alphabet,
$\alp{}{}$, and a partial recursive {\Sfunction}\, $f : \alp{}{*}
\rightarrow \alp{}{*}$, we construct a {\name} program, $\prog_f$,
that expresses $f$.  To construct $\prog_f$, let $\tm_f$ be a Turing
machine that computes $f$.  Given an input sequence, $x$, if $f$ is
defined at $x$, then $\tm_f$ halts and returns $f(x)$ as output;
otherwise, $\tm_f$ does not halt.  We construct $\prog_f$ so that it
simulates the computations of $\tm_f$.  In particular, suppose
$\tm_f=(\alp{}{},K,s_0,\delta)$, where $\alp{}{}$ is the tape
alphabet, $K$ is the set of control states, $s_0$ is the initial
state, and $\delta$ is the transition function.  We use a special
symbol, $\rhd$, to mark the left end of the tape, and we assume the
machine never tries to overwrite this left-end marker or move beyond
it.

We represent machine configurations with a 4-ary predicate, {\em
conf(state,$\seq{l}$,a,$\seq{r}$)}, where:
%
\begin{itemize}
  \item
    {\em state}\, is the state of the machine's finite control,
  \item
    $\seq{l}$\,  is a sequence representing the portion of the tape to the
    {\it left\/} of the tape head,
  \item
    {\em a}\, is the symbol scanned by the tape head, and
  \item
    $\seq{r}$\, is a sequence representing the portion of the tape to the
    {\it right\/} of the tape head.
\end{itemize}
%
Intuitively, the atom {\em conf(state, $\seq{l}$, a, $\seq{r}$)}
represents a {\it reachable\/} machine configuration, $i.e.$, one that
can be reached from the initial configuration after some finite amount
of computation.  For instance, the tuple \,{\em conf$(q,abc,d,ef)$}\,
says that from the initial state, the machine can reach a
configuration in which the finite control is in state $q$, the tape
content is $abcdef$, and the tape head is scanning the symbol $d$.

We can assume that at the beginning of a computation, the machine
scans the left-end marker, $\rhd$, and that the finite control is in
state $q_0$.  The initial configuration of the machine is thus
specified by the following rule, which simply says that the initial
configuration is reachable:
\[
        \cl{1}:~~{\it conf}(q_0,\e,\rhd, X) \IF input(X).
\]

The computation itself is specified by a set of rules, one rule for
each machine transition.  In general, each rule simply says that the
successor of a reachable configuration is also reachable.  For
example, consider the transition \,$\delta(q,a)=(q',b,-)$.\, This
means that if the machine is currently in state $q$ and scanning tape
symbol $a$, then the machine goes into state $q'$, writes the symbol
$b$ on the tape, and does not move the tape head.  This transition is
specified by the following rule:
\[
   \cl{i}:~~{\it conf}(q', X_l, b, X_r) \IF {\it conf}(q, X_l, a, X_r).
\]
As another example, consider the transition
$\delta(q,a)=(q',b,\leftarrow)$, in which the machine writes a $b$ on
the tape and then moves one position to the left.  This transition is
specified by the following rule:
%
\[
   \cl{j}:~~{\it conf}(q', X_l\sdue{1}{\eos-1}, X_l\suno{\eos}, b\conc X_r)
                         \IF {\it conf}(q,X_l, a, X_r).
\]
The situation is slightly more complicated if the tape head moves to
the right.  In this case, we append a blank symbol to the right end of
the tape, since otherwise, the tape head might move beyond the right
end of the tape.  By appending blanks, we effectively simulate a tape
of unbounded ($i.e.$, infinite) length.  For example, to express the
transition \,$\delta(q,a)=(q',b,\rightarrow)$,\, we use the following
rule, where $\blank$ denotes the blank tape symbol:%
%
\footnote{This approach can generate longer tape sequences than the
Turing machine actually needs.  For instance, sequences of unbounded
length will be generated whenever the machine enters an infinite loop,
even if the machine uses only a finite amount of tape.  Of course,
this generation of overly-long sequences does not detract from the
theorem.  Moreover, it is exploited in the proof of
Theorem~\ref{th:und}.}
%
\[
   \cl{k}:~~{\it conf}(q', X_l\conc b, X_r\suno{1}, X_r\sdue{2}{\eos} \conc \blank)
                         \IF {\it conf}(q,X_l, a, X_r).
\]

Finally, the following rule detects the end of a computation and
returns the contents of the machine tape:
\[
        \cl{2}:~~output(X_l\sdue{2}{\eos}\conc S\conc X_r)
                             \IF {\it conf}(q_h, X_l, S, X_r).
\]
The body of this rule simply checks whether the machine has reached a
configuration with a halting state, $q_h$.  If so, then the contents
of the machine tape (minus the left-end marker) are extracted,
converted to a single sequence, and passed to the rule head.  This
sequence is the output of the Turing machine computation.

It is not hard to see that program $\prog_f$ consisting of the rules
above correctly simulates the computation of machine $\tm_f$.
Formally, we have the following result: for any database $\inst$ of
the form $\{input(x)\}$,
%
\begin{center}
   $output(y) ~\in~ T_{\prog_f,\inst}\uparrow\omega$ ~~if and only if
   on input $x$, machine $\tm_f$ halts and outputs $y$,
\end{center}
%
$i.e.$, if and only if $f$ is defined at $x$ and $y = f(x)$.  This
proves that program $\prog_f$ expresses sequence function $f$.
\end{Proof}

Note that although {\name} is {\Fcompl}, it is not {\Qcompl}, since it
expresses only {\em monotonic\/} queries.




%%%%%%%%%%%%%%% FINITENESS %%%%%%%%%%%%%%%%%%%%

\section{The Finiteness Problem}
\label{sec:finite}

As shown in Examples~\ref{es:multrep} and~\ref{es:echo1}, the least
fixpoint of a {\name} program can be infinite.  In this section, we
focus on programs that are guaranteed to have a finite least fixpoint,
and which are thus guaranteed to be safe.


\begin{definition}[Finite Semantics]
A {\name} program has a finite semantics for a database schema if it
has a finite least fixpoint for all instances of the schema.
\end{definition}


The problem of determining whether a {\name} program has a finite
semantics is called the {\it finiteness problem}.


\begin{theorem} \label{th:und}
The finiteness problem for {\name} is fully undecidable, $i.e.$, is
outside of RE.
\end{theorem}

\begin{Proof}
The proof of Theorem~\ref{th:complexitysd} constructed a {\name}
program, $\prog$, that encodes an arbitrary Turing machine, $M$.  The
database schema for program $P$ consists of a single unary relation,
$input$.  We show that program $P$ has a finite semantics for all
instances of this schema if and only if machine $M$ halts on all
inputs.  Thus, if we can solve the finiteness problem for {\name},
then we can determine whether an arbitrary Turing machine accepts all
its inputs, a problem that is outside of RE.

We must consider {\it all\/} instances of the database schema.  First,
though, we consider those instances that consist of a {\it single\/}
atom, $input(x)$.  These are the instances for which the program was
designed.  For such an instance, program $P$ simulates the computation
of machine $M$ on input $x$.  Specifically, the program derives all
the machine configurations that are reachable from the initial
configuration.  At each step of the computation, the program generates
a new sequence to represent the next configuration.  Moreover, it
generates a {\it longer\/} sequence each time the machine's tape head
moves to the right (by rule~$\cl{k}$ in the proof of
Theorem~\ref{th:complexitysd}).  If the computation halts, then a
finite number of new sequences are generated, and the least fixpoint
is finite.  However, if the computation does not halt, then the tape
head moves to the right an infinite number of times,\footnote{Without
loss of generality, we can assume that the tape head moves at every
computation step.} so longer and longer sequences are generated
without bound, and the least fixpoint is infinite.  Thus, for database
instances of the form $\{input(x)\}$, the least fixpoint is finite if
and only if the machine halts on input $x$.

Now consider an arbitrary instance of the schema.  Such a database has
the form \,$\{input(x_1),$ $input(x_2),...$ $,input(x_n)\}$,\,
representing $n$ machine inputs.  In this case, program $P$ carries
out $n$ independent computations, one for each input.  Specifically,
the program derives all the machine configurations reachable from any
of the $n$ initial configurations.  In this case, the least fixpoint
is finite if and only if the machine halts on all $n$ inputs.  Thus,
program $P$ has a finite least fixpoint for all instances of the
schema if and only if machine $M$ halts on all inputs.
\end{Proof}


Since finiteness is undecidable, the challenge is to identify subsets
of {\name} that guarantee finiteness.  The simplest way to do this is
to forbid the construction of new sequences.  The resulting language,
in which constructive terms of the form $\sterm{1}\conc \sterm{2}$
cannot be used, is called {\em Non-constructive\/} {\name}.  In this
language, we cannot express queries beyond {\sc ptime}, since for each
non-constructive program $\prog$, and each database $\inst$, the
extended active domain is fixed and does not grow during the
computation.  Theorem~\ref{th:complexitync-sd} below shows that
Non-constructive {\name} has low complexity.  In addition, it
expresses a wide range of {\em pattern matching\/} queries, as shown
in Example~\ref{es:abcn}, which retrieves sequences in a non
context-free language.


\begin{theorem} \label{th:complexitync-sd}
The data complexity of Non-constructive {\name} is complete for {\sc
ptime}.
\end{theorem}

\begin{Proof}
The {\sc ptime} lower bound follows because {\name} includes Datalog
as a sublanguage.  The {\sc ptime} upper bound follows because the
least fixpoint of a non-constructive program has the same extended
active domain as the database.  Thus, the number of atoms in the least
fixpoint is at most polynomial in the size of the database.  Thus, the
least-fixpoint computation saturates after polynomially many
iterations, each taking polynomial time.
\end{Proof}


As less drastic way of guaranteeing finiteness is to allow for {\em
non-recursive construction}.  That is, we can require that programs be
{\em stratified\/} with respect to construction.  Stratified
construction can be formally defined along the same lines as
stratified negation in classical logic programs~\cite{ApBW88}, and can
be efficiently checked.  Programs with stratified construction have a
finite semantics even though new sequences can be constructed (in a
limited way) during query evaluation.


\begin{example} \label{es:stratified}
~{\bf [Stratified Construction]}~ The following program is stratified
with respect to construction:
%
\begin{center}
\begin{tabular}{llcl}
$\cl{1}:$ & $double(X\conc X)$     & $\IF$ & $r(X).$ \\
$\cl{2}:$ & $quadruple(X\conc X)$  & $\IF$ & $double(X)$.
\end{tabular}
\end{center}
%
Suppose $r$ is a base predicate.  Rule $\cl{1}$ doubles the length of
any sequence $X$ in relation $r$ by appending $X$ to itself.  Rule
$\cl{2}$ then produces sequences of quadruple length by doubling each
doubled sequence.  Each sequence in $double$ is thus the result of
exactly two concatenations.
%
%Note that the rules are stratified with respect to construction, since
%the rules can be evaluated in {\em strata} such that, for every
%constructive rule, predicates in the body are defined in lower strata
%with respect to the predicate in the head. In fact, in this case, we
%can first evaluate rule $\cl{1}$, taking every sequence in relation
%$R$ and appending it to itself. Then, once we have derived the extent
%of predicate $double$, we can evaluate predicate $quadruple$ and then
%terminate. Thus, although constructive rules are present, the program
%has a finite semantics over every input database.
\end{example}


Unfortunately, programs with stratified construction still have weak
sequence-restructuring capabilities.  This is because, in constructing
a new sequence, a stratified program only performs a fixed number of
concatenations, independent of the database.  Thus, a stratified
program cannot concatenate together all the sequences in the database.
Likewise, it cannot convert a sequence of length $n$ stored in the
database into a sequence of length $n^2$.  Nor can it compute the
complement or reverse of a sequence.  Thus, even though stratified
programs can express queries whose data complexity is complete for
{\sc ptime}, they cannot express many low-complexity sequence
restructurings.  Of course, we could increase the expressibility by
allowing recursion through constructive terms, but this greatly
increases the complexity of the language and leads to a non-finite
semantics.  The rest of this paper addresses this conundrum.




%%%%%%%%%%%   TRANSDUCERS  %%%%%%%%%%%%%

\section{Generalized Sequence Transducers}
\label{sec:seqtrans}

{\name} uses concatenation to construct new sequences.  Unfortunately,
as described above, concatenation is at once too powerful and too
weak: without recursion, it is unexpressive; but with recursion, it is
intractable.  We tackle this problem by developing a combination of
sequence operations and syntactic restrictions that, together, provide
the right blend of expressiveness and tractability.  This section
focuses on the sequence operations.  Later sections will blend them
into {\name} and provide syntactic restrictions.

One way to provide constructive sequence operations is with {\it
sequence transducers}, that is, finite automata that read input
sequences and generate output sequences.  Transducers support a
variety of low-complexity sequence restructurings, including
concatenation and complementation.  For this reason, transducers have
been incorporated into a number of data models and query languages for
sequence databases~\cite{GiWa92,GrNU94,Gonn94,SPSV92}.  Unfortunately,
like sequence concatenation, transducers tend to be both too powerful
and too weak.  As described in Section~\ref{sec:background}, query
languages based on transducers are either highly expressive but
unsafe, or safe but unexpressive.

Our solution to this problem is to generalize the transducer model.
When combined with simple syntactic restrictions, these more-powerful
machines lead to a query language with all the properties we want:
finite semantics, low complexity, and good sequence expressibility,
$i.e.$, the ability to express a wide range of sequence functions and
sequence queries.  In fact, we show (in Section~\ref{sec:safetd}) that
the new language expresses all the sequence functions in {\sc ptime}.
In addition, the new machine model provides natural ``levers'' with
which users can tune the data complexity of the query language.  In
all cases, however, the new machines are guaranteed to terminate,
which leads directly to a query language with a finite semantics.

This section defines the machine model and establishes its basic
complexity properties.  Section~\ref{sec:td} then incorporates the
model into {\name}, and Section~\ref{sec:safetd} develops syntactic
restrictions for the resulting language.



\subsection{The Machine Model}
\label{sec:seqtrans:model}

Intuitively, a {\it generalized sequence transducer\/} is a transducer
that can invoke other transducers as subroutines.  At each computation
step, a generalized transducer must consume an input symbol, and may
append a new symbol to its output, just like an ordinary transducer.
In addition, at each step, a generalized transducer may transform its
entire output sequence by sending it to another transducer, which we
call a {\it subtransducer}.  This process of invoking subtransducers
may continue non-recursively to many levels.  Thus a subtransducer may
transform its own output by invoking a subsubtransducer, etc.
Subtransducers are somewhat like oracle Turing machines of low
complexity.

We shall actually define a hierarchy of transducers.  $\transducers^k$
represents the set of generalized transducers that invoke
subtransducers to a maximum depth of $k-1$.  $k$ is called the {\em
order\/} of the transducer.  $\transducers^1$ thus represents the set
of ordinary transducers, which do not invoke any subtransducers.  We
define $\transducers^{k+1}$ in terms of $\transducers^k$, where
$\transducers^0$ is the empty set.  For convenience, we shall often
refer to members of $\transducers^1$ as {\it base transducers\/}, and
to any generalized sequence transducer simply as a transducer.

To formally define the notion of generalized sequence transducers, we
use three special symbols, $\inizio$, $\move$ and $\stay$.  $\inizio$
is an end-of-tape marker, and is the last symbol (rightmost) of every
input tape.  $\move$ and $\stay$ are commands for the input tape
heads: $\move$ tells a tape head to move one symbol to the right
($i.e.$, to consume an input symbol); and $\stay$ tells a tape head to
stay where it is.  Although the following definition is for
deterministic transducers, it can easily be generalized to allow
nondeterministic computations.  As such, it generalizes many of the
transducer models proposed in the literature (see for
example~\cite{GiWa92,SPSV92}).


\begin{definition} ~{\bf (Generalized Transducers)}~
A generalized m-input sequence transducer of order $k>0$ is a 4-tuple
$\left<K,q_0,\alp{}{},\delta\right>$ where:
%
\begin{enumerate}
\item
$K$ is a finite set of elements, called {\em states};

\item
$q_0 \in K$ is a distinguished state, called the {\em initial state}.

\item
$\alp{}{}$ is a finite set of symbols, not including the special
symbols, called the {\em alphabet};

\item
$\delta$ is a partial mapping from \,$K \times
\{\alp{}{}\cup\{\inizio\}\}^m$\, to \,$K \times \{\stay,\move\}^m
\times \{\alp{}{}\cup\{\e\}\cup\transducers^{k-1}\}$,\, called the {\em
transition function}.

\item
For each transition, $\delta(q,a_1,\ldots,a_m)$ of the form
$\langle q',c_1,\ldots,c_m,\out\rangle$, we impose three
restrictions: $(i)$ at least one of the $c_i$ must be $\move$, $(ii)$
if $a_i=\inizio$ then $c_i=\stay$, and $(iii)$ if \,$\out \in
\transducers^{k-1}$\, then it must be an $m+1$-input transducer.

\end{enumerate}
%
$\transducers^k$ consists of all generalized transducers of order at
most $k$, for \,$k > 0$;\ $\transducers^0 = \{\}$.
\end{definition}

In this definition, the restrictions in item {\it 5\/} have a simple
interpretation.  Restriction $(i)$ says that at least one input symbol
must be consumed at each step of a computation ($c_i$ is a command to
input head $i$).  Restriction $(ii)$ says that an input head cannot
move past the end of its tape ($a_i$ is the symbol below input head
$i$).  Restriction $(iii)$ says that a subtransducer must have one
more input than its calling transducer.

The computation of a generalized sequence transducer over input
strings $\left<\seq{1}, \ldots, \seq{m}\right>$ proceeds as follows.
To start, the machine is in its initial state, $q_0$, each input head
scans the first ($i.e.$, leftmost) symbol of its tape, and the output
tape is empty.  At each point of the computation, the internal state
and the tape symbols below the input heads determine what transition
to perform.  If the internal state is $q$ and the tape symbols are
$a_1\ldots a_m$, then the transition is
\,$\delta(q,a_1,\ldots,a_m)=\langle q',c_1,\ldots,c_m,\out\rangle$.
This transition is carried out as follows:
%
\begin{itemize}
\item
If $\out$ is a symbol in $\alp{}{}$, then it is appended to the output
sequence; if $\out = \e$, then the output is unchanged.

\item
If $\out$ represents a call to a transducer $\ST \in
\transducers^{k-1}$ then $\ST$ is invoked as a subtransducer.  In this
case, the transducer suspends its computation, and the subtransducer
starts.  The subtransducer has $m+1$ inputs: a copy of each input of
the calling transducer, plus a copy of its current output.  When the
subtransducer starts, its output tape is empty, and its input heads
are at the beginning of its input tapes.  The subtransducer then
consumes its inputs and produces an output sequence.  When it is
finished, the output of the subtransducer is copied to (overwrites)
the output tape of the calling transducer.  These ideas are
illustrated in Figure~\ref{fig:trans}.

\item
The transducer ``consumes'' some input by moving at least one tape
head one symbol to the right.

\item
The transducer enters the next state, $q'$, and resumes its
computation.
\end{itemize}
%
The transducer stops when every input tape has been completely
consumed, that is, when every input head reads the symbol $\inizio$.
Since transducers (and subtransducers) must consume all their input,
the computation of every generalized transducer is guaranteed to
terminate.  In measuring the time complexity of a generalized
transducer, we count the number of transitions performed by the
top-level transducer and all its subtransducers.


\begin{figure}
\begin{center}
%\framebox{\input{trans.pic}}
\framebox{ \unitlength=1.00mm \special{em:linewidth 0.4pt}
\linethickness{0.4pt}
\begin{picture}(149.00,73.00)
\put(27.00,43.00){\framebox(40.00,20.00)[cc]{$\ST_1$}}
\put(82.00,13.00){\framebox(40.00,20.00)[cc]{$\ST_2$}}
\put(74.00,58.00){\makebox(0,0)[cc]{$\sigma_{out}^{old}$}}
\put(129.00,28.00){\makebox(0,0)[cc]{$\sigma_{out}^{new}$}}
\put(67.00,53.00){\line(1,0){82.00}}
\put(14.00,60.00){\line(1,0){13.00}}
\put(14.00,54.00){\line(1,0){13.00}}
\put(14.00,47.00){\line(1,0){13.00}}
\put(24.00,25.00){\line(1,0){58.00}}
\put(20.00,21.00){\line(1,0){62.00}}
\put(16.00,15.00){\line(1,0){66.00}}
\put(74.00,30.00){\line(1,0){8.00}}
\put(122.00,23.00){\line(1,0){16.00}}
\put(6.00,61.00){\makebox(0,0)[cc]{$\seq{in,1}$}}
\put(6.00,54.00){\makebox(0,0)[cc]{$\seq{in,2}$}}
\put(6.00,50.00){\makebox(0,0)[cc]{$\ldots$}}
\put(6.00,46.00){\makebox(0,0)[cc]{$\seq{in,m}$}}
\put(6.00,73.00){\makebox(0,0)[cc]{ }}
\put(24.00,60.00){\vector(0,-1){20.00}}
\put(24.00,40.00){\line(0,-1){15.00}}
\put(20.00,60.00){\vector(0,-1){25.00}}
\put(20.00,35.00){\line(0,-1){14.00}}
\put(16.00,60.00){\vector(0,-1){30.00}}
\put(16.00,30.00){\line(0,-1){15.00}}
\put(74.00,53.00){\vector(0,-1){13.00}}
\put(74.00,40.00){\line(0,-1){10.00}}
\put(138.00,23.00){\vector(0,1){17.00}}
\put(138.00,40.00){\line(0,1){13.00}}
\end{picture}
}
\end{center}
\caption{Transducer $\ST_1$ calls subtransducer $\ST_2$.}
\label{fig:trans}
\end{figure}

Finally, note that a m-input transducer defines a {\em sequence
mapping}, \,$\ST: (\alp{}{*})^m \rightarrow \alp{}{*}$,\, where
$\ST(\seq{1},\ldots,\seq{m})$ is the output of the transducer on
inputs $\seq{1},\ldots,\seq{m}$.  Generalized transducers express a
much wider class of mappings than ordinary transducers.  For instance,
they can compute outputs whose length is polynomial and even
exponential in the input lengths, as the following example
illustrates.


%\begin{figure}
%\begin{center}
%\framebox{\input{square.pic}}
%\end{center}
%\caption{Squaring the input.}
%\label{fig:square}
%\it
%\begin{quotation}
%This figure illustrates the transducer of Example~\ref{es:n2} at
%various stages of computation.  The numbers on the input and output
%lines indicate sequence lengths.
%\end{quotation}
%\end{figure}

\begin{figure}
\begin{center}
\begin{tabular}{|c|c|c|c|c|}
\hline
step & input         & output   &  operation         & new output\\
\hline
\hline
 1   & $\fbox{\em a}bc\inizio$  & $\e$     &  invoke\, $\ST_{append}$  & $abc$ \\
\hline
 2   & $a\fbox{\em b}c\inizio$  & $abc$    &  invoke\, $\ST_{append}$ & $abcabc$ \\
\hline
 3   & $ab\fbox{\em c}\inizio$  & $abcabc$ &  invoke\, $\ST_{append}$ & $abcabcabc$ \\
 \hline
\hline
\end{tabular}
\end{center}
\caption{Squaring the input.}
\label{fig:square}
\it
\begin{quotation}
This table illustrates the computation of transducer $\ST_{square}$
from Example~\ref{es:n2} on the input sequence {\em abc}.  Each row of
the table represents one step of the computation.  The column labelled
{\em ``input''} shows the position of the input head just before the
step, the column labelled {\em ``output''} shows the contents of the
output tape just before the step, and the column labelled {\em ``new
output''} shows the contents of the output tape just after the step.
The column labelled {\em ``operation''} describes what the step does.
The table shows that at each step, $\ST_{square}$ appends a copy of
its input to its output by invoking the subtransducer $\ST_{append}$.
\end{quotation}
\end{figure}


\begin{example} ~{\bf [Quadratic Output]}~
\label{es:n2}
Let $\ST_{square}$ be a generalized transducer with one input and one
subtransducer.  At each computation step, $\ST_{square}$ appends a
copy of its input to its output.  After $k$ steps, the output consists
of $k$ copies of the input concatenated together.  At the end of the
entire computation, the output has length $n^2$, where $n$ is the
length of the input.  To append its input to its output,
$\ST_{square}$ invokes a subtransducer called $\ST_{append}$ with two
inputs.  One input to $\ST_{append}$ is the input to $\ST_{square}$
and the other input is the output of $\ST_{square}$.  $\ST_{append}$
simply appends its two inputs.  The output of $\ST_{append}$ then
becomes the output for $\ST_{square}$, overwriting the old output.

To illustrate the combined effect of transducer and subtransducer, let
$\seq{in}$ be the input to $\ST_{square}$.  Just before the $i^{th}$
invocation of the subtransducer, one input to $\ST_{append}$ is
$\seq{in}$ and the other input is $i-1$ copies of $\seq{in}$
concatenated together.  Thus, when $\ST_{append}$ finishes this
computation, its output is $i$ copies of $\seq{in}$ concatenated
together.  This behaviour is illustrated in Figure~\ref{fig:square},
in which the transducer input is $abc$, and the output is $abcabcabc$.

%Let $\seq{in}$ be the input to $\ST_{square}$.  If $\seq{in}$ has
%length $n$, then at the end of its computation, the output of
%$\ST_{square}$ will have length $n^2$, obtained by concatenating
%$\seq{in}$ with itself $n$ times.  To see this, note that
%$\ST_{square}$ calls $\ST_{append}$ exactly $n$ times, once for each
%symbol in $\seq{in}$ (see Figure~\ref{fig:square}):
%
%\begin{itemize}
%\item
%At time $1$, the two inputs to $\ST_{append}$ are $\seq{in}$ and the
%empty sequence, $\e$ (since the output of $\ST_{square}$ is initially
%empty).  Thus, the output of $\ST_{append}$ at this step is
%$\seq{in}$, which becomes the new output for $\ST_{square}$.
%
%\item
%At time $2$, the two inputs to $\ST_{append}$ both contain a copy of
%$\seq{in}$.  Thus, the output of $\ST_{append}$ at this step is the
%concatenation of $\seq{in}$ with itself, which is a sequence of length
%$2n$.  This sequence then becomes the new output for $\ST_{square}$.
%
%\item
%In general, at time $i$, for $1 \leq i \leq n$, the two inputs to
%$\ST_{append}$ are $\seq{in}$ and the sequence obtained by
%concatenating $\seq{in}$ with itself $i-1$ times.  Thus, the output of
%$\ST_{append}$ at this step is the sequence obtained by concatenating
%$\seq{in}$ with itself $i$ times.  This sequence then becomes the new
%output for $\ST_{square}$.
%\end{itemize}
%
%Thus, after $n$ steps, the output of $\ST_{square}$ is a sequence of
%length $n^2$, namely the $n$-fold concatenation of $\seq{in}$ with
%itself.
\end{example}


\paragraph{Remark:}
A generalized sequence transducer can be simulated by a multi-tape
Turing machine with at most a constant factor increase in execution
time.  This can be done with a Turing machine that has one tape for
each transducer input and output.  For instance, the generalized
transducer in Figure~\ref{fig:trans} can be simulated by a Turing
machine with $2m+3$ tapes: $m$ tapes for the inputs to transducer
$T_1$, and one tape for the output of $T_1$; and $m+1$ tapes for the
inputs to subtransducer $T_2$, and one tape for the output of $T_2$.
The input sequences to the generalized transducer are stored on the
$m$ input tapes for $T_1$.  With this configuration, a single
transducer step can be simulated by a constant number of
Turing-machine steps.  The only exception is the copying of sequences
between transducers and subtransducers.  However, it is not hard to
show that copying increases the total simulation time by at most a
constant factor.  For instance, each time $T_2$ begins executing, the
$m+1$ input sequences that it needs are first copied to its input
tapes (and, simultaneously, the output tape of $T_1$ is erased.)  The
number of steps required to do this is linear in the total length of
the copied sequences.  Since $T_2$ consumes all these sequences during
its execution, this copying increases $T_2$'s execution time by at
most a constant factor.  Likewise, each time $T_2$ finishes executing,
its output tape is copied to the output tape of $T_1$ (and,
simultaneously, the output tape of $T_2$ is erased).  However, since
$T_2$ generated the sequence, this copying increases $T_2$'s execution
time by at most a constant factor.  In general, every sequence that is
copied is either consumed or generated somewhere else, so the effect
of copying is to increase the total execution time by at most a
constant factor.  Thus, a generalized transducer that runs in time
$O[f(n)]$ can be simulated by a Turing machine that also runs in time
$O[f(n)]$.

One subtley in the simulation is that after input tapes are copied,
they must be restored to their original state.  (In contrast, after
copying, output tapes are simply erased.)  For instance, after copying
sequences from the inputs of $T_1$ to the inputs of $T_2$, the input
tape heads of $T_1$ must be returned to their original positions.
This can be done in a number of ways.  One way is to mark the original
positions with compound symbols.  In particular, if $b$ is the symbol
currently under an input tape head, then the tape head overwrites it
with the compound symbol \,\mbox{$\left< b,*\right>$}.\, During tape
copying, all tape symbols are copied exactly, except for the compound
symbol, which is copied as $b$.  After copying, the input tape head
moves back to its original (marked) position, and the compound symbol
is replaced by the original symbol, $b$.  In this way, the tape is
copied and restored in linear time.




%%%%%%%%%%  TRANSDUCER NETWORKS  %%%%%%%%%%%%%

\subsection{Transducer Networks}
\label{sec:networks}

Transducers can be combined to form {\em networks}, in which the
output of one transducer is an input to other transducers.  Since we
are interested in finite computations, we only consider {\em acyclic
networks}, in which the output of a transducer is never fed back to
its own input.  For each transducer network, some transducer inputs
are designated as network inputs, and some transducer outputs are
designated as network outputs.  Each network then computes a {\em
mapping} from sequence tuples to sequence tuples.  When the network
has only one output, the network computes a {\Sfunction}.  This
section presents basic results about the complexity of generalized
transducer networks.  For an expanded analysis
see~\cite{Mecc96,BoMe97DBPL}.

The computational complexity of the sequence function computed by a
transducer network depends on two parameters.  The first is the {\em
diameter}\/ of the network, $i.e.$, the maximum length of a path in
the network.  The diameter determines the maximum number of
transformations that a sequence will undergo in traveling from the
input to the output of a network.  The second parameter is the {\em
order}\/ of the network.  This is maximum order of any transducer in
the network.  If the set of transducers in the network is a subset of
$\transducers^k$, then the order of the network is at most $k$.
Intuitively, the order of a network is the maximum depth of
subtransducer nesting.

We now establish a basic result about the complexity of acyclic
networks.  This result involves the elementary sequence
functions~\cite{Papa94}, which are defined in terms of the {\em
hyper-exponential functions}, $\hyp_i(n)$.  These latter functions are
defined recursively as follows:
%
\begin{itemize}
\item  $\hyp_0(n)=n$
\item  $\hyp_{i+1}(n) = 2^{\hyp_i(n)}$~~~ for ~$i \geq 1$
\end{itemize}
%
$\hyp_i$ is called the hyper-exponential function of level $i$.  The
set of {\em elementary sequence functions} is the set of sequence
functions that have hyper-exponential time complexity, that is, the
set of sequence functions in \,$\bigcup_{i \geq 0}{\rm
DTIME}[\hyp_i(\Omicron(n))]$.

The theorems below characterize the complexity and expressibility of
two classes of transducer networks, those of order 2 and 3,
respectively.  Higher order networks are investigated
in~\cite{Mecc96,BoMe97DBPL}. Our first results concern the output size
of transducer networks.


\begin{theorem} \label{th:networks}
{\bf (Complexity of Transducer Networks)} Consider an acyclic network
of transducers with multiple inputs and one output.
%
\begin{itemize}
\item
If the network has order 2, then the length of the output is (at most)
polynomial in the sum of input lengths.

\item
If the network has order 3, then the length of the output is (at most)
hyper-exponential in the sum of input lengths.
\end{itemize}
%
Moreover, these bounds can be attained.
\end{theorem}
%
\begin{Proof}
In the following, $\outputsize{j}{}$ denotes the {\em length\/} of the
final output of transducer $\ST_j$, and $\inputsize{j}{}$ denotes the
{\em total length\/} of its initial inputs, $i.e.$, the sum of the
lengths of all input sequences.  Superscripts denote particular steps
of a computation; $e.g.$, $\outputsize{j}{i}$ denotes the output
length of transducer $\ST_j$ at step $i$ of its computation.

First note that the output length of a base transducer is linear with
respect to its total input length.  In fact, the output can be at most
as long as the the concatenation of its inputs.  In symbols,
$\outputsize{j}{} \leq \inputsize{j}{}$.  With this in mind, we prove
each of the two items of the theorem in turn.  In each proof, we first
consider a single transducer, {\em i.e.} a network of diameter 1; and
then we extend the proof to networks of arbitrary diameter.



\paragraph{\em Networks of Order 2.}
Let $\ST_1$ be a transducer of order 2.  At step $i$ of its
computation, either $\ST_1$ may append a symbol to its output, or it
calls a subtransducer, $\ST_2$, whose output overwrites the output of
$\ST_1$.  Thus, one of the following is true for each $i$:
\[
\left\{
  \begin{array}{l}
  \outputsize{1}{i+1} \leq \outputsize{1}{i}+1 \smallskip\\
  \outputsize{1}{i+1} =
        \outputsize{2}{} \leq \inputsize{1}{} + \outputsize{1}{i}
  \end{array}
\right.
\]
The second inequality follows because the input to $\ST_2$ is the
initial input to $\ST_1$ plus the current output of $\ST_1$.

In the worst case, $\ST_1$ calls a subtransducer at each step of its
computation, and the subtransducer produces an output as long as its
total input.  In this case, the second inequality above becomes an
equality.  The following recursive equation thus describes the worst
case:
\[
\left\{
  \begin{array}{l}
  \outputsize{1}{0}=0 \\
  \outputsize{1}{i+1}= \inputsize{1}{} + \outputsize{1}{i}
  \end{array}
\right.
\]
Solving the equation, we get ~$\outputsize{1}{i}= i\,\inputsize{1}{}$.
~The computation terminates after $n$ steps, where $n=
\inputsize{1}{}$ is the total input length of $\ST_1$.  Thus, in the
worst case, the final output is quadratic in the initial input,
$i.e.$,\, $\outputsize{1}{}=n^2$.

Now consider an acyclic network of transducers with diameter $d$ and
order $2$.  Let $\ST_1,\ldots,\ST_d$ be the transducers on the longest
path in the network.  In the worst case, the output of each transducer
is quadratic in its total input; and each network input goes to
transducer $\ST_1$.  Thus, if $n$ is the total length of the network
input, then the total input length of $\ST_1$ is $n$, and
\[
\left\{
  \begin{array}{rcccl}
  n^2 & \leq & \outputsize{1}{} & \leq & \Omicron(n^2) \\
  n^4 & \leq & \outputsize{2}{} & \leq & \Omicron(n^4) \\
  n^8 & \leq & \outputsize{3}{} & \leq & \Omicron(n^8) \\
      &      & \ldots \\
  n^{2^d} & \leq & \outputsize{d}{} & \leq & \Omicron(n^{2^d})
  \end{array}
\right.
\]
The left-hand inequalities arise because at least one copy of the
output of $\ST_i$ forms an input to $\ST_{i+1}$.  The right hand
inequalities arise because $\ST_{i+1}$ may have several inputs.  In
any event, since the diameter $d$ is fixed, the final output length is
polynomial in $n$.  This proves the first part of the theorem.


\paragraph{\em Networks of Order 3.}
The proof for this case is similar.  Let $\ST_1$ be a transducer of
order 3.  At each step of its computation, $\ST_1$ may call a
subtransducer, $\ST_2$, of order 2.  In the worst case, $\ST_1$ calls
$\ST_2$ at every step, and $\ST_2$ squares its input, as shown above.
Thus, at step $i$ of $\ST_1$'s computation, we have:
\[
  \outputsize{1}{i} = \outputsize{2}{} =
        (\inputsize{1}{} + \outputsize{1}{i-1})^2
\]
The worst case is therefore described by the following recursive
equation:
\[
\left\{
  \begin{array}{l}
  \outputsize{1}{0}=0 \\
  \outputsize{1}{i}= (\inputsize{1}{} + \outputsize{1}{i-1})^2
  \end{array}
\right.
\]
Solving the equation, we get ~\mbox{$\outputsize{1}{i} =
\inputsize{1}{}^{2^i} + \Omicron(\inputsize{1}{}^{2^i-1})$}.  ~The
computation terminates after $n$ steps, where $n = \inputsize{1}{}$ is
the total input length of $\ST_1$.  Thus ~\mbox{$\outputsize{1}{} =
n^{2^n} + \Omicron(n^{2^n-1})$}.  Thus ~\mbox{$2^{2^n} \leq
\outputsize{1}{} \leq 2^{2^{\Omicron(n)}}$}~ in the worst case;
$i.e.$, the final output is double exponential in the initial input.
Intuitively, this comes about because $\ST_1$ can use $\ST_2$ to
square the input length, $n$, and it can do this $n$ times.

Now consider an acyclic network of transducers with diameter $d$ and
order $3$.  Let $\ST_1,\ldots,\ST_d$ be the transducers on the longest
path in the network.  The output of each transducer is at most double
exponential in its total input.  Thus, if $n$ is the total length of
the network input, then in the worst case
\[
\left\{
  \begin{array}{rcccl}
  \hyp_2(n) ~=~ 2^{2^n} & \leq & \outputsize{1}{} & \leq &
        2^{2^{\Omicron(n)}} ~=~ \hyp_{2}(\Omicron(n)) \\

  \hyp_4(n) ~=~ 2^{2^{hyp_2(n)}}& \leq & \outputsize{2}{} & \leq &
        2^{2^{\hyp_{2}(\Omicron(n))}} ~=~ \hyp_{4}(\Omicron(n)) \\

  \hyp_6(n) ~=~ 2^{2^{hyp_4(n)}} & \leq & \outputsize{3}{} & \leq &
        2^{2^{\hyp_{4}(\Omicron(n))}} ~=~ \hyp_{6}(\Omicron(n)) \\

        & & \ldots \\

  \hyp_{2d}(n) & \leq & \outputsize{d}{} & \leq &
        \hyp_{2d}(\Omicron(n)) \\
  \end{array}
\right.
\]
This proves the second part of the theorem.
%
\end{Proof}


Building on Theorem~\ref{th:networks}, we prove two expressibility
theorems for acyclic networks of transducers.  Both theorems are
concerned with transducer networks that have a single input and a
single output.  Such networks compute a function from sequences to
sequences.  Theorem~\ref{th:expressibility1} first characterizes the
sequence functions computable in polynomial time.  (Other
characterizations can be found in \cite{CRSV94,BeCo92,GrMi95}.)
Theorem~\ref{th:expressibilityk} then characterizes the sequence
functions computable in elementary time.  In these theorems, and in
the rest of the paper, we assume that the alphabet $\Sigma$ is finite,
and that the domain of every sequence function is a (possibly
infinite) subset of $\Sigma^*$.  Because the alphabet is finite, a
transducer (or a Turing machine) whose tape alphabet includes $\Sigma$
expresses a sequence function in a natural way, $i.e.$, without any
special encoding of sequences onto machine tapes.


\begin{theorem} \label{th:expressibility1}
{\bf (Expressibility of Order-2 Networks)} Acyclic transducer networks
of order 2 express exactly the class of sequence functions computable
in {\sc ptime}.
\end{theorem}

\begin{Proof}
To prove the upper expressibility bound, suppose we are given a
transducer network of order 2.  By Theorem~\ref{th:networks}, the
input to each transducer in the network is of polynomial size
(polynomial in the size of the network input).  Moreover, each
transducer in the network is of order 1 or 2, so it consumes its input
in polynomial time.  Each transducer therefore runs in polynomial time
wrt to the size of the network input.  By the remark at the end of
Section~\ref{sec:seqtrans:model}, the transducer network can be
simulated by a Turing machine that also runs in polynomial time.  The
function computed by the network is thus in {\sc ptime}.

To prove the lower expressibility bound, we must show that every
sequence function in {\sc ptime} can be computed by an acyclic
transducer network of order 2.  Any such sequence function is computed
by a Turing machine, $M$, that runs in polynomial time.  Without loss
of generality, we can assume that $M$ has only one tape and runs in
time $n^k$ for some $k$, where $n$ is the length of its input.  We
shall simulate the computations of $M$ using a transducer network.

We encode a configuration of the Turing machine as a sequence in a
standard way.  Suppose that the contents of the machine tape is \,$b_1
b_2 \ldots b_n$,\, that the tape head is currently scanning symbol
$b_i$, and that the machine is in state $q$.  We represent this
configuration by the sequence \,$b_1b_2\ldots b_{i-1}qb_ib_{i+1}\ldots
b_n$.  With this representation, we can construct a base transducer
that transforms one Turing machine configuration into the next.  That
is, if the input to the transducer is a configuration of $M$, then the
output is the next configuration of $M$.

To compute a sequence function, our transducer network performs three
tasks: it constructs the initial configuration of the Turing machine,
it simulates $n^k$ Turing-machine steps, and it extracts the output
sequence from the final configuration.  These tasks are carried out as
follows:
%
\begin{itemize}

\item
Given an input sequence \,$a_1a_2\ldots a_n$,\, a transducer
constructs the initial configuration of the Turing machine.  This
configuration is simply the sequence \,$q_0a_1a_2\ldots a_n$,\, where
$q_0$ is the initial state of the Turing machine.  This construction
is easily carried out by a transducer of order 2.

\item
Given the input sequence (of length $n$), a series of transducers
generates a sequence, $\seq{count}$, of length at least $n^k$.  We
shall use this sequence to count time.  It is easily generated using
$\lceil log_2(k)\rceil$ transducers of order 2, where the output
length of each transducer is the square of its input length.

\item
A transducer $\ST_{M}$ of order $2$ simulates the computation of
Turing machine $M$.  This transducer has two inputs: the counter
sequence $\seq{count}$, and the initial configuration of $M$.
$\ST_{M}$ first moves the initial configuration from its input to its
output.  It then repeatedly calls a subtransducer while consuming its
other input.  It thus calls the subtransducer at least $n^k$ times.
The subtransducer encodes the transition function of machine $M$.
With each call, the subtransducer transforms the output of $\ST_{M}$
from one configuration of $M$ to the next.  When $\ST_{M}$ has
completely consumed its input, its output represents the final
configuration of machine $M$.

\item
A transducer $\ST_{decode}$ decodes the final configuration of machine
$M$.  To do this, we can assume the final configuration has the form
\,$c_1c_2\ldots c_mq_zxxxxxx\ldots x$,\, where $c_1c_2\ldots c_m$ is
the output sequence computed by $M$, $q_z$ is the final state of $M$,
and each $x$ denotes a blank tape character.  $\ST_{decode}$ simply
removes the blanks and the machine state, leaving the output of
machine $M$.

\end{itemize}
%
\end{Proof}


\begin{theorem} \label{th:expressibilityk}
{\bf (Expressibility of Order-3 Networks)} Acyclic transducer networks
of order 3 express exactly the class of sequence functions computable
in elementary time.
\end{theorem}

\begin{Proof}
The proof is similar to that of Theorem~\ref{th:expressibility1}.  The
main difference is that the sequence $\seq{count}$ must be of
hyper-exponential length.  This is easily accomplished by a series of
transducers of order 3, as shown in the proof of
Theorem~\ref{th:networks}.
\end{Proof}

%There is a close relationship between the diameter of transducer
%networks and levels in the hyper-exponential hierarchy.  For instance,
%any sequence function in {\sc exptime} can be expressed by a single
%transducer of order 3.  These ideas are further developed
%in~\cite{BoMe97DBPL}.




%%%%%%%%%%%%%%  TRANSDUCER DATALOG  %%%%%%%%%%%%%%%

\section{{\name} with Transducers}
\label{sec:td}

This section develops a new, logic-based language by incorporating
generalized transducers into {\name}.  Using this language, the next
section develops a safe and finite query language for sequence
databases.


\subsection{Syntax and Semantics}
\label{sec:td:syntax}

To invoke transducer computations from within a logical rule, we
augment the syntax of {\name} with special interpreted function
symbols, one for each generalized sequence transducer.  From these
function symbols, we build function terms of the form
$\ST(\sterm{1},\ldots,\sterm{m})$, called {\em transducer terms}.  The
term $\ST(\sterm{1},\ldots,\sterm{m})$ is interpreted as the output of
transducer $\ST$ on inputs $\sterm{1},\ldots,\sterm{m}$.  Like
constructive terms, such as \mbox{$x \conc y$}, transducer terms are
allowed only in the heads of rules.  Transducer terms are also closed
under composition.  For example, if $T_1$ and $T_2$ denote 2-input
transducers, then \,\mbox{$T_1(x,T_2(y,z))$}\, is a transducer term.
The resulting language is called {\em \name\ with Transducers}, or
simply {\em \Tname}.  We show that any program in {\em \Tname} can be
translated into an equivalent program in {\name}.  In other words, we
can implement generalized sequence transducers in {\name}. To clearly
distinguish programs in {\Tname} from those in {\name}, we use two
different implication symbols.  Whereas rules in {\name} use the
symbol $\IF$, rules in {\Tname} use the symbol $\IFT$, as in\, $p \IFT
q,r$.

{\Tname} generalizes an idea already present in {\name}, namely, the
use of interpreted function terms.  To illustrate, consider the
following constructive rule in {\name}:
%
\[
        p(X\conc Y) ~\IF~ q(X,Y).
\]
%
This rule concatenates every pair of sequences $X$ and $Y$ in
predicate $q$.  The constructive term $X\conc Y$ in the head is {\em
interpreted} as the result of concatenating the two sequences
together.  {\Tname} generalizes this mechanism to arbitrary
transducers.  For example, the following {\Tname} program is
equivalent to the {\name} program above:
%
\[
        p(\ST_{\it append}(X,Y)) ~\IFT~ q(X,Y).
\]
%
where $\ST_{\it append}$ is a transducer that concatenates its two
inputs.  As this example shows, constructive terms are not needed in
{\Tname}, since they can be replaced by transducer terms.  Thus, in the
sequel, they will not be used in {\Tname} programs.  In {\name}, rules
with constructive terms in the head are called constructive rules (or
clauses).  The above example suggests a natural extension of this idea:
in {\Tname}, rules with transducer terms in the head will also be called
{\em constructive rules}. We also say that a program in {\Tname} has
{\em order} $k$ if $k$ is the maximum order of all transducers in the
program.  A program with no transducers has order $0$.

The semantics of {\Tname} is an extension of the semantics of {\name}.
The only change is to extend the interpretation of sequence terms to
include transducer terms.  This can be done in a natural way.  Let
$\subs{}$ be a substitution based on a domain ${\cal D}$.  Thus,
$\subs{}(\sterm{})$ is a sequence in ${\cal D}$ for any sequence term
$\sterm{}$.  To extend $\subs{}$ to transducer terms, define
\,$\subs{}(\ST(\sterm{1},\ldots,\sterm{m}))$\, to be the output of
transducer $\ST$ on inputs $\subs{}(\sterm{1}), \ldots,
\subs{}(\sterm{m})$, where the symbols of each $\subs{}(\sterm{i})$
are consumed from left to right.  Except for this change, the
semantics of {\Tname} is identical to that of {\name}.  In particular,
all the definitions and results in Section~\ref{sec:fix} are still
valid.

A {\Tname} program can be thought of as a {\em network\/} of
transducers, and vice-versa.  This is because the {\em result}\/ of a
transducer term in one rule can be used as an {\em argument\/} for a
transducer term in another rule.  This corresponds to feeding the
output of one transducer to an input of another transducer. Below we
give an example of sequence restructuring in Molecular Biology. It is
naturally represented as a transducer network.  By embedding this
network in {\Tname}, an entire database of sequences can be
restructured and queried.


\begin{example} ~{\bf [From DNA to RNA to Protein]}~
\label{es:transcribe}
Two fundamental operations in Molecular Biology are the transcription
of DNA into RNA, and the translation of RNA into protein.  All three
molecules in this process can be modelled as sequences.  DNA molecules
are modeled as sequences over the alphabet $\{a,c,g,t\}$, where each
character represents a {\em nucleotide}.  RNA molecules are modeled as
sequences over the alphabet $\{a,c,g,u\}$, where each character
represents a {\em ribonucleotide}.  During transcription, each
nucleotide in a DNA sequence is converted into a ribonucleotide in an
RNA sequence according to the following rules:
%
\begin{center}
\begin{tabular}{ll}
        Each $a$ becomes $u$. & Each $c$ becomes $g$. \\
        Each $g$ becomes $c$. & Each $t$ becomes $a$.
\end{tabular}
\end{center}
%
Thus, the DNA sequence $acgtacgt$ is transcribed into the RNA sequence
$ugcaugca$.\footnote{
%
For simplicity, this example ignores biological complications such as
intron splicing~\cite{watson}, even though it can be encoded in
{\Tname} without difficulty.}

Protein molecules are modeled as sequences over a twenty-character
alphabet, ~{\sc$\{$A, R, N, D, C, Q, E, G, H, I, L, K, M, F, P, S, T,
W, Y, V$\}$},~ where each character represents an {\em amino acid}.
To translate RNA into protein, ribonucleotides are grouped into
triplets, called {\em codons}, such as $aug$, $acg$, $ggu$,
$\ldots$\footnote{
%
This grouping is analogous to the grouping of {\em bits}\/ into {\em
bytes\/} in computers.}
%
Each codon is then translated into a single amino-acid.  Different
codons may have the same translation.  For example, the codons $gau$
and $gac$ both translate to {\em aspartic acid}, denoted {\sc D} in
the twenty-letter alphabet.  Thus, the RNA sequence $gaugacuuacac$ is
first grouped into a sequence of four codons, $gau/gac/uua/cac$, and
then translated into a sequence of four amino acids, {\sc
DDLH}.\footnote{
%
For simplicity, this example ignores biological complications such as
reading frames, ribosomal binding sites, and stop
codons~\cite{watson}.}

The transformation of DNA into the corresponding protein is easily and
naturally expressed using a {\Tname} program. Given a relation,
$dna\_seq$, containing DNA sequences, the following {\Tname} program
associates a protein with each sequence.
%
\begin{center}
\begin{math}
\begin{array}{rcl}
        rna\_seq(D,\ST_{transcribe}(D)) & \IFT & dna\_seq(D). \\
        protein\_seq(D,\ST_{translate}(R))  & \IFT & rna\_seq(D,R).
\end{array}
\end{math}
\end{center}
%
The program implements a simple serial network which transforms DNA
into RNA, and then RNA into protein.  It uses two sequence
transducers: (i) $\ST_{transcribe}$, in which the input is a DNA
sequence, and the output is a RNA sequence; (ii) $\ST_{translate}$, in
which the input is a RNA sequence, and the output is a protein
sequence.  Intuitively, the predicate $rna\_seq(D,R)$ means that $D$ is
a DNA sequence, and $R$ is the corresponding RNA sequence.  Likewise,
the predicate $protein\_seq(D,P)$ means that $D$ is a DNA sequence,
and $P$ is the corresponding protein sequence.

Although the {\Tname} program consists of only two rules, two features
are worth noting: $(i)$ all sequence restructurings performed by the
program take place ``inside'' the transducers; and $(ii)$ the program
terminates for every database, since there is no recursion through
construction of new sequences.

\end{example}



%%%%%%%%%%  EQUIVALENCE  %%%%%%%%%%%

\subsection{Equivalence to {\name}}
\label{sec:equiv}

Since {\Tname} has more machinery than {\name}, it might appear to be
a more powerful language.  However, this is not the case since every
{\Tname} program can be simulated by a {\name} program.
Example~\ref{es:transcribe} below illustrates a special case of this,
and Theorem~\ref{th:equivalence} proves the result in general.


\begin{example} {\bf [Simulating Transducers]}~
\label{es:transducer}
The {\name} program below simulates the first {\Tname} rule in
Example~\ref{es:transcribe}:
%
\begin{mathlines}{rcl}
rna\_seq(D,R) & \IF & dna\_seq(D), \\
            &       & transcribe(D,R). \medskip\\

transcribe(\e,\e)   & \IF & true. \\

transcribe(D\sdue{1}{N+1},\,R \conc T) & \IF & dna\_seq(D), \\
                                       &       & transcribe(D\sdue{1}{N},R), \\
                                       &       & trans(D[N+1],T). \medskip\\

trans(a,u)  & \IF & true. \\
trans(t,a)  & \IF & true. \\
trans(c,g)  & \IF & true. \\
trans(g,c)  & \IF & true.
\end{mathlines}
%
The first rule transcribes every DNA sequence in the relation
$dna\_seq$ into an RNA sequence, by invoking the predicate
$transcribe$.  The formula $transcribe(D,R)$ is true iff $D$ is a
prefix of a DNA sequence in the database and $R$ is the RNA
transcription of $D$.  The two rules defining this predicate simulate
the transducer $\ST_{transcribe}$ in Example \ref{es:transcribe}.  The
second rule initiates the simulation, and the third rule carries it
out, by recursively scanning each DNA sequence while constructing an
RNA sequence.  For each character in a DNA sequence, its
transcription, $T$, is concatenated to the growing RNA sequence.  The
last four rules specify the transcription of individual
characters. $i.e.$, The formula $trans(d,r)$ means that $d$ is a
character in the DNA alphabet, and $r$ is its transcription in the RNA
alphabet.
%
\end{example}



\begin{theorem} \label{th:equivalence}
For any {\Tname} program $\prog_{td}$, there is a {\name} program
$\prog_{sd}$ that expresses the same queries.  That is, for every
database $\inst$, and every predicate $p(X_1,\ldots,X_m)$ mentioned in
$\prog_{td}\cup\inst$,
\[
        p(\sigma_1,\ldots,\sigma_m) ~\in~
        T_{\prog_{sd},\inst} \uparrow \omega
        ~~~~~~{\it iff}~~~~~~
        p(\sigma_1,\ldots,\sigma_m) ~\in~
        T_{\prog_{td},\inst} \uparrow \omega
\]
Moreover, $\prog_{sd}$ has a finite semantics over $\inst$ if and only
if $\prog_{td}$ does.  (So $\prog_{sd}$ preserves finiteness.)
\end{theorem}


\begin{Proof}
For each transducer mentioned in $\prog_{td}$, we will construct a set
of rules for $\prog_{sd}$ that simulate the transducer's computations.
As a side effect, the simulation may create sequences that
$\prog_{td}$ does not create.  Thus, the minimal models of
$\prog_{td}$ and $\prog_{sd}$ may not have the same extended active
domain.  We shall therefore assume that $\prog_{td}$ is guarded, since
guarded programs are insensitive to differences in domain.  By
Theorem~\ref{th:guarded} in Appendix~\ref{app:guarded}, this
assumption does not result in any loss of generality.

To preserve finiteness, our construction has the following property:
$\prog_{sd}$ simulates a transducer on input
$\sigma_1,\ldots,\sigma_m$ if and only if $\prog_{td}$ invokes the
transducer on this input.  Intuitively, this property means that
$\prog_{sd}$ creates new sequences only when $\prog_{td}$ does.  To
see how finiteness is preserved, recall that $\prog_{td}$ creates new
sequences only by invoking transducers and adding the transducer
output to the active domain.  Each transducer invocation thus adds at
most {\it one\/} new sequence to the active domain.  In contrast, when
$\prog_{sd}$ simulates the computation of a transducer, $\ST$, it
creates not just the {\it final\/} output sequence, but all {\it
intermediate\/} output sequences as well.  It also simulates the
computations of any subtransducers invoked by $\ST$, and creates all
their output sequences.  Thus, each transducer simulation in
$\prog_{sd}$ may add {\it many\/} new sequences to the active domain.
However, because generalized transducers always terminate, they
produce only a finite number of intermediate outputs.  Thus, for each
sequence created by $\prog_{td}$, a finite number of sequences are
created by $\prog_{sd}$.  Thus, if $\prog_{td}$ creates a finite
number of new sequences, then so does $\prog_{sd}$.  In this way, the
construction preserves finiteness.

The construction itself has several steps.  In the first step, each
rule in $\prog_{td}$ is modified and copied into $\prog_{sd}$.  In
modifying a rule, we replace each transducer term,
$\ST(\sterm{1},\ldots,\sterm{m})$, by a new predicate
$p_{\ST}(\sterm{1},\ldots,\sterm{m},X)$.  Intuitively, this predicate
means that $X$ is the output of transducer $\ST$ on inputs
$\sterm{1},\ldots,\sterm{m}$.  For example, if a rule has a single
transducer term, then it has the following form:
\[
        \cl{}:~ p(\dots,\ST(\sterm{1},\ldots,\sterm{m}),\ldots)
                ~\IFT~ \body(\cl{}).
\]
For each such rule in $\prog_{td}$, we add the following rule to
$\prog_{sd}$:
\[
        \cl{}':~ p(\dots,X,\ldots) ~\IF~
                 \body(\cl{}),~p_{\ST}(\sterm{1},\ldots,\sterm{m},X).
\]
where $X$ is a variable that does not appear in $\gamma$.  This idea
is easily generalized to rules with multiple transducer terms.  If a
rule in $\prog_{td}$ has $k$ transducer terms, involving transducers
$\ST_1,\ldots\ST_k$, then we transform it into a rule whose body
invokes the predicates $p_{\ST_1},\ldots,p_{\ST_k}$.

The main step in our construction is defining the predicate $p_{\ST}$
for any generalized transducer $\ST$.  In doing so, we take care to
preserve finiteness.  In particular, we ensure that
$p_{\ST}(\sigma_1,\ldots,\sigma_m,x)$ is true only if program
$\prog_{td}$ invokes transducer $\ST$ on input
$\sigma_1,\ldots,\sigma_n$.  We do this by defining a predicate called
$input_{\ST}$ that specifies the set of input tuples for $\ST$.  This
predicate is easily defined.  If the function term
$\ST(\sterm{1},\ldots,\sterm{m})$ occurs in rule $\cl{}$ in
$\prog_{td}$, then we add the following rule to $\prog_{sd}$:
\[
        \cl{}'':~
          input_{\ST}(\sterm{1}\conc\inizio,\ldots,\sterm{m}\conc\inizio)
                ~\IF~ \body(\cl{}).
\]
We do this for each occurrence of $\ST$ in each rule in $\prog_{td}$.
Note that rule~$\cl{}''$ appends an end-of-tape marker to the end of
each input sequence.  The model of generalized transducers developed
in Section~\ref{sec:seqtrans:model} assumes that such markers appear
at the end of every input tape.  In the worst case, appending these
markers could double the number of sequences in the active domain; so
finiteness is still preserved.

To define the predicate $p_{\ST}$, we write a set of rules in {\name}
that simulate the computations of transducer $\ST$ on every sequence
tuple in $input_{\ST}$.  We first construct rules for base
transducers, and then extend the construction to higher-order
transducers.


\paragraph{\it Base Transducers.}~
For simplicity, let $\ST$ be a base transducer with two inputs and one
output.  (The proof can be easily generalized to any number of inputs
and outputs.)  We encode the transition function of $\ST$ with the
following database predicate:

\begin{center}
\it     $delta_{\ST}$(state, input$_1$, input$_2$,
                      next$\_$state, move$_1$, move$_2$, output)
\end{center}

\noindent
Here, $state$ is the state of the finite control, $input_1$ and
$input_2$ are the symbols scanned by the two input heads,
$next\_state$ is the next state of the finite control, $move_1$ and
$move_2$ describe the motion of the input heads, and $output$ is the
symbol appended to the output sequence.  Given this encoding, the
rules below define the predicate $p_{\ST}(X,Y,Z)$, which means that
$Z$ is the output of transducer $\ST$ on input $X$ and $Y$.  This
predicate is evaluated for every pair of input sequences in the
predicate $input_{\ST}(X,Y)$.  $P_{\ST}$ is defined in terms of the
more general predicate $comp_{\ST}$, which represents a partial
computation of transducer $\ST$.  Intuitively, $comp_{\ST}(X,Y,Z,Q)$
means that after consuming inputs $X$ and $Y$, the output is $Z$ and
the control state is $Q$.

\begin{small}
\begin{mathlines}{rrcl}
\cl{1}: & p_{\ST}(X,Y,Z) &  \IF & input_{\ST}(X,Y,Z), \\
        &  &  & comp_{\ST}(X,Y,Z,Q). \smallskip\\

\cl{2}: & comp_{\ST}(\e,\e,\e,q_0) &  \IF & true. \smallskip\\

\cl{3}: & comp_{\ST}(X\sdue{1}{N_1+1},Y\sdue{1}{N_2+1},Z\conc O,Q')
        & \IF & input_{\ST}(X,Y), \\
        &  &  & comp_{\ST}(X\sdue{1}{N_1},Y\sdue{1}{N_2},Z,Q), \\
        &  &  & delta_{\ST}(Q,X\suno{N_1+1},Y\suno{N_2+1},Q',\move,\move,O).
             \smallskip\\

\cl{4}: & comp_{\ST}(X\sdue{1}{N_1},Y\sdue{1}{N_2+1},Z\conc O,Q')
        & \IF & input_{\ST}(X,Y), \\
        &  &  & comp_{\ST}(X\sdue{1}{N_1},Y\sdue{1}{N_2},Z,Q), \\
        &  &  & delta_{\ST}(Q,X\suno{N_1+1},Y\suno{N_2+1},Q',\stay,\move,O).
               \smallskip\\

\cl{5}: & comp_{\ST}(X\sdue{1}{N_1+1},Y\sdue{1}{N_2},Z\conc O,Q')
        & \IF & input_{\ST}(X,Y), \\
        &  &  & comp_{\ST}(X\sdue{1}{N_1},Y\sdue{1}{N_2},Z,Q), \\
        &  &  & delta_{\ST}(Q,X\suno{N_1+1},Y\suno{N_2+1},Q',\move,\stay,O).
\end{mathlines}
\end{small}
%
Rule $\cl{2}$ initiates a simulation of transducer $\ST$.  It says
that when no input has been consumed, the output is empty and the
finite control is in the initial state, $q_0$.  Rules $\cl{3}$,
$\cl{4}$ and $\cl{5}$ then simulate the transition of the machine from
one state to the next.  The three rules simulate three different
combinations of tape-head movements.  Rule $\cl{3}$ simulates the
movement of both tape heads, while rules $\cl{4}$ and $\cl{5}$
simulate the movement of just one tape head.  In these rules, the
sequence terms $X\sdue{1}{N_1}$ and $Y\sdue{1}{N_2}$ represent the
portions of the input sequences consumed so far; and the terms
$X\suno{N_1+1}$ and $Y\suno{N_2+1}$ represent the input symbols
currently being scanned by the tape heads.


\paragraph{\it Higher-Order Transducers.}
Given rules for simulating transducers of order $k-1$, it is not
difficult to write rules for simulating transducers of order $k$.  We
illustrate the idea on a simple example, one that brings out all the
essential elements of the general construction.  Let $\ST'$ be a
transducer of order 2 with one input and one output.  We encode the
transition function of $\ST'$ in the following database predicate:
%
\begin{center}
\it     $delta_{\ST'}$(state, input, next$\_$state, move, output)
\end{center}
%
Here, {\it state\/} is the state of the finite control, {\it input\/}
is the symbol scanned by the input head, {\it next$\_$state\/} is the
next state of the finite control, and {\it move\/} describes the
motion of the input head.  $output$ is a tape symbol or the name of a
subtransducer: in the former case, the symbol is appended to the
output sequence; in the later case, the subtransducer is executed.
Given this encoding, the rules below define the predicate
$p_{\ST'}(X,Y)$, which means that $Y$ is the output of transducer
$\ST'$ on input $X$.  This predicate is evaluated for every input
sequence in the predicate $input_{\ST'}(X)$.
%
\begin{mathlines}{rrcl}
\cl{1}': & p_{\ST'}(X,Y) &  \IF & input_{\ST'}(X), \\
         &  &  & comp_{\ST'}(X,Y,Q). \smallskip\\

\cl{2}': & comp_{\ST'}(\e,\e,q_0) &  \IF & true. \smallskip\\

\cl{3}': & comp_{\ST'}(X\sdue{1}{N+1},Y\conc O,Q') &  \IF & input_{\ST'}(X), \\
         &  &  & comp_{\ST'}(X\sdue{1}{N},Y,Q), \\
         &  &  & delta_{\ST'}(Q,X\suno{N+1},Q',\move,O). \smallskip\\
\end{mathlines}
%
In addition, for each subtransducer $\ST$ invoked by $\ST'$, we
construct the following two rules:
%
\begin{mathlines}{rrcl}
\cl{4}': & comp_{\ST'}(X\sdue{1}{N+1},Z,Q') &  \IF & input_{\ST'}(X), \\
         &  &  & comp_{\ST'}(X\sdue{1}{N},Y,Q), \\
         &  &  & delta_{\ST'}(Q,X\suno{N+1},Q',\move,\mbox{{\sc t}}), \\
         &  &  & p_{\ST}(X,Y,Z). \smallskip\\

\cl{5}': & input_{\ST}(X\conc\inizio,Y\conc\inizio) & \IF & input_{\ST'}(X), \\
         &  &  & comp_{\ST'}(X\sdue{1}{N},Y,Q), \\
         &  &  & delta_{\ST'}(Q,X\suno{N+1},Q',\move,\mbox{{\sc t}}).
\end{mathlines}
%
As before, $p_{\ST'}$ is defined in terms of the more general predicate
$comp_{\ST'}$.  Intuitively, atoms of the form $comp_{\ST'}(X,Y,Q)$
mean that after consuming input $X$, the output of $\ST'$ is $Y$ and
the finite control is in state $Q$.  As before, rule~$\cl{2}'$ initiates
a simulation of transducer $\ST'$, and rule~$\cl{3}'$ simulates basic
state transitions, in which a symbol is appended to the output.
Rules~$\cl{4}'$ and ~$\cl{5}'$ are new.  Rule~$\cl{4}'$ simulates state
transitions involving the subtransducer $\ST$ (denoted {\sc t} in the
predicate $delta_{\ST'}$).  The body of the rule invokes the
subtransducer via the predicate $p_{\ST}(X,Y,Z)$.  The subtransducer has
{\it two\/} input sequences.  One is $X$, the initial input to $\ST'$,
and the other is $Y$, the current output of $\ST'$.  After the
subtransducer has executed, its output, $Z$, becomes the new output of
$\ST'$.  The actual simulation of the subtransducer is carried out by
rules~$\cl{1}$--$\cl{5}$.  For the simulation to work, the input tuples
for $\ST$ must be specified in the predicate $input_{\ST}(X)$. This is
done by rule~$\cl{5}'$.
%
\end{Proof}


\begin{corollary} \label{cor:equivalence} {\bf (Equivalence)}
{\Tname} and {\name} are expressively equivalent; $i.e.$, every
database query expressible in {\Tname} can be expressed in {\name},
and vice-versa.  Moreover, the equivalence preserves finiteness;
$i.e.$, if a program in {\Tname} has finite semantics, then the
equivalent program in {\name} has finite semantics too, and
vice-versa.
\end{corollary}

\begin{Proof}
One direction is proved by Theorem~\ref{th:equivalence}.  In the other
direction, given a {\name} program, we construct an equivalent
{\Tname} program by simply replacing each constructive sequence term,
$S_1 \conc S_2$, by the transducer term $\ST_{\it append}(S_1,S_2)$,
as described in Section~\ref{sec:td:syntax}.  This transformation
clearly preserves finiteness, since it produces a program with exactly
the same least fixpoint.
\end{Proof}


Theorem~\ref{th:equivalence} shows that the introduction of
transducers into {\name} does not increase the expressive power of the
logic.  However, transducers do provide a framework for defining
natural syntactic restrictions that guarantee safety and finiteness
while preserving much of the expressive power of the full logic, as
the next section shows.




%%%%%%%%%%  STRONGLY SAFE T-DATALOG  %%%%%%%%%%%%%

\section{A Safe Query Language for Sequences}
\label{sec:safetd}

This section develops syntactic restrictions that define a sublanguage
of {\Tname}, called {\em \Ssafe\ \Tname}, that has finite semantics
{\it and\/} is highly expressive.  The restrictions limit the creation
of new sequences by forbidding recursion through transducer terms,
just as object query languages sometimes forbid recursion through
object creation~\cite{AbKa89}.  Intuitively, this ensures that the
transducer network corresponding to a program is acyclic.  The
syntactic restrictions are defined in terms of predicate dependency
graphs. These graphs represent dependencies between predicates in rule
heads and rule bodies.  To keep the development simple, we assume that
all programs are guarded.  By Theorem~\ref{th:guarded} in
Appendix~\ref{app:guarded}, this assumption does not result in any
loss of expressibility.


\begin{definition} ~{\bf (Dependent Predicates)}~
Let $P$ be a {\Tname} program.  A predicate symbol $p$ {\em depends}
on predicate symbol $q$ in program $P$ if for some rule in $P$, $p$ is
the predicate symbol in the head and $q$ is a predicate symbol in the
body.  If the rule is constructive, then $p$ {\em depends
constructively} on $q$.
\end{definition}


\begin{definition} ~{\bf (Dependency Graph)}~
Let $P$ be a {\Tname} program.  The predicate dependency graph of $P$
is a directed graph whose nodes are the predicate symbols in $P$.
There is an edge from $p$ to $q$ in the graph if $p$ depends on $q$ in
program $P$.  The edge is {\em constructive} if $p$ depends
constructively on $q$.  A {\em constructive cycle} is a cycle in the
graph containing a constructive edge.
\end{definition}


\begin{definition} ~{\bf (Strongly-Safe Programs)}~
A {\Tname} program is {\em \ssafe} if its predicate dependency graph
does not contain any constructive cycles.
\end{definition}


The program in Example~\ref{es:transcribe} is {\ssafe} since it is
non-recursive, and thus its dependency graphs contain no cycles.  In
the following example, all the programs are recursive, and one of them
is {\ssafe}.


\begin{figure}
\begin{center}
%\framebox{\input{pdg.pic}}
\framebox{
%TexCad Options
%\grade{\on}
%\emlines{\off}
%\beziermacro{\off}
%\reduce{\on}
%\snapping{\off}
%\quality{2.00}
%\graddiff{0.01}
%\snapasp{1}
%\zoom{1.00}
\unitlength 1.00mm
\linethickness{0.4pt}
\begin{picture}(141.67,84.67)
\put(77.00,17.00){\circle{10.00}}
\put(127.00,17.00){\circle{10.00}}
\put(97.00,37.00){\circle{10.00}}
\put(80.00,21.00){\vector(1,1){13.00}}
\put(101.00,34.00){\vector(3,-2){22.00}}
\put(122.00,14.00){\vector(-1,0){41.00}}
\put(20.00,20.00){\circle{10.00}}
\put(21.00,49.00){\circle{10.00}}
\put(71.00,49.00){\circle{10.00}}
\put(41.00,69.00){\circle{10.00}}
\put(45.00,66.00){\vector(3,-2){22.00}}
\put(66.00,46.00){\vector(-1,0){41.00}}
\put(105.00,66.00){\circle{10.00}}
\put(100.00,68.00){\vector(-1,0){54.00}}
\put(37.00,66.00){\vector(-1,-1){13.00}}
\put(41.00,69.00){\makebox(0,0)[cc]{$r$}}
\put(21.00,49.00){\makebox(0,0)[cc]{$p$}}
\put(71.00,49.00){\makebox(0,0)[cc]{$q$}}
\put(26.00,50.00){\vector(1,0){40.00}}
\put(105.00,66.00){\makebox(0,0)[cc]{$a$}}
\put(68.00,72.00){\makebox(0,0)[cc]{$\ST_1,\ST_2$}}
\put(20.00,20.00){\makebox(0,0)[cc]{$p$}}
\put(24.47,30.52){\makebox(0,0)[cc]{$\ST$}}
\put(77.00,17.00){\makebox(0,0)[cc]{$p$}}
\put(97.00,37.00){\makebox(0,0)[cc]{$r$}}
\put(127.00,17.00){\makebox(0,0)[cc]{$q$}}
\put(82.00,30.00){\makebox(0,0)[cc]{$\ST$}}
\put(4.67,84.67){\makebox(0,0)[cc]{ }}
\put(141.67,84.67){\makebox(0,0)[cc]{ }}
\put(10.00,69.00){\makebox(0,0)[cc]{$P_1:$}}
\put(10.00,39.00){\makebox(0,0)[cc]{$P_2:$}}
\put(75.00,38.00){\makebox(0,0)[cc]{$P_3:$}}
%\emline(15.00,20.01)(11.87,20.01)
\put(15.00,20.01){\line(-1,0){3.13}}
%\end
\put(11.87,21.17){\oval(2.33,2.33)[lb]}
%\emline(10.70,21.08)(10.70,27.25)
\put(10.70,21.08){\line(0,1){6.17}}
%\end
\put(11.62,27.16){\oval(1.83,3.04)[lt]}
%\emline(11.69,28.69)(19.25,28.69)
\put(11.69,28.69){\line(1,0){7.56}}
%\end
\put(19.38,27.66){\oval(1.70,2.06)[rt]}
%\vector(20.23,27.61)(20.23,25.06)
\put(20.23,25.06){\vector(0,-1){0.2}}
\put(20.23,27.61){\line(0,-1){2.55}}
%\end
\end{picture}
}
\end{center}
%
\caption{Predicate dependency graphs}
\label{fig:pdg}
\it
\begin{quotation}
\begin{center}
\noindent
These three graphs correspond to the three programs
in Example~\ref{es:ssafe}.  Constructive edges are labeled by transducer
names.
\end{center}
\end{quotation}
%
\end{figure}

\begin{example}
\label{es:ssafe}
Consider the following three {\Tname} programs, $\prog_1$, $\prog_2$
and $\prog_3$:
%
\begin{center}
\begin{math}
\begin{array}{rl}
\prog_1: & \left\{ \begin{array}{rcl}
        p(X) & \IFT & r(X,Y),~q(Y). \\ q(X) & \IFT & r(X,Y),~p(Y). \\
r(\ST_1(X),\ST_2(Y)) & \IFT & a(X,Y). \\ \end{array} \right. \\ ~\\
\prog_2: & \left\{ \begin{array}{rcl}
        p(\ST(X)) & \IFT & p(X).  \end{array} \right. \\ ~\\
\prog_3: & \left\{ \begin{array}{rcl}
        q(X) & \IFT & r(X). \\ r(\ST(X)) & \IFT & p(X). \\ p(X) & \IFT
& q(X).  \end{array} \right.
\end{array}
\end{math}
\end{center}
%
All three programs are recursive, so their predicate dependency graphs
all have cycles.  (See Figure~\ref{fig:pdg}.)  The graphs of $\prog_2$
and $\prog_3$ have constructive cycles, while the graph of $\prog_1$
does not.  Thus, $\prog_1$ is {\ssafe}, while $\prog_2$ and $\prog_3$
are not.
\end{example}


Intuitively, {\ssafe} programs are stratified with respect to sequence
construction.  Thus, each new sequence generated by a {\ssafe} program
is the result of a fixed number of constructive operations; $i.e.$,
the number of constructive operations is independent of the database.
This idea is developed more precisely in the proof of
Theorem~\ref{th:ssafe1}.  It was also discussed informally at the end
of Section~\ref{sec:finite} in the context of Sequence Datalog.
There, it was seen that stratification limits the ability of Sequence
Datalog to express some simple sequence restructurings.  Not so for
Transducer Datalog, as we shall soon see.



\subsection{Finiteness of {\Ssafe} Programs}

Because {\ssafe} programs are acyclic wrt transducer calls, their
semantics is finite; that is, they have a finite minimal model for
every database.  We prove this result for programs of order $k\leq 3$.
In fact, we establish stronger results than mere finiteness.  By
considering programs of order 2 and order 3 separately, we establish
tight bounds on the size of their minimal models.  The proofs can be
extended to higher-order programs~\cite{Mecc96,BoMe97DBPL}.


\begin{definition} ~{\bf (Database Size)}~
The {\em size} of a database (or a finite interpretation) is the
number of sequences in its extended active domain.
\end{definition}


Theorem~\ref{th:ssafe1} below shows that for programs of order 2, the
size of the minimal model is polynomial in the database size.  The
intuition behind the proof is simple.  Since the program is {\ssafe},
there is no recursion through transducer terms.  The program can
therefore be stratified into constructive and non-constructive layers,
where recursion occurs only within non-constructive layers.  Bottom-up
evaluation of the program then takes place is a standard way: first
the rules in the bottom layer are applied repeatedly until saturation,
$i.e.$, until no more facts are inferred; then the rules in the second
layer are applied until saturation; then the third layer, etc.  There
are two important points about this evaluation: $(i)$ the extended
active domain expands only when constructive layers are evaluated; and
$(ii)$ the rules in a constructive layer only need to be applied once.
The first point follows trivially because non-constructive layers do
not construct new sequences.  The second point follows because a
constructive layer does not contain rules that depend on each other.
(When one constructive rule depends on another, the rules can be put
into different layers.)  Consequently, for programs of order 2,
evaluating a constructive layer increases the size of the extended
active domain by at most a polynomial, as shown below.  Thus, during
bottom-up evaluation of a program, the extended active domain
undergoes a constant number of polynomial expansions, one for each
constructive layer.  The total expansion is therefore polynomial.  The
details of this argument are spelled out in the proof of
Theorem~\ref{th:ssafe1}.  An essential detail of the proof is showing
that as the extended active domain expands, rules in lower layers do
not have to be re-evaluated, $i.e.$, they do not have to be applied to
new sequences created in higher layers.


\begin{theorem} \label{th:ssafe1}
Let $\prog$ be a {\Tname} program that is {\ssafe} and of order 2.
For any database $\inst$, the size of the minimal model of $\prog$ and
$\inst$ is polynomial in the size of $\inst$.
\end{theorem}


\begin{Proof}
Without loss of generality, we can assume that transducer terms in
$\prog$ are not nested.  Thus, $\prog$ does not contain rules such as
\,$p(\ST_1(\ST_2(X))) \leftarrow q(X)$.  Instead, such rules can be
decomposed into simpler ones, such as the following:
\[
        p(\ST_1(Y)) \leftarrow r(Y) ~~~~~~~~~~~~~~~
        r(\ST_2(X)) \leftarrow q(X)
\]
where $r$ is a new predicate symbol.  This decomposition can only {\it
increase\/} the extended active domain of the minimal model.  In this
example, both the original rule and the decomposed rules contribute
ground instances of $\ST_1(\ST_2(X))$ to the extended active domain,
while the decomposed rules also contribute ground instances of
$\ST_2(X)$.  We can therefore assume that all transducer terms in
$\prog$ have the form $\ST(\sterm{1},\ldots,\sterm{m})$ where each
$\sterm{i}$ is a non-constructive sequence term.

The rest of the proof is based on the strongly connected components of
the predicate dependency graph of $\prog$.  Recall that any two nodes
in a strongly connected component have a cycle passing through them.
If a node in the graph belongs to no cycle, then the node is treated
as a singleton component.  By hypothesis, the predicate dependency
graph of $\prog$ has no constructive cycles.  Constructive edges thus
occur only between different components.

For any graph, the relation {\em ``there is an arc from component i to
component j''}\, is finite and acyclic.  We can therefore linearize
the components by a topological sort.  That is, if there are $k$
strongly connected components in a graph, then we can assign a
distinct integer \,$i \in \{1,\ldots,k\}$\, to each component in such
a way that there is an arc from component $i$ to component $j$ \,iff\,
$i < j$.  Let us denote the linearized components by
$\nodi_1,\ldots,\nodi_k$.  The linearization induces a {\it
stratification\/} on the program $\prog$, where the $i^{th}$ stratum
consists of those rules in $\prog$ that define predicates in
$\nodi_i$.  Let $\prog_i$ denote the $i^{th}$ stratum of $\prog$.
Observe that the $\prog_i$ are disjoint, and $\prog =
\prog_1\cup\prog_2\cup\cdots\cup\prog_k$.

Because {\Tname} has a fixpoint semantics based on a monotonic and
continuous T-operator, the exact order in which rules are applied does
not matter.  Any order will converge to the least model of $\prog$ and
$\inst$, so long as the rules are applied until the extent of each
predicate stops growing, just as in classical Datalog and Horn logic
programming.  In addition, because $\prog$ is guarded, the extent of a
predicate defined in $\prog_i$ depends only on the rules in
$\prog_1\cup\cdots\cup\prog_i$.  We can therefore apply the rules in a
bottom-up fashion, one stratum at a time.  That is, we can first apply
the rules in $\prog_1$ to saturation, then the rules in $\prog_2$,
then those in $\prog_3$, etc.  Formally, given a database $\inst$, we
define a sequence of minimal models
$\model{1},\ldots,\model{k},\,\model{k+1}$ as follows:
%
\begin{mathlines}{rcll}
          \model{1} & = & \inst \\
        \model{i+1} & = & T_{\prog_i,\model{i}} \uparrow \omega
                        & ~{\it for}~~ 1 \leq i \leq k
\end{mathlines}
%
$\model{i+1}$ is the minimal model of $\prog_i$ and $\model{i}$.  Once
$\model{i+1}$ has been computed, the extent of each predicate defined
in $\prog_1\cup\cdots\cup\prog_i$ is completely materialized.  Thus,
$\model{i+1}$ is also the minimal model of
$\prog_1\cup\cdots\cup\prog_i$ and $\inst$.  In particular,
$\model{k+1}$ is the minimal model of $\prog$ and $\inst$.

The rules in $\prog_i$ are of two types: constructive and
non-constructive.  In a constructive rule, each predicate symbol in
the body is defined at a {\it lower\/} stratum, that is, in
$\prog_1\cup\cdots\cup\prog_{i-1}$.  The extent of these predicates is
completely materialized in $\model{i}$.  In addition, each
constructive rule, like the entire program, is {\it guarded}.  Thus,
each sequence variable can bind only to sequences in $\model{i}$.
Consequently, the constructive rules need only be applied {\it once},
since additional applications will not infer any new atoms.  After
this, the non-constructive rules in $\prog_i$ can be applied
repeatedly until the minimal model of $\prog_i$ and $\model{i}$ is
reached.  Formally, if $\prog_i^c$ and $\prog_i^u$ denote respectively
the constructive and non-constructive rules in $\prog_i$, then%
%
\footnote{In terms of the intuitive argument given just before
Theorem~\ref{th:ssafe1}, $\prog_i^c$ and $\prog_i^u$ are constructive
and non-constructive layers, respectively.}
%
\[
        \model{i+1} ~=~  T_{\prog_i^u,\model{i}'}\uparrow\omega
        ~~~~~{\it where}~~~
        \model{i}' ~=~ T_{\prog_i^c,\model{i}}(\model{i})
\]

Only constructive rules can expand the extended active domain.  Thus,
$\model{i+1}$ and $\model{i}'$ have the same extended active domain,
and all new sequences are created in computing $\model{i}'$ from
$\model{i}$.  We shall show that the size of $\model{i}'$ is at most
polynomial in the size of $\model{i}$.  Let $n_i'$ and $n_i$ denote
these two sizes, respectively.  Also, let $l_i'$ and $l_i$ denote the
maximum lengths of any sequence in the extended active domains of
$\model{i}'$ and $\model{i}$, respectively.  We first derive upper
bounds for $l_i'$ and $n_i'$ in terms of $l_i$ and $n_i$, from which
we derive an upper bound for $n_i'$ in terms of $n_i$.

To bound $l_i'$, observe that $\domact{ext}{\model{i}'}$ consists of
the sequences in $\model{i}$, plus the sequences created by transducer
terms in $\prog_i^c$, plus all their contiguous subsequences.  By
hypothesis, each transducer in $\prog_i^c$ has order at most 2.  By
Theorem~\ref{th:networks}, such transducers create sequences of at
most polynomial length, polynomial in the length of the longest input.
Thus, the longest sequence created by any transducer in $\prog_i^c$ is
polynomial in the length of the longest sequence in $\model{i}$.  Thus
\,$l_i' = l_i^{O(1)}$.

To bound $n_i'$, let $\ST(\sterm{1},\ldots,\sterm{m})$ be a transducer
term in $\prog_i^c$.  As described above, each sequence variable will
bind only to sequences occurring in $\model{i}$.  Each sequence term
$\sterm{i}$ will thus bind only to sequences in
$\domact{ext}{\model{i}}$.  Thus, the number of input tuples to this
transducer term is at most $n_i^m$; so the number of output sequences
is also at most $n_i^m$.  Each output sequence can contribute up to
$O(l_i'^{\,2})$ sequences and subsequences to
$\domact{ext}{\model{i}'}$.  The transducer term thus contributes at
most \,$n_i^m \cdot O(l_i'^{\,2}) \leq n_i^{O(1)} \cdot
l_i'^{\,O(1)}$\, sequences to $\domact{ext}{\model{i}'}$.  This is
true for each transducer term in $\prog_i^c$.  In addition,
$\domact{ext}{\model{i}'}$ contains all the sequences in
$\domact{ext}{\model{i}}$.  Thus, if $\prog_i^c$ has $q$ transducer
terms, then
\[
        n_i' ~~\leq~~ q \cdot n_i^{O(1)} \cdot l_i'^{\,O(1)} + n_i
             ~~=~~ n_i^{O(1)} \cdot l_i'^{\,O(1)}
\]
since $q$ is fixed.  Combining this with the upper bound on $l_i'$, we
get \,$n_i' \leq n_i^{O(1)} l_i^{O(1)}$.

An extended active domain includes all the subsequences of its longest
sequence, of which there are quadratically many.  Thus \,$n_i \geq
O(l_i^2)$~ so ~$l_i \leq O(n_i^{1/2}) \leq n_i^{O(1)}$.  \,Thus
\,$n_i' \leq n_i^{O(1)}$.  \,Each stratum of program $\prog$ thus
increases the size of the minimal model by at most a polynomial.
Thus, since the number of strata is fixed, the size of the minimal
model of $\prog$ and $\inst$ is at most polynomial in the size of
$\inst$.
\end{Proof}


A similar result holds for programs of order 3, as shown in
Theorem~\ref{th:ssafe2} below.  The intuition behind the proof is
similar to that of Theorem~\ref{th:ssafe1}.  The main difference is
that for programs of order 3, the evaluation of a constructive layer
can expand the extended active domain by a hyper-exponential.  Thus,
during bottom-up evaluation of a program, the extended active domain
undergoes a constant number of hyper-exponential expansions, one for
each constructive layer.  The total expansion is therefore
hyper-exponential.


\begin{theorem} \label{th:ssafe2}
Let $\prog$ be a {\Tname} program that is {\ssafe} and of order 3.
For any database $\inst$, the size of the minimal model of $\prog$ and
$\inst$ is hyper-exponential in the size of $\inst$.
\end{theorem}


\begin{Proof}
The proof is similar to that of Theorem~\ref{th:ssafe1}.  In
particular, the following upper bounds are still valid, since they are
independent of the order of the transducers:
\[
        n_i' ~\leq~ n_i^{O(1)} \cdot l_i'^{\,O(1)} ~~~~~~~~~~~~~~~
         l_i ~\leq~ n_i^{O(1)}
\]
When the transducers are of order 3, we get additional bounds.  By
Theorem~\ref{th:networks}, such transducers can generate sequences of
hyper-exponential length.  Thus \,$l_i' \leq \hyp_m(l_i^{O(1)})$\, for
some integer $m$.  Combining all these inequalities, we get the
following upper bound on $n_i'$:
\[
        n_i' ~\leq~ n_i^{O(1)} \cdot \hyp_m(l_i^{O(1)})
             ~\leq~ n_i^{O(1)} \cdot \hyp_m(n_i^{O(1)})
               ~=~  \hyp_m(n_i^{O(1)})
\]

Each stratum of program $\prog$ thus increases the size of the minimal
model by at most a hyper-exponential.  Thus, since the number of
strata is fixed, the size of the minimal model of $\prog$ and $\inst$
is at most hyper-exponential in the size of $\inst$.
\end{Proof}


We can now state the finiteness result for {\ssafe} programs.


\begin{corollary} \label{cor:finiteness}
~{\bf (Finiteness)} ~If a {\Tname} program of order at most 3 is
{\ssafe}, then it has a finite semantics.
\end{corollary}

\begin{Proof}
Follows immediately from Theorems~\ref{th:ssafe1} and~\ref{th:ssafe2},
since a model is finite iff its extended active domain in finite.
\end{Proof}

Using a similar technique, Corollary~\ref{cor:finiteness} can be
extended to higher-order {\Tname} programs~\cite{Mecc96,BoMe97DBPL}.
Thus, any safe program has a finite semantics.



\subsection{Expressibility of {\Ssafe} Programs}

Building on Theorems~\ref{th:ssafe1} and~\ref{th:ssafe2}, this section
establishes expressibility results for {\ssafe} programs.


\begin{corollary} \label{cor:expressibilitytd2}
{\Ssafe\ \Tname} programs of order $2$ express exactly the class of
sequence functions computable in {\sc ptime}.
\end{corollary}

\begin{Proof}
It is not hard to show that the computation of any acyclic network of
transducers of order $k$ can be simulated by a {\Ssafe\ \Tname}
program of order $k$.  When $k=2$, these programs can express any
sequence function in {\sc ptime}, by Theorem~\ref{th:expressibility1}.
This proves the lower expressibility bound.

To prove the upper bound, let $\inst$ be a database, and let $\prog$
be a {\Ssafe\ \Tname} program of order 2.  Theorem~\ref{th:ssafe1}
guarantees that the size of the minimal model \,$\trasfi{}{\omega}$\,
is polynomial in the size of $\inst$.  In general, each application of
the operator $\trasf{}$, except the last, adds at least one new atom
to the minimal model.  Thus, the minimal model is computed after at
most polynomially many applications of $\trasf{}$.  Moreover, each
application of $\trasf{}$ takes polynomial time, since the input and
output are of polynomial size, and each ground instance of each
transducer term can be evaluated in polynomial time, since the
transducers are of order 2.  The entire fixpoint computation thus
takes at most polynomial time, polynomial in the size of $\inst$.
This is true for any database, $\inst$.

Since $\prog$ computes a sequence function, $\inst$ contains just a
single atom, $in(\sigma)$, where $\sigma$ is the input sequence for
the function.  The size of $\inst$ is the number of sequences in its
extended active domain.  In this case, the size is just the number of
subsequences of $\sigma$, that is, $O(n^2)$ where $n$ is the length of
$\sigma$.  Thus, the minimal model can be computed in time that is
polynomial in $n^2$, and thus polynomial in $n$.
\end{Proof}


\begin{corollary} \label{cor:expressibilitytd3}
{\Ssafe\ \Tname} programs of order $3$ express exactly the class of
elementary sequence functions.
\end{corollary}

\begin{Proof}
Similar to the proof of Corollary~\ref{cor:expressibilitytd2}.  In
this case, by Theorem~\ref{th:ssafe2} and Theorem~\ref{th:networks},
the size of the minimal model and the running time of each transducer
are hyper-exponential.  This yields the upper bound.
\end{Proof}



%%%%%%%%%%%%%  APPENDIX  %%%%%%%%%%%%%%

\appendix

%%%%%%%%%%%%%%% MODEL THEORETIC SEMANTICS %%%%%%%%%%%%%%%%%%%%

\section{Appendix: Model Theory}
\label{app:model}

In this section we develop a model-theoretic semantics for {\name}
programs, and show that it is equivalent to the fixpoint semantics
developed in Section~\ref{sec:fix}.  Our notion of {\it model\/} is
similar to the classical notion except that we restrict our attention
to substitutions based on the extended active domain.


\begin{definition}[Models]
An interpretation \(\interp\) is a {\em model\/} of a clause
\(\cl{}\), written $\interp \models \cl{}$, iff the following is true
for each substitution \(\subs{}\) based on $\domact{ext}{\interp}$ and
defined at $\cl{}$:
\[
        {\it if}~~~ \subs{}(\body(\cl{})) \subseteq \interp
        ~~~{\it then}~~~ \subs{}(\head(\cl{})) \in \interp
\]
An interpretation is a model of a {\name} program $\prog$ and a
database $\inst$ if it is a model of each clause in $\prog{} \cup
\inst{}$.
\end{definition}


\begin{definition}[Entailment]
Let $\prog$ be a {\name} program, $\inst$ be a database, and $\alpha$
be a ground atomic formula.  Then, $\prog$ and $\inst$ entail
$\alpha$, written $\prog,\inst \models \alpha$, if and only if every
model of $\prog$ and $\inst$ is also a model of $\alpha$.
\end{definition}


\begin{lemma}
\label{lem-equiv}
Let $\prog$ be a {\name} program, $\inst$ be a database, and $\interp$
be an interpretation.  Then $\interp$ is a model of $\prog$ and
$\inst$ iff it is a fixpoint of $\trasf{}$, ~$i.e.$, ~iff~
$\trasf{}(\interp) \subseteq \interp$.
\end{lemma}

\begin{Proof}
Suppose that $\interp$ is a model of $\prog\cup\inst$.  If \,$\alpha
\in \trasf{}(\interp)$\, then by Definition~\ref{def-T}, \,$\alpha =
\subs{}(\head(\cl{}))$\, for some clause $\cl{}$ in $\prog\cup\inst$,
and some substitution $\subs{}$ based on $\domact{ext}{\interp}$.
Moreover \,$\subs{}(\body(\cl{})) \subseteq \interp$.\, But $\interp$
is a model of $\prog\cup\inst$ by hypothesis, and thus of $\cl{}$.
Hence \,$\subs{}(\head(\cl{})) \in \interp$,\, so \,$\alpha \in
\interp$.\, Thus, any atom in $\trasf{}(\interp)$ is also in
$\interp$, so \,$\trasf{}(\interp) \subseteq \interp$.

In the other direction, suppose that \,$\trasf{}(\interp) \subseteq
\interp$.\, Let $\cl{}$ be any clause in $\prog\cup\inst$, and let
$\subs{}$ be any substitution based on $\domact{ext}{\interp}$ and
defined at $\cl{}$.  If \,$\subs{}(\body(\cl{})) \subseteq \interp$\,
then \,$\subs{}(\head(\cl{})) \in \trasf{}(\interp)$,\, by
Definition~\ref{def-T}.  Thus \,$\subs{}(\head(\cl{})) \in \interp$,\,
since \,$\trasf{}(\interp) \subseteq \interp$\, by hypothesis.  Thus,
since $\subs{}$ is arbitrary, $\interp$ is a model of $\cl{}$.  And,
since $\cl{}$ is arbitrary, $\interp$ is a model of $\prog\cup\inst$.
\end{Proof}


The following corollaries are immediate consequences of
Lemma~\ref{lem-equiv} and the fixpoint theory of
Section~\ref{sec:fix}.  They show that the model-theoretic semantics
and the fixpoint semantics for {\name} are equivalent.


\begin{corollary} \label{cor:models1}
A {\name} program $\prog$ and a database $\inst$ have a unique minimal
model, and it is identical to the least fixpoint of the operator
$\trasf{}$.
\end{corollary}

\begin{corollary} \label{cor:models2}
Let $\prog$ be a {\name} program, $\inst$ be a database, and $\alpha$
be a ground atomic formula.  Then ~$\prog,\inst \models \alpha$~ if
and only if ~$\alpha \in \trasfi{}{\omega}$.
\end{corollary}




\section{Appendix:~ Guarded Programs}
\label{app:guarded}

This appendix uses the fixpoint theory of Section~\ref{sec:fix} and
the model theory of Appendix~\ref{app:model} to prove a basic result
about {\name} and {\Tname}.  This result, which is used in
Theorem~\ref{th:equivalence} and Section~\ref{sec:safetd}, allows us
to assume that programs are guarded.  A program is guarded if all its
clauses are guarded, and a clause is guarded if every sequence
variable in the clause appears in the body of the clause as an
argument of some predicate.  For instance, the clause
\,\mbox{$p(X\suno{1}) \IF q(X)$}\, is guarded, but \,\mbox{$p(X) \IF
q(X\suno{1})$}\, is not.


\begin{theorem} \label{th:guarded}
In {\name} and in {\Tname}, for any program $\prog$, there is guarded
program $\prog^G$ that expresses the same sequence queries.  That is,
for any database $\inst$, and any predicate $p(X_1,\ldots,X_m)$
mentioned in $\prog\cup\inst$,
\[
        \prog,\inst \models p(\sigma_1,\ldots,\sigma_m)
        ~~~~~~{\it iff}~~~~~~
        \prog^G,\inst \models p(\sigma_1,\ldots,\sigma_m)
\]
Moreover, $\prog$ has a finite semantics over $\inst$ if and only if
$\prog^G$ does.
\end{theorem}
%
We shall prove Theorem~\ref{th:guarded} in a series of short lemmas.

The construction of $\prog^G$ is simple.  The first step is to
introduce a new predicate, $dom(X)$.  Intuitively, this predicate
means that $X$ is a sequence in the extended active domain.  Next, for
each clause $\cl{}$ in $\prog$, we add the following guarded clause to
$\prog^G$:
%
\begin{equation} \label{rule:guarded1}
        \head(\cl{}) \leftarrow \body(\cl{}),\,
                dom(X_1),\, dom(X_2), \ldots, dom(X_m).
\end{equation}
%
where $X_1,X_2,\ldots,X_m$ are all the sequence variables in $\cl{}$.

The predicate $dom(X)$ is defined by guarded clauses in $\prog^G$.
First, we add the following clause to $\prog^G$:
%
\begin{equation} \label{rule:guarded2}
        dom(X[M,N]) \leftarrow dom(X)
\end{equation}
%
This clause ensures that for each sequence in the extent of $dom$, all
its subsequences are also there.  Second, if $p(X_1,X_2,\ldots,X_m)$
is a base predicate\footnote{
%
Recall from Section~\ref{sec:preliminary} that the set of base
predicates is fixed and finite.}
%
or a predicate mentioned in $\prog$, then we add the following $m$
clauses to $\prog^G$:
%
\begin{equation} \label{rule:guarded3}
\begin{array}{l}
        dom(X_1) \leftarrow p(X_1,X_2,\ldots,X_m) \\
        dom(X_2) \leftarrow p(X_1,X_2,\ldots,X_m) \\
        ~~~~~~\cdots \\
        dom(X_m) \leftarrow p(X_1,X_2,\ldots,X_m)
\end{array}
\end{equation}

We must now show that $\prog$ and $\prog^G$ express the same queries.
To do this, we introduce two operations on interpretations.
Intuitively, these operations allow us to transform models of $\prog$
into models of $\prog^G$, and vice-versa.  This will allow us to
establish a correspondence between the models of $\prog$ and
$\prog^G$, which is the basis for their expressive equivalence.


\begin{definition}
Let $\interp$ be an interpretation.  $\interp^-$ is an interpretation
constructed from $\interp$ by removing all atoms of the form
$dom(\sigma)$.  $\interp^+$ is an interpretation constructed from
$\interp$ by adding atoms of the form $dom(\sigma)$ for every sequence
$\sigma$ in $\domact{ext}{\interp}$, the extended active domain of
$\interp$.
\end{definition}
%
Observe that $\interp^-$ and $\interp^+$ have the following basic
properties:
%
\begin{itemize}
\item
$\domact{ext}{\interp^-} \subseteq \domact{ext}{\interp}$

\item
$\domact{ext}{\interp^+} = \domact{ext}{\interp}$

\item
$(\interp^+)^- \subseteq \interp$

\item
If ~$\interp_1 \subseteq \interp_2$~
then ~$\interp_1^- \subseteq \interp_2^-$~
and ~$\interp_1^+ \subseteq \interp_2^+$

\end{itemize}
%
The following lemmas establish other properties of these two
operations, properties that lead directly to a proof of
Theorem~\ref{th:guarded}.


\begin{lemma} \label{lem:guarded1}
~$\interp$ is a model of \,$\prog\cup\inst$\, if and only if
$\interp^+$ is a model of \,$\prog^G\cup\inst$.
\end{lemma}

\begin{Proof}
First, let $\cl{}$ be any clause of the form (\ref{rule:guarded2}) or
(\ref{rule:guarded3}), and let $\subs{}$ be any substitution based on
$\domact{ext}{\interp}$ and defined at $\cl{}$.  Then
$\subs{}(\head(\cl{}))$ has the form $dom(\sigma)$, for some sequence
$\sigma$ in $\domact{ext}{\interp}$.  Thus \,$\subs{}(\head(\cl{}))
\in \interp^+$,\, so $\interp^+$ is a model of $\cl{}$.  $\interp^+$
is therefore a model of clauses~(\ref{rule:guarded2})
and~(\ref{rule:guarded3}).

Next, let $\cl{}$ be any clause in $\prog\cup\inst$.  We must show
that $\interp$ is a model of $\cl{}$ if and only if $\interp^+$ is a
model of clause~(\ref{rule:guarded1}).  To see this, note that
\,$\subs{}(dom(X)) \in \interp^+$\, for any sequence variable $X$, and
any substitution $\subs{}$ based on $\domact{ext}{\interp}$.  Thus,
all premises of the form $dom(X)$ in clause~(\ref{rule:guarded1}) are
satisfied in $\interp^+$.
\end{Proof}


\begin{lemma} \label{lem:guarded2}
Suppose $\interp$ is constructed only from predicates mentioned in
$\prog^G\cup\inst$.  If $\interp$ is a model of
\,$\prog^G\cup\inst$,\, then $\interp^-$ is a model of
\,$\prog\cup\inst$.
\end{lemma}

\begin{Proof}
$\interp$ is a model of clauses~(\ref{rule:guarded2})
and~(\ref{rule:guarded3}).  By clauses~(\ref{rule:guarded3}), if
$\sigma$ is a sequence in the active domain of $\interp$, then
$dom(\sigma) \in \interp$.  Thus, by clauses~(\ref{rule:guarded2}), if
$\sigma$ is a sequence in the extended active domain of $\interp$,
then $dom(\sigma) \in \interp$.  Thus, \,$\subs{}(dom(X)) \in
\interp$\, for any sequence variable $X$, and any substitution
$\subs{}$ based on $\domact{ext}{\interp}$.

Let $\cl{}$ be a clause in $\prog\cup\inst$.  We must show that
$\interp^-$ is a model of $\cl{}$.  To see this, note that in
clause~(\ref{rule:guarded1}), all premises of the form $dom(X)$ are
satisfied in $\interp$.  Thus, $\interp$ is a model of
clause~($\ref{rule:guarded1}$) if and only if $\interp^-$ is a model
of $\cl{}$.  But $\interp$ {\it is\/} a model of
clause~($\ref{rule:guarded1}$), since this clause is in $\prog^G$, and
$\interp$ is a model of $\prog^G\cup\inst$ by hypothesis.
\end{Proof}


\begin{lemma} \label{lem:guarded3}
If $\interp$ is the minimal model of \,$\prog^G\cup\inst$,\, then
$\interp^-$ is the minimal model of \,$\prog\cup\inst$, and $\interp$
and $\interp^-$ have the same extended active domain.
\end{lemma}

\begin{Proof}
Since $\interp$ is the minimal model of $\prog^G\cup\inst$, it is
constructed only from predicates mentioned in $\prog^G\cup\inst$.
Thus, $\interp^-$ is a model of $\prog\cup\inst$, by
Lemma~\ref{lem:guarded2}.  Thus, letting $\interp_0$ be the minimal
model of $\prog\cup\inst$, we have
%
\begin{enumerate}
\item
$\interp_0 \subseteq \interp^-$

\item
$\interp \subseteq \interp_0^+$,~ since $\interp_0^+$ is a model of
$\prog^G\cup\inst$, by Lemma~\ref{lem:guarded1}, and $\interp$ is the
minimal model.

\item
$\interp^- \subseteq \interp_0$,~ since \,$\interp^- \subseteq
(\interp_0^+)^-$\, by item 2, and \,$(\interp_0^+)^- \subseteq
\interp_0$\, in general.

\item
$\interp_0 = \interp^-$,~ by items 1 and 3.

\end{enumerate}
%
This proves the first part of the lemma.  To prove the second part,
observe that $\domact{ext}{\interp^-} \subseteq
\domact{ext}{\interp}$.  To prove the reverse containment, note that
$(\interp^-)^+$ is a model of $\prog^G\cup\inst$, by
Lemma~\ref{lem:guarded1}.  Thus \,$\interp \subseteq (\interp^-)^+$\,
since $\interp$ is the minimal model.  Thus \,$\domact{ext}{\interp}
\subseteq \domact{ext}{(\interp^-)^+} = \domact{ext}{\interp^-}$.
\end{Proof}


Theorem~\ref{th:guarded} follows immediately from
Lemma~\ref{lem:guarded3} and Corollaries~\ref{cor:models1}
and~\ref{cor:models2}.


\subsubsection*{Acknowledgements:}

The authors would like to thank several people for their
contributions: Steve Cook, Faith Fich and Charles Rackoff for fruitful
discussions on the use of machines for computing sequence functions;
and Paolo Atzeni and Victor Vianu for numerous comments and
suggestions about the language.  The first author was partially
supported by a research grant from the Natural Sciences and
Engineering Research Council of Canada (NSERC), and the second author
was partially supported by MURST and Consiglio Nazionale delle
Ricerche (CNR).



%%%%%%%%%%%  REFERENCES  %%%%%%%%%%%%%%

\nocite{Bonn90}

\bibliographystyle{plain}
%\bibliography{../pa,../gianni}
\bibliography{latex/gianni}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}
