\chapter[Introduction]{Introduction: Logic and Logic Programming Languages}
{Michael J. O'Donnell}\label{cha:introduction}

\vspace{2ex}
This text is a preprint of Chapter 1 in the {\em Handbook of Logic in
Artificial Intelligence and Logic Programming,} volume 5 on {\em Logic
Programming,} Dov Gabbay editor, Oxford University Press. Jos\'e
Meseguer, Dale Miller, and Edward L.~ Wimmers served as official
readers, and provided useful feedback on drafts of the chapter.

\section{Introduction}

\subsection{Motivation}
{\em Logic}\subind{logic!dictionary definition}, according to
Webster's dictionary \cite{Webster}, is {\em `a science that deals
with the principles and criteria of validity of inference and
demonstration: the science of the formal principles of reasoning.'}
Such {\em `principles and criteria'} are always described in terms of
a {\em language\/} in which inference, demonstration, and reasoning
may be expressed. One of the most useful accomplishments of logic for
mathematics is the design of a particular formal language, the {\em
First Order Predicate Calculus\/} (FOPC). FOPC is so successful at
expressing the assertions arising in mathematical discourse that
mathematicians and computer scientists often identify logic with
classical logic expressed in FOPC. In order to explore a range of
possible uses of logic in the design of programming languages, we
discard the conventional identification of logic with FOPC, and
formalize a general schema for a variety of logical systems, based on
the dictionary meaning of the word. Then, we show how logic
programming languages may be designed systematically for any
sufficiently effective logic, and explain how to view Prolog, Datalog,
$\lambda$Prolog, Equational Logic Programming, and similar programming
languages, as instances of the general schema of logic programming.
Other generalizations of logic programming have been proposed
independently by Meseguer \cite{Meseguer-general}\auind{Meseguer, J.},
Miller, Nadathur, Pfenning and Scedrov
\cite{Miller-Nadathur-Pfenning-Scedrov},
\auind{Miller, D.}\auind{Nadathur, G.}\auind{Pfenning, F.}
\auind{Scedrov, A.}
Goguen and Burstall
\cite{Goguen-Burstall}.\auind{Goguen, J. A.}\auind{Burstall, R. M.}

The purpose of this chapter is to introduce a set of basic concepts
for understanding logic programming, not in terms of its historical
development, but in a systematic way based on retrospective insights.
In order to achieve a systematic treatment, we need to review a number
of elementary definitions from logic and theoretical computer science
and adapt them to the needs of logic programming. The result is a
slightly modified logical notation, which should be recognizable to
those who know the traditional notation. Conventional logical notation
is also extended to new and analogous concepts, designed to make the
similarities and differences between logical relations and
computational relations as transparent as possible. Computational
notation is revised radically to make it look similar to logical
notation. The chapter is self-contained, but it includes references to
the logic and theoretical computer science literature for those who
wish to explore connections.

There are a number of possible motivations for developing, studying,
and using logic programming languages.  Many people are attracted to
Prolog, the best known logic programming language, simply for the
special programming tools based on unification and backtracking search
that it provides.  This chapter is not concerned with the utility of
particular logic programming languages as programming tools, but with
the value of concepts from logic, particularly semantic concepts, in
the design, implementation, and use of programming languages.  In
particular, while denotational and algebraic semantics provide
excellent tools to {\em describe\/} important aspects of programming
systems, and often to prove correctness of implementations, we will
see that logical semantics can exploit the strong traditional
consensus about the meanings of certain logical notations to {\em
prescribe\/} the behavior of programming systems.  Logical semantics
also provides a natural approach, through proof systems, to verifiably
correct implementations, that is sometimes simpler than the
denotational and algebraic approaches.  A comparison of the three
styles of semantics will show that denotational and algebraic
semantics provide {\em descriptive\/} tools, logical semantics
provides {\em prescriptive\/} tools, and the methods of algebraic
semantics may be used to translate logical semantics into
denotational/algebraic semantics.

In this chapter, a relation is called {\em
computable\/}\subind{computable relation} if and only if its
characteristic function is total recursive, and a relation is {\em
semicomputable\/}\subind{semicomputable relation} if and only if the
set of ordered pairs in the relation is recursively enumerable.
Recursion theorists and theoretical computer scientists often refer to
computable sets as {\em decidable\/}\subind{decidable} sets, but
logicians sometimes call a theory {\em decidable\/} when every formula
is either provable or refutable in the theory. The two meanings of
`decidable' are closely connected, but not identical, and we avoid
confusion by choosing a different word. When some component of a
relation is a finite set, the set is assumed to be represented by a
list of its members for the purpose of discussing computability and
semicomputability.

\subsection{A Notational Apology}

In order to understand logic programming rigorously in terms of formal
concepts from mathematical logic, and at the same time intuitively, we
need to look closely at the details of several formal relations from
logic and from theory of computation. We must come to understand the
formal similarities and differences between these relations, and how
those formal properties arise from the intuitive similarities and
differences in our intended applications of these relations.
Unfortunately, the conventional notations for logic and computation
look radically different, and take advantage of different simplifying
assumptions, which obscures those connections that are essential to
intuitive applications of the corresponding concepts. So, we will
make visually small variations on conventional logical notation,
extending it to deal with questions and their answers as well as the
traditional assertions and their semantic interpretations. Then, we
will radically redesign conventional recursion-theoretic notation in
order to display visually the connections between computational
relations and logical relations. In order to be prepared for the
strange look of the notations, we need to review them all briefly in
advance, although the precise definitions for the concepts that they
denote will be introduced gradually through
sections~\ref{sec:specifying}--\ref{sec:implementing}.

The important domains of conventional logical objects for our study
are the sets of
\begin{itemize}
\item logical assertions\subind{assertion}\subind{formula},
  or formulae $\mathbold{F}$\notind{$\mathbold{F}$ (formulae)}
\item sets of formulae, or theories\subind{theory}
  $\mathbold{T}\in\powerset{\mathbold{F}}$\notind{$\mathbold{T}$ (theory)}
\item semantic interpretations\subind{interpretation},
  or models\subind{model} $\mathbold{M}$\notind{$\mathbold{M}$
  (models, interpretations)}
\item sets of models, representing knowledge\subind{knowledge}
  $\mathbold{K}\in\powerset{\mathbold{M}}$\notind{$\mathbold{K}$
  (knowledge, models)}
\item proofs,\subind{proof} or derivations\subind{derivation}
  $\mathbold{D}$\notind{$\mathbold{D}$ (proofs, derivations)}
\end{itemize}
We add the unconventional domain of
\begin{itemize}
\item questions\subind{question}
  $\mathbold{Q}$\notind{$\mathbold{Q}$ (questions)}
\end{itemize}
Answers\subind{answer} to questions are particular formulae, so no
additional domain is required for them. The domains of conventional
computational objects are the sets of
\begin{itemize}
\item programs\subind{program}
  $\mathbold{P}$\notind{$\mathbold{P}$ (programs)}
\item inputs\subind{input} $\mathbold{I}$\notind{$\mathbold{I}$ (inputs)}
\item computations\subind{computation}
  $\mathbold{C}$\notind{$\mathbold{C}$ (computations)}
\item outputs\subind{output} $\mathbold{O}$\notind{$\mathbold{O}$ (outputs)}
\end{itemize}
In recursion-theoretic treatments of computation, programs, inputs,
and outputs are all integers, but our analysis is more convenient when
they are allowed to be different domains.  We will find strong intuitive
analogies and formal connections between
\begin{itemize}
\item programs and sets of formulae
\item inputs and questions
\item computations and proofs
\item outputs and formulae (intended as answers to questions)
\end{itemize}

In order to understand the analogies and formal connections
thoroughly, we must investigate a number of relations between domains
with varying arities from two to four. In all cases, we will use {\em
multiple infix\/} notation.  That is, each $n$-ary relation will be
denoted by $n-1$ symbols separating its arguments. With some care in
the geometrical design of the separator symbols, we get a reasonably
mnemonic notation.

There are two quaternary relational notations from which all the other
notations may be derived. Let $Q$ be a question, $\mathbold{T}$ a set
of formulae, $D$ a proof, and $F$ a formula. The notation
$$Q\answers\mathbold{T}\hypos D\proves
F$$\notind{$\answers\hypos\:\proves$ (quaternary answer relation)}
means that in response to the question $Q$, given the
postulates\subind{postulate} in $\mathbold{T}$, we may discover the
proof $D$ of the answer $F$. Similarly, let $I$ be an input, $P$ a
program, $C$ a computation, and $O$ an output. The notation $$I\inputs
P\computes C\outputs O$$\notind{$\inputs\:\computes\:\outputs$ (quaternary
computation relation)}
means that in response to the input $I$, the
program $P$ may perform the computation $C$, yielding output $O$. The
correspondence between the arguments $Q$ and $I$, $\mathbold{T}$ and
$P$, $D$ and $C$, $F$ and $O$ displays the crucial correspondence
between logic and computation that is at the heart of logic
programming.

There are two closely related trinary notations.
$$Q\answers\mathbold{T}\hyproves F$$\notind{$\answers\hyproves$
(trinary answer relation)}
means that there exists a proof $D$ such
that $Q\answers\mathbold{T}\hypos D\proves F$, and $$I\inputs
P\compout O$$\notind{$\inputs\:\compout$ (computed-output relation)}
means that there exists a computation $C$ such that
$I\inputs P\computes C\outputs O$. The symbol $\hyproves$ in
$Q\answers\mathbold{F}\hyproves F$ is the conventional symbol for
proof in mathematical logic; we take the liberty of decomposing it
into the two symbols $\hypos$ and $\proves$ for the quaternary
notation. The conventional recursion-theoretic notation for our
$I\inputs P\compout O$ is \mbox{$\phi_P(I)=O$}. The computational
symbol $\compout$ and its components $\computes$ and $\outputs$ are
designed to have similar shapes to $\hyproves$, $\hypos$, and
$\proves$.

Other relations from logic do {\em not\/} correspond directly to
computational relations, but can be understood by their connections to
the quaternary form, in which the logic/computation correspondence is
direct and transparent. In Section~\ref{sec:sound-complete-proof} I
define $Q\answers\mathbold{T}\hypos D\proves F$ to hold exactly when
both $$\filldisplay Q\answers
F\filldisplay\mbox{and}\filldisplay\mathbold{T}\hypos D\proves
F\filldisplay$$ where $Q\answers F$ means that $F$ is an answer (not
necessarily a correct one) to the question $Q$, and
$\mathbold{T}\hypos D\proves F$
\notind{$\hypos\:\proves$ (trinary proof relation)}
means that $D$ is a proof of $F$, using postulates
in the set $\mathbold{T}$. $\mathbold{T}\hypos D\proves F$ is a
conventional concept from mathematical logic (often written
$\mathbold{T},D\hyproves F$ or $\mathbold{T}\hyproves_D F$).  The
question-answer relation $\answers$ is not conventional.  Notice that
each separating symbol in the quaternary notation
$Q\answers\mathbold{T}\hypos D\proves F$ is used exactly once in the
binary and trinary forms from which it is defined, so the notational
conjunction of symbols suggests the logical conjunction of the denoted
relations. Unfortunately, while the symbol $\answers$ appears between
the question $Q$ and the answer formula $F$ in the binary notation
$Q\answers F$, it is not adjacent to $F$ in the quaternary notation
$Q\answers\mathbold{T}\hypos D\proves F$. The dash component $\proves$
of the symbol $\answers$ mimics the $\proves$ symbol at the end of the
quaternary notation, and the similar component of the $\hyproves$
symbol from the trinary notation above, as a reminder that the
$\answers$ symbol is expressing a relation to the final answer formula
$F$, rather than to the set $\mathbold{T}$ of postulated formulae.

The quaternary computational relation is also defined as the
conjunction of a binary and a trinary relation, but the arguments
involved in these relations do {\em not\/} correspond to the arguments
of the binary and trinary relations from logic. In
Section~\ref{sec:programming-system} I define $I\inputs P\computes
C\outputs O$ to hold exactly when both $$\filldisplay
I\inputs P\computes C\filldisplay\mbox{and}\filldisplay C\outputs
O\filldisplay$$\notind{$\inputs\:\computes$ (trinary computation relation)}
where $I\inputs P\computes C$ means that the program $P$ on
input $I$ may perform the computation $C$, and $C\outputs
O$\notind{$\outputs$ (output relation)} means that the
computation $C$ yields output $O$. In this case, the mnemonic
suggestion of the conjunction of the trinary and binary relations in
the quaternary notation works out perfectly, as all argument positions
are adjacent to the appropriate separator symbols.

A few other derived notations are useful for denoting relations from
logic. These all agree with conventional notation in mathematical
logic. $$\mathbold{T}\hyproves F$$\notind{$\hyproves$ (binary proof relation)}
means that there exists a proof $D$ such that
$\mathbold{T}\hypos D\proves F$---that is, $F$ is formally derivable
from $\mathbold{T}$. Corresponding to the relation $\hyproves$ of {\em
formal derivability\/} is the relation $\models$ of {\em semantic
entailment}.
$$\mathbold{T}\models F$$\notind{$\models$ (semantic entailment relation)}
means that $F$ is semantically entailed by
$\mathbold{T}$. Similarly, $$Q\answers\mathbold{T}\models
F$$\notind{$\answers\models$ (semantically correct answer)}
means that $F$ is an answer to $Q$ semantically entailed by $\mathbold{T}$
($Q\answers F$ and $\mathbold{T}\models F$) in analogy to
$Q\answers\mathbold{T}\hyproves F$. The mathematical definition of
semantic entailment involves one more semantic relation.  Let $M$ be a
model, and $F$ a formula.  $$M\models F$$\notind{$\models$ (truth
relation)}
means that $F$ is true in $M$.

Table~\ref{tab:notations} displays all of the special notations for
semantic, proof-theoretic, and computational relations.  The precise
meanings and applications of these notations are developed at length
in subsequent sections.  The notation described above is subscripted
when necessary to distinguish the logical and computational relations
of different systems.
\begin{table}[hbtp]
\begin{center}
{\renewcommand{\arraystretch}{1.5}
\begin{tabular}{|c|c|c|}
\hline
\multicolumn{2}{|c|}{{\bf Logic}} & {\bf Computation}\\
{\bf Semantics} & {\bf Proof} & \\
\hline\hline
 & $Q\answers\mathbold{T}\hypos D\proves F$ & $I\inputs P\computes C\outputs O$\\
\hline
$Q\answers\mathbold{T}\models F$ & $Q\answers\mathbold{T}\hyproves F$ &
                                $I\inputs P\compout O$\\
\hline
\multicolumn{2}{|c|}{\relax} & $I\inputs P\computes C$\\
\hline
\multicolumn{2}{|c|}{$Q\answers F$} & \\
\hline
\multicolumn{2}{|c|}{\relax} & $C\outputs O$\\
\hline
 & $\mathbold{T}\hypos D\proves F$ & \\
\hline
$\mathbold{T}\models F$ & $\mathbold{T}\hyproves F$ & \\
\hline
$M\models F$ & & \\
\hline
\end{tabular}
}
\end{center}
\caption{\label{tab:notations}
Special Notations for Logical and Computational Relations}
\end{table}

\section{Specifying Logic Programming Languages}
\label{sec:specifying}

Logic typically develops its {\em `principles and criteria of validity
of inference'} by studying the relations between {\em notations\/}
for assertions\subind{assertion}, the {\em meanings\/} of those
assertions, and {\em derivations\/}\subind{derivation} of notations
expressing true assertions. Mathematical logic formalizes these
concepts using {\em logical formulae\/}\subind{formula} as notations,
sets of {\em models\/}\subind{model} to analyze meanings and
characterize truth, and {\em demonstrations\/}\subind{demonstration}
or {\em proofs\/}\subind{proof} as derivations of true formulae and
inferences\subind{inference}. The structure of formulae alone is {\em
syntax}\subind{syntax}, their relation to models is {\em
semantics}\subind{semantics}, and their relation to proofs is {\em
proof theory}\subind{proof theory}. Syntax is not relevant to the
present discussion. We must examine formal systems of semantics, and
augment them with formal concepts of questions and their answers, in
order to understand the specification of a logic programming language.
In Section~\ref{sec:implementing} we see how formal systems of proof
provide a natural approach to the implementation of computations for
logic programming.

\subsection[Semantic Systems]{Semantic Systems and Semantic Consequences}
\label{sec:semantic-systems}

\subind{semantic system|(}
A {\em semantic system\/} relates a set $\mathbold{F}$ of logical formulae
to a set $\mathbold{M}$ of formal models, each representing a conceivable
state of the world in enough detail to determine when a given formula
represents a true assertion in that state of the world.
\begin{definition}\label{def:semantic-system}
A\/ {\em semantic system\/} is a system\/ \mbox{${\cal
S}=\langle\mathbold{F},\mathbold{M},\models\rangle$}, where
\notind{$\mathbold{M}$ (models, interpretations)}
\begin{enumerate}
\item $\mathbold{F}$\notind{$\mathbold{F}$ (formulae)} is a set of\/ {\em
logical formulae}\subind{formula}
\item $\mathbold{M}$\subind{model} is a set of\/ {\em models}
\item $\models$\notind{$\models$ (semantic entailment relation)}
  is a relation on\/ \mbox{$\mathbold{M}\times\mathbold{F}$}
\end{enumerate}
Let \mbox{$\mathbold{K}\subseteq\mathbold{M}$}.
\mbox{$\theoryfunc(\mathbold{K})=\{F\in\mathbold{F}\setsep M\models
F\mbox{ {\it for all} }
M\in\mathbold{K}\}$}\subind{theory}\notind{$\theoryfunc$}.\\ Let
\mbox{$\mathbold{T}\subseteq\mathbold{F}$}.
\mbox{$\modelfunc(\mathbold{T})=
\{M\in\mathbold{M}\setsep M\models F\mbox{ {\it for all}
}F\in\mathbold{T}\}$}\notind{$\modelfunc$}.
\end{definition}
Intuitively, \mbox{$M\models F$} is intended to mean that formula\/
$F$ {\em holds in}, or\/ {\em is valid in}, or\/ {\em is satisfied
by}\subind{satisfaction}, model\/
$M$. \mbox{$\theoryfunc(\mathbold{K})$} is the fullest possible
description of $\mathbold{K}$ using a set of formulae in the language
of the system. \mbox{$\modelfunc(\mathbold{T})$} represents the state
of knowledge\subind{knowledge} given implicitly by the formulae in
$\mathbold{T}$---knowing $\mathbold{T}$ we know that reality
corresponds to one of the models in $\modelfunc(\mathbold{T})$, but we
do not know which one. Notice the antimonotone relation between
$\mathbold{F}$ and $\mathbold{M}$:
$$\begin{array}{rcl}
\multicolumn{3}{c}{\mathbold{T}_1\subseteq\mathbold{T}_2\mbox{ if and
  only if }\modelfunc(\mathbold{T}_1)\supseteq\modelfunc(\mathbold{T}_2)} \\
\multicolumn{3}{c}{\mathbold{K}_1\subseteq\mathbold{K}_2\mbox{ if and
    only if }\theoryfunc(\mathbold{K}_1)\supseteq\theoryfunc(\mathbold{K}_2)}\\
\modelfunc(\mathbold{T}_1\cup\mathbold{T}_2) & = &
  \modelfunc(\mathbold{T}_1)\cap\modelfunc(\mathbold{T}_2) \\
\modelfunc(\mathbold{T}_1\cap\mathbold{T}_2) & = &
  \modelfunc(\mathbold{T}_1)\cup\modelfunc(\mathbold{T}_2) \\
\theoryfunc(\mathbold{K}_1\cup\mathbold{K}_2) & = &
  \theoryfunc(\mathbold{K}_1)\cap\theoryfunc(\mathbold{K}_2) \\
\theoryfunc(\mathbold{K}_1\cap\mathbold{K}_2) & = &
  \theoryfunc(\mathbold{K}_1)\cup\theoryfunc(\mathbold{K}_2)
\end{array}$$

In order to provide satisfactory intuitive insight, a semantic system
must relate the syntactic structure of formulae to the determination
of truth. For example, well-known sets of formulae often come with a
syntactic operator to construct, from two formulae $A$ and $B$, their
{\em logical conjunction} $A\land B$. The semantics for conjunctions
is defined structurally, by the rule {\em $\mathbold{M}\models A\land
B$ if and only if $\mathbold{M}\models A$ and $\mathbold{M}\models
B$}. The formal analysis of this chapter deals only with the abstract
relation of a model to a formula that holds in the state of the world
represented by that model, not the internal structure of that
relation, because we are interested here in the {\em use\/} of
semantics for understanding logic programming, rather than the deeper
structure of semantics itself. Goguen's and Burstall's {\em
institututions\/} \cite{Goguen-Burstall}\auind{Goguen, J. A.}
\auind{Burstall, R. M.} are similar to semantic systems, but they
capture in addition the structural connection between syntax and
semantics through category theory, and show that the functions
$\modelfunc$ and $\theoryfunc$ form a {\em Galois connection.}

Notice that the sets $\mathbold{F}$ of formulae and $\mathbold{M}$ of
models are not required to be given effectively. In well-known
semantic systems, the set of formulae is normally computable, since
formulae are normally finite syntactic objects, and it is easy to
determine mechanically whether a given object is a formula or
not. Infinite formulae\subind{infinite formula}, however, have
important uses, and they can be given practical computational
interpretations, so we do {\em not\/} add any formal requirement of
computability. The set of models, on the other hand, is typically
quite complex, because models represent conceivable states of an
external world, rather than finite constructions of our own minds. In
fact, for many semantic systems there are technical set-theoretic
problems even in regarding the collection of models in the system as a
set, but those problems do not affect any of the results of this
chapter.

\subind{Shallow Implicational Calculus|(}
\notind{SIC (Shallow Implicational Calculus)|(}
In this chapter, basic concepts are illustrated through a running
example based on the {\em Shallow Implicational Calculus\/} (SIC),
designed to be almost trivial, but just complex enough to make an
interesting example. More realistic examples are treated toward the
end of the chapter.
\begin{example}\label{exa:semantic-system}
Let\/ $\mbox{\bf At}$ be a set of\/ {\em atomic propositional formulae}.
The set\/ $\sicformulae$\notind{$\sicformulae$
(shallow implicational formulae)} of formulae in the\/ {\em
Shallow Implicational Calculus\/} is the smallest set such that:
\begin{enumerate}
   \item\mbox{$\mbox{\bf At}\subseteq\sicformulae$}
   \item If\/ \mbox{$a,b\in\mbox{\bf At}$}, then\/
      \mbox{$(a\limplies b)\in\sicformulae$}
\end{enumerate}
The set\/ $\sicmodels$ of models in SIC is defined by
$$\sicmodels =\powerset{\mbox{\bf At}}$$  The semantic relation\/
\mbox{$\sicsemrel\subseteq\sicmodels\times\sicformulae$} is defined by:
\begin{enumerate}
   \item For\/ \mbox{$a\in\mbox{\bf At}$}, $M\sicsemrel a$ if and only
      if\/ \mbox{$a\in M$}
   \item \mbox{$M\sicsemrel(a\limplies b)$} if and only if either\/
      \mbox{$b\in M$} or\/ \mbox{$a\not\in M$}
\end{enumerate}
Now\/ \mbox{$\langle\sicformulae,\sicmodels,\sicsemrel\rangle$} is a
semantic system, representing the classical concept of meaning for the
implicational formulae of SIC.
\end{example}
SIC is just the restriction of the Classical Propositional Calculus
\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}\auind{Kleene, S. C.}
\auind{Gallier, J. H.}
to atomic propositional formulae, and
implications between atomic propositional formulae. It is called
`shallow' because no nesting of implications is allowed. Since the
truth of formulae in SIC (as in the Propositional Calculus) is
determined entirely by the truth of atomic formulae, a model merely
specifies the set of atomic formulae that are true in a given
conceivable state of the world. Following the tradition of material
implication in classical logic, an implication is true precisely when
its conclusion is true, or its hypothesis is false.

\subind{semantic consequence|(}\subind{consequence!semantic|)}
For the formal definition of a logic programming language, the
important thing about a semantic system is the {\em
semantic-consequence\/} relation that it defines, determining when the
truth of a set of formulae justifies inferring the truth of an
additional formula.\subind{compact!semantics}
\begin{definition}[\cite{Andrews,Gallier}\auind{Andrews, P. B.}
\auind{Gallier, J. H.}]
\label{def:semantic-consequence}
\notind{$\models$ (semantic consequence relation)}
Let\/ \mbox{${\cal S}=\langle\mathbold{F},\mathbold{M},\models\rangle$} be a
semantic system.  The\/ {\em semantic-consequence\/} relation defined
by\/ ${\cal S}$ is\/
\mbox{$\models\subseteq\powerset{\mathbold{F}}\times\mathbold{F}$},
where\/ \mbox{$\mathbold{T}\models F$} if and only if\/
\mbox{$M\models F$} for all\/ \mbox{$M\in\modelfunc(\mathbold{T})$}.

The semantic-consequence relation\/ $\models$ is\/ {\em compact\/} if
and only if, for all\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}$} and\/
\mbox{$F\in\mathbold{F}$}, whenever\/ \mbox{$\mathbold{T}\models F$} then there
exists a finite subset\/ \mbox{$\mathbold{T}^{\rm f}\subseteq\mathbold{T}$} such
that\/ \mbox{$\mathbold{T}^{\rm f}\models F$}.
\end{definition}
Intuitively, \mbox{$\mathbold{T}\models F$} means that $F$ is a {\em
semantic consequence\/} of $\mathbold{T}$, since $F$ must be true
whenever all formulae in $\mathbold{T}$ are true. Semantic
consequences are often called {\em logical
consequences\/}\subind{logical consequence}; our terminology is chosen
to highlight the contrast between semantic consequences and the {\em
provable consequences\/} of Definition~\ref{def:provable-consequence}.
Notice that
\mbox{$\theoryfunc(\modelfunc(\mathbold{T}))$}\subind{theory}\notind{$\theoryfunc$}
is the set of semantic consequences of $\mathbold{T}$. It is easy to
show that an arbitrary relation $\models$ on
\mbox{$\powerset{\mathbold{F}}\times\mathbold{F}$}
is the semantic-consequence relation of some semantic system if and
only if it is
\begin{enumerate}
\item {\em reflexive\/}\subind{reflexive}:
  \mbox{$F\in\mathbold{T}$} implies that
  \mbox{$\mathbold{T}\models F$}
\item {\em monotone\/}\subind{monotone}:
  \mbox{$\mathbold{T}\models F$} and
  \mbox{$\mathbold{T}\subseteq\mathbold{U}$} imply that
  \mbox{$\mathbold{U}\models F$}
\item {\em transitive\/}\subind{transitive}:
  \mbox{$\mathbold{T}\models F$} and
  \mbox{$\mathbold{T}\cup\{F\}\models G$} imply that
  \mbox{$\mathbold{T}\models G$}
\end{enumerate}
In order for a semantic-consequence relation to be useful for logic
programming, or for rigorous formal reasoning, it must be sufficiently
effective. Well-known semantic systems normally define
semantic-consequence relations that are compact---their behavior on
arbitrary sets is determined by their behavior on finite sets. Normal
semantic-consequence relations are semicomputable, but not necessarily
computable, when restricted to finite sets of formulae in the first
component. Fortunately, semicomputability is enough for logic
programming.

\begin{example}\label{exa:semantic-consequence}
The semantic-consequence relation $\sicsemrel$ of the Shallow
Implicational Calculus of Example~\ref{exa:semantic-system} is
compact, and has a particularly simple behavior:
\begin{enumerate}
\item for atomic
formulae\/ \mbox{$a\in\mbox{\bf At}$}, \mbox{$\mathbold{T}\sicsemrel a$} if
and only if there is a finite sequence\/
\mbox{$\langle a_0,\ldots,a_m\rangle$} of atomic formulae such that\/
\mbox{$a_0\in\mathbold{T}$}, and
\mbox{$(a_i\limplies a_{i+1})\in\mathbold{T}$} for all\/ \mbox{$i<m$},
and\/ \mbox{$a_m=a$}
\item \mbox{$\mathbold{T}\sicsemrel(a\limplies b)$}
  if and only if there is a finite
  sequence\/ \mbox{$\langle a_0,\ldots,a_m\rangle$} of atomic formulae
  such that\/
\mbox{$a_0\in\mathbold{T}\cup\{a\}$}, and \mbox{$(a_i\limplies
a_{i+1})\in\mathbold{T}$} for all\/ \mbox{$i<m$}, and\/ \mbox{$a_m=b$}
\end{enumerate}
\end{example}
We may think of the implications in $\mathbold{T}$ as directed edges
in a graph whose vertices are atomic formulae.  Atomic formulae in
$\mathbold{T}$ are marked {\em true}. An atomic formula $a$ is a
semantic consequence of $\mathbold{T}$ precisely if there is a
directed path from some atomic formula in\/ $\mathbold{T}$ to $a$.
Similarly, an implication \mbox{$a\limplies b$} is a semantic
consequence of $\mathbold{T}$ precisely if there is a directed path
from $a$, or from an atomic formula in $\mathbold{T}$, to $b$. Notice
that SIC satisfies the
{\em deduction property}\subind{deduction property}:
\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}\auind{Kleene, S. C.}
\auind{Gallier, J. H.}
$$\mathbold{T}\sicsemrel(a\limplies
b)\mbox{ if and only if }\mathbold{T}\cup\{a\}\sicsemrel b$$
\subind{Shallow Implicational Calculus|)}
\notind{SIC (Shallow Implicational Calculus)|)}
\subind{semantic consequence|)}\subind{consequence!semantic|)}

\subind{logic!representing communication and knowledge|(}
\subind{knowledge|(}
\subind{communication|(}
\subind{speaker|(}
\subind{auditor|(}
\subind{programmer|(}
\subind{processor|(}
A semantic system provides a conceptual tool for analyzing a primitive
sort of communication in a monologue. A state of implicit knowledge
is naturally represented by the set of models corresponding to
conceivable states of the world that are consistent with that
knowledge. Notice that larger sets of models represent smaller
amounts of knowledge. For a general discussion of knowledge as sets
of models, the shortcomings of such representations, and problems and
paradoxes that arise when subtle sorts of knowledge are considered,
see \cite{Fagin-Halpern-Vardi}.
\auind{Fagin, R.}\auind{Halpern, J. Y.}\auind{Vardi, M. Y.}
The knowledge involved in formal analysis of the examples of logic
programming in this chapter is simple enough to be represented by sets
of models without presenting the problems that arise in a more general
setting.  Explicit knowledge is naturally represented by a set of
formulae.  $\modelfunc(\mathbold{T})$ is the implicit knowledge given
explicitly by $\mathbold{T}$. Similarly, $\theoryfunc(\mathbold{K})$
is the strongest explicit representation of the implicit knowledge
$\mathbold{K}$ that is expressible in a given language, but there is
no guarantee that an agent with implicit knowledge $\mathbold{K}$ can
effectively produce all of the explicit knowledge
$\theoryfunc(\mathbold{K})$.

Consider a {\em speaker\/}, whose state of knowledge is represented by
$\mathbold{K}_{\rm s}$, and an {\em auditor} with initial knowledge
$\mathbold{K}^0_{\rm a}$. The speaker wishes to communicate some of
her knowledge to the auditor, so she utters a set of formulae
\mbox{$\mathbold{T}\subseteq\theoryfunc(\mathbold{K}_{\rm s})$}.  The
impact of the speaker's utterance on the auditor's state of knowledge
is to remove from the auditor's set of models those that do not
satisfy $\mathbold{T}$.  That is, $\mathbold{K}^0_{\rm a}$ is replaced
by
\mbox{$\mathbold{K}^1_{\rm a}=\mathbold{K}^0_{\rm a}\cap\modelfunc(\mathbold{T})$}.
Notice that, if the auditor's initial knowledge is minimal, that is if
\mbox{$\mathbold{K}^0_{\rm a}$} is the set of all models in the semantic
system, then \mbox{$\mathbold{K}^1_{\rm a}=\modelfunc(\mathbold{T})$},
so the formulae implied by the new knowledge,
\mbox{$\theoryfunc(\mathbold{K}^1_{\rm a})$}, are exactly the semantic
consequences of $\mathbold{T}$.  In logic programming systems, the
programmer plays the part of the speaker above, the processor plays
the part of the auditor, the program is the utterance, and the logical
meaning of the program is the resulting state of knowledge produced in
the auditor/processor.  Inputs to, computations of, and outputs from
logic programs are treated later.

Notice that this style of semantic analysis of communication does not
give either speaker or auditor direct access to inspect or modify the
models constituting the other's state of implicit knowledge.  Rather,
all such access is mediated by the utterance of explicit logical
formulae.  Also, notice that there is no attempt to construct a {\em
unique\/} model to represent a state of knowledge, or the information
communicated by an utterance.  Rather, an increase in implicit
knowledge is represented by a reduction in the variability of members
of a set of models, any one of which might represent the real state of
the world.  Unless the semantic-consequence relation of a semantic
system is very easy to compute---which it seldom is---the difference
between implicit knowledge and effectively utterable explicit
knowledge can be quite significant.  The {\em proof systems\/} of
Section~\ref{sec:proof-system} help describe a way in which implicit
knowledge is made explicit, and yield a rough description of the
computations of logic programs.

The preceding scheme for representing communication of knowledge deals
naturally with a sequence of utterances, by iterating the process of
shrinking the auditor's set of models.  There is no provision,
however, for analyzing any sort of interactive {\em dialogue,} other
than as a pair of formally unrelated monologues.  The {\em query
systems\/} of the next section introduce a primitive sort of
interactive question-answering dialogue.
\subind{communication|)}
\subind{knowledge|)}
\subind{semantic system|)}
\subind{logic!representing communication and knowledge|)}
\subind{speaker|)}
\subind{auditor|)}
\subind{programmer|)}
\subind{processor|)}

\subsection[Query Systems]{Query Systems, Questions and Answers}
\label{sec:query-systems}

\subind{query system|(}
\subind{question|(}
Semantic systems and semantic-consequence relations are conventional
subjects for logical investigation. They suffice for discussions of
the truth of a formula and the validity of the inference of a new
formula from a given set of formulae. In order to analyze the relation
between input to a logic program and the corresponding output, we need
a formal basis for discussing questions and their
answers. Mathematical logicians have given very little attention to
this branch of logic---one exception is the formal treatment by Belnap
and Steel \cite{Belnap-Steel}\auind{Belnap, N. D.}\auind{Steel,
T. B.}. {\em Query systems} are an abstraction of the common formal
schema from a number of instances of question-answer domains defined
by Belnap and Steel.
\begin{definition}\label{def:query-system}
A\/ {\em query system\/} is a system\/ \mbox{${\cal
Q}=\langle\mathbold{F},\mathbold{Q},\answers\rangle$}, where
\begin{enumerate}
\item $\mathbold{F}$\notind{$\mathbold{F}$ (formulae)}
  is a set of\/ {\em logical formulae\/}
\item $\mathbold{Q}$\notind{$\mathbold{Q}$ (questions)}
  is a set of\/ {\em questions}
\item $\answers$\notind{$\answers$ (answer relation)}
  is a relation on\/ \mbox{$\mathbold{Q}\times\mathbold{F}$}
\end{enumerate}
\end{definition}
Questions, like formulae, are normally finite syntactic objects, and
the set of all questions is normally computable, but we allow
exceptions to the normal case.

\mbox{$Q\answers F$} is intended to mean that $F$ is an {\em
answer\/} to $Q$. $\answers$ is intended only to determine the
acceptable form for an answer to a question, {\em not\/} to carry any
information about {\em correctness\/} of an answer. For example, it
is reasonable to say that `$2+2=5$' is an incorrect answer to `what
is $2+2$?', while `$2+2=2^2$' is correct, but not an answer. The
correctness or incorrectness of an answer is evaluated semantically
with respect to explicit
knowledge.\subind{correct answer}\subind{semantically answerable question}
\begin{definition}\label{def:semantically-correct-answer}
Let\/ \mbox{${\cal Q}=\langle\mathbold{F}_{\rm
Q},\mathbold{Q},\answers\rangle$} be a query system, and let\/
\mbox{${\cal S}=\langle\mathbold{F}_{\rm
S},\mathbold{M},\models\rangle$} be a semantic system with\/
\mbox{$\mathbold{F}_{\rm Q}\subseteq\mathbold{F}_{\rm S}$}.

\mbox{$Q\answers\mathbold{T}\models F$}\notind{$\answers\models$ (semantically correct answer)} means that\/ $F\in\mathbold{F}_{\rm Q}$
is a\/ {\em semantically correct\/} answer to $Q\in\mathbold{Q}$ for
explicit knowledge\/ $\mathbold{T}\subseteq\mathbold{F}_{\rm S}$,
defined by $$Q\answers\mathbold{T}\models F\mbox{ if and only if
}Q\answers F\mbox{ and }\mathbold{T}\models F$$

A question\/ \mbox{$Q\in\mathbold{Q}$} is\/ {\em semantically answerable\/}
for explicit knowledge\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}_{\rm S}$} if
and only if there exists a formula\/ \mbox{$F\in\mathbold{F}_{\rm Q}$} such
that $F$ is a semantically correct answer to\/ $Q$ in\/ $\mathbold{T}$.
\end{definition}
Meseguer \cite{Meseguer-general,Meseguer-multiparadigm}\auind{Meseguer,
J.} proposes a different notion of question answering, in which a
question is a formula, and an answer is a proof (in an abstract
notation omitting many details) of the formula. (This is an
interesting twist on the {\em formulae as types\/} concept
\cite{Howard,Tait}\auind{Howard, W.}\auind{Tait, W. W.}, which is more
usually applied by letting a program specification be a formula, and a
program be a proof of the formula \cite{Constable-Allen-Bromley}.)
\auind{Constable, R. L.}\auind{Allen, S. F.}\auind{Bromley, H. M.}
\auind{Cleaveland, W. R.}\auind{Cremer, J. F.}\auind{Harper, R. W.}
\auind{Howe, D. J.}\auind{Knoblock, T. B.}\auind{Mendler, N. P.}
\auind{Panangaden, P.}\auind{Sasaki, J. T.}\auind{Smith, S. F.}

\subind{Shallow Implicational Calculus|(}
\notind{SIC (Shallow Implicational Calculus)|(}
Several interesting query systems may be defined for the Shallow
Implicational Calculus.
\begin{example}\label{exa:query-system-1}
\notind{$\mbox{\bf imp}$ (implication question)}
Let\/ $\mbox{\bf imp}$ be a new formal symbol, and let\/
$\sicformulae$ be the set of formulae in SIC defined in
Example~\ref{exa:semantic-system}.  Let
$$\sicquestionsa=\{\mbox{\bf imp}(F)\setsep
F\in\mbox{\bf At}\}$$\notind{$\sicquestionsa$ (implication questions)}
Define the relation\/
\mbox{$\sicanswersa\subseteq\sicquestionsa\times\sicformulae$} by
$$\mbox{\bf imp}(c)\sicanswersa(a\limplies b)\mbox{ if and
only if\/ }a=c$$\notind{$\sicanswersa$ (implication answer relation)}
Now\/
\mbox{$\langle\sicformulae,\sicquestionsa,\sicanswersa\rangle$} is a
query system representing the conceivable answers to questions of the
form `what atomic formula does $a$ imply?'
\end{example}
The query system of Example~\ref{exa:query-system-1} above is susceptible
to two sorts of answers that may be intuitively unsatisfying. First,
in a state of knowledge in which an atomic formula $b$ is known to be
true, \mbox{$(a\limplies b)$} is a correct answer to questions
\mbox{$\mbox{\bf imp}(a)$} for all atomic formulae $a$. This
problem may be avoided by considering states of knowledge in which
only implications are known, or it may be addressed by changing the
underlying semantic system to one with a {\em
relevant\/}\subind{relevant implication} interpretation of
implication \cite{Anderson-Belnap}\auind{Belnap, N. D.}\auind{Anderson, A. R.}.
Second, \mbox{$(a\limplies a)$} is a correct answer to the question
\mbox{$\mbox{\bf imp}(a)$}. \mbox{$(a\limplies a)$} is a
{\em tautology}\subind{tautological
answer}\subind{answer!tautological}, that is, it holds in all models,
so it cannot give any information about a state of knowledge. We could
define a new query system, in which only nontautologies are considered
to be answers. Since, for most useful logics, the detection of
tautologies ranges from intractable to impossible, such a technique is
generally unsatisfying. A better approach is to let a question present
a set of atomic formulae that must not be used in an answer, since the
questioner considers them to be insufficiently informative. We may
find later that certain nontautological formulae are uninformative for
various reasons, and this technique reserves the flexibility to handle
those cases.
\begin{example}\label{exa:query-system-2}
\notind{$\mbox{\bf rest-imp}$ (restricted implication question)}
Let\/ $\mbox{\bf rest-imp}$ be a new formal symbol, and let
$$\sicquestionsb=\{\mbox{\bf rest-imp}(a,\mathbold{A})\setsep
a\in\mbox{\bf At}\mbox{ and }\mathbold{A}\subseteq\mbox{\bf At}\}$$
\notind{$\sicquestionsb$ (restricted implication questions)}
Define the relation\/
\mbox{$\sicanswersb\subseteq\sicquestionsb\times\sicformulae$} by
$$\mbox{\bf rest-imp}(c,\mathbold{C})\sicanswersa(a\limplies b)\mbox{ if and
only if\/ }a=c\mbox{ and\/ }b\not\in\mathbold{C}$$
\notind{$\sicanswersb$ (restricted implication answer relation)}
Now\/
\mbox{$\langle\sicformulae,\sicquestionsa,\sicanswersa\rangle$} is a
query system representing the conceivable answers to questions of the
form `what atomic formula not in $\mathbold{A}$ does $a$ imply?'
\end{example}
The new query system of Example~\ref{exa:query-system-2} may be used
very flexibly to guide answers toward the most informative
implications of an atomic formula $a$. If the explicit knowledge
available to the auditor to answer questions is finite, then there are
only a finite number of atomic formulae that can appear in an answer,
so the sets of prohibited formulae may simply be listed. In more
sophisticated languages than SIC, we need some sort of finite notation
for describing large and even infinite sets of prohibited answers.
\notind{SIC (Shallow Implicational Calculus)|)}
\subind{Shallow Implicational Calculus|)}

\subind{communication|(}
\subind{knowledge|(}
\subind{logic!representing communication and knowledge|(}
\subind{answer|(}
\subind{questioner|(}
\subind{speaker|(}
\subind{auditor|(}
Query systems allow a further enrichment of the analysis of
communication. Once a speaker has communicated some implicit
knowledge $\mathbold{K}$ to an auditor by uttering formulae, a {\em
questioner\/} (sometimes, but not always, identical with the speaker)
may ask a question $Q$, which the auditor tries to answer by
discovering a formula $F$ such that \mbox{$Q\answers F$} ($F$ is an
answer to the question $Q$), and \mbox{$F\in\theoryfunc(\mathbold{K})$}
($Q$ is correct according to the implicit knowledge $\mathbold{K}$).

\subind{consequentially strongest answer|(}
So, given a set $\mathbold{T}$ of formulae expressing the knowledge
$\modelfunc(\mathbold{T})$, a question $Q$ provides an additional
constraint on the search for a formula $F$ such that
\mbox{$\mathbold{T}\models F$}, to ensure that \mbox{$Q\answers F$} as
well. In many cases, there is more than one correct answer $F$ such
that
\mbox{$Q\answers\mathbold{T}\models F$}. Depending on the context, the
questioner may want a single answer chosen nondeterministically from
the set of correct answers, or a best answer under some criterion.
The case where the questioner wants a list of all answers may be
modelled by representing that list by a single formula giving the
conjunction of all the list elements. A particularly useful criterion
for best answer uses the logical consequence relation.
\begin{definition}\label{def:strongest-answer}
Let\/ \mbox{${\cal Q}=\langle\mathbold{F}_{\rm
Q},\mathbold{Q},\answers\rangle$} be a query system, and let\/
\mbox{${\cal S}=\langle\mathbold{F}_{\rm
S},\mathbold{W},\models\rangle$} be a semantic system with\/
\mbox{$\mathbold{F}_{\rm Q}\subseteq\mathbold{F}_{\rm S}$}.  $F$ is
a\/ {\em consequentially strongest\/} correct answer to the question\/
$Q$ for explicit knowledge\/ $\mathbold{T}$ if and only if
\begin{enumerate}
\item \mbox{$Q\answers\mathbold{T}\models F$}
\item for all\/ \mbox{$G\in\mathbold{F}_{\rm Q}$}, whenever\/
\mbox{$Q\answers\mathbold{T}\models G$}, then\/ \mbox{$\{F\}\models G$}
\end{enumerate}
\end{definition}
Consequentially strongest answers are not necessarily unique, but all
consequentially strongest answers are semantically equivalent. Notice
that the comparison of strength for two answers $F$ and $G$ is done
without taking into account the knowledge $\mathbold{T}$. That is, we
require \mbox{$\{F\}\models G$}, rather than
\mbox{$\mathbold{T}\cup\{F\}\models G$}. This makes sense because
$\mathbold{T}$ is known to the auditor, but not necessarily to the
questioner. Even if the questioner knows $\mathbold{T}$, he may not
be able to derive its consequences. The whole purpose of the
communication between questioner and auditor is to give the questioner
the benefit of the auditor's knowledge and inferential power. So, the
value of an answer to the questioner must be determined independently
of the knowledge used by the auditor in its construction (the
alternative form \mbox{$\mathbold{T}\cup\{F\}\models G$} holds
trivially by monotonicity, so it carries no information anyway).
\subind{questioner|)}
\subind{speaker|)}
\subind{auditor|)}

\notind{SIC (Shallow Implicational Calculus)|(}
\subind{Shallow Implicational Calculus|(}
\notind{SICC (Shallow Implicational-Conjunctive Calculus)|(}
\subind{Shallow Implicational-Conjunctive Calculus|(}
In order to illustrate the use of consequentially strongest answers,
we extend SIC to deal with conjunctions of implications.
\begin{example}\label{exa:strongest-answer}
Expand the formulae of SIC to the set
$$\siccformulae=\sicformulae\cup\{F_1\land\cdots\land F_m\setsep
F,G\in\sicformulae\}$$\notind{$\siccformulae$ (shallow
implicational-conjunctive formulae)}
of formulae in the\/ {\em Shallow
Implicational-Conjunctive Calculus\/} (SICC). The semantic systems and
proof systems of Examples \ref{exa:semantic-system},
\ref{exa:proof-system-natural}, \ref{exa:proof-system-linear} extend
in the natural way to deal with conjunctive formulae. Let\/
$\mbox{\bf conj-imp}$\notind{$\mbox{\bf conj-imp}$ (conjunctive implication
question)}
be a new formal symbol, and let
$$\sicquestionsc=\{\mbox{\bf conj-imp}(a)\setsep a\in\mbox{\bf
At}\}$$\notind{$\sicquestionsc$ (conjunctive implication questions)}
Define the relation\/
\mbox{$\sicanswersc\subseteq\sicquestionsc\times\siccformulae$} by
$$\mbox{\bf conj-imp}(c)\sicanswersc(a_1\limplies
b_1)\land\cdots\land(a_m\limplies b_m)\mbox{ if and
only if }a_i=c\mbox{ for all }i\leq m$$
\notind{$\sicanswersc$ (conjunctive implication answer relation)}
Now\/
\mbox{$\langle\siccformulae,\sicquestionsc,\sicanswersc\rangle$} is a
query system representing the conceivable answers to questions of the
form `what are some atomic formulae implied by $a$?' A
consequentially strongest answer to \mbox{$\mbox{\bf conj-imp}(a)$} is
a conjunction of\/ {\em all\/} of the implications with hypothesis $a$
that hold in a given state of knowledge.
\end{example}
The concept of consequentially strongest answers is particularly
helpful in systems where a potentially infinite answer\subind{infinite
answer}\subind{infinite formula} is produced
incrementally. The entire infinite answer may often be read as an
infinite conjunction of finite formulae, and the requirement of
consequentially strongest answers guarantees that the incremental
production of the answer does not stop prematurely, before all
available information is expressed.
\notind{SICC (Shallow Implicational-Conjunctive Calculus)|)}
\subind{Shallow Implicational-Conjunctive Calculus|)}
\notind{SIC (Shallow Implicational Calculus)|)}
\subind{Shallow Implicational Calculus|)}
\subind{consequentially strongest answer|)}

In logic programming systems\subind{logic programming system}, the
{\em user\/}\subind{user} of a program plays the part of the
questioner. The input is the question, and the output is the answer,
if any, discovered and proved by the
processor/auditor\subind{processor}\subind{auditor}.  This scenario
allows the knowledge resources of a
programmer/speaker\subind{programmer}\subind{speaker} to be combined
with the deductive powers of a processor/auditor, in order to answer
questions from the user/questioner.
\subind{communication|)}
\subind{knowledge|)}
\subind{logic!representing communication and knowledge|)}
\subind{answer|)}
\subind{query system|)}
\subind{question|)}

\subsection{Examples of Logic Programming Languages}
\label{sec:examples-logic-programming}

\subind{logic programming languages|(}
Now we can design a wide variety of logic programming languages, by
defining appropriate semantic systems and query systems.

\subsubsection[First-Order Predicate Calculus]{Programming in First-Order
        Predicate Calculus}
\label{sec:fopc}

\subind{First-Order Predicate Calculus|(}
\notind{FOPC (First-Order Predicate Calculus)|(}
Several logic programming systems, particularly Prolog and Relational
Databases, are essentially sublanguages of a general language for
logic programming in FOPC.
\begin{definition}[\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}
\auind{Kleene, S. C.}\auind{Gallier, J. H.}]\label{def:FOPC-formula}
Let\/
$\mathbold{V}$\notind{$\mathbold{V}$ (variables)}\subind{variable}
be a countably infinite set. Members of\/ $\mathbold{V}$ are
called\/ {\em variables,} and are written\/ $u,v,w,x,y,z$, sometimes
with subscripts.

\notind{$\mbox{\bf Fun}_i$ ($i$-ary function symbols)}
\subind{function symbols}\subind{arity}
Let\/ $\mbox{\bf Fun}_i$ be a countably infinite set for each\/ \mbox{$i\geq
0$}, with\/ $\mbox{\bf Fun}_i$ and\/ $\mbox{\bf Fun}_j$ disjoint when\/
$i\neq j$. Members of $\mbox{\bf Fun}_i$ are called\/ {\em function
symbols of arity\/ $i$,} and are written\/ $f,g,h$, sometimes with
subscripts. A function symbol of arity\/ $0$ in\/ $\mbox{\bf Fun}_0$
is called a\/ {\em constant,} and may be written\/ $a,b,c,d,e$.
\subind{constant symbol}

\notind{$\mbox{\bf Pred}_i$ ($i$-ary predicate symbols)}
\subind{predicate symbol}\subind{relation symbol}
Let\/ $\mbox{\bf Pred}_i$ be a countably infinite set for each\/
$i\geq 0$, with\/ $\mbox{\bf Pred}_i$ and\/ $\mbox{\bf Pred}_j$
disjoint when\/ \mbox{$i\neq j$}, $\mbox{\bf Pred}_i$ and\/ $\mbox{\bf
Fun}_j$ disjoint for all\/ $i$ and\/ $j$.  Members of\/ $\mbox{\bf
Pred}_i$ are called\/ {\em predicate\/} or\/ {\em relation symbols of
arity\/ $i$,} and are written\/ $P,Q,R$, sometimes with subscripts.  A
predicate symbol of arity\/ $0$ in\/ $\mbox{\bf Pred}_0$ is called a\/
{\em propositional symbol\/}, and is closely analogous to an atomic
propositional formula in\/ $\mbox{\bf At}$ as used in
Example~\ref{exa:semantic-system}.
\subind{propositional symbol}

\notind{$\mathbold{T}_P$ (FOPC terms)}
\subind{term}
The set\/ $\mathbold{T}_P$ of\/ {\em terms\/} in FOPC is defined inductively as
the least set such that:
\begin{enumerate}
        \item if\/ $x\in\mathbold{V}$ then\/ $x\in\mathbold{T}_P$
        \item if\/ $a\in\mbox{\bf Fun}_0$ then\/ $a\in\mathbold{T}_P$
        \item\label{enu:term-term} if\/ \mbox{$f\in\mbox{\bf Fun}_i$}
           for some\/ \mbox{$i>0$} and\/
           \mbox{$t_1,\ldots,t_i\in\mathbold{T}_P$}, then\/
           \mbox{$f(t_1,\ldots,t_i)\in\mathbold{T}_P$}
\end{enumerate}
Terms are intended to represent objects in some universe of discourse.
\mbox{$f(t_1,\ldots,t_i)$} is intended to represent the result
of applying the function denoted by\/ $f$ to the objects represented
by $t_1,\ldots,t_i$. We often take the liberty of writing binary
function application in infix notation. For example, if\/
\mbox{$+\in\mbox{\bf Fun}_2$} we may write\/ \mbox{$(t_1+t_2)$} for\/
\mbox{$+(t_1,t_2)$}.  A\/ {\em ground term\/} is a term containing no
variables.\subind{ground term}

\notind{$\mathbold{F}_P$ (FOPC formulae)}
\subind{formula!FOPC}\subind{First-Order Predicate Calculus!formula}
\notind{$\land$ (conjunction)}
\notind{$\lor$ (disjunction)}\notind{$\lnot$ (negation)}
\notind{$\limplies$ (implication)}
\notind{$\forall x\quantsep$ (for all $x$)}
\notind{$\exists x\quantsep$ (there exists $x$)}
\notind{$\mbox{True}$}\notind{$\mbox{False}$}
\subind{conjunction}\subind{disjunction}\subind{quantification}
\subind{for all}\subind{all}\subind{some}\subind{exists}
The set\/ $\mathbold{F}_P$ of\/ {\em formulae\/} in FOPC, is defined
inductively as
the least set such that:
\begin{enumerate}
        \item \mbox{$\mbox{True},\mbox{False}\in\mathbold{F}_P$}
        \item if\/ \mbox{$P\in\mbox{\bf Pred}_0$}, then\/
           \mbox{$P\in\mathbold{F}_P$}
        \item if\/ \mbox{$P\in\mbox{\bf Pred}_i$} for some\/ \mbox{$i>0$} and\/
           \mbox{$t_1,\ldots,t_i\in\mathbold{T}_P$}, then\/
           \mbox{$P(t_1,\ldots,t_i)\in\mathbold{F}_P$}
        \item if\/ \mbox{$A,B\in\mathbold{F}_P$}, then\/
           \mbox{$(A\land B),(A\lor B),(A\limplies B),(\lnot A)\in\mathbold{F}_P$}
        \item if\/ \mbox{$A\in\mathbold{F}_P$} and\/ \mbox{$x\in\mathbold{V}$}, then\/
           \mbox{$(\exists x\quantsep A),(\forall x\quantsep A)\in\mathbold{F}_P$}
\end{enumerate}
\subind{assertion}
Formulae in FOPC are intended to represent assertions about the
objects represented by their component terms. $\mbox{True}$ and\/
$\mbox{False}$ are the trivially true and false assertions,
respectively. \mbox{$P(t_1,\ldots,t_i)$} represents the assertion that the
relation denoted by\/ $P$ holds between\/ $t_1,\ldots,t_i$. \mbox{$(A\land
B)$}, \mbox{$(A\lor B)$}, \mbox{$(A\limplies B)$},
\mbox{$(\lnot A)$} represent the usual
conjunction, disjunction, implication, and negation.  \mbox{$(\exists
x\quantsep A)$} represents `there exists\/ $x$ such that\/ $A$,' and
\mbox{$(\forall x\quantsep A)$} represents `for all\/ $x$ $A$.'
Parentheses may dropped when they can be inferred from normal
precedence rules.
\end{definition}
In a more general setting, it is best to understand $\mbox{\bf Fun}_i$ and
$\mbox{\bf Pred}_i$ as parameters giving a {\em signature\/} for
first-order logic, and let them vary to produce an infinite class of
predicate calculi. For this chapter, we may take $\mbox{\bf Fun}_i$
and $\mbox{\bf Pred}_i$ to be arbitrary but fixed.
\notind{$\formeq$ (formal equality symbol)}\subind{equality}
In many texts on mathematical logic, the language of FOPC includes a
special binary predicate symbol `$\formeq$' for equality.  We follow the
Prolog tradition in using the {\em Pure First-Order Predicate
Calculus,} without equality, and referring to it simply as FOPC.

The intended meanings of FOPC formulae sketched above are formalized
by the traditional semantic system defined below.  First, we need a
set of models for FOPC.
\begin{definition}[\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}
\auind{Kleene, S. C.}\auind{Gallier, J. H.}]\label{def:FOPC-model}
\notind{$\mathbold{U}$ (universe)}
\subind{universe}
\subind{model!FOPC}
\subind{First-Order Predicate Calculus!model}
\subind{variable assignment}
\subind{predicate assignment}
\subind{function assignment}
Let\/ $\mathbold{U}$ be an infinite set, called the\/ {\em universe}.
Let\/ \mbox{$U\subseteq\mathbold{U}$}.\\ A\/ {\em variable assignment\/} over\/
$U$ is a function\/ \mbox{$\nu:\mathbold{V}\funcarrow U$}.\\ A\/ {\em predicate
assignment\/} over\/ $U$ is a function\/ \mbox{$\rho:\bigcup\{\mbox{\bf
Pred}_i\setsep i\geq0\}\funcarrow\bigcup\{\powerset{(U^i)}\setsep
i\geq0\}$} such that\/ \mbox{$P\in\mbox{\bf Pred}_i$} implies\/
\mbox{$\rho(P)\subseteq U^i$} for all\/ \mbox{$i\geq0$}.\\ A\/ {\em function
assignment\/} over\/ $U$ is a function\/
\mbox{$\tau:\bigcup\{\mbox{\bf Fun}_i\setsep
i\geq0\}\funcarrow\bigcup\{U^{(U^i)}\setsep i\geq0\}$} such that\/
\mbox{$f\in\mbox{\bf Fun}_i$} implies\/ \mbox{$\tau(f):U^i\funcarrow
U$} for all\/ \mbox{$i\geq0$}.

\notind{$\mathbold{M}_P$ (FOPC models)}
If\/ \mbox{$U\subseteq\mathbold{U}$}, $\tau$ is a function assignment
over\/ $U$, and\/ $\rho$ is a predicate assignment over $U$, then\/
\mbox{$\langle U,\tau,\rho\rangle$} is a\/ {\em model of FOPC}.
$\mathbold{M}_P$ is the set of all models of FOPC.
\end{definition}
Notice that FOPC models assign values to function and predicate
symbols, but not to variables. The exclusion of variable assignments
from models is the only technically significant distinction between
variables and constant symbols. A function assignment and a variable
assignment together determine a valuation of terms.  With a predicate
assignment, they also define a valuation of formulae.
\begin{definition}[\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}
\auind{Kleene, S. C.}\auind{Gallier, J. H.}]\label{def:FOPC-valuation}
\subind{valuation}\subind{term valuation}
Let\/ $\tau$ be a function assignment over\/ $U$, $\nu$ a variable
assignment over\/ $U$.  The\/ {\em term valuation\/}
\mbox{$\tau_\nu:\mathbold{T}_P\funcarrow U$} is defined inductively by
\begin{enumerate}
        \item if \mbox{$x\in\mathbold{V}$}, then\/ \mbox{$\tau_\nu(x)=\nu(x)$}
        \item if\/ \mbox{$f\in\mbox{\bf Fun}_i$}, and\/
        \mbox{$t_1,\ldots,t_i\in\mathbold{T}_P$}, then\/
        \mbox{$\tau_\nu(f(t_1,\ldots,t_i))=
        \tau(f)(\tau_\nu(t_1),\ldots,\tau_\nu(t_i))$}
\end{enumerate}
\subind{formula valuation}
In addition, let\/ $\rho$ be a predicate assignment over\/ $U$.  The\/
{\em formula valuation\/} \mbox{$\rho_{\tau,\nu}:\mathbold{F}_P\funcarrow\{0,1\}$} is
defined inductively by
\begin{enumerate}
        \item \mbox{$\rho_{\tau,\nu}(\mbox{False})=0$}
        \item \mbox{$\rho_{\tau,\nu}(\mbox{True})=1$}
        \item if\/ \mbox{$P\in\mbox{\bf Pred}_i$, and $t_1,\ldots,t_i\in
                \mathbold{T}_P$}, then \mbox{$\rho_{\tau,\nu}(P(t_1,\ldots,
                t_i))=1$} if and only if\/
                \mbox{$\langle\tau_{\tau,\nu}(t_1),\ldots,
                \tau_{\tau,\nu}(t_i)\rangle\in\rho(P)$}
        \item \mbox{$\rho_{\tau,\nu}(A\land B)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu}(A)=1$} and\/
                \mbox{$\rho_{\tau,\nu}(B)=1$}
        \item \mbox{$\rho_{\tau,\nu}(A\lor B)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu}(A)=1$} or\/
                \mbox{$\rho_{\tau,\nu}(B)=1$}
        \item \mbox{$\rho_{\tau,\nu}(A\limplies B)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu}(A)=0$} or\/
                \mbox{$\rho_{\tau,\nu}(B)=1$}
        \item \mbox{$\rho_{\tau,\nu}(\lnot A)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu}(A)=0$}
        \item \mbox{$\rho_{\tau,\nu}(\exists x\quantsep A)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu^\prime}(A)=1$}
                for some\/ $\nu^\prime$ such that\/ \mbox{$y\neq x$} implies\/
                \mbox{$\nu(y)=\nu^\prime(y)$}
        \item \mbox{$\rho_{\tau,\nu}(\forall x\quantsep A)=1$} if and only if\/
                \mbox{$\rho_{\tau,\nu^\prime}(A)=1$}
                for all\/ $\nu^\prime$ such that\/ \mbox{$y\neq x$} implies\/
                \mbox{$\nu(y)=\nu^\prime(y)$}
\end{enumerate}
\end{definition}
\subind{First-Order Predicate Calculus!semantic system}
\subind{semantic system!FOPC}
Now, we may define an appropriate semantic system for FOPC.
\begin{definition}\label{def:FOPC-semantic-system}
\notind{$\Pmodels$ (FOPC truth relation)}
The classical semantic system for FOPC is\/
\mbox{$\langle\mathbold{F}_P,\mathbold{M}_P,\Pmodels\rangle$}, where\/
\mbox{$\langle U,\tau,\rho\rangle\Pmodels F$} if and only if\/
\mbox{$\rho_{\tau,\nu}(F)=1$} for all variable assignments\/ $\nu$
over\/ $U$.
\end{definition}

\subind{bound variable|(}
\subind{free variable|(}
FOPC is particularly well suited to defining relations, letting
variables stand for the parameters in the relations. For such
purposes, it is important to distinguish between uses of variables
that are {\em bound\/} by the quantifiers\subind{quantifier} $\exists$
and $\forall$, and those that are {\em free\/} to be used as
relational parameters.
\begin{definition}[\cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}
\auind{Kleene, S. C.}\auind{Gallier, J. H.}]\label{def:free-variable}
An occurrence of a variable\/ $x$ in a formula is\/ {\em bound\/} if
and only if it is located within a subformula of the form\/ \mbox{$(\exists
x\quantsep F)$} or the form\/ \mbox{$(\forall x\quantsep F)$}. 
An occurrence of a variable\/ $x$ in a formula is\/ {\em free\/}
if and only if it is not bound.
\subind{bound variable|)}

A\/ {\em sentence\/}\subind{sentence} is a formula with no free
occurrences of variables. If\/ \mbox{$F\in\mathbold{F}_P$} is a
formula, and all free occurrences of variables in\/ $F$ are among\/
\mbox{$x_1,\ldots,x_i$}, then the sentence\/ \mbox{$(\forall
x_1\quantsep\cdots\forall x_i\quantsep F)$} is a\/ {\em
closure\/}\subind{closure of formula} of\/ $F$.  It is easy to see
that\/ $F$ is semantically equivalent to each of its closures.

Let\/ \mbox{$x_1,\ldots,x_i$} be a list of variables with no
repetitions, and let\/ \mbox{$t_1,\ldots,t_i\in\mathbold{T}_P$}.
$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$\notind{$\subst{t}{x}{F}$
(substitution)}\subind{substitution} is the formula that results
from substituting the term\/ $t_j$ for every free occurrence of the
variable\/ $x_j$ in the formula\/ $F$, for each\/ $j$, $1\leq j\leq
i$, renaming bound variables of\/ $F$ when necessary so that the
variables of\/ $t_1,\ldots,t_i$ are free\subind{free variable|)} in
the result \cite{Andrews,Kleene,Gallier}\auind{Andrews, P. B.}
\auind{Kleene, S. C.}\auind{Gallier, J. H.}.  When\/
\mbox{$G=\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$}, we say that\/
$G$ is an\/ {\em instance\/}\subind{instance} of\/ $F$, and that\/ $F$
is\/ {\em more general\/}\subind{generality} than\/ $G$. These
relations apply naturally to terms as well as formulae.

$G$ is a\/ {\em variable renaming\/}\subind{variable renaming}
of $F$ if and only if\/
\mbox{$G=\subst{y_1,\ldots,y_i}{x_1,\ldots,x_i}{F}$}, for some list of
variables\/ \mbox{$y_1,\ldots,y_i$} with no repetitions (equivalently,
$G$ is an instance of\/ $F$ and\/ $F$ is an instance of\/ $G$, since
we get\/ \mbox{$F=\subst{x_1,\ldots,x_i}{y_1,\ldots,y_i}{G}$}).
\end{definition}
\subind{what question@`what' question|(}
\subind{question!what@`what'|(}\subind{question!FOPC|(}
\subind{First-Order Predicate Calculus!question|(}
\subind{query system!FOPC|(}\subind{query system!what@`what'|(}
It is very natural to think of a query system in which we may ask what
substitutions for the free variables of a formula make it true.
\auind{Belnap, N. D.}\auind{Steel, T. B.}
\begin{definition}[\cite{Belnap-Steel}]\label{def:FOPC-query-system}
\auind{Belnap, N. D.}\auind{Steel, T. B.}
\notind{$\what$ (`what' question)}
\notind{$\mathbold{Q}_P$ (`what' questions)}
\notind{$\answers_P$ (`what' answer relation)}
Let\/ $\what$ be a new formal symbol. Let $$\mathbold{Q}_P=\{(\what
x_1,\ldots,x_i\quantsep F)\setsep F\in\mathbold{F}_P\}$$ Define the
relation\/ \mbox{$\answers_P\subseteq\mathbold{Q}_P\times\mathbold{F}_P$} by
$$(\what x_1,\ldots,x_i\quantsep F)\answers_P G$$ if and only if
$$G=\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}\mbox{ for some\/
}t_1,\ldots,t_i\in\mathbold{T}_P$$

Now\/ \mbox{$\langle\mathbold{F}_P,\mathbold{Q}_P,\answers_P\rangle$} is a query
system representing the conceivable single answers to questions of the
form `for what terms\/ $t_1,\ldots,t_i$ does\/
$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$ hold?'
\end{definition}
\subind{semicomputable|(}
The query system above has a crucial role in the profound theoretical
connections between logic and computation. For each finite (or even
semicomputable) set \mbox{$\mathbold{T}\subseteq\mathbold{F}_P$} of
formulae, and each question \mbox{$Q=(\what x_1,\ldots,x_i\quantsep
F)$}, the set $$\{\langle t_1,\ldots,t_i\rangle\setsep
Q\answers_P\mathbold{T}\models_P\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}\}$$
is semicomputable. If we use some constant symbol
\mbox{$c\in\mbox{\bf Fun}_0$} to represent the number $0$, some
unary function symbol \mbox{$f\in\mbox{\bf Fun}_1$} to represent the
successor function, and some binary predicate symbol $E$ to represent
the equality relation, then we may define all semicomputable sets of
integers by formulae in a simple and natural way. We let
\mbox{$\mathbold{R}\subseteq\mathbold{F}_P$} be a finite set of postulates
for {\em Robinson's Arithmetic\/}\subind{Robinson's Arithmetic}
(system $Q$ of \cite{Mostowski})\auind{Mostowski, A.}\auind{Tarski,
A.}\auind{Robinson, R. M.}---a primitive theory sufficient for
deriving answers to all addition and multiplication problems. Then
{\em every\/} semicomputable set is of the form $$\{j\setsep (\what
x\quantsep F)\answers_P\mathbold{R}\models_P\subst{f^j(c)}{x}{F}\}$$
for some formula
\mbox{$F\in\mathbold{F}_P$}.  Similarly, every partial computable function
$\phi$ may be defined by choosing an appropriate formula
\mbox{$F\in\mathbold{F}_P$}, and letting $\phi(i)$ be the unique number $j$
such that
$$(\what y\quantsep\subst{f^i(c)}{x}{F})\answers_P
\mathbold{R}\models_P\subst{f^i(c),f^j(c)}{x,y}{F}$$
\subind{semicomputable|)}

\subind{tautological answer|(}\subind{answer!tautological|(}
Notice that the FOPC questions \mbox{$(\what x_1,\ldots,x_i\quantsep
F)$} do not allow trivial tautological answers, such as the correct answer
\mbox{$(a\limplies a)$} to the question \mbox{$\mbox{\bf imp}(a)$}
(`what atomic formula does $a$ imply?',
Example~\ref{exa:query-system-1}, Section~\ref{sec:query-systems}).
In fact, \mbox{$(\what x_1,\ldots,x_i\quantsep F)$} has a tautological
answer if and only if $F$ is a tautology. FOPC questions avoid this
problem through the distinction between predicate symbols and function
symbols. When we try to find an answer
\mbox{$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$} to the question
\mbox{$(\what x_1,\ldots,x_i\quantsep F)$},
the information in the question \mbox{$(\what x_1,\ldots,x_i\quantsep
F)$} is carried largely through predicate symbols, while the
information in the answer
\mbox{$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$} is carried entirely
by the function symbols in $t_1,\ldots,t_i$, since the predicate
symbols in the formula $F$ are already fixed by the question. It is
the syntactic incompatibility between the formula given in the
question and the terms substituted in by the answer that prevents
tautological answers. Suppose that FOPC were extended with a symbol
$\mbox{\bf choose}$\notind{$\mbox{\bf choose}\:x\quantsep$},
where \mbox{$(\mbox{\bf choose}\:x\quantsep F)$}
is a term such that \mbox{$(\exists x\quantsep F)$} implies
\mbox{$\subst{(\mbox{\bf choose}\:x\quantsep F)}{x}{F}$}. Then
\mbox{$\subst{(\mbox{\bf choose}\:x\quantsep F)}{x}{F}$} would be a
trivially (but not quite tautologically) correct answer to
\mbox{$(\what x\quantsep F)$} except when no correct answer exists.
\subind{tautological answer|)}\subind{answer!tautological|)}

The absence of trivial tautological answers does {\em not\/} mean that
all answers to FOPC questions are equally useful. In some cases a
question has a most general semantically correct answer. This
provides a nice syntactic way to recognize certain consequentially
strongest answers, and a useful characterization of all answers even
when there is no consequentially strongest answer.
\begin{proposition}\label{pro:instance-consequence}
\subind{instance}
If\/ $G^\prime$ is an instance of\/ $G$, then\/ $G^\prime$ is a
semantic consequence of\/ $G$ (\/\mbox{$G\models_P G^\prime$}). It
follows immediately that if\/ $G$ is a semantically correct answer
to\/ \mbox{$Q\in\mathbold{Q}_P$} (\/\mbox{$Q\answers_P\mathbold{T}\models_P G$}),
then\/ $G^\prime$ is also a semantically correct answer\/
(\/\mbox{$Q\answers_P\mathbold{T}\models_P G^\prime$}).

\subind{variable renaming}
If\/ $G^\prime$ is a variable renaming of\/ $G$, then they are
semantically equivalent.
\end{proposition}
\subind{most general answer|(}
\begin{definition}\label{def:most-general}
Let\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}_P$} be a set of
formulae, and let\/ \mbox{$Q=(\what x_1,\ldots,x_i\quantsep
F)\in\mathbold{Q}_P$} be a question. $G$ is a\/ {\em most general\/}
answer to\/ $Q$ for explicit knowledge\/ $\mathbold{T}$ if and only if
\begin{enumerate}
        \item \mbox{$Q\answers_P\mathbold{T}\models_P G$}
        \item for all\/ \mbox{$G_0\in\mathbold{F}_P$}, if\/ $G$ is an instance of\/
                $G_0$ and\/ \mbox{$Q\answers_P\mathbold{T}\models_P G_0$},
                then $G_0$ is a variable renaming of\/ $G$.
\end{enumerate}

A set\/ \mbox{$\mathbold{A}\subseteq\mathbold{F}_P$} of formulae is a\/ {\em
most general set\/} of correct answers to\/ $Q$ for\/ $\mathbold{T}$ if and
only if
\begin{enumerate}
        \item each formula\/ \mbox{$F\in\mathbold{A}$} is a most general
                answer to\/ $Q$ for\/ $\mathbold{T}$
        \item for all formulae\/ \mbox{$G\in\mathbold{F}_P$}, if\/
                \mbox{$Q\answers_P\mathbold{T}\models_P G$}, then\/
                $G$ is an instance of some\/ \mbox{$F\in\mathbold{A}$}
        \item for all formulae\/ \mbox{$F_1,F_2\in\mathbold{A}$}, if\/
                $F_2$ is an instance of\/ $F_1$, then \mbox{$F_2=F_1$}
\end{enumerate}
It is easy to see that for each question\/ \mbox{$Q\in\mathbold{Q}_P$} and
set of formulae\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}_P$} there is a most
general set of correct answers (possibly empty or infinite).
Furthermore, the most general set of correct answers is unique up to
variable renaming of its members.
\end{definition}
Notice that it is very easy to generate all correct answers to a
question in $\mathbold{Q}_P$ from the most general set---they are precisely
the instances of its members. If $Q$ has a consequentially strongest
answer, then it has a consequentially strongest answer that is also
most general. If the most general set of correct answers is the
singleton set \mbox{$\{F\}$}, then $F$ is a consequentially strongest answer.
\begin{example}\label{exa:most-general-answer}
Let\/ \mbox{$G\in\mbox{\bf Pred}_2$} be a binary predicate symbol,
where\/ \mbox{$G(t_1,t_2)$} is intended to assert that\/ $t_1$ is
strictly larger than\/ $t_2$. Suppose that objects in the universe
have left and right portions, and that\/ \mbox{$l,r\in\mbox{\bf
Fun}_1$} denote the operations that produce those portions.  A minimal
natural state of knowledge about such a situation is
$$\mathbold{T}_0=\{\forall x\quantsep G(x,l(x))\land G(x,r(x))\}$$ A
natural question is\/ \mbox{$Q=(\what x,y\quantsep G(x,y))$}.  The
most general set of answers is
$$\mathbold{A}_0=\{G(x,l(x)),\:G(x,r(x))\}$$ Other answers include\/
\mbox{$G(l(x),r(l(x)))$}, \mbox{$G(r(x),l(r(x)))$}, etc.

$\mathbold{T}_0$ has only the specific knowledge that a whole is
larger than its portions, but not the general knowledge that the
relation $G$ is a strict ordering relation.  Let
$$\mathbold{T}_1=\mathbold{T}_0\cup\{\forall
x,y,z\quantsep(G(x,y)\land G(y,z))\limplies G(x,z),\;\forall
x,y\quantsep\lnot(G(x,y)\land G(y,x))\}$$ For this extended knowledge,
the most general set of answers to $Q$ is the infinite set
$$\mathbold{A}_1=\mathbold{A}_0\cup\{G(x,l(l(x))),\:
G(x,l(r(x))),\:G(x,r(r(x))),\:G(x,l(l(l(x)))),\ldots\}$$
The first formula added to\/ $\mathbold{T}_1$ above, which expresses
the transitivity of ordering, leads to the additional answers.
\end{example}
\subind{most general answer|)}

In some cases, it is convenient to allow conjunctions of answers to
questions in $\mathbold{Q}_P$ to be conjoined into a single answer.
\begin{definition}\label{def:FOPC-conj-query-system}
\notind{$\cwhat$ (conjunctive `what' question)}
\subind{conjunctive what question@conjunctive `what' question}
Let\/ $\cwhat$ be a new formal symbol.  Let
$$\mathbold{Q}_{P\land}=\{(\cwhat x_1,\ldots,x_i\quantsep F)\setsep
F\in\mathbold{F}_P\}$$ Define the relation\/
\mbox{$\answers_{P\land}\subseteq\mathbold{Q}_{P\land}\times\mathbold{F}_P$}
by $$(\cwhat x_1,\ldots,x_i\quantsep
F)\answers_{P\land} G$$ if and only if
$$G=\subst{t_1^1,\ldots,t_i^1}{x_1,\ldots,x_i}{F}\land\cdots\land
\subst{t_1^n,\ldots,t_i^n}{x_1,\ldots,x_i}{F}\mbox{ for some\/
}t_1^1,\ldots,t_i^n\in\mathbold{T}_P$$\notind{$\answers_{P\land}$
(conjunctive `what' answer relation)}

Now\/
\mbox{$\langle\mathbold{F}_{P\land},\mathbold{Q}_{P\land},
\answers_{P\land}\rangle$}
is a query system representing the conceivable conjunctive answers to
questions of the form `for what terms\/ $t_1,\ldots,t_i$ does\/
$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{F}$ hold?'
\end{definition}
Answers to \mbox{$(\cwhat x_1,\ldots,x_i\quantsep F)$} are precisely
conjunctions of answers to \mbox{$(\what x_1,\ldots,x_i\quantsep F)$}.
\mbox{$(\cwhat x_1,\ldots,x_i\quantsep F)$} may have a consequentially
strongest answer even though \mbox{$(\what x_1,\ldots,x_i\quantsep F)$} does
not. In particular, whenever the most general set of answers to
\mbox{$(\what x_1,\ldots,x_i\quantsep F)$} is finite, the conjunction of those
answers is a consequentially strongest answer to \mbox{$(\cwhat
x_1,\ldots,x_i\quantsep F)$}.
\subind{First-Order Predicate Calculus|)}
\notind{FOPC (First-Order Predicate Calculus)|)}
\subind{what question@`what' question|)}
\subind{question!what@`what'|)}\subind{question!FOPC|)}
\subind{First-Order Predicate Calculus!question|)}
\subind{query system!FOPC|)}\subind{query system!what@`what'|)}

\subsubsection{Prolog}
\label{sec:prolog}

\subind{Prolog|(} \subind{Horn clause|(} The most famous programming
language associated with logic programming, and the one that
instigated scientists to study logic programming as a specialty within
computer science, is
Prolog \cite{Kowalski-predicate,vanEmden-Kowalski}\auind{van Emden, M.
H.}, the creation of Kowalski\auind{Kowalski, R.} and
Colmerauer\auind{Colmerauer, A.}.  The name `Prolog' is usually
associated with a group of very similar programming languages based on
logic programming in Horn clauses---a particular sublanguage of the
First-Order Predicate Calculus. Prolog as it is actually used deviates
from pure logic programming in several ways: it fails to produce some
logically entailed answers; in rare cases it produces logically
incorrect answers; and it contains constructs that are not definable
naturally in FOPC, and which are normally understood in conventional
imperative ways. Furthermore, the criteria by which Prolog chooses one
of several possible answers cannot be explained naturally in terms of
the semantics of FOPC. The discrepancy between Prolog and Horn-clause
logic programming is closely comparable to the discrepancy between
Lisp and the purely functional language based on the lambda calculus
that is sometimes called `pure lazy Lisp.' In spite of the
discrepancies, the best way to understand Prolog is to conceive of it
as an approximation to, and extension of, a Horn-clause logic
programming language.

The essential idea behind Prolog is to find correct answers to
predicate calculus questions in $\mathbold{Q}_P$ of
Section~\ref{sec:fopc} above. In principle, all such answers are
computable. Currently known implementation techniques require fairly
stringent conditions on the sets of formulae that may be used as
explicit knowledge for question answering, and on the questions that
may be asked, in order to search for and generate proofs in a
relatively simple and disciplined way. Prolog is based on the
restriction of programs to sets of {\em Horn clauses,} and questions
to simple conjunctions of positive atomic formulae.
\begin{definition}\label{def:horn-clause}
\subind{Prolog!program}
\subind{clause}
A formula\/ \mbox{$F\in\mathbold{F}_P$} is a\/ {\em Horn clause\/} if and only
if it is in one of the forms
\begin{enumerate}
        \item\label{enu:head-tail}
                \mbox{$F=(R_1(t_{1,1},\ldots,t_{1,i_1})\land\cdots\land
                R_m(t_{m,1},\ldots,t_{m,i_m})\limplies P(u_1,\ldots,u_j))$}
        \item\label{enu:tail}
                \mbox{$F=(R_1(t_{1,1},\ldots,t_{1,i_1})\land\cdots\land
                R_m(t_{m,1},\ldots,t_{m,i_m})\limplies\mbox{False})$}
        \item\label{enu:head}
                \mbox{$F=(\mbox{True}\limplies P(u_1,\ldots,u_j))$}
        \item\label{enu:false}
                \mbox{$F=(\mbox{True}\limplies\mbox{False})$}
\end{enumerate}
where\/ \mbox{$R_1,\ldots,R_m,P$} are predicate symbols, and\/
\mbox{$t_{1,1},\ldots,t_{m,i_m},u_1,\ldots,u_j$} are terms.

A\/ {\em pure Prolog program\/} is a finite set of Horn clauses.

\subind{Prolog!input}
A\/ {\em pure Prolog input\/} is a question of the form $$(
\what x_1,\ldots,x_i\quantsep
P_1(t_{1,1},\ldots,t_{1,i_1})\land\cdots\land
P_m(t_{m,1},\ldots,t_{m,i_m}))$$ where\/ $x_1,\ldots,x_i$ are
precisely the free variables of\/
\mbox{$P_1(t_{1,1},\ldots,t_{1,i_1})\land\cdots\land
P_m(t_{m,1},\ldots,t_{m,i_m})$}.
\end{definition}
In order to promote readability of programs, within the limitations of
older keyboards and printers, typical Prolog implementations replace
the conventional logical symbol `$\land$' by `$;$'\notind{$;$ (Prolog
conjunction)}, they write the arguments to implications in the
reverse of the usual order and replace the symbol `$\limplied$' by
`$\pimplies$'\notind{$\pimplies$ (Prolog implication)}. Also, they
denote the symbol `$\mbox{False}$' in the conclusion of an
implication, and `$\mbox{True}$' in the hypothesis, by the empty
string. Predicate symbols are written in lower case, and variables are
written in upper case. So, the four forms of Horn clause in actual
Prolog programs look like
\begin{enumerate}
        \item \mbox{$p(u_1,\ldots,u_j)\pimplies r_1(t_{1,1},
                \ldots,t_{1,i_1});\cdots ;
                r_m(t_{m,1},\ldots,t_{m,i_m})$}
        \item \mbox{$\pimplies r_1(t_{1,1},\ldots,t_{1,i_1});\cdots ;
                r_m(t_{m,1},\ldots,t_{m,i_m})$}
        \item \mbox{$p(u_1,\ldots,u_j)\pimplies$}
        \item \mbox{$\pimplies$}
\end{enumerate}
\subind{Horn clause|)}
Since a question always requests substitutions for all free variables,
the header `\mbox{$\what x_1,\ldots,x_i$}' is omitted and the
question is abbreviated in the form
$$r_1(t_{1,1},\ldots,t_{1,i_1});\cdots
;r_m(t_{m,1},\ldots,t_{m,i_m})$$ Since the substitution in an answer
of the form $$\subst{s_1,\ldots,s_i}{x_1,\ldots,x_i}{(R_1(t_{1,1},
\ldots,t_{1,i_1})\land\cdots\land R_m(t_{m,1},\ldots,t_{m,i_m}))}$$
completely determines the answer, actual Prolog output presents only
the substitution, in the form $$x_1=s_1;\cdots;x_i=s_i$$ These
notational variations and abbreviations have a substantial impact on
the way Prolog programs, inputs, and outputs {\em look,} but they
are completely transparent to the logical meaning.

When a pure Prolog input is presented to a pure Prolog program, all
possible answers may be derived systematically by treating each clause
of form~\ref{enu:head-tail} as a recursive part of a definition of the
procedure $P$ in terms of calls to the procedures
\mbox{$R_1,\ldots,R_m$}. Because the same predicate symbol $P$ may
appear in the conclusion of more than one clause, each clause normally
provides only a part of the definition of $P$. Clauses of
form~\ref{enu:head} are nonrecursive parts of the definition of a
procedure $P$. Clauses of form~\ref{enu:tail} are somewhat peculiar:
they act like extra hardcoded parts of the input. Clauses of
form~\ref{enu:false} are useless in programs, but allowed by the
formal definition. Different implementations may or may not prohibit
the degenerate forms. Prolog tries to choose more general answers
instead of their instances, but it does not guarantee that all answers
produced are most general. An understanding of the precise
correspondence of Prolog to the answering of pure Prolog input
questions using pure Prolog programs requires a lot of detail that
must wait until the chapter `Horn Clause Logic Programming.'

\subind{LambdaProlog|(}\subind{$\lambda$Prolog|(} A notable variation
on Prolog is $\lambda$Prolog
\cite{Nadathur-Miller-higher,Nadathur-Miller-lambda}.
\auind{Nadathur, G.}\auind{Miller, D.} This language extends Predicate
Calculus logic programming into the {\em Omega-Order Predicate
Calculus,}\subind{Omega-Order Predicate Calculus} also called {\em
Type Theory\/} \cite{Andrews}\auind{Andrews, P. B.}\subind{Type
Theory}. Higher-order predicate calculi add variables ranging over
predicates, quantification over such variables, and predicates that
apply to other predicates. $\lambda$Prolog generalizes the Horn clauses
of FOPC to the hereditary Harrop formulae\subind{hereditary Harrop
formula}\subind{Harrop formula!hereditary}
of the Omega-Order Predicate calculus
\cite{Miller-Nadathur-Pfenning-Scedrov}\auind{Pfenning, F.}\auind{Scedrov, A.}.
\subind{LambdaProlog|)}\subind{$\lambda$Prolog|)}\subind{Prolog|)}

\subsubsection{Relational Databases and Datalog}
\label{sec:relational-database}

\subind{relational database|(} \subind{Datalog|(} Relational databases
\cite{Date,Codd-model}\auind{Date, C. J.} were invented by
Codd\auind{Codd, E. F.}, completely independently of the development
of Prolog and logic programming in the programming language community.
Nonetheless, relational databases and their queries may be understood
very naturally in terms of logic programming concepts. This point has
been noted by the Prolog community, leading to the definition of
Datalog \cite{Maier-Warren}\auind{Maier, D.}\auind{Warren, D. S.}, a
variant of relational databases in the style of Prolog.
Gallaire\auind{Gallaire, H.}, Minker\auind{Minker, J.}, and
Nicolas\auind{Nicolas, J. M.} have developed the concept of {\em
deductive databases\/}
\cite{Gallaire-Minker-Nicolas}\subind{deductive database} to capture
the logical content of relational databases and their variants. Reiter
\cite{Reiter-towards}\auind{Reiter, R.} has shown how a logical view
of databases has advantages of robustness under several useful
generalizations of database functionality. My proposed approach to
logic programming applies logic to programming languages in
essentially the same way that Reiter applies logic to databases.

Like Prolog, relational database systems find correct answers to
predicate calculus questions in $\mathbold{Q}_P$
\subind{what question@`what' question}\subind{question!what@`what'}
of Section~\ref{sec:fopc}. The different natural
assumptions and performance requirements of the database world lead to
far more stringent restrictions on the sets of formulae that may be
used for question answering. The questions, which correspond to
database queries, are essentially unrestricted.  Because of the
stringent restrictions on knowledge formulae, which limit answers to a
predetermined finite set of possibilities, actual relational database
implementations do not deviate from pure logic programming, except by
offering constructs that go beyond the logical definitions. On purely
relational queries, they produce precisely all of the semantically
correct answers.\subind{relational database!contents|(}
\begin{definition}\label{def:relational-database}
A\/ {\em pure relational database\/} is a finite set of formulae of
the form\/ \mbox{$P(c_1,\ldots,c_i)$}, where\/ \mbox{$P\in\mbox{\bf
Pred}_i$} is a predicate symbol and\/
\mbox{$c_1,\ldots,c_i\in\mbox{\bf Fun}_0$} are constant symbols.
\end{definition}
A pure relational database as defined above is the natural logical
view of the contents of a relational database system at any given
time. The constant symbols are the objects that may appear in fields
of relations in the database. Each predicate symbol represents one of
the relations in the database. Each formula \mbox{$P(c_1,\ldots,c_i)$}
represents the presence of the tuple \mbox{$\langle
c_1,\ldots,c_i\rangle$} in the relation $P$.
\subind{relational database!contents|)}

\subind{relational database!query|(} Pure relational database query
languages are equivalent to $\mathbold{Q}_{P}$---all queries of the
form \mbox{$(\what x_1,\ldots,x_i\quantsep F)$} are
allowed.\subind{what question@`what' question}
\subind{question!what@`what'}
Because of the simplicity of the formulae in the database,
restrictions on the queries are not required for tractable
implementation. Notice the complementarity of Prolog and relational
database query languages.  Prolog allows relatively powerful Horn
clauses as knowledge formulae, but restricts queries to conjunctions
of atomic formulae. Relational database query languages restrict
knowledge formulae to the very simple form of predicate symbols
applied to constant symbols, but allow unrestricted FOPC $\what$
queries.

The simplicity of the formulae in a pure relational database
guarantees that the set of answers to \mbox{$(\what
x_1,\ldots,x_i\quantsep F)$} is finite, and relational database query
systems actually produce {\em all\/} the semantically correct answers.
Equivalently, we may think of a relational database query system as
producing the consequentially strongest answer (unique up to the order
of the conjuncts) to \mbox{$(\cwhat x_1,\ldots,x_i\quantsep F)$}. The
consequentially strongest answer to the $\cwhat$
\subind{conjunctive what question@conjunctive `what' question}
form of the question is simply the conjunction of
all the answers to the $\what$\subind{what question@`what' question}
\subind{question!what@`what'}
form.

Datalog restricts queries to the Prolog form, but allows
Horn clauses with no function symbols (no `functors' in Prolog
jargon) to be added to the formulae of the database to provide
additional knowledge for the purpose of answering a given query. The
Horn clauses are thought of as defining new relations to be used in
the query, rather than as adding information to the database.

\subind{DSL ALPHA|(} A variety of notations have been used for the
expression of FOPC queries in relational database systems. These
variant notations may look very different from FOPC at first glance,
but in fact they are equivalent in querying power. The complete
translations between notations are clumsy to define formally, so we
consider the general principles behind the notation, and illustrate
the translation with examples. I use Codd's\auind{Codd, E. F.}
language DSL ALPHA \cite{Date,Codd-sublanguage}, \auind{Date, C. J.}
often called {\em relational calculus,}\subind{relational calculus}
for the database notation.

Instead of referring directly to objects in the universe
$\mathbold{U}$, relational database languages generally refer to
tuples in relations, because they correspond to records in a
conventional file. Instead of the positional notation
\mbox{$P(t_1,\ldots,t_i)$}, they give {\em domain
names\/}\subind{domain!relational database} $D_1,\ldots,D_i$ to the
parameter positions. The name of a relation (predicate
symbol)\subind{predicate symbol} is treated as a variable ranging over
the set of tuples in that relation. The value of the domain $D$ in an
arbitrary tuple of the relation $P$ is denoted by the
record\subind{record} notation
\mbox{$P.D$}. \mbox{$P.D=c$} means that the value in the domain $D$
of an unknown tuple in the relation $P$ is $c$, and
\mbox{$P.D=Q.E$} means that the value in the domain $D$ of some tuple
in $P$ is the same as that in domain $E$ of some tuple in $Q$.
Because of the absence of function symbols with arity greater than
$0$, this use of equality does not introduce the general capabilities
of FOPC with equality, it merely captures the limited sort of equality
information that is represented in pure FOPC by multiple occurrences
of constants and variables. For example, if $P$ and $Q$ are binary
predicates and $D,E,F,G$ are appropriate domain names, then the DSL
ALPHA expression $$P.D=c\land P.E=Q.F\land Q.G=d$$ is equivalent to
the FOPC formula $$P(c,x)\land Q(x,d)$$

Additional variables may be declared in DSL ALPHA to range over the
tuples of a relation in the database, and these variables may be
quantified with $\forall$ and $\exists$. So, in the presence of the
declarations
\notind{$\coddrange$ (DSL ALPHA declaration)}
\begin{eqnarray*}
\coddrange X\; P\\
\coddrange Y\; Q
\end{eqnarray*}
which declare the variable $X$ to range over tuples of the relation
$P$ and $Y$ to range over tuples of $Q$, the expression $$\forall
X(X.D=c\lor\exists Y(X.E=Y.F\land Y.G=d))$$ is equivalent to the FOPC
formula $$\forall x\quantsep(P(c,x)\lor Q(x,d))$$ Notice that the
existential quantifier in the DSL ALPHA expression is left out of the
FOPC formula, because one of its components is bound to the constant
$d$, and the other to the $E$ component of the variable $X$, whose
quantification occurs before that of $Y$. In general, a FOPC
quantifier is required for each domain position of a quantified tuple
in a DSL ALPHA expression that is not bound by equality either to a
constant or to a component of a variable that has already been
quantified. With the same $\coddrange$ declarations above, the DSL
ALPHA expression $$\forall X\exists Y(X.D=Y.G)$$ is equivalent to the
FOPC formula $$\forall x_1\quantsep\forall x_2\quantsep
P(x_1,x_2)\limplies\exists y\quantsep Q(y,x_1)$$ So, there are some
syntactic subtleties in translating quantification from DSL ALPHA into
FOPC, but they are all solvable with sufficient care.

There is one semantic problem that prevents DSL ALPHA from expressing
everything that can be expressed by FOPC formulae with only $0$-ary
function symbols. That is the limitation of the range of quantified
variables in DSL ALPHA to the set of tuples actually occurring in a
relation in the database, while FOPC may quantify over an abstract
universe $\mathbold{U}$. There is no expression in DSL ALPHA
semantically equivalent to \mbox{$\forall x\quantsep P(x)$}, since DSL
ALPHA can only express the fact that every object in a tuple of the
database satisfies the predicate $P$. Because these objects are
exactly those mentioned by the knowledge formulae, however, the
restricted quantification of DSL ALPHA yields the same answers to
queries as the unrestricted quantification of FOPC, so in terms of the
behavior of query-answering systems the notations are equivalent.
Another way of viewing this semantic difference is to suppose that
each database implicitly contains a {\em closed world
assumption\/} \cite{Reiter-closed}\auind{Reiter, R.} \subind{closed
world assumption} expressing the fact that only the objects
mentioned in the database exist. In FOPC with equality, the closed
world assumption may be expressed by the formula \mbox{$\forall
x\quantsep x\formeq c_0\lor\cdots\lor x\formeq c_n$}, where
$c_0,\ldots,c_n$ are all of the constant symbols appearing in the
database. Without equality, we can only express the fact that every
object acts just like one of $c_0,\ldots,c_n$ (i.e., it satisfies
exactly the same formulae), and even that requires an infinite number
of formulae.

\subind{DSL ALPHA!query|(}
Given the translation of DSL ALPHA expressions to FOPC formulae
suggested above, we may translate DSL ALPHA queries into FOPC
questions. DSL ALPHA queries have the general form $$\coddget Q
(P_1.D_1,\ldots,P_i.D_i)\coddsep E$$ where $P_1,\ldots,P_i$ are
relations in the database, $Q$ is a new relational symbol not
occurring in the database, $D_1,\ldots,D_i$ are domain names, and $E$
is an expression.  Appropriate declarations of the ranges of variables
in $E$ must be given before the query.  Let $F$ be a FOPC formula
equivalent to $E$, using the variables $x_1,\ldots,x_i$ for the values
$P_1.D_1,\ldots,P_i.D_i$.  Then, the effect of the DSL ALPHA query
above is to assign to $Q$ the relation (set of tuples) answering the
question $$\what x_1,\ldots,x_i\quantsep F$$ That is, $$Q=\{\langle
c_1,\ldots,c_i\rangle\setsep(\what x_1,\ldots,x_i\quantsep
F)\answers_P\mathbold{D}\models_P\subst{c_1,\ldots,c_i}{x_1,\ldots,x_i}{F}\}$$
where $\mathbold{D}$ is the set of formulae in the database.  Equivalently,
the value of $Q$ may be thought of as an abbreviation for the
consequentially strongest answer to \mbox{$\cwhat
x_1,\ldots,x_i\quantsep F$} for $\mathbold{D}$, which is just the
conjunction of all the answers to
\mbox{$\what x_1,\ldots,x_i\quantsep F$}.
\subind{DSL ALPHA!query|(}

Another type of notation for relational database queries avoids
explicit quantification entirely, and uses the relational operations
of {\em projection, join,} etc. to define new relations from those in
the database. Notation in the style of DSL ALPHA above is called {\em
relational calculus,}\subind{relational calculus} because of the
similarity to Predicate Calculus in the use of explicit
quantification. The alternate approach through operations on relations
is called {\em relational algebra,}\subind{relational algebra} because
the equations that express the properties of the relational operations
resemble well-known definitions of algebras. In fact, each notation
has its own algebra and its own calculus, and the difference is just
the way in which relations are denoted. Most recent work on relational
databases refers to the relational algebra notation, which looks even
more distant from FOPC than the relational calculus notation, but is
still easily translatable into FOPC.
See \cite{Date,Codd-complete}\auind{Date, C. J.}\auind{Codd, E. F.}
for a description of relational algebra notation for database
queries, and a translation to the relational calculus notation.
\subind{relational database!query|)}
\subind{DSL ALPHA|)}
\subind{relational database|)}
\subind{Datalog|)}

\subsubsection[Equational Logic]{Programming in Equational Logic}
\label{sec:equational-logic}

\subind{equational logic|(}\subind{equations|(}
Another natural logical system in which to program is Equational
Logic. A large number of programming languages may be viewed
essentially as different restrictions of programming in Equational
Logic.
\begin{definition}\label{def:equation-formula}
Let the set $\mathbold{V}$ of variables, the sets $\mbox{\bf
Fun}_0,\mbox{\bf Fun}_1,\ldots$ of constant and function symbols, and
the set $\mathbold{T}_P$ of terms be the same as in FOPC (see
Definition~\ref{def:FOPC-formula}). Let $\formeq$\notind{$\formeq$
(formal equality symbol)} be a new formal symbol (we add the dot to
distinguish between the formal symbol for equality in our language and
the meaningful equality symbol $=$\notind{$=$ (metalanguage equality)}
used in discussing the language). The set\/
$\mathbold{F}_{\formeq}$\notind{$\mathbold{F}_{\formeq}$ (equational
formulae)} of\/ {\em equational formulae\/}\subind{equational
formula}\subind{formula!equational} (or simply\/ {\em
equations\/}\subind{equation}) is
$$\mathbold{F}_{\formeq}=\{t_1\formeq t_2\setsep
t_1,t_2\in\mathbold{T}_P\}$$\notind{$\formeq$ (formal equality symbol)}
\end{definition}
\subind{model!equational|(}\subind{equational logic!model|(}
Models for Equational Logic are the same as models for FOPC, omitting
the predicate assignments. Although $\formeq$\notind{$\formeq$ (formal
equality symbol)} behaves like a special
binary predicate symbol, it is given a fixed meaning (as are $\land$,
$\lor$, $\lnot$, $\limplies$, $\exists$, $\forall$), so it need not be
specified in each model. An equational formula \mbox{$t_1\formeq
t_2$} holds in a model precisely when $t_1$ denotes the same object as
$t_2$ for every variable assignment.
\begin{definition}
\label{def:equation-semantic-system}
\subind{semantic system!equational}\subind{equational
logic!semantic system}
Let the infinite universe\/ $\mathbold{U}$ and the set of function
assignments be the same as in FOPC
(Definition~\ref{def:FOPC-semantic-system}). If\/
\mbox{$U\subseteq\mathbold{U}$} and $\tau$ is a function assignment over\/
$U$, then\/
\mbox{$\langle U,\tau\rangle$} is a\/ {\em model of Equational Logic.}
$\mathbold{M}_{\formeq}$ is the set of all models of Equational Logic.

Let the set of variable assignments be the same as in FOPC
(Definition~\ref{def:FOPC-model}), as well as the definition of a term
valuation\/ $\tau_\nu$ from a function assignment\/ $\tau$ and
variable assignment\/ $\nu$ (Definition~\ref{def:FOPC-valuation}).
The classical semantic system for Equational Logic is\/
\mbox{$\langle\mathbold{F}_{\formeq},\mathbold{M}_{\formeq},\Emodels\rangle$},
where\/ \mbox{$\langle U,\tau\rangle\Emodels t_1\formeq t_2$} if and
only if\/
\mbox{$\tau_\nu(t_1)=\tau_\nu(t_2)$} for all variable assignments\/
$\nu$ over $U$.
\end{definition}
Models of Equational Logic are essentially {\em algebras\/}
\cite{Cohn,Graetzer,MacLane-Birkhoff}\auind{Cohn, P. M.}\auind{Gr\"atzer, G.}
\auind{MacLane, S.}\auind{Birkhoff, G.}\subind{algebra}. The only
difference is that algebras are restricted to {\em
signatures\/}\subind{signature}---subsets, usually finite, of the
set of constant and function symbols. Such restriction does not affect
any of the properties discussed in this chapter. If $\mathbold{T}$ is
a finite subset of $\mathbold{T}_{\formeq}$, then the set of algebras
\mbox{$\modelfunc(\mathbold{T})$} (restricted, of course, to an
appropriate signature) is called a {\em variety.}\subind{variety} For
example, the {\em monoids\/}\subind{monoid} are the models of
\mbox{$\{m(x,m(y,z))\formeq m(m(x,y),z),\;m(x,e)\formeq
x,\;m(e,x)\formeq e\}$} restricted to the signature with one
constant symbol $e$ and one binary function symbol $m$.
\subind{model!equational|)}\subind{equational logic!model|)}

\subind{equational query system|(}\subind{equational logic!query system|(}
\subind{query system!equational|(}
\subind{equational question|(}\subind{question!equational|(}
Perhaps the simplest sort of question that is naturally answered by an
equation is `what is $t_0$?' for a term $t_0$. For each term $t_1$,
the equation $t_0\formeq t_1$ is an answer to this question.  The
trouble with such a primitive question is that it admits too many
answers. For example, the tautology $t_0\formeq t_0$ is always a
correct answer to `what is $t_0$?'.\subind{tautological
answer}\subind{answer!tautological} This problem is closely analogous
to the problem of the tautological answer \mbox{$(a\limplies a)$} to
the question \mbox{$\mbox{\bf imp}(a)$} (`what atomic formula does $a$
imply?', Example~\ref{exa:query-system-1},
Section~\ref{sec:query-systems}). For the Shallow Implicational
Calculus, we avoided undesired answers simply by listing a set
$\mathbold{A}$ of them, in the form \mbox{$\mbox{\bf
rest-imp}(a,\mathbold{A})$} (`what atomic formula not in
$\mathbold{A}$ does $a$ imply?', Example~\ref{exa:query-system-2}).
Since the number of terms $t_1$ making \mbox{$t_0\formeq t_1$} true is
generally infinite, we need a finite notation for describing the
prohibited answers. A particularly useful way is to give a finite set
of terms with variables, and prohibit all instances of those terms
from appearing as subterms in an answer term.

\begin{definition}\label{def:term-substitution}
\subind{substitution}\notind{$\subst{t}{x}{s}$ (substitution)}
Let\/ \mbox{$x_1,\ldots,x_i$} be a list of variables with no
repetitions, and let\/ \mbox{$t,t_1,\ldots,t_i\in\mathbold{T}_P$}.
$\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{t}$ is the formula that
results from substituting the term\/ $t_j$ for every occurrence
of the variable\/ $x_j$ in the term\/ $t$, for each\/ $j$, \mbox{$1\leq
j\leq i$}.  When\/
\mbox{$s=\subst{t_1,\ldots,t_i}{x_1,\ldots,x_i}{t}$}, we say that\/
$s$ is an\/ {\em instance\/} of\/ $t$, and that\/ $t$ is\/ {\em more
general\/} than\/ $s$.\subind{instance}\subind{generality}
\end{definition}
The concepts of substitution, instance, and generality for terms are
analogous to the corresponding concepts defined for formulae in
Definition~\ref{def:free-variable}, simplified because all occurrences
of variables in terms are free.
\begin{definition}\label{def:equational-query-system}
Let\/ \mbox{$t_1,\ldots,t_i\in\mathbold{T}_P$} be terms.  A term\/ $s$
is a\/ {\em normal form\/}\subind{normal form} for\/
\mbox{$\{t_1,\ldots,t_i\}$} if and only if no subterm of\/ $s$ is an
instance of a term in\/
\mbox{$\{t_1,\ldots,t_i\}$}.

\notind{$\normalize$ (normal form question)}
Let\/ $\normalize$ be a new formal symbol.  Let
$$\mathbold{Q}_{\formeq}=\{(\normalize t_1,\ldots,t_i\quantsep
t)\setsep
t,t_1,\ldots,t_i\in\mathbold{T}_P\}$$\notind{$\mathbold{Q}_{\formeq}$
(normal form questions)} Define the relation\/
\mbox{$\answers_{\formeq}\subseteq\mathbold{Q}_{\formeq}\times\mathbold{F}_{\formeq}$} by $$(\normalize
t_1,\ldots,t_i\quantsep t)\answers_{\formeq}(s_1\formeq s_2)$$
\notind{$\answers_{\formeq}$ (normal form answer relation)} if and only
if\/ \mbox{$s_1=t$} and\/ $s_2$ is a normal form for
\mbox{$\{t_1,\ldots,t_i\}$}.

Now\/ \mbox{$\langle\mathbold{F}_{\formeq},\mathbold{Q}_{\formeq},\answers_{\formeq}\rangle$} is a query
system representing the answers to questions of the form `what normal
form for\/ $t_1,\ldots,t_i$ is equal to\/ $t$?'
\end{definition}
\subind{equational query system|)}\subind{equational logic!query system|)}
\subind{query system!equational|)}
For every semicomputable set
\mbox{$\mathbold{T}\subseteq\mathbold{F}_{\formeq}$}\subind{semicomputable},
the set of equations \mbox{$(t\formeq s)$} such that
\mbox{$(\normalize t_1,\ldots,t_i\quantsep t)\answers_{\formeq}
\mathbold{T}\models_{\formeq}(t\formeq s)$} is semicomputable.  It is
easy to define a query system with conjunctive equational answers,
similar to the conjunctive FOPC answers of
Definition~\ref{def:FOPC-conj-query-system}. Such a step is most
useful when {\em infinite\/} conjunctions are allowed, so it is
reserved for Section~\ref{sec:inc-inf-IO} of the
chapter `Equational Logic Programming.'
\begin{example}\label{exa:normalize}
Let\/ \mbox{$a\in{\bf Fun}_0$} be a constant symbol representing\/
{\em zero,} let\/ \mbox{$s\in{\bf Fun}_1$} be a unary function symbol
representing the\/ {\em successor\/} function, and let\/
\mbox{$p\in{\bf Fun}_2$} be a binary function symbol representing\/
{\em addition.}  A natural state of knowledge about these symbols is
$$\mathbold{T}=\{p(a,x)\formeq x,\:p(s(x),y)\formeq s(p(x,y))\}$$ A
natural question is\/ \mbox{$(\normalize p(x,y)\quantsep
p(s(s(a)),s(s(s(a)))))$}.  The unique correct answer is\/
\mbox{$(p(s(s(a)),s(s(s(a))))\formeq s(s(s(s(s(a))))))$}. That is,
the answer to the question `what is a term for\/ $2$ plus\/ $3$, not
using the plus operator?' is `$2$ plus\/ $3$ equals $5$.'

Another question, peculiar but formally legitimate, is\/
\mbox{$(\normalize s(s(x)),s(p(x,y))\quantsep s(s(a)))$}. Correct answers
include\/ \mbox{$(s(s(a))\formeq p(s(a),s(a)))$},
\mbox{$(s(s(a))\formeq p(s(a),p(s(a),a)))$}, \mbox{$(s(s(a))\formeq
p(p(s(a),a),s(a)))$}, etc. The answers to this question express\/ $2$
as sums of\/ $1$ and\/ $0$. The simplest form is\/ $1$ plus\/ $1$; all
other forms simply add extraneous\/ $0$s.
\end{example}
Every partial computable function\subind{partial computable function}
$\phi$ may be defined similarly by letting \mbox{$\phi(i)$} be the
unique $j$ such that $$(\normalize t_1,\ldots,t_i\quantsep
f(s^i(a)))\answers_{\formeq}\mathbold{T}\models_{\formeq}(f(s^i(a))\formeq
s^j(a))$$ for appropriately chosen $t_1,\ldots,t_i$ and finite set
$\mathbold{T}$ of equations defining $f$. In principle, we might ask
for most general or consequentially strongest answers to questions in
$\mathbold{Q}_{\formeq}$. In practice, multiple answers to such
questions are usually incomparable.

\subind{solving equations|(}\subind{equality!solving|(}
A more powerful form of equational question answering involves the
solution of equations.
\begin{definition}\label{def:solve-equation}
\notind{$\solve$ (equation solving question)}
\notind{$\answers_{s\formeq}$ (equation solving answer relation)}
\notind{$\mathbold{Q}_{s\formeq}$ (equation solving questions)}
\subind{query system!equation solving}
\subind{equation solving query system}
\subind{equation solving!query system}
Let\/ $\solve$ be a new formal symbol. Let $$\mathbold{Q}_{s\formeq}=\{(\solve
x_1,\ldots,x_i\quantsep t_1\formeq t_2)\setsep t_1,t_2\in\mathbold{T}_P\}$$
Define the relation\/ \mbox{$\answers_{s\formeq}$} by $$(\solve
x_1,\ldots,x_i\quantsep t_1\formeq t_2)\answers_{s\formeq}(s_1\formeq s_2)$$
if and only if there are terms\/ \mbox{$u_1,\ldots,u_i\in\mathbold{T}_P$}
such that\/ \mbox{$s_1=\subst{u_1,\ldots,u_i}{x_1,\ldots,x_i}{t_1}$}
and\/ \mbox{$s_2=\subst{u_1,\ldots,u_i}{x_1,\ldots,x_i}{t_2}$}.

Now\/
\mbox{$\langle\mathbold{Q}_{s=},\mathbold{F}_{\formeq},\answers_{s=}\rangle$}
is a query system representing the answer to questions of the form `what
values of\/ $x_1,\ldots,x_i$ solve the equation\/ \mbox{$t_1\formeq
t_2$}?'
\end{definition}
Notice the close analogy between the question \mbox{$(\solve
x_1,\ldots,x_i\quantsep t_1\formeq t_2)$} above, and the FOPC question
\mbox{$(\what x_1,\ldots,x_i\quantsep F)$} of
Definition~\ref{def:FOPC-query-system}, Section~\ref{sec:fopc}.
Syntactically, the equational question is merely the special case of
the FOPC question where the formula $F$ is restricted to be an
equation. The semantics of Equational Logic lead, however, to very
different typical uses for, and implementations of, equation solving.
\subind{equational question|)}\subind{question!equational|)}

\subsubsection[Functional and Equational Languages]
        {Functional and Equational Programming Languages}
\label{sec:functional-programming}

\subind{functional programming|(}\subind{equational logic
programming|(} A wide variety of nonprocedural programming
languages\subind{nonprocedural programming language} have been
inspired by Backus'\auind{Backus, J.} proposal of {\em functional
programming languages\/} \cite{Backus-red,Backus-turing}
\auind{Backus, J.} defined by equations. The previous development of
Lisp\subind{Lisp} by McCarthy \cite{McCarthy}\auind{McCarthy, J.},
although not originally conceived in terms of functional programming,
fits in retrospect into the functional approach, and its success has
boosted the interest in functional languages substantially. Languages
for the algebraic description of abstract data types
\cite{Guttag-Horning,Wand,Futatsugi-Goguen-Jouannaud-Meseguer}
\subind{abstract data types}
\auind{Guttag, J. V.}\auind{Horning, J. J.}\auind{Wand, M.}
\auind{Futatsugi, K.}\auind{Goguen, J. A.}\auind{Jouannaud, J.-P.}
\auind{Meseguer, J.} use equations in individual programs,
rather than in the language design, and one experimental language is
defined explicitly in terms of equational logic programming
\cite{Hoffmann-O'Donnell-programming,Hoffmann-O'Donnell-Strandh,O'Donnell-MIT}.
\auind{O'Donnell, M. J.}\auind{Hoffmann, C. M.}\auind{Strandh, R. I.}
The essential idea behind functional, algebraic,\subind{algebraic
programming languages} and equational, programming languages is to
find correct answers to normalization questions in
$\mathbold{Q}_{\formeq}$ of Section~\ref{sec:equational-logic}
above. A number of different styles are used to specify these
languages, often obscuring the logic programming content. In this
section, `functional programming languages' include all programming
languages that {\em can be\/} described naturally as answering
normalization questions, and we view them as a form of equational
logic programming, whether or not they are conventionally thought of
in that way. Actual functional languages differ widely on a number of
dimensions:
\begin{itemize}
\item the notation in which terms are written;
\item the way in which the knowledge formulae are determined by the
  language design and the program;
\item the way in which questions are determined by the
  language design, the program, and the input;
\item deviations from pure equational logic programming.
\end{itemize}
Because of the complexity of these variations, the discussion in this
section is organized around the various decisions involved in
designing a functional programming language, rather than around a
survey of the most important languages.

The style in which many functional programming languages are specified
creates an impression that there are fundamental logical differences
between functional programming and equational logic programming. This
impression is false---functional programming and equational logic
programming are two different ways of describing the same behaviors.
The different styles of description may encourage different choices in
language design, but they do {\em not\/} introduce any fundamental
logical deviations. In particular, `higher order'\subind{higher order
programming} functional programming languages are {\em not\/} higher
order in any fundamental logical sense, and may be described very
naturally by first order equational logic
\cite{Goguen-higher}\auind{Goguen, J. A.}. The chapter `Equational
Logic Programming,' Section~\ref{sec:motivation}, provides more
discussion of the connection between functional and equational
programming ideologies.

\paragraph*{Determining Equational Knowledge from Language Design and Program.}

The equational formulae used as explicit knowledge for answering
normalization questions in functional programming languages are
derived from the language design itself and from the program that is
being executed. In principle, they could also be given in the input,
but this possibility has not been exploited explicitly. Many
functional languages are processed by interactive interpreters, which
blur the distinction between program and input, and many functional
languages have mechanisms, such as {\em lambda abstraction\/}
\cite{McCarthy}\auind{McCarthy, J.}\subind{lambda
abstraction}\subind{lambda calculus} or the {\em let\/} construct,
that simulate the introduction of certain equations within an input
term. Interactive interpretive processing, and the simulation of
additional equations within terms, provide implicitly a lot of the
power of explicit equations in the input.

\subind{primitive operations!functional|(}
\subind{functional programming!primitives|(}
Most functional languages are designed around substantial sets of
primitive operations, defined by equations. For example, the
primitives $\cons$\notind{$\cons$ (list constructor)} (construct
ordered pair), $\car$\notind{$\car$ (first projection)} (first
component of pair), and $\cdr$\notind{$\cdr$ (second projection)}
(second component of pair) in Lisp\subind{Lisp} are defined by the two
equations \mbox{$(\car(\cons(x,y))\formeq x)$} and
\mbox{$(\cdr(\cons(x,y))\formeq y)$} \cite{McCarthy}\auind{McCarthy,
J.}. Primitive operators that manipulate term structure, or provide
program control structures, are usually defined by explicitly given
small finite sets of equations. Primitive operators for basic
mathematical operations are defined by large or infinite sets of
equations that must be described rather than listed. For example, the
conventional arithmetic operation of addition is defined by the
equations
\mbox{$\add(0,0)\formeq 0$}, \mbox{$\add(0,1)\formeq 1$},\ldots,
\mbox{$\add(1,0)\formeq 1$}, \mbox{$\add(1,1)\formeq 2$},\ldots,
\mbox{$\add(2,0)\formeq 2$}, \mbox{$\add(2,1)\formeq 3$},
\mbox{$\add(2,2)\formeq 4$},\ldots

Most functional programming languages have rich enough
primitive sets of operators defined by equations in the language
design that it is not necessary to introduce new equations in a
program---the goals of the program may be accomplished by appropriate
combinations of primitive operations. In particular, many
functional languages have operators that simulate the
introduction of additional local equations within a term. Even in
languages with powerful primitives, it is often convenient to
introduce explicit equations defining new operators in a given
program. A few functional languages have weak primitives, and depend
upon equations in programs for their expressive power.
\subind{primitive operations!functional|)}
\subind{functional programming!primitives|)}

Most functional languages impose restrictions on the equations that
may be introduced by programs, in order to allow simple and efficient
proof searches in the implementation. Typical restrictions are
surveyed in the chapter `Equational Logic Programming,'
Section~\ref{sec:testing-confluence}. In most languages, the
restrictions on equations in programs allow each equation
\mbox{$f(t_1,\ldots,t_i)\formeq t$} in a program to be treated as a
part of the definition of a procedure to compute $f$. Note the similarity to
the treatment of clauses in Prolog programs (Section~\ref{sec:prolog}).

\paragraph*{Determining a Question from Language Design, Program, and Input.}

\subind{normal form|(}
Recall that the form of a normalization question is \mbox{$(\normalize
t_1,\ldots,t_i\quantsep t)$}. An answer to such a question gives a
term equal to $t$ that does not contain a subterm of any of the forms
$t_1,\ldots,t_i$. The determination of a question divides naturally
into the determination of the prohibited forms $t_1,\ldots,t_i$ and the
term $t$ to normalize.

\subind{constructor|(}
In most functional programming languages, the prohibited forms
$t_1,\ldots,t_i$ are determined by partitioning the set of symbols
into {\em constructors, primitive functions,} and {\em defined
functions.} Constructors are intended to be computationally
inert---they are treated as elements of a data structure.  The use of
constructors in equations is highly restricted to ensure this
inertness.  The binary symbol $\cons$ in Lisp is the archetypal
constructor.  In languages that distinguish constructors, the
prohibited forms in normalization questions are precisely the terms
\mbox{$f(x_1,\ldots,x_i)$}, where $f$ is a primitive function or a
defined function of arity $i$.  That is, the normal forms for
questions in constructor systems are precisely the {\em constructor
expressions\/}---terms composed entirely of variables and
constructors.  The set of constructors may be fixed by the language
design, or a program may be allowed to introduce new constructors, in
explicit declarations of the symbols or in recursive type definitions.
\subind{constructor|)}

In a functional language without constructors, the prohibited forms
may be implicit in the equations of a program. Most functional
languages infer from the presentation of the equation
\mbox{$t_1\formeq t_2$} that the left-hand side $t_1$ is to be
transformed into the right-hand side $t_2$. Such an inference is not
justified directly by the semantics of equational logic, but it is
often justified by restrictions on the form of equations imposed by
the language. So, the prohibited forms in questions are often taken
to be precisely the terms on the left-hand sides of equations in the
program.
\subind{normal form|)}

The term to be normalized is typically in the form
$$\subst{t_1^{\mbox{\scriptsize in}},\ldots t_{i_{\mbox{\tiny
in}}}^{\mbox{\scriptsize in}}}{y_1,\ldots,y_{i_{\mbox{\tiny in}}}}
{(\subst{t_1^{\mbox{\scriptsize pr}},\ldots, t_{i_{\mbox{\tiny
pr}}}^{\mbox{\scriptsize pr}}} {x_1,\ldots,x_{i_{\mbox{\tiny
pr}}}}{t^{\mbox{\scriptsize la}}})}$$ where $t^{\mbox{\scriptsize
la}}$ is fixed by the language design, $t_1^{\mbox{\scriptsize
pr}},\ldots, t_{i_{\mbox{\tiny pr}}}^{\mbox{\scriptsize pr}}$
are determined by the program, and $t_1^{\mbox{\scriptsize
in}},\ldots, t_{i_{\mbox{\tiny in}}}^{\mbox{\scriptsize in}}$ are
determined by the input. In principle, other forms are possible, but
it seems most natural to view the language design as providing an
operation to be applied to the program, producing an operation to be
applied to the input. For example, in a pure Lisp $\eval$
interpreter, \mbox{$t^{\mbox{\scriptsize la}}=\eval(x_1,\nil)$}.
The program to be evaluated is $t_1^{\mbox{\scriptsize pr}}$ (the
second argument $\nil$ to the $\eval$ function indicates an empty list
of definitions under which to evaluate the program). Pure Lisp has no
input---conceptual input may be encoded into the program, or
extralogical features may be used to accomplish input. A natural
extension of pure Lisp to allow definitions of symbols in a program
yields \mbox{$t^{\mbox{\scriptsize la}}=\eval(x_1,x_2)$},
$t_1^{\mbox{\scriptsize pr}}$ is the expression given by the program
to be interpreted, and $t_2^{\mbox{\scriptsize pr}}$ is a list of
bindings representing the definitions given in the program.  In a
language, unlike Lisp, where a program designates a particular defined
function $f$ as the {\em main\/} procedure to be executed on the
input, we can have \mbox{$t^{\mbox{\scriptsize la}}=x_1$} (the
language design does not contribute to the term to be normalized),
\mbox{$t_1^{\mbox{\scriptsize pr}}=f(y_1)$} where $f$ is the
designated main function, and $t_1^{\mbox{\scriptsize in}}$ is the
input. In yet other languages, the term to be normalized is given
entirely by the input.

\paragraph*{Notational Variations and Abbreviations.}

Functional programming languages vary widely in the notations used for
terms, using all sorts of prefix, infix, postfix, and mixfix forms.  A
survey of the possibilities is pointless.  All current functional
languages determine the prohibited forms in questions implicitly,
either from the language design or from the left-hand sides of
equations in a program. Questions are presented by specifying some or
all of the term to be normalized---other parts of the term may be
implicit as described above. Outputs always present only the
normal form $s$ rather than the equation \mbox{$t\formeq s$}, since
the question term $t$ is already given explicitly or implicitly.

\paragraph*{Deviations From Pure Equational Logic Programming.}

\subind{equational logic programming!deviations|(} Implementations of
functional programming languages have generally come closer to the
ideal of pure equational logic programming than Prolog systems have to
pure Horn-clause logic programming, largely because of a simpler
correspondence between logical and procedural concepts in functional
languages than in Prolog.  Many functional languages extend pure logic
programming with side-effect-producing\subind{side effects}
operations, similar to those in Prolog. These extensions are usually
used to deal with input and
output\subind{input/output!functional}\subind{functional
programming!input/output}. Some functional languages avoid such
extensions by modelling the entire input and output as an expression,
called a {\em stream,} that lists the atomic elements of the input and output
\cite{Karlsson,Thompson,Hudak-Sundaresh,Hudak-Peyton-Jones-Wadler,Gordon,Dwelly};
\auind{Karlsson, K.}\auind{Dwelly, A.}
\auind{Thompson, S.}\auind{Hudak, P.}\auind{Sundaresh, R. S.}
\auind{Peyton Jones, S.}\auind{Wadler, P.}\auind{Gordon, A. D.}
others use a functional representation of input and output based on {\em
continuations\/} \cite{Perry,Hudak-Sundaresh,Hudak-Peyton-Jones-Wadler}.
\auind{Perry, N.} Also see~\cite{Williams}\auind{Williams, J.
H.}\auind{Wimmers, E. L.} for an implicit approach to functional
I/O. A protocol that decouples the temporal order of input and output
from its representation in a functional program has been proposed as
well \cite{Rebelsky-thesis,Rebelsky-tree}
\subind{tour protocol}\auind{Rebelsky, S. A.}.

The purely functional subsets of functional programming languages
usually avoid giving incorrect answers. Implementations of
Lisp\subind{Lisp!dynamic scope} before the 1980s are arguably
incorrect in that their use of {\em dynamic scope\/} \cite{Stark,Moses}
\auind{Stark, W. R.}\auind{Moses, J.}
\subind{scope!dynamic vs.\ static} for
parameter bindings gives answers that are incorrect according to the
conventional logical equations for substitution\subind{substitution}
of terms for parameters, taken from the lambda
calculus \cite{Church,Stenlund,Barendregt}\auind{Church, A.}
\auind{Stenlund, S.}\auind{Barendregt, H. P.}\subind{lambda calculus}.
Since the equations for manipulating bindings were never formalized
precisely in the early days of Lisp, implementors may argue that their
work is correct with respect to an unconventional definition of
substitution. Early Lispers seem to have been unaware of the logical
literature on variable substitution, and referred to the dynamic
binding problem as the `funarg' problem.

Essentially all functional programming languages before the 1980s fail
to find certain semantically correct answers, due to infinite
evaluation of irrelevant portions of a term. In conventional Lisp
implementations, for example, the defining equation
\mbox{$\car(\cons(x,y))\formeq x$} is not applied to a term
\mbox{$\car(\cons(t_1,t_2))$} until both $t_1$ and $t_2$ have been
converted to normal forms. If the attempt to normalize $t_2$ fails
due to infinite computation, then the computation as a whole fails,
even though a semantically correct answer might have been derived
using only $t_1$. Systems that fail to find a normal form for
\mbox{$\car(\cons(t_1,t_2))$} unless {\em both\/} of $t_1$ and $t_2$
have normal forms are said to have {\em strict\/}\subind{strict
evaluation}\subind{evaluation!strict vs.\ lazy} $\cons$ functions.
The discovery of {\em lazy
evaluation\/} \cite{Friedman-Wise,Henderson-Morris,O'Donnell-Springer}
\auind{Henderson, P.}\auind{Morris, J. H.}\auind{Friedman, D.}
\auind{Wise, D.}\auind{O'Donnell, M. J.}\subind{lazy evaluation} showed
how to avoid imposing unnecessary strictness on $\cons$ and other
functions, and many recent implementations of functional programming
languages are guaranteed to find all semantically correct answers. Of
course, it is always possible to modify defining equations so that the
strict interpretation of a function is semantically complete.
\begin{example}\label{exa:strictify}
Consider Lisp, with the standard equations
$$\car(\cons(x,y))\formeq x\mbox{ and }\cdr(\cons(x,y))\formeq
y$$ To enforce strict evaluation of lists, even in a lazily evaluated
implementation of equational logic programming, add new function
symbols\/ $\test$, $\strict$, $\sand$, and a new constant\/ $\true$, with the
equations
$$\begin{array}{cc}\test(\true,x)\formeq x, &
\sand(\true,\true)\formeq\true, \\
\strict(\cons(x,y))\formeq\sand(\strict(x),\strict(y)), &
\strict(a)\formeq\true\end{array}$$ for each atomic symbol\/ $a$. Then,
redefine\/ $\car$ and\/ $\cdr$ by
$$\car(\cons(x,y))\formeq\test(\strict(y),x)\mbox{ and }
\cdr(\cons(x,y))\formeq\test(\strict(x),y)$$ Lazy evaluation with
the new set of equations has the same effect as strict evaluation with
the old set.
\end{example}
Some definitions of functional programming language specify strictness
explicitly. One might argue that the strict version of $\cons$ was
intended in the original definition of
Lisp \cite{McCarthy}\auind{McCarthy, J.}\subind{Lisp!strict vs.\ lazy}, but
strictness was never stated explicitly there.
\subind{equational logic programming!deviations|)}
\subind{functional programming|)}\subind{equational logic programming|)}

\subsubsection[Equation Solving and FOPC with Equality]
{Equation Solving and Predicate Calculus with Equality}

\subind{equation solving|(}
Given successful applications of logic programming in the pure
First-Order Predicate Calculus without equality, and in pure
Equational Logic, it is very tempting to develop languages for logic
programming in the First-Order Predicate Calculus with Equality
($\mbox{FOPC}_{\formeq}$)\notind{$\mbox{FOPC}_{\formeq}$ (First-Order
Predicate Calculus with Equality)}.\subind{First-Order Predicate
Calculus!with equality} Unfortunately, there is a mismatch between the
style of questions used in the two sorts of logic programming. FOPC
Logic Programming uses questions of the form \mbox{$(\what
x_1,\ldots,x_i\quantsep F)$} (Definition~\ref{def:FOPC-query-system}),
whose answers supply substitutions for the variables $x_1,\ldots,x_i$
satisfying $F$.  Equational Logic Programming uses questions of the
form
\mbox{$(\normalize t_1,\ldots,t_i\quantsep t)$}\ 
(Definition~\ref{def:equational-query-system}), whose answers supply
normal forms equal to $t$, not containing the forms $t_1,\ldots,t_i$.
The implementation techniques for answering these two sorts of
questions do not appear to combine well.

The most natural idea for achieving logic programming in
$\mbox{FOPC}_{\formeq}$ is to use the FOPC style of question, and
extend it to deal with equations.  In principle that is feasible,
because the formal equality symbol $\formeq$ may be treated as another
binary predicate symbol in $\mbox{\bf Pred}_2$, and Horn clauses
expressing its crucial properties are easy to find. Unfortunately, the
natural Horn clauses for the equality predicate, when treated by
current implementation techniques for FOPC Logic Programming, yield
unacceptably inefficient results. In practice, a satisfactory
realization of logic programming in $\mbox{FOPC}_{\formeq}$ will require new
techniques for solving equations---that is, for answering questions of
the form \mbox{$(\solve x_1,\ldots,x_i\quantsep t_1\formeq
t_2)$}\notind{$\solve$ (equation solving question)}
(Definition~\ref{def:solve-equation}). An interesting experimental
language incorporating significant steps toward logic programming in
$\mbox{FOPC}_{\formeq}$ is EqL \cite{Jayaraman}\subind{EqL}\auind{Jayaraman, B.}, but
this language only finds solutions consisting of constructor
expressions. The problem of finding nonconstructor solutions is much
more difficult.

It is also possible to define FOPC Logic Programming in terms of a
normalization-style query. Consider a question `what acceptable
formula implies $F_0$', which presents a goal formula $F_0$, and some
description of which answer formulae are acceptable and which are
prohibited (the problem of describing such prohibited formulae is more
complex in FOPC than in Equational Logic because of the structural
properties of the logical connectives $\land,\lor,\ldots$). An answer
to such a question is an implication of the form \mbox{$F_1\limplies
F_0$}, where $F_1$ is an acceptable formula. The conventional FOPC
questions \mbox{$(\what x_1,\ldots,x_i\quantsep F_0)$} may be
understood as a variant of the `what implies $F_0$' questions, where
the acceptable formulae are precisely those of the form
\mbox{$x_1\formeq t_1\land\cdots\land x_i\formeq t_i$}. The proposed
new style of FOPC question may be seen as presenting a set of
constraints expressed by $F_0$, and requesting a normalized expression
of constraints $F_1$ such that every solution to the constraints
expressed by $F_1$ is also a solution to the constraints of
$F_0$. {\em Constraint Logic Programming\/}
\cite{Jaffar-Lassez,Lassez}\auind{Jaffar, J.}\auind{Lassez, J.-L.}
\subind{constraint logic programming} has taken some
steps in this direction, although Constraint Logic Programming
generally views the normalized constraints expressed by $F_1$ not as a
final result to be output as an answer, but as something to be solved
by techniques outside of FOPC, such as numerical techniques for
solving linear systems of equations.
\subind{equation solving|)}
\subind{equational logic|)}\subind{equations|)}

\section{Implementing Logic Programming Languages}
\label{sec:implementing}

\subind{logic programming!abstract implementation|(}
Semantic systems and query systems are convenient tools for specifying
logic programming languages: we require a language to provide
semantically correct answers to questions. In order to implement
logic programming languages, we first develop sound (correct) and
complete (powerful) {\em proof systems\/} to provide effective
certificates of the semantic correctness of inferences. Then, we
convert proof systems to {\em programming systems\/} that process
inputs and programs efficiently to produce outputs, by introducing
{\em strategies\/} for choosing incrementally which proofs to
construct. In this chapter we consider only the abstract forms of
implementations, far above the level of actual code for real machines.
Truly practical implementations do, however, follow these abstract
forms quite closely.
\subind{logic programming languages|)}

\subsection[Proof Systems]{Proof Systems and Provable Consequences}
\label{sec:proof-system}

\subind{proof system|(}
A semantic-consequence relation determines in principle whether it is
correct to infer one logical formula from others. In order to give a
formal justification for an inference, we need a notation for {\em
proofs}. We reserve the initial $P$ for programs, so $D$ is used to
stand for proofs\subind{proof}, which might also be called {\em
demonstrations\/}\subind{demonstration} or
{\em derivations}\subind{derivation}.
\begin{definition}\label{def:proof-system}
A\/ {\em proof system\/} is a system\/ \mbox{${\cal
D}=\langle\mathbold{F},\mathbold{D},\hypos\:\proves\rangle$}, where
\begin{enumerate}
\item $\mathbold{F}$\notind{$\mathbold{F}$ (formulae)} is a set of\/ {\em
formulae}
\item $\mathbold{D}$\notind{$\mathbold{D}$ (proofs, derivations)}
  is a set of {\em proofs}
\item $\hypos\:\proves$\notind{$\hypos\:\proves$ (trinary proof relation)}
  is a relation on\/
  \mbox{$\powerset{\mathbold{F}}\times\mathbold{D}\times\mathbold{F}$}
  (when\/ \mbox{$\langle\mathbold{T},D,F\rangle$} are in the relation\/
  $\hypos\:\proves$, we write \mbox{$\mathbold{T}\hypos D\proves F$})
\item $\hypos\:\proves$ is monotone\subind{monotone proof}
  (if\/ \mbox{$\mathbold{T}\hypos
  D\proves F$} and\/ \mbox{$\mathbold{T}\subseteq\mathbold{U}$},
  then\/ \mbox{$\mathbold{U}\hypos D\proves F$})
\end{enumerate}

The proof system\/ ${\cal D}$ is\/ {\em compact\/}\subind{compact!proof}
if and only if, for all\/
\mbox{$\mathbold{T}\subseteq\mathbold{F}$}, \mbox{$P\in\mathbold{D}$}, and\/
\mbox{$F\in\mathbold{F}$}, whenever\/ \mbox{$\mathbold{T}\hypos D\proves F$}
then there exists a finite subset\/ \mbox{$\mathbold{T}^{\rm
f}\subseteq\mathbold{T}$} such that\/ \mbox{$\mathbold{T}^{\rm f}
\hypos D\proves F$}.
\end{definition}
\mbox{$\mathbold{T}\hypos D\proves F$} is intended to mean that $D$ is a {\em
proof\/} of $F$ which is allowed to use hypotheses\subind{hypothesis}
in $\mathbold{T}$. The fact that $D$ is not {\em required\/} to use
all hypotheses leads to monotonicity (4). There are a number of
proposals for systems of `nonmonotonic logic,' but they may be
regarded as studies of different relations between proofs and formulae
than the notion of derivability represented by $\hypos\:\proves$
above, rather than as arguments about the properties of
$\hypos\:\proves$. The controversy about nonmonotonic logic is not
relevant to the discussion in this chapter, and fans of nonmonotonic
relations between proofs and formulae may translate into their own
notation if they like.

In well-known proof systems, proofs as well as formulae are finite
syntactic objects, and the set $\mathbold{D}$ of all proofs is
computable. There are important uses, however, for infinite proofs of
infinite formulae, so we do not add a formal requirement of
computability. Typically, a proof $D$ determines uniquely the
conclusion\subind{conclusion} formula $F$ and minimum hypothesis set
$\mathbold{T}$ such that \mbox{$\mathbold{T}\hypos D\proves F$}, but
there is no need to require such a property. Meseguer
\cite{Meseguer-general}\auind{Meseguer, J.} proposed a similar general
notion of {\em proof calculus.}

\subind{Shallow Implicational Calculus|(}
\notind{SIC (Shallow Implicational Calculus)|(}
\subind{linear proof|(}\subind{proof!linear|(}
It is straightforward to design a proof system for SIC. The following
proof system follows the conventional style of textbooks in logic.
Proofs are sequences of formulae, each one either a hypothesis, a
postulate, or a consequence of earlier formulae in the proof.
\begin{example}\label{exa:proof-system-linear}
Let\/ $\sicformulae$ be the set of formulae in SIC. The set of\/ {\em
linear proofs\/} in SIC is\/
\mbox{$\sicproofslin=\sicformulae^+$},
\notind{$\sicproofslin$ (linear proofs in SIC)}
the set of nonempty finite sequences of formulae.\\
The proof relation\/ \mbox{$\hypos\:\sicproveslin$}
\notind{$\hypos\:\sicproveslin$ (linear proof relation in SIC)}
is defined by
\begin{center}
$\mathbold{T}\hypos\langle F_0,\ldots,F_m\rangle\sicproveslin F$ if and only
if\/ $F_m=F$ and,\\ for all\/ $i\leq m$, one of the
following cases holds:
\end{center}
\subind{modus ponens}\subind{reflexive}\subind{hypothesis}
\subind{transitive}
\begin{enumerate}
   \item\label{enu:hypothesis} \mbox{$F_i\in\mathbold{T}$}
   \item\label{enu:reflexivity} \mbox{$F_i=(a\limplies a)$}
      for some atomic formula\/
      \mbox{$a\in\mbox{\bf At}$}
   \item\label{enu:l-modus-ponens} \mbox{$F_i=b$},
     and there exist\/ \mbox{$j,k<i$} such that\/
      \mbox{$F_j=a$} and\/ \mbox{$F_k=(a\limplies b)$} for some atomic
      formulae\/ \mbox{$a,b\in\mbox{\bf At}$}
   \item\label{enu:transitivity} \mbox{$F_i=(a\limplies c)$},
      and there exist\/ \mbox{$j,k<i$}
      such that\/ \mbox{$F_j=(a\limplies b)$} and\/
      \mbox{$F_k=(b\limplies c)$} for some atomic formulae\/
      \mbox{$a,b,c\in\mbox{\bf At}$}
\end{enumerate}
Now\/
\mbox{$\langle\sicformulae,\sicproofslin,\hypos\:\sicproveslin\rangle$}
is a compact proof system, representing the\/ {\em
Hilbert\/}\subind{Hilbert proof}\subind{proof!Hilbert-style}, or\/
{\em linear\/}, style of proof for implications.
\end{example}
Intuitively, a linear or Hilbert-style proof is a finite sequence of
formulae, each one being either a {\em hypothesis\/}\subind{hypothesis}
(case~\ref{enu:hypothesis} above), a {\em
postulate\/}\subind{postulate} (case~\ref{enu:reflexivity} above,
expressing the postulate scheme of {\em reflexivity\/} of
implication), or the consequence of previous formulae by a {\em rule
of inference\/}\subind{rule of inference}\subind{inference!rule}
(case~\ref{enu:l-modus-ponens} above, expressing the rule of {\em
modus ponens\/}, and case~\ref{enu:transitivity}, expressing the rule
of {\em transitivity\/} of implication). The
conclusion\subind{conclusion} of a linear proof is the last formula in
the list.
\subind{linear proof|)}\subind{proof!linear|)}

\subind{natural deduction|(}\subind{proof!natural deduction|(}
An alternative proof system for SIC, less conventional but more
convenient for some purposes, follows the {\em natural
deduction\/}
style of proof \cite{Prawitz}\auind{Prawitz, D.}. Natural deduction proofs are
trees, rather than sequences, to display the actual logical
dependencies of formulae. They also allow the introduction and
discharging of temporary assumptions in proofs, to mimic the informal
style in which we prove $a\limplies b$ by assuming $a$ and proving $b$. 
\begin{example}\label{exa:proof-system-natural}
Let\/ $\sicformulae$ be the set of formulae in the Shallow
Implicational Calculus defined in Example~\ref{exa:semantic-system}.
Let\/ $\mbox{\bf assume}$\notind{$\mbox{\bf assume}$}, $\mbox{\bf
modus-ponens}$\notind{$\mbox{\bf modus-ponens}$}, and\/ $\mbox{\bf
deduction-rule}$\notind{$\mbox{\bf deduction-rule}$} be new formal symbols.\\
The set\/ $\sicproofsnat$
\notind{$\sicproofsnat$ (natural deduction proofs in SIC)}
of\/ {\em natural deduction proofs\/} in SIC and the proof relation\/
\mbox{$\hypos\:\sicprovesnat\subseteq\powerset{\sicformulae}\times
\sicproofsnat\times\sicformulae$}
\notind{$\hypos\:\sicprovesnat$ (natural deduction proof relation in SIC)}
are defined by simultaneous inductive
definition to be the least set and relation such that:

\begin{enumerate}
   \item\label{enu:assume} for each atomic
      formula\/ \mbox{$a\in\mbox{\bf At}$}, and each set of formulae\/
      \mbox{$\mathbold{T}\subseteq\sicformulae$},
      \begin{center}
      $\mbox{\bf assume}(a)\in\sicproofsnat$\\
      and\\
      $\mathbold{T}\cup\{a\}\hypos\mbox{\bf assume}(a)\sicprovesnat a$
      \end{center}
   \item\label{enu:modus-ponens} if\/
      \mbox{$\alpha,\beta\in\sicproofsnat$},
      and\/ \mbox{$\mathbold{T}\hypos\alpha\sicprovesnat a$}
      for some atomic formula\/
      \mbox{$a\in\mbox{\bf At}$}, and\/
      \mbox{$\mathbold{U}\hypos\beta\sicprovesnat(a\limplies b)$}, then\/
      $$\mbox{\bf modus-ponens}(\alpha,\beta)\in\sicproofsnat\mbox{ and }
      \mathbold{T}\cup\mathbold{U}\hypos\mbox{\bf
      modus-ponens}(\alpha,\beta)\sicprovesnat b$$
   \item\label{enu:deduction-rule} if\/ \mbox{$\beta\in\sicproofsnat$}
      and\/ \mbox{$\mathbold{T}\cup\{a\}\hypos\beta\sicprovesnat b$}
      for some atomic formula\/
      \mbox{$a\in\mbox{\bf At}$}, then $$\mbox{\bf deduction-rule}(
      a,\beta)\in\sicproofsnat\mbox{ and }\mathbold{T}\hypos\mbox{\bf
      deduction-rule}(a,\beta)\sicprovesnat(a\limplies b)$$
\end{enumerate}
Now\/ \mbox{$\langle\sicformulae,\sicproofsnat,\hypos\:\sicprovesnat\rangle$}
is a compact proof system, representing the\/ {\em natural
deduction\/} style of proof for implications.
\end{example}
Intuitively, $\mbox{\bf assume}(a)$ is a trivial proof of $a$ from
hypothesis $a$. \mbox{$\mbox{\bf modus-ponens}(\alpha,\beta)$} is the
result of using a proof $\alpha$ of some atomic formula $a$, a proof
$\beta$ of an implication \mbox{$(a\limplies b)$}, and combining the
results along with the rule of {\em modus ponens\/} to conclude $b$.
The set of hypotheses for the resulting proof includes all hypotheses
of $\alpha$ and all hypotheses of $\beta$. \mbox{$\mbox{\bf
deduction-rule}(a,\beta)$} is the result of taking a proof $\beta$ of
$b$ from hypotheses including $a$, and discharging\subind{discharge
hypothesis}\subind{hypothesis!discharging} some (possibly 0) of the
assumptions of $a$ from the proof, to get a proof of $(a\limplies b)$
by the {\em deduction rule}. In clause~\ref{enu:deduction-rule} of the
inductive definition above, notice that the hypothesis set
$\mathbold{T}$ may contain $a$, in which case
\mbox{$\mathbold{T}\cup\{a\}=\mathbold{T}$}. It is this case that
allows for the possibility that one or more assumptions of $a$ remain
undischarged in an application of the deduction rule.
\subind{Shallow Implicational Calculus|)}
\notind{SIC (Shallow Implicational Calculus)|)}

The style of proof formalized in
Example~\ref{exa:proof-system-natural} is called {\em natural
deduction}, since it mimics one popular informal style of proof in
which an implication is proved by assuming its hypothesis and deriving
its conclusion. Natural deduction style\cite{Prawitz}\auind{Prawitz,
D.}, and the similar style of sequent derivation
\cite{Gentzen,Kleene}\auind{Kleene, S. C.}\subind{sequent}, both due to
Gentzen,\auind{Gentzen, G.} are the styles of proof most commonly
treated by research in {\em proof theory\/}
\cite{Stenlund,Prawitz,Takeuti,Schutte,Girard}\subind{proof theory}.
\auind{Stenlund, S.}\auind{Prawitz, D.}\auind{Takeuti,
G.}\auind{Schutte, K.}\auind{Girard, J.-Y.}\auind{Lafont,
Y.}\auind{Taylor, P.} In proof theory, natural deduction rules are
expressed very naturally as terms in a typed lambda
calculus\subind{lambda calculus!typed}\subind{typed lambda calculus},
where the type of a lambda term is the formula that it proves
\cite{Howard,Tait}\auind{Howard, W.}\auind{Tait, W. W.}.
\subind{natural deduction|)}\subind{proof!natural deduction|)}

In many cases, we are interested only in the provability of an
inference, and not the proof itself. So, we let each proof system
define a {\em provable-consequence\/}\subind{provable
consequence}\subind{consequence!provable} relation, analogous to the
semantic-consequence relation associated with a semantic system.
\begin{definition}\label{def:provable-consequence}
Let\/ \mbox{${\cal
D}=\langle\mathbold{F},\mathbold{D},\hypos\:\proves\rangle$}
be a proof system. The\/ {\em prov\-able-consequence\/}
relation defined by\/ ${\cal D}$ is\/
\mbox{$\hyproves\subseteq\powerset{\mathbold{F}}\times\mathbold{F}$}, where
$$\mathbold{T}\hyproves F\mbox{ if and only if there exists a proof }
D\in\mathbold{D}\mbox{ such that }\mathbold{T}\hypos D\proves F$$
\notind{$\hyproves$ (binary proof relation)}

The provable-consequence relation\/ $\hyproves$ is\/ {\em
compact\/}\subind{compact!proof} if and only if, for all\/
\mbox{$\mathbold{T}\subseteq\mathbold{F}$}, and\/
\mbox{$F\in\mathbold{F}$}, whenever\/ \mbox{$\mathbold{T}\hyproves F$}
then there exists a finite subset\/
\mbox{$\mathbold{T}^{\rm f}\subseteq\mathbold{T}$} such
that\/ \mbox{$\mathbold{T}^{\rm f}\hyproves F$}.
\end{definition}
Intuitively, $\mathbold{T}\hyproves F$ means that $F$ is {\em
provable\/}\subind{provable} from hypotheses\subind{hypothesis} in
$\mathbold{T}$. It is easy to show that an arbitrary relation $\hyproves$ on
\mbox{$\powerset{\mathbold{F}}\times\mathbold{F}$} is the
provable-consequence relation of some proof system if and only if it
is {\em monotone\/} (\mbox{$\mathbold{T}\hyproves F$} and
\mbox{$\mathbold{T}\subseteq\mathbold{U}$} imply that
\mbox{$\mathbold{U}\hyproves F$}). See
\cite{Meseguer-general}\auind{Meseguer, J.} for another abstract
definition of provable consequence relations, with more stringent
requirements.

Most well-known semantic/provable-consequence relations are compact,
and semicomputable on the finite sets of formulae. The trinary proof
relations of proof systems (restricted to finite sets of hypotheses)
are normally computable. That is, in a reasonable proof system we can
determine definitely and mechanically whether or not a supposed proof
is in fact a proof of a given conclusion from a given finite set of
hypotheses. It is easy to see that a proof system with
semicomputable\subind{semicomputable} set $\mathbold{D}$ of proofs and
semicomputable trinary proof relation $\hypos\:\proves$ also has a
semicomputable provable-consequence relation, and that compactness of
the proof system implies compactness of the provable-consequence
relation. In fact, every semicomputable provable-consequence relation
is defined by some proof system with computable $\mathbold{D}$ and
trinary proof relation $\hypos\:\proves$. In this respect the trinary
proof relation acts as a {\em G\"odel T-predicate\/}
\cite{Kleene}\subind{T-predicate}\auind{Kleene, S. C.}\auind{G\"odel, K.}
\subind{Godel T-predicate@G\"odel T-predicate}
to the binary provable consequence relation.

\subsection{Soundness and Completeness of Proof Systems}
\label{sec:sound-complete-proof}

\subind{sound proof system|(}\subind{proof system!sound|(}
\subind{complete proof system|(}\subind{proof system!complete|(}
The behavior of a proof system may be evaluated in a natural way with
respect to a semantic system with the same or larger set of formulae.
We say that the proof system is {\em sound\/} for the semantic system
when every provable consequence is a semantic consequence, and that
the proof system is {\em complete\/} when every semantic consequence
is provable.  Roughly, soundness means correctness, and completeness
means maximal power within the constraints imposed by the set of
formulae available in the proof system.
\begin{definition}\label{def:sound-complete-proof}
Let\/ \mbox{${\cal D}=\langle\mathbold{F}_{\rm
D},\mathbold{D},\hypos\:\proves\rangle$} be a proof system, and let\/
\mbox{${\cal S}=\langle\mathbold{F}_{\rm
S},\mathbold{M},\models\rangle$} be a semantic system, with\/
\mbox{$\mathbold{F}_{\rm D}\subseteq\mathbold{F}_{\rm S}$}.

${\cal D}$ is\/ {\em sound\/} for\/ ${\cal S}$ if and only if, for
all\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}$} and\/ \mbox{$F\in\mathbold{F}_{\rm
D}$} $$\mathbold{T}\hyproves F\mbox{ implies }\mathbold{T}\models F$$

${\cal D}$ is\/ {\em complete\/} for\/ ${\cal S}$ if and only if, for
all\/ \mbox{$\mathbold{T}\subseteq\mathbold{F}$} and\/ \mbox{$F\in\mathbold{F}_{\rm
D}$}, $$\mathbold{T}\models F\mbox{ implies }\mathbold{T}\hyproves F$$
\end{definition}

\subind{Shallow Implicational Calculus!sound and complete|(}
Each of the proposed proof systems for SIC is sound and complete for
the semantic system of SIC. The following proofs of completeness for
SIC are similar in form to completeness proofs in general, but
unusually simple. Given a set of hypotheses $\mathbold{T}$, and a
formula $F$ that is not provable from $\mathbold{T}$, we construct a
model $M$ satisfying exactly the set of provable consequences of
$\mathbold{T}$ within some sublanguage $\mathbold{F}_F$ containing $F$
(\mbox{$\theoryfunc(M)\cap\mathbold{F}_F=
\theoryfunc(\modelfunc(\mathbold{T}))\cap\mathbold{F}_F$}). In
our example below, $\mathbold{F}_F$ is just the set of all shallow
implicational formulae ($\sicformulae$), and the model construction is
particularly simple.
\begin{example}\label{exa:sound-complete-proof}
Each of the proof systems
\mbox{$\langle\sicformulae,\sicproofsnat,\hypos\:\sicprovesnat\rangle$}
of Example~\ref{exa:proof-system-natural} and
\mbox{$\langle\sicformulae,\sicproofslin,\hypos\:\sicproveslin\rangle$}
of Example~\ref{exa:proof-system-linear} is sound and complete for the
semantic system
\mbox{$\langle\sicformulae,\sicmodels,\sicsemrel\rangle$} of
Example~\ref{exa:semantic-system}.

The proofs of soundness involve elementary inductions on the size of
proofs. For the natural deduction system, the semantic correctness of
a proof follows from the correctness of its components; for the linear
system correctness of a proof $\langle F_0,\ldots,F_{m+1}\rangle$
follows from the correctness of the prefix $\langle F_0,\ldots,F_m\rangle$.

The proofs of completeness require construction, for each set\/
$\mathbold{T}$ of formulae, of a model\/ \mbox{$M=\{a\in\mbox{\bf
At}\setsep\mathbold{T}\sichyprovesnat a\}$} (or\/
\mbox{$\mathbold{T}\sichyproveslin a$}). So\/ \mbox{$M\sicsemrel a$}
for all atomic formulae\/ \mbox{$a\in\mathbold{T}\cap\mbox{\bf At}$}
trivially. It is easy to show that\/ \mbox{$M\sicsemrel(a\limplies
b)$} for all implications\/ \mbox{$(a\limplies b)\in\mathbold{T}$} as
well, since either\/ \mbox{$a\not\in M$}, or\/ $b$ follows by modus
ponens from\/ $a$ and\/ \mbox{$a\limplies b$}, so\/ \mbox{$b\in M$}.
Finally, it is easy to show that\/ \mbox{$M\sicsemrel F$} if and only
if\/
\mbox{$\mathbold{T}\sichyprovesnat F$} (or\/ \mbox{$\mathbold{T}\sichyproveslin F$}).
\end{example}
In richer languages than SIC, containing for example disjunctions or
negations, things may be more complicated. For example, if the
disjunction \mbox{$(A\lor B)$} is in the set of hypotheses $\mathbold{T}$,
each model satisfying $\mathbold{T}$ must satisfy one of $A$ or $B$, yet
neither may be a logical consequence of $\mathbold{T}$, so one of them must
be omitted from $\mathbold{F}_F$. Similarly, in a language allowing
negation, we often require that every model satisfy either $A$ or
$\lnot A$. Such considerations complicate the construction of a model
substantially.
\subind{Shallow Implicational Calculus!sound and complete|)}

\subind{logic!distinct from other sciences|(}
\subind{logic programming!distinct from other approaches|(}
Notice that the formal definitions above do {\em not\/} restrict the
nature of semantic systems and proof systems significantly.  All sorts
of nonsensical formal systems fit the definitions. Rather, the
relationships of soundness and completeness provide us with conceptual
tools for evaluating the behavior of a proof system, with respect to a
semantic system that we have already accepted as appropriate.  Logic
is distinguished from other technical sciences, not by the formal
definition of the systems that it studies, but rather by the use of
logical concepts to evaluate these systems. The distinction between
logic programming and other forms of programming is similarly based on
the approach to evaluating the systems, rather than the formal
qualities of the systems. \subind{logic!distinct from other sciences|)}
\subind{logic programming!distinct from other approaches|)}

While formal studies may reveal pleasing or disturbing properties of
semantic systems, there is also an unavoidable intuitive component in
the evaluation of a semantic system. A semantic system is reasonable
only if it accurately captures enough of the structure of the mental
meaning that we want to associate with a formula to allow a sensible
determination of the correctness or incorrectness of steps of
reasoning. Since different people have different intuitive notions
about the proper meanings of formulae, and the same person may find
different intuitions useful for different purposes, we should be open
minded about considering a broad variety of semantic systems. But, the
mere satisfaction of a given form of definition, whether the form in
Definition~\ref{def:semantic-system} above, or one of the popular
`denotational' forms using lattices or chain-complete partial
orderings and fixpoints, does not make a `semantics' meaningful. A
number of additional mathematical and philosophical dissertations are
needed to give practical aid in the evaluation and selection of
semantic proposals. The best one-sentence advice that I can offer is
to always ask of a proposed semantic system, `for a given formula $F$,
what does the semantic system tell about the information regarding the
world that is asserted by $F$.' For this chapter, I use only systems
of semantics based on first-order classical forms of logic that have
been shaken down very thoroughly over the years. In these systems, the
individual models clearly present enough alleged facts about a
possible state of the world to determine the truth or falsehood of
each formula. So, the information asserted by a formula is that the
world under discussion is one of the ones satisfying the formula in
the sense of $\models$. There are many reasons to prefer nonclassical
logics for programming and for other purposes. But, we must never rest
satisfied with `semantic' treatments of these logics until they have
been connected convincingly to an intuitive notion of {\em meaning.}

\subind{knowledge!implicit made explicit|(}
A semantic system and a sound proof system may be used to analyze the
process by which implicit knowledge is made explicit---we are
particularly interested in the derivation of explicit knowledge in
order to answer a question. Consider an agent with {\em implicit\/}
knowledge given by the set $\mathbold{K}$ of models consistent with
that knowledge, and represent the agent's {\em explicit\/} knowledge
by a set $\mathbold{T}$ of formulae that he can utter effectively.
The correctness of the explicit knowledge requires that
\mbox{$\mathbold{T}\subseteq\theoryfunc(\mathbold{K})$}. Suppose that
the agent knows that the proof system is sound, and suppose that he
can recognize at least some cases when the relation
$\mathbold{T}\hypos D\proves F$ holds---often this capability results
from computing the appropriate decision procedure for a computable
proof system (or enumeration procedure for a semicomputable proof
system), with an appropriate finite subset of $\mathbold{T}$. Then,
whenever he finds a formula $F$ and a proof $D$ such that
\mbox{$\mathbold{T}\hypos D\proves F$}, the agent may add the formula
$F$ to his explicit knowledge. The soundness of the proof system
guarantees that
\mbox{$F\in\theoryfunc(\mathbold{K})$}. Notice that sound proofs can never
extend explicit knowledge beyond the bound determined by implicit
knowledge, which is \mbox{$\theoryfunc(\mathbold{K})$}.
\subind{knowledge!implicit made explicit|)}
\begin{definition}\label{def:provably-correct-answer}
\subind{provably correct answer}
\notind{$\answers\hyproves$ (trinary answer relation)}
Let\/ \mbox{${\cal Q}=\langle\mathbold{F}_{\rm
Q},\mathbold{Q},\answers\rangle$} be a query system, and let\/
\mbox{${\cal D}=\langle\mathbold{F}_{\rm
D},\mathbold{D},\hypos\:\proves\rangle$} be a proof system with\/
\mbox{$\mathbold{F}_{\rm Q}\subseteq\mathbold{F}_{\rm D}$}.

\mbox{$Q\answers\mathbold{T}\hyproves F$} means that\/
$F\in\mathbold{F}_{\rm Q}$
is a\/ {\em provably correct\/} answer to $Q\in\mathbold{Q}$ for
explicit knowledge\/ $\mathbold{T}\subseteq\mathbold{F}_{\rm S}$, defined by
$$Q\answers\mathbold{T}\hyproves F\mbox{ if and only if }Q\answers F\mbox{
and }\mathbold{T}\hyproves F$$

\notind{$\answers\hypos\:\proves$ (quaternary answer relation)}
Similarly, $$Q\answers\mathbold{T}\hypos D\proves F\mbox{ if and only if
}Q\answers F\mbox{ and }\mathbold{T}\hypos D\proves F$$
\end{definition}
If ${\cal P}$ is sound, then provable correctness implies semantic
correctness (Definition~\ref{def:semantically-correct-answer}). If
${\cal P}$ is complete, then semantic correctness implies provable
correctness.

\subind{communication|(}
\subind{knowledge|(}
\subind{logic!representing communication and knowledge|(}
\subind{answer|(}
\subind{query system|(}
\subind{question|(}
\subind{questioner|(}
\subind{speaker|(}
\subind{auditor|(}
Going back to the communication analysis of previous sections, let
$\mathbold{K}_{\rm s}$ be the speaker's implicit knowledge, let
$\mathbold{K}^0_{\rm a}$ be the auditor's initial implicit knowledge,
and let $\mathbold{T}^0_{\rm a}$ be the auditor's initial explicit
knowledge. When the speaker utters a set of formulae
$\mathbold{T}_{\rm u}$, consistent with her implicit knowledge, the
auditor's implicit knowledge improves as before to
\mbox{$\mathbold{K}^1_{\rm a}=\mathbold{K}^0_{\rm
a}\cap\modelfunc(\mathbold{T}_{\rm u})$}, and the auditor's explicit
knowledge improves to \mbox{$\mathbold{T}^1_{\rm
a}=\mathbold{T}^0_{\rm a}\cup\mathbold{T}_{\rm u}$}. Let a questioner
ask a question $Q$ of the auditor. Without further communication from
the speaker, the auditor may improve his explicit knowledge by proving
new formulae from hypotheses in $\mathbold{T}^1_{\rm a}$ in order to
answer the question $Q$. If the auditor's initial explicit knowledge
is empty, then \mbox{$\mathbold{T}^1_{\rm a}=\mathbold{T}_{\rm u}$}, so the
formulae derivable in this way are exactly the provable consequences
of $\mathbold{T}_{\rm u}$, and the answers that may be found are
exactly the provably correct answers to $Q$ for $\mathbold{T}_{\rm
u}$. If the proof system used by the auditor is sound, then all such
answers are semantically correct; if the proof system is complete then
all semantically correct answers are provable.  Now let the speaker be
a programmer who utters a set of formulae constituting a logic
program, let the auditor be a processor, and let the questioner be a
user whose question is given as input to the program. Then, computations
performed by the processor take the form of search for and
construction of proofs deriving the explicit knowledge needed to
produce an output answer, from the explicit knowledge given in the
program.
\subind{communication|)}
\subind{knowledge|)}
\subind{logic!representing communication and knowledge|)}
\subind{answer|)}
\subind{query system|)}
\subind{question|)}
\subind{proof system|)}
\subind{questioner|)}
\subind{speaker|)}
\subind{auditor|)}

\subsection{Programming Systems}
\label{sec:programming-system}

\subind{programming system|(}
A {\em programming system\/} represents the computational behavior of
a processor. In order to understand logic programming, we consider an
arbitrary, possibly ineffective and nondeterministic, programming
system, and then show how to evaluate its behavior logically with
respect to a given semantic system and query system. We choose an
unconventional formal notation for programming systems in order to
expose the close analogy of sets of formulae to programs,
questions to inputs, proofs to computations, answers to outputs.
\begin{definition}\label{def:programming-system}
A\/ {\em programming system\/} is a system\/ \mbox{${\cal
P}=\langle\mathbold{P},\mathbold{I},\mathbold{C},\mathbold{O},
\inputs\:\computes,\outputs\rangle$},
where\notind{$\inputs\:\computes$ (trinary computation relation)}
\notind{$\outputs$ (output relation)}
\notind{$\mathbold{P}$ (programs)}
\notind{$\mathbold{I}$ (inputs)}
\notind{$\mathbold{C}$ (computations)}
\notind{$\mathbold{O}$ (outputs)}
\begin{enumerate}
\item $\mathbold{P}$ is a set of\/
{\em programs}
\item $\mathbold{I}$ is a set of\/ {\em inputs}
\item $\mathbold{C}$ is a
set of\/ {\em computations}
\item $\mathbold{O}$ is a set of\/ {\em outputs}
\item $\inputs\:\computes$ is a relation on\/
\mbox{$\mathbold{I}\times\mathbold{P}\times\mathbold{C}$} (when\/ \mbox{$\langle I,P,C\rangle$} are in
the relation\/ $\inputs\:\computes$, we write\/ \mbox{$I\inputs
P\computes C$})
\item For each\/
\mbox{$I\in\mathbold{I}$} and\/ \mbox{$P\in\mathbold{P}$}, there is at least one
\mbox{$C\in\mathbold{C}$} with\/ \mbox{$I\inputs P\computes C$}
\item $\outputs$ is a
relation on\/ \mbox{$\mathbold{C}\times\mathbold{O}$}
\item For each\/
\mbox{$C\in\mathbold{C}$}, there is at most one\/ \mbox{$O\in\mathbold{O}$} with\/
\mbox{$C\outputs O$} (that is, $\outputs$ is a partial function from
$\mathbold{C}$ to $\mathbold{O}$)
\end{enumerate}

We define the relation\/
\mbox{$\inputs\:\computes\:\outputs\subseteq
\mathbold{I}\times\mathbold{P}\times\mathbold{C}\times\mathbold{O}$}
by $$I\inputs P\computes C\outputs
O\mbox{ if and only if }I\inputs P\computes C\mbox{ and }C\outputs O$$
\notind{$\inputs\:\computes\:\outputs$ (quaternary computation relation)}
\end{definition}
\mbox{$I\inputs P\computes C$} is intended to mean that, when input
$I$ is presented to program $P$, one possible resulting computation is
$C$. \mbox{$C\outputs O$} is intended to mean that the computation
$C$ produces output $O$. Multiple computations\subind{multiple
computations}\subind{computation!multiple} for a given $P$ and $I$
are allowed, indicating nondeterminism,\subind{nondeterminism} but
each computation produces at most one output. The intended meaning of
a nondeterministic computation relation is that we do not know which
of the several possible computations will occur for a given input and
output \cite{Dijkstra}\auind{Dijkstra, E. W.}. The choice may be
determined by unknown and time-dependent factors, or it may be random.
In order to guarantee some property of the result of computation, we
must ensure that it holds for all possible nondeterministic choices.

In well-known programming systems from theory textbooks, programs,
inputs, and outputs (like formulae, proofs, and questions) are finite
syntactic objects, and the sets $\mathbold{P}$, $\mathbold{I}$, and
$\mathbold{O}$ are computable. Infinite computations\subind{infinite
computation}\subind{computation!infinite}, in the form of infinite
sequences of finite memory-state descriptions, are allowed, but in
theory textbooks the infinite computations normally have no output.
On the other hand, the straightforward abstractions of well-known
programming systems from real life (abstracted only by ignoring all
bounds on time and space resources in the computation) allow infinite
computations to consume infinite inputs and produce infinite outputs.
\subind{infinite input}\subind{infinite output}
\subind{output!infinite}\subind{input!infinite}

In many cases, we are interested only in the input-output behavior of
a program, and not in the computations themselves. So, we let each
programming system define a trinary relation determining the possible outputs
for a given program and input.
\begin{definition}\label{def:computed-output}
Let\/ \mbox{${\cal
P}=\langle\mathbold{P},\mathbold{I},\mathbold{C},\mathbold{O},
\inputs\:\computes,\outputs\rangle$}
be a programming system. The\/ {\em computed-output\/} relation
defined by\/ ${\cal P}$ is\/
\mbox{$\inputs\:\compout\subseteq\mathbold{P}\times
\mathbold{I}\times\mathbold{O}$}, where
\notind{$\inputs\:\compout$ (computed-output relation)}
\begin{center}
\mbox{$I\inputs P\compout O$} if and only if there exists a computation\/
\mbox{$C\in\mathbold{C}$}\\
such that\/ \mbox{$I\inputs P\computes C\outputs O$}.
\end{center}
\end{definition}
For a programming system to be useful, the computed-output relation
\mbox{$\inputs\:\compout$} must be sufficiently effective to allow a
mechanical implementation. Computed-output relations in theory
textbooks, like provable-consequence relations, are normally
semicomputable; computation and output relations $\inputs\:\computes$
and $\outputs$, like trinary proof relations $\hypos\:\proves$, are
normally computable (and even primitive recursive).  If $C$,
$\inputs\:\computes$, and $\outputs$ are all semicomputable, then so
is $\inputs\:\compout$. In fact, every
semicomputable\subind{semicomputable} computed-output relation
$\inputs\:\compout$ may be defined from computable $C$,
$\inputs\:\computes$, and $\outputs$. Systems with infinite inputs
and/or infinite outputs require more liberal, and less conventional,
notions of effectiveness.
\subind{infinite input}\subind{infinite output}
\subind{output!infinite}\subind{input!infinite}

The programming systems of Definition~\ref{def:programming-system} are
not required to be deterministic, or effective. They are a simple
generalization of the programming systems, also called {\em
indexings\/}\subind{indexing} and {\em G\"odel
numberings}\subind{Godel numbering@G\"odel numbering}, of recursion
theory \cite{Machtey-Young,Kleene}.
\auind{Machtey, M.}\auind{Young, P.}\auind{Kleene, S. C.}
Our \mbox{$I\inputs P\compout O$} corresponds
to the recursion-theoretic notation \mbox{$\phi_P(I)=O$}. Recursion
theory normally considers only {\em determinate\/} programming
systems.
\subind{deterministic}\subind{determinate}
\begin{definition}\label{def:deterministic}
A programming system\/ \mbox{${\cal
P}=\langle\mathbold{P},\mathbold{I},\mathbold{C},
\mathbold{O},\inputs\:\computes,\outputs\rangle$}
is\/ {\em determinate\/} if and only if, for each program\/ $P$ and
input\/ $I$, there is at most one output\/ $O$ such that\/
\mbox{$I\inputs P\compout O$}.  That is, $\inputs\:\compout$ is a
partial function from\/ \mbox{$\mathbold{P}\times\mathbold{I}$} to\/
$\mathbold{O}$.

A programming system\/ \mbox{${\cal
P}=\langle\mathbold{P},\mathbold{I},\mathbold{C},
\mathbold{O},\inputs\:\computes,\outputs\rangle$}
is\/ {\em deterministic\/} if and only if, for each program\/ $P$ and
input\/ $I$, there is a unique computation\/ $C$ such that\/
\mbox{$I\inputs P\computes C$}. That is, $\inputs\:\computes$ is a
partial function from\/ \mbox{$\mathbold{P}\times\mathbold{I}$} to\/
$\mathbold{C}$.
\end{definition}
Determinism implies determinacy, but not the converse---a
nondeterministic programming system may provide many computations that
yield the same determinate output.

\subind{Shallow Implicational Calculus|(}
\notind{SIC (Shallow Implicational Calculus)|(}
A number of different programming systems may be defined to answer
questions in the shallow implicational calculus, depending on the type
of question and the stringency of requirements for the answer.
\begin{example}\label{exa:programming-system-1}
Let\/ \mbox{$\impformulae=\{(a\limplies b)\setsep a,b\in\mbox{\bf At}\}$}
be the set of implicational SIC formulae (\/\mbox{$\sicformulae-\mbox{\bf
At}$}, with $\sicformulae$ and $\mbox{\bf At}$ defined in
Example~\ref{exa:semantic-system}). The set of\/ {\em implicational
logic programs\/} (\/$\impprograms$) is the set of finite subsets of
$\impformulae$.\\
\subind{implicational logic program}\notind{$\impprograms$
(implicational logic programs)}
Let the set of inputs to implicational logic programs
be\/ $\sicquestionsa$---the set of questions of the form
\mbox{$\mbox{\bf imp}(a)$} (`what atomic formula does $a$ imply?')
defined in Example~\ref{exa:query-system-1}.\\
The set of\/ {\em
naive implicational computations\/} ($\siccomputationsa$) is the set of
nonempty finite and infinite sequences of atomic formulae.\\
\subind{naive implicational computation}
\notind{$\siccomputationsa$ (naive implicational computations)}
The computation relation\/
\mbox{$\inputs\:\siccomputesa$}\notind{$\inputs\:\siccomputesa$ (naive
implicational computation relation)} is defined by\/
\mbox{$\mbox{\bf imp}(a)\inputs \mathbold{T}\siccomputesa\langle
c_0,c_1,\ldots\rangle$} if and only if
\begin{enumerate}
\item \mbox{$c_0=a$}
\item \mbox{$(c_{i-1}\limplies c_i)\in\mathbold{T}$} for all\/ \mbox{$i>0$}
in the (finite or infinite) range of the sequence\/ \mbox{$\langle
c_0,\ldots\rangle$}
\end{enumerate}
The output relation\/ $\sicoutputsa$\notind{$\sicoutputsa$
(implicational logic output relation)} is defined by $$\langle
c_0,\ldots,c_m\rangle\sicoutputsa(c_0\limplies c_m)$$ Infinite
computations have no output.\\
Now\/
\mbox{$\langle\impprograms,\sicquestionsa,\siccomputationsa,
\mathbold{F}_\limplies,\inputs\:\siccomputesa,\sicoutputsa\rangle$} is a
programming system, computing answers to questions of the form `what
atomic formula does $a$ imply?'
\end{example}
The programming system above behaves
nondeterministically\subind{nondeterminism} and
indeterminately\subind{indeterminacy} in proving some implication of
$a$. Its computations may halt at any point and output the latest
atomic conclusion found. Loops in the graph of implications lead to
infinite computations with no output. Notice that each finite
computation $\langle c_0,\ldots c_i,\ldots,c_m\rangle$, with output
\mbox{$(c_0\limplies c_m)$}, translates very easily into the linear
proof $$\langle(c_0\limplies c_0),\ldots,(c_{i-1}\limplies
c_i),(c_0\limplies c_i),\ldots,(c_{m-1}\limplies c_m),(c_0\limplies
c_m)\rangle$$ of \mbox{$(c_0\limplies c_m)$} in the proof system of
Example~\ref{exa:proof-system-linear}. The first line is an instance of
the reflexive rule, and subsequent lines alternate between
implications in $\mathbold{T}$, and applications of transitivity.

In order to avoid uninformative outputs, such as \mbox{$(a\limplies
a)$}, we need a programming system with a slightly more sophisticated
notion of when to stop a computation.
\subind{computation!with failure}
\begin{example}\label{exa:programming-system-2}
Let\/ $\mbox{\bf fail}$\notind{$fail$} be a new formal symbol, and let
the set of\/ {\em naive implicational computations with failure\/} be
\notind{$\siccomputationsb$ (implicational computations with failure)}
$$\siccomputationsb=\siccomputationsa\cup\{\langle
c_0,\ldots,c_m,\mbox{\bf fail}\rangle\setsep
c_0,\ldots,c_m\in\mbox{\bf At}\}$$ (the set of finite and infinite
sequences of atomic formulae, possibly ending in the special object
$\mbox{\bf fail}$).\\ Let the set of inputs to implicational logic
programs be\/ $\sicquestionsb$---the set of questions of the form
\mbox{$\mbox{\bf rest-imp}(a,\mathbold{A})$} (`what atomic formula not
in $\mathbold{A}$ does $a$ imply?').\\ The computation relation\/
\mbox{$\inputs\:\siccomputesb$}\notind{$\inputs\:\siccomputesb$}
is defined by\/ \mbox{$\mbox{\bf rest-imp}(a,\mathbold{A})\inputs
\mathbold{T}\siccomputesb\langle c_0,\ldots\rangle$} if and only if
\begin{enumerate}
\item \mbox{$c_0=a$}
\item if\/ \mbox{$c_i\in\mathbold{A}$}, and there is a\/
\mbox{$d\in\mbox{\bf At}$} such that\/
\mbox{$(c_i\limplies d)\in\mathbold{T}$}, then the sequence has an\/
$i+1$st element \mbox{$c_{i+1}$}, and\/
\mbox{$(c_i\limplies c_{i+1})\in\mathbold{T}$}
\item if\/ \mbox{$c_i\in\mathbold{A}$}, and there is no\/
\mbox{$d\in\mbox{\bf At}$} such that\/
\mbox{$(c_i\limplies d)\in\mathbold{T}$}, then the sequence has an\/
$i+1$st element, and\/
\mbox{$c_{i+1}=\mbox{\bf fail}$}
\item if\/ \mbox{$c_i\in\mbox{\bf At}-\mathbold{A}$}, then either there is no\/
$i+1$st element, or\/ \mbox{$(c_i\limplies c_{i+1})\in\mathbold{T}$}
\item if\/ \mbox{$c_i=\mbox{\bf fail}$}, then there is no $i+1$st element
\end{enumerate}
So, \mbox{$\inputs\:\siccomputesb$} allows computations to terminate
only when an atomic formula outside of $\mathbold{A}$ has been
found, or a dead end in the implication graph has been reached.\\
The output relation\/ $\sicoutputsb$ is defined by $$\langle
c_0,\ldots,c_m\rangle\sicoutputsb(c_0\limplies c_m)\mbox{ for }
c_m\in\mbox{\bf At}$$  Infinite
computations and finite computations ending in $\mbox{\bf fail}$ have
no output.\\
Now\/
\mbox{$\langle\impprograms,\sicquestionsb,\siccomputationsb,
\mathbold{F}_\limplies,\inputs\:\siccomputesb,\sicoutputsb\rangle$} is a
programming system, computing answers to questions of the form `what
atomic formula not in $\mathbold{A}$ does $a$ imply?'
\end{example}
The programming system of Example~\ref{exa:programming-system-2} is
nondeterministic\subind{nondeterminism} and
indeterminate\subind{indeterminacy}. It avoids useless answers, but it
still may fall into infinite or finite failing computations, even when
a legitimate answer exists. It also may find an answer, but fail to
output it and proceed instead into a failure or an infinite
computation. Successful computations translate into proofs as in
Example~\ref{exa:programming-system-1}.

We may further strengthen the behavior of a programming system by
letting it back up and try new proofs after finite failures, and by
insisting that answers be output as soon as they are found.
\subind{backtracking}
\begin{example}\label{exa:programming-system-3}
Let the set of inputs to implicational logic programs again be\/
$\sicquestionsb$---the set of questions of the form\/ \mbox{$\mbox{\bf
rest-imp}(a,\mathbold{A})$} (`what atomic formula not in $\mathbold{A}$ does $a$
imply?').\\ Let\/ $\mbox{\bf print}$\notind{$\mbox{\bf print}$} be a
new formal symbol. The set of\/ {\em backtracking implicational
computations\/} ($\siccomputationsc$)\notind{$\siccomputationsc$
(backtracking implicational computations)} is the set of nonempty
finite and infinite sequences of finite sets of atomic formulae,
possibly ending in the special form\/
\mbox{$\mbox{\bf print}(a)$} where\/ $a$ is an atomic formula
(\/$\mbox{\bf fail}$ of Example~\ref{exa:programming-system-2} is
represented now by the empty set).\\
The computation relation\/
\mbox{$\inputs\:\siccomputesc$}\notind{$\inputs:\siccomputesc$}
is defined by\/ \mbox{$\mbox{\bf rest-imp}(a,\mathbold{A})\inputs
\mathbold{T}\siccomputesc\langle\mathbold{C}_0,\ldots\rangle$}
if and only if\/
\begin{enumerate}
\item \mbox{$\mathbold{C}_0=\{a\}$}
\item if\/ \mbox{$\mathbold{C}_i\subseteq\mathbold{A}$} and\/
\mbox{$\mathbold{C}_i\neq\emptyset$}, then there is an\/ $i+1$st element,
and $$\mathbold{C}_{i+1}=\mathbold{C}_i-\{c\}\cup\{d\setsep(c\limplies
d)\in\mathbold{T}\}$$
for some atomic formula\/ \mbox{$c\in\mathbold{C}_i$}
\item if\/ \mbox{$\mathbold{C}_i\subseteq\mbox{\bf At}$}, and\/
\mbox{$\mathbold{C}_i-\mathbold{A}\neq\emptyset$}, then there is an\/
$i+1$st element, and\/
\mbox{$\mathbold{C}_{i+1}=\mbox{\bf print}(c)$} for some\/
\mbox{$c\in\mathbold{C}_i-\mathbold{A}$}
\item if\/ \mbox{$\mathbold{C}_i=\emptyset$}, or\/
\mbox{$\mathbold{C}_i=\mbox{\bf print}(c)$}, then there is no\/ $i+1$st element
\end{enumerate}
So, \mbox{$\inputs\:\siccomputesc$} allows a computation to replace
any atomic formula that has already been proved with the set of atomic
formulae that it implies directly in $\mathbold{T}$. A computation
halts precisely when it chooses a unique atomic formula not in
$\mathbold{A}$ to output, or when it fails by producing the empty
set.\\ The output relation\/ $\sicoutputsc$ is defined by
$$\langle\{a\},\ldots,\mbox{\bf
print}(b)\rangle\sicoutputsc(a\limplies b)$$ Infinite computations,
and finite computations ending in $\emptyset$, have no output.\\ Now\/
\mbox{$\langle\impprograms,\sicquestionsb,\siccomputationsc,
\mathbold{F}_\limplies,\inputs\:\siccomputesc,\sicoutputsc\rangle$}
is another programming system, computing answers to questions of the
form `what atomic formula not in $\mathbold{A}$ does $a$ imply?'
\end{example}
The programming system of Example~\ref{exa:programming-system-3} is
nondeterministic\subind{nondeterminism} and
indeterminate\subind{indeterminacy}. It is less susceptible to missing
answers than that of Example~\ref{exa:programming-system-2}. The new
system does not get stuck with a failure when a single path in the
implication graph leads to a dead end: a computation ends in
$\emptyset$ only when {\em all} paths have been followed to a dead
end. When there is a finite path to an answer, and also a cycle, the
nondeterministic choice of which formula to replace at each step
determines which path is followed in the computation, and so
determines success or infinite computation. The translation of a
computation in the latest system to a proof is not quite as
transparent as in Examples
\ref{exa:programming-system-1} and
\ref{exa:programming-system-2}, but it is still simple. Each
successful computation
\mbox{$\langle\{c_0\},\mathbold{C}_1,\ldots,\mathbold{C}_{m-1},\mbox{\bf
print}(c_m)\rangle$} must contain a sequence of atomic formulae
\mbox{$\langle c_0,c_1,\ldots,c_{m-1},c_m\rangle$}, where for $i<m$
\mbox{$c_i\in\mathbold{C}_i$}, and for adjacent pairs $c_i,c_{i+1}$, either
\mbox{$c_i=c_{i+1}$}, or \mbox{$(c_i\limplies c_{i+1})\in\mathbold{T}$}.
This sequence of atomic formulae transforms to a linear proof as
before.
\subind{Shallow Implicational Calculus|)}
\notind{SIC (Shallow Implicational Calculus)|)}

\subind{incremental output|(}\subind{output!incremental|(}
A final example of a programming system illustrates the use of
incremental output from possibly infinite computations to produce
consequentially strong answers.
\begin{example}\label{exa:programming-system-4}
\subind{conjunctive implicational computation}
Let the set of inputs to implicational logic programs be\/
$\sicquestionsc$---the set of questions of the form\/ \mbox{$\mbox{\bf
conj-imp}(a)$} (`what are some atomic formulae that $a$ implies?')
from Example~\ref{exa:strongest-answer}.\\ The set of\/ {\em
conjunctive implicational computations\/} (\/$\siccomputationsd$) is
\notind{$\siccomputationsd$ (conjunctive implicational computations)}
the set of nonempty finite or infinite sequences of finite sets of
atomic formulae (the same as\/ $\siccomputationsc$, without the final
elements\/ \mbox{$\mbox{\bf print}(a)$}).\\ The computation relation\/
\mbox{$\inputs\:\siccomputesd$}\notind{$\inputs\:\siccomputesd$}
is defined by\/ \mbox{$\mbox{\bf conj-imp}(a)\inputs\mathbold{T}\siccomputesd
\langle\mathbold{C}_0,\ldots\rangle$}
if and only if\/
\begin{enumerate}
\item \mbox{$\mathbold{C}_0=\{a\}$}
\item if\/ \mbox{$\mathbold{C}_i\neq\emptyset$}, then there is an\/ $i+1$st
element, and $$\mathbold{C}_{i+1}=
(\mathbold{C}_i-\{c\})\cup\{d\setsep(c\limplies d)\in\mathbold{T}\}$$
for some atomic formula\/ \mbox{$c\in\mathbold{C}_i$}
\item if\/ \mbox{$\mathbold{C}_i=\emptyset$}, then there is no\/ $i+1$st
element
\end{enumerate}
The computations above are the same as those of
Example~\ref{exa:programming-system-3}, except that we never choose a
single atomic formula to output. $\emptyset$ is no longer regarded as
a failure.\\
The output relation\/ $\sicoutputsd$ is defined by\/
\mbox{$\langle\mathbold{C}_0,\ldots\rangle\sicoutputsd(a\limplies
b_1)\land\cdots\land(a\limplies b_m)$} if and only if
\begin{enumerate}
\item \mbox{$\mathbold{C}_0=\{a\}$}
\item \mbox{$\{b_1,\ldots b_m\}=\mathbold{C}_0\cup\mathbold{C}_1\cup\cdots$},
and $b_1,\ldots b_m$ are given in the order of first appearance in the
sequence $\mathbold{C}_0,\ldots$, with ties broken by some arbitrary
ordering of atomic formulae
\end{enumerate}
Notice that even infinite computations have output.\\
Now\/ \mbox{$\langle\impprograms,\sicquestionsc,\siccomputationsd,
\mathbold{F}_\limplies,\inputs\:\siccomputesd,\sicoutputsd\rangle$} is a
programming system, computing answers to questions of the form `what
are some atomic formulae that $a$ implies?'
\end{example}
The programming system above should be thought of as producing its
output incrementally at each computation step. It is
nondeterministic\subind{nondeterminism} and
indeterminate\subind{indeterminacy}. Even though the computation may
be infinite, it never fails to produce an answer, although the output
may be the trivial formula \mbox{$a\limplies a$}. The strength of
the answer produced depends on the nondeterministic choices of the
atomic formula replaced in each computation step.
\subind{incremental output|)}\subind{output!incremental|)}

\subsection{Soundness and Completeness of Programming Systems}
\label{sec:sound-complete-program}

\subind{sound programming system|(}\subind{programming system!sound|(}
\subind{complete programming system|(}\subind{programming system!complete|(}
A query system determining what constitutes an answer, and the
semantic-consequence relation of a semantic system determining the
correctness of an answer, yield criteria for evaluating the behavior
of a programming system, similarly to the criteria for evaluating a
proof system in Section~\ref{sec:proof-system}. We define {\em
soundness\/} and {\em completeness\/} of programming systems, in
analogy to the soundness and completeness of proof systems. Logic
programming is distinguished from other sorts of programming by the
use of such logical concepts to evaluate programming systems.
\subind{logic programming!distinct from other approaches|)}

There is only one sensible concept of soundness for a programming
system: every output is a correct answer to the input program.  When a
given question has more than one correct answer, completeness criteria
vary depending on the way in which we expect an output answer to be
chosen.
\begin{definition}\label{def:sound-complete-program}
Let\/ \mbox{${\cal P}=\langle\mathbold{P},\mathbold{I},
\mathbold{C},\mathbold{O},\inputs\:\computes,\outputs\rangle$}
be a programming system, let\/
\mbox{${\cal S}=\langle\mathbold{F}_{\rm S},\mathbold{M},\models\rangle$} be a
semantic system, and let\/ \mbox{${\cal Q}=\langle\mathbold{F}_{\rm Q},
\mathbold{Q},\answers\rangle$} be a query system, with\/
\mbox{$\mathbold{P}\subseteq\powerset{\mathbold{F}_{\rm S}}$},
\mbox{$\mathbold{I}\subseteq\mathbold{Q}$}, and\/
\mbox{$\mathbold{O}\subseteq\mathbold{F}_{\rm S}\cap\mathbold{F}_{\rm
Q}$}.

${\cal P}$ is\/ {\em sound\/} for\/ ${\cal S}$ and\/ ${\cal Q}$ if and
only if, for all\/ \mbox{$P\in\mathbold{P}$} and\/ \mbox{$I\in\mathbold{I}$},
$$I\inputs P\compout O\mbox{ implies }I\answers P\models O$$

\subind{weakly complete}\subind{complete!weakly}
${\cal P}$ is\/ {\em weakly complete\/} for\/ ${\cal S}$ and\/ ${\cal
Q}$ if and only if, for all\/ \mbox{$P\in\mathbold{P}$} and\/
\mbox{$I\in\mathbold{I}$} such that\/ $I$ is semantically answerable for
$P$ (Definition~\ref{def:semantically-correct-answer}), and for all
computations\/ \mbox{$C\in\mathbold{C}$} such that\/
\mbox{$I\inputs P\computes C$}, there exists\/ \mbox{$O\in\mathbold{O}$}
such that $$C\outputs O\mbox{ and }I\answers P\models O$$
($O$ is unique because $\outputs$ is a partial function).

\subind{consequentially complete}\subind{complete!consequentially}
${\cal P}$ is\/ {\em consequentially complete\/} for\/ ${\cal S}$
and\/ ${\cal Q}$ if and only if ${\cal P}$ is weakly complete and, in
addition, $O$ above is a consequentially strongest correct answer
(\/\mbox{$\{O\}\models N$} for all\/ \mbox{$N\in\mathbold{F}_{\rm Q}$} such
that\/ \mbox{$I\answers P\models N$}).
\end{definition}
So, a programming system is sound if all of its outputs are correct
answers to input questions, based on the knowledge represented
explicitly by programs. A system is weakly complete if, whenever a
correct answer exists, every computation outputs some correct answer.
A system is consequentially complete if, whenever a correct answer
exists, every computation outputs a consequentially strongest correct
answer. Notice that, for consequential completeness, the strength of
the output answer is judged against all possible answers in the query
system, not just those that are possible outputs in the programming
system, so we cannot achieve consequential completeness by the
trickery of disallowing the truly strongest answers.

\subind{communication|(}
\subind{knowledge|(}
\subind{logic!representing communication and knowledge|(}
\subind{answer|(}
\subind{query system|(}
\subind{question|(}
\subind{proof system|(}
\subind{questioner|(}
\subind{speaker|(}
\subind{auditor|(}
\subind{programmer|(}
\subind{processor|(}
\subind{user|(}
\subind{input|(}
\subind{output|(}
\subind{computation|(}
A programming system provides another approach to analyzing a simple
form of communication. While semantic systems, proof systems, and
query systems yield insight into the meaning of communication and
criteria for evaluating the behavior of communicating agents,
programming systems merely describe that behavior. A programmer
provides a program $P$ to a processor. A user (sometimes, but not
always, identical with the programmer) provides an input $I$, and the
processor performs a computation $C$ such that \mbox{$I\inputs
P\computes C$} from which the output $O$, if any, such that
\mbox{$C\outputs O$}, may be extracted. We allow the mapping from
computation to output to depend on purely conventional rules that are
adopted by the three agents. What aspects of a computation are taken
to be significant to the output is really a matter of convention, not
necessity. Often, only the string of symbols displayed on some
printing device is taken to be the output, but in various contexts the
temporal order in which they are displayed (which may be different
from the printed order if the device can backspace), the temporal or
spatial interleaving of input and output, the speed with which output
occurs, the color in which the symbols are displayed, which of several
devices is used for display, all may be taken as significant.  Also,
convention determines the treatment of infinite computation as having
no output, null output, or some nontrivial and possibly infinite
output produced incrementally. The presentation of input to a
computation is similarly a matter of accepted convention, rather than
formal computation.

In logic programming, where the programmer acts as speaker, the
processor as auditor, and the user as questioner, soundness of the
programming system guarantees that all outputs constitute correct
answers. Various forms of completeness guarantee that answers will
always be produced when they exist.  In this sense, soundness and
completeness mean that a programming system provides a correct and
powerful implementation of the auditor in the
speaker-auditor-questioner scenario of
Section~\ref{sec:query-systems}.
\subind{communication|)}
\subind{knowledge|)}
\subind{logic!representing communication and knowledge|)}
\subind{answer|)}
\subind{query system|)}
\subind{question|)}
\subind{proof system|)}
\subind{questioner|)}
\subind{speaker|)}
\subind{auditor|)}
\subind{programmer|)}
\subind{processor|)}
\subind{user|)}
\subind{input|)}
\subind{output|)}
\subind{computation|)}

\subind{program!vs.\ theory|(}\subind{proof!vs.\ theory|(}
\subind{input!vs.\ query|(}\subind{query!vs.\ input|(}
\subind{output!vs.\ theorem|(}\subind{theorem!vs.\ output|(}
\subind{computation!vs.\ proof|(}\subind{proof!vs.\ computation|(}
There is a close formal correspondence between programming systems and
pairs of proof and query systems: inputs correspond to questions,
programs correspond to sets of hypotheses, computations to proofs, and
outputs to theorems (for a different correspondence, in which programs
in the form of lambda terms correspond to natural deduction proofs,
see \cite{Howard,Tait,Constable-Allen-Bromley}---compare
\auind{Constable, R. L.}\auind{Allen, S. F.}\auind{Bromley, H. M.}
\auind{Cleaveland, W. R.}\auind{Cremer, J. F.}\auind{Harper, R. W.}
\auind{Howe, D. J.}\auind{Knoblock, T. B.}\auind{Mendler, N. P.}
\auind{Panangaden, P.}\auind{Sasaki, J. T.}\auind{Smith, S. F.}
\auind{Howard, W.}\auind{Tait, W. W.} this
to the interpretation of formulae as queries and proofs as answers
\cite{Meseguer-general}\auind{Meseguer, J.}). Notice that both
quaternary relations \mbox{$Q\answers\mathbold{T}\hypos D\proves F$}
and \mbox{$I\inputs P\computes C\outputs O$} are typically computable,
while both of the trinary relations $Q\answers\mathbold{T}\hyproves F$
and \mbox{$I\inputs P\compout O$} are typically
semicomputable\subind{semicomputable}. Furthermore, the definitions of
the trinary relations from the corresponding quaternary relations are
analogous. In both cases we quantify existentially over the third
argument, which is variously a proof or a computation.

There is an important difference, however, between the forms of
definition of the provable-answer relation
\mbox{$Q\answers\mathbold{T}\hypos D\proves
F$},\notind{$\answers\hypos\:\proves$ (quaternary answer relation)}
and of the computational relation \mbox{$I\inputs P\computes C\outputs
O$},\notind{$\inputs\:\computes\:\outputs$ (quaternary computation
relation)} reflecting the difference in intended uses of these
relations. This difference has only a minor impact on the relations
definable in each form, but a substantial impact on the efficiency of
straightforward implementations based on the definitions. In the
query-proof domain, we relate formulae giving explicit knowledge
(program) to the proofs (computations) that can be constructed from
that knowledge, yielding formulae (outputs) that are provable
consequences of the given knowledge in the relation
\mbox{$\mathbold{T}\hypos D\proves F$}.\notind{$\hypos\:\proves$
(trinary proof relation)} We independently relate
questions (inputs) to the answers (outputs) in the relation
\mbox{$Q\answers F$}\notind{$\answers$ (answer relation)},
and then take the conjunction of the two. There is no formal provision
for the question (input) to interact with the knowledge formulae
(program) to guide the construction of the proof (computation)---the
question (input) is only used to select a completed proof. In the
computational domain, we relate inputs (questions) directly to
programs (knowledge formulae) to determine computations (proofs) that
they can produce in the relation
\mbox{$I\inputs P\computes C$}\notind{$\inputs\:\computes$ (trinary
computation relation)}. Then, we extract outputs (answer
formulae) from computations (proofs) in the relation
\mbox{$C\outputs O$}\notind{$\outputs$ (output relation)}.
The relation \mbox{$I\inputs P\computes C$} provides a formal concept
that may be used to represent the interaction of input (question) with
program (knowledge) to guide the construction of the computation
(proof).

Given a proof system and a query system, we can construct a
programming system with essentially the same behavior. This
translation is intended as an exercise in understanding the formal
correspondence between proofs and computations. Since our
requirements for proof systems and programming systems are quite
different, this construction does {\em not\/} normally lead to useful
implementations.
\begin{proposition}\label{pro:proof-to-program}
Let\/ \mbox{${\cal D}=\langle\mathbold{F},\mathbold{D},\hypos\:\proves\rangle$}
be a proof system, and let\/ \mbox{${\cal Q}=\langle\mathbold{F},
\mathbold{Q},\answers\rangle$} be a query system.  Define the programming
system
$${\cal P}=\langle\powerset{\mathbold{F}},\mathbold{Q},(\mathbold{D}\times
\mathbold{F})\cup\{\mbox{\bf fail}\},\mathbold{F},\inputs\:
\computes,\outputs\rangle$$ where
\begin{enumerate}
\item \mbox{$Q\inputs\mathbold{T}\computes\langle P,F\rangle$}
if and only if\/ \mbox{$Q\answers\mathbold{T}\hypos P\proves F$}
\item \mbox{$Q\inputs\mathbold{T}\computes\mbox{\bf fail}$} if and only if
there are no\/ $P$ and\/ $F$ such that\/ \mbox{$Q\answers\mathbold{T}\hypos
P\proves F$}
\item \mbox{$\langle P,F\rangle\outputs
G$} if and only if\/ \mbox{$F=G$}
\item \mbox{$\mbox{\bf fail}\outputs F$} is false for all\/
\mbox{$F\in\mathbold{F}$}
\end{enumerate}
Then, $$Q\answers\mathbold{T}\hypos P\proves F\mbox{ if and only if }
Q\inputs\mathbold{T}\computes\langle P,F\rangle\outputs F$$  Therefore,
$$Q\answers\mathbold{T}\hyproves F\mbox{ if and only if }
Q\inputs\mathbold{T}\compout F$$
\end{proposition}
If ${\cal D}$ above is sound for some semantic system ${\cal S}$, then
${\cal P}$ is sound for ${\cal S}$ and ${\cal Q}$, but the
converse fails because some formulae may never occur as answers to
questions.  Proposition~\ref{pro:proof-to-program} shows that a proof
may be interpreted as a nondeterministically chosen computation that
outputs a theorem.

Because hypotheses to proofs are sets of formulae, rather than single
formulae, and the proof relation must be monotone with respect to the
subset relation, there are computational relations
\mbox{$\inputs\:\compout$} defined by programming systems that are not
the same as the relation \mbox{$\answers\:\hyproves$} of any proof and
query systems. Intuitively, in order to mimic an arbitrary
programming system with a proof system and a query system, we must
augment the output $O$ resulting from input $I$ into a formula
asserting that {\em input $I$ produces output $O$}. This augmentation
is almost trivial, in the sense that echoed input may just as well be
regarded as an implicit part of the output. Informal question
answering uses such implicit augmentation:  in response to the
question `what is the capital city of Idaho?' the abbreviated answer
`Boise' is generally accepted as equivalent to the full answer `the
capital city of Idaho is Boise.'

\begin{proposition}\label{pro:program-to-proof}
Let\/ \mbox{${\cal P}=\langle\mathbold{P},\mathbold{I},\mathbold{C},\mathbold{O}\rangle$} be a
programming system. Define the proof system\/ \mbox{${\cal D}=\langle
\mathbold{P}\cup(\mathbold{I}\times\mathbold{O}),\mathbold{C},\hypos\:
\proves\rangle$}, where
\begin{enumerate}
\item \mbox{$\mathbold{T}\hypos C\proves\langle I,O\rangle$} if and only if\/
\mbox{$I\inputs P\computes C\outputs O$} for some\/ \mbox{$P\in\mathbold{T}$}
\item \mbox{$\mathbold{T}\hypos C\proves P$} is false for all\/ \mbox{$P\in\mathbold{P}$}
\end{enumerate}
Also define the query system\/
\mbox{${\cal Q}=\langle\mathbold{I}\times\mathbold{O},\mathbold{I},\answers\rangle$},
where
\begin{enumerate}
\item \mbox{$I\answers\langle J,O\rangle$} if and only if\/
\mbox{$I=J$}.
\end{enumerate}
Then, $$I\inputs P\computes C\outputs O\mbox{ if and only if
}I\answers\{P\}\hypos C\proves\langle I,O\rangle$$ Therefore,
$$I\inputs P\compout O\mbox{ if and only if }
I\answers\{P\}\hyproves\langle I,O\rangle$$
\end{proposition}
As in the construction of Proposition~\ref{pro:proof-to-program},
soundness of ${\cal D}$ implies soundness of ${\cal P}$, but the
converse fails, and completeness does not transfer either way.
Proposition~\ref{pro:program-to-proof} shows that a computation may be
interpreted as a proof that a given program and input produce a
certain output.
\subind{program!vs.\ theory|)}\subind{proof!vs.\ theory|)}
\subind{input!vs.\ query|)}\subind{query!vs.\ input|)}
\subind{output!vs.\ theorem|)}\subind{theorem!vs.\ output|)}
\subind{computation!vs.\ proof|)}\subind{proof!vs.\ computation|)}

\begin{example}\label{exa:sound-complete-program}
The programming systems of Examples \ref{exa:programming-system-1},
\ref{exa:programming-system-2},
\ref{exa:programming-system-3}, and
\ref{exa:programming-system-4} are all sound for their appropriate
semantic and query systems.  The proof of soundness is easy---every
computation can be transformed easily into a proof in a sound proof
system.

\subind{naive implicational computation|(}
The programming system of naive implicational computations in
Example~\ref{exa:programming-system-1} is not weakly complete.
Consider the program $$\{a\limplies b,\;b\limplies
a,\;a\limplies c\}$$  Given the input question\/ \mbox{$\mbox{\bf
imp}(a)$} (`what logical formula does\/ $a$ imply?'), a possible
computation is the infinite sequence
$$\langle a,b,a,b,\ldots\rangle$$ which has no output.  There
are three correct answers, $$a\limplies a\mbox{, }a\limplies
b\mbox{, and }a\limplies c$$ each of which is found by a short
computation.
\subind{naive implicational computation|)}

\subind{computation!with failure|(}
The programming system of naive implicational computations with
failure in Example~\ref{exa:programming-system-2} is not weakly
complete.  Consider the program $$\{a\limplies b,\;a\limplies
c,\;c\limplies a,\;a\limplies d\}$$  Given the input question\/
\mbox{$\mbox{\bf rest-imp}(a,\{a,b,c\})$} (`what logical formula not
in\/ \mbox{$\{a,b,c\}$} does\/ $a$ imply?'), two possible computations
with no output are $$\langle a,b,\mbox{\bf fail}\rangle\mbox{ and }
\langle a,c,a,c,\ldots\rangle$$  There is a correct answer,
\mbox{$a\limplies d$}, which is found by the computation\/
\mbox{$\langle a,d\rangle$}.
\subind{computation!with failure|)}

\subind{backtracking|(}
The programming system of backtracking implicational computations in
Example~\ref{exa:programming-system-3} avoids the finite failure of
the naive computations with failure, but is still not weakly complete
because of infinite computations.  It succeeds on the program and
question above, with the unique computation
$$\langle\{a\},\{b,c,d\},\{d\}\rangle$$ but fails on a slightly
trickier case.  Consider the program $$\{a\limplies b,\;a\limplies
c,\;c\limplies a,\;a\limplies d,\;d\limplies e\}$$ and the question\/
\mbox{$\mbox{\bf rest-imp}(a,\{a,b,c,d\})$}.  There is no finite
failing computation, and the correct answer\/
\mbox{$a\limplies e$} is output by the computation
$$\langle\{a\},\{b,c,d\},\{b,d\},\{a,d\},\{a,e\},
\mbox{\bf print}(e)\rangle$$
But there is still an infinite computation that misses the output:
$$\langle\{a\},\{b,c,d\},\{b,a,d\},\{b,c,d\},\ldots\rangle$$
\subind{backtracking|)}

\subind{conjunctive implicational computation|(}
The programming system of conjunctive implicational computations in
Example~\ref{exa:programming-system-4} is weakly complete, simply
because every computation outputs some correct answer of the form\/
\mbox{$(a\limplies a)\land\ldots$}, where in the worst case only the
first conjunct is given.  This system was clearly aimed, however,
toward producing consequentially strong answers.  It is not
consequentially complete.  Consider again the program
$$\{a\limplies b,\;a\limplies c,\;c\limplies a,\;a\limplies
d,\;d\limplies e\}$$ and the new question\/ \mbox{$\mbox{\bf
conj-imp}(a)$}.  The computation
$$\langle\{a\},\{b,c,d\},\{b,c,e\},\{b,a,e\},\{b,c,d,e\},\{b,a,d,e\},\{b,c,d,e\},\ldots\rangle$$
outputs the consequentially strongest answer
$$(a\limplies a)\land(a\limplies b)\land(a\limplies
c)\land(a\limplies d)\land(a\limplies e)$$
But the computation
$$\langle\{a\},\{b,c,d\},\{b,a,d\},\{b,c,d\},\ldots\rangle$$
outputs only the weaker answer
$$(a\limplies a)\land(a\limplies b)\land(a\limplies c)\land(a\limplies d)$$
missing the conjunct\/ \mbox{$a\limplies e$}.
\end{example}
\subind{conjunctive implicational computation|)}
In each case above, the failure of completeness results from the
possibility of unfortunate choices for the next computational step.

\subind{implementation!evaluating soundness and completeness|(}
Most practical implementations of logic programming languages are not
complete, and many are not even sound. Nonetheless, soundness and
completeness are useful standards against which to judge
implementations. Most implementations are sound and complete for
well-characterized subsets of their possible programs and inputs.  The
cases where soundness and/or completeness fail are typically
considered at least peculiar, and sometimes pathological, and they are
the topics of much discussion and debate. The history of programming
languages gives some hope for a trend toward stricter adherence at
least to soundness criteria. For example, early
Lisp\subind{Lisp!dynamic scope} processors employed dynamic scoping,
which is essentially an unsound implementation of logical
substitution. Modern Lisp processors are usually statically scoped,
and provide sound implementations of
substitution \cite{Muchnick-Pleban,Brooks-Gabriel-Steele,Rees-Clinger}.
\auind{Brooks, R. A.}\auind{Gabriel, R. P.}\auind{Steele, G. L.}
\auind{Rees, J.}\auind{Clinger, W.}\auind{Muchnick, S. S.}
\auind{Pleban, U. F.}
As compiler technology matured, the logically correct static scoping
was found to be more efficient than dynamic scoping, although early
work assumed the contrary. \subind{implementation!evaluating
soundness and completeness|)}

In spite of the close formal correspondence outlined above between
proof and computation, our natural requirements for proof systems and
programming systems differ significantly. The requirements for
correctness, formalized as soundness, are essentially the
same---everything that is proved/computed must be a logical
consequence of given information. But, the requirements for power,
formalized as completeness, vary substantially.

\subind{complete!proof vs.\ computation|(}
Proofs are thought of as things to search for, using any available
tools whether formal, intuitive, or inspirational, and we only demand
formal or mechanical verification of the correctness of a proof, not
mechanical discovery of the proof. So, proofs are quantified
existentially in the definition of completeness of a proof system, and
we are satisfied with the mere existence of a proof of a given true
formula. Computations, on the other hand, are thought of as being
generated on demand by a computing agent in order to satisfy the
requirement of a user. So, we require that a complete programming
system be guaranteed to produce a sufficiently strong correct answer
whenever a correct answer exists. Since we do not know which of
several possible computations will be generated nondeterministically
by the computing agent, we quantify universally over computations.
\subind{complete!proof vs.\ computation|)}

Because of the requirement that {\em all\/} computations in a complete
programming system yield correct answers, merely mimicking the
relational behavior of a proof system, as in
Proposition~\ref{pro:proof-to-program}, is not sufficient for useful
implementation. Practical implementations must use complete {\em
strategies\/} for choosing proofs in order to provide programming
systems with the desired guaranteed results.
\subind{logic programming!abstract implementation|)}
\subind{sound programming system|)}\subind{programming system!sound|)}
\subind{complete programming system|)}\subind{programming system!complete|)}

\subsection{Proof-Theoretic Foundations for Logic Programming}
\label{sec:proof-theory}

\subind{proof theory|(}\subind{proof strategy|(}
Given a suitable proof system, a practical implementation of a logic
programming language still must solve the difficult problem of
searching the set of proofs for one that provides an answer to a given
input question. Methods for choosing and generating proofs are called
{\em proof strategies.} While logical semantics provides the
conceptual tools for specifying logic programming languages, {\em
proof theory\/} \cite{Stenlund,Prawitz,Takeuti,Schutte,Girard}\subind{proof theory}.
\auind{Stenlund, S.}\auind{Prawitz, D.}\auind{Takeuti,
G.}\auind{Schutte, K.}\auind{Girard, J.-Y.}\auind{Lafont,
Y.}\auind{Taylor, P.} provides the tools for developing proof
strategies. Once a proof strategy has been defined, the remaining
problems in implementation are the invention of appropriate algorithms
and data structures for the strategy, and the details of code
generation or interpreting. The organization of logic programming into
the application of semantics to specification, and the application of
proof theory to implementation, does {\em not\/} mean, however, that
the former precedes the latter in the design of a logic programming
language. Design normally requires the simultaneous consideration of
specification and implementation, and the designer must search the two
spaces of semantic specifications and proof-theoretic strategies in
parallel for a compatible pair of ideas. In different circumstances
either topic can be the primary driver of design decisions.  In
writing this chapter, I have not been able to develop the proof
theoretic side of logic programming design as thoroughly as the
semantic side, merely because I ran out of time, pages, and energy. In
this section, I will only outline the issues involved in applying
proof theory to logic programming.

The choice of a proof strategy affects both the power and the
complexity of an implementation, but not the soundness. Given a sound
proof system, a proof strategy can only choose (or fail to find) a
correct proof, it cannot expand the class of proofs.
\subind{sound proof system}\subind{proof system!sound}
\subind{sound programming system}\subind{programming system!sound}
But, a given proof strategy may be incapable of discovering certain
provably correct answers, so it may yield an incomplete computing
system, even when starting with a complete proof system.
\subind{complete proof system}\subind{proof system!complete}
\subind{complete programming system}\subind{programming system!complete}
So, there is great value in proof theoretic theorems demonstrating
that, whenever a formula $F$ is provable, there is a proof in some
usefully restricted form. Even when these do not lead to complete
implementations, they can improve the power/complexity tradeoff
dramatically. Fortunately, proof theorists have concentrated a lot of
attention on such results, particularly in the form of {\em proof
normalization\/} theorems, which show that all proofs may be reduced
to a normal form with special structure. Many normalization results
are expressed as {\em cut elimination\/} theorems, showing that a
particular version of {\em modus ponens\/} called the {\em cut\/} rule
may be removed from proofs. Cut elimination theorems are usually
associated with the predicate calculus and its fragments, variants,
and extensions. The impact of cut elimination on proof strategies has
been studied very thoroughly, leading to an excellent characterization
of the sequent-style proof systems that are susceptible to
generalizations of the simple goal-directed proof strategy used in
Prolog~\cite{Miller-Nadathur-Pfenning-Scedrov}\auind{Pfenning,
F.}\auind{Scedrov, A.}. These proof-theoretic methods have been
applied successfully in some novel logics where the model-theoretic
semantics are not yet properly understood.

\subind{equational logic|(}\subind{term rewriting|(}
In the term rewriting literature, there are similar results on the
normalization of equational proofs. Many of these come from {\em
confluence\/} (also called {\em Church-Rosser\/}) results.
\subind{confluence}\subind{Church-Rosser property}
A system of equations $$\{l_1\formeq r_1,\ldots,l_m\formeq r_m\}$$
presented with each equation oriented in a particular left-right
order, is {\em confluent\/} precisely if every proof of an equation
$s\formeq t$ may be transformed into a rewriting of each of $s$ and
$t$ to a common form $u$. {\em Rewriting\/} means here that an
equational hypothesis $l_i\formeq r_i$ may only be used from left to
right, to replace instances of $l_i$ by corresponding instances of
$r_i$ but not the reverse. The restriction of equational proofs to
rewritings allows complete strategies that are much simpler and more
efficient than those that search through all equational proofs. See
Sections
\ref{sec:rewrite-proof} and \ref{sec:confluence} of the chapter
`Equational Logic Programming' in this volume, as well as
\cite{Klop-term}, for more on the application of term rewriting to
equational proofs.
\subind{equational logic|)}\subind{term rewriting|)}
\subind{proof theory|)}\subind{proof strategy|)}

\section{The Uses of Semantics}
\label{sec:uses-of-semantics}

\subind{semantics!uses|(}
The development of logic programming systems from logics, given above,
provides a particular flavor of semantics, called {\em logical
semantics,} for logic programming languages. Logical semantics,
rather than competing directly with other flavors of programming
language semantics, provides different insights, and is useful for
different purposes. The careful comparison of different styles of
semantics is a wide-open area for further research. In this section, I
sketch the sort of relations that I believe should be explored between
logical semantics, denotational semantics, and algebraic semantics.
Meseguer proposes two sorts of logic programming---`weak' logic
programming uses essentially the same notion of logical semantics as
mine, while `strong' logic programming uses the theory of a single
model, such as a model derived by algebraic semantics
\cite{Meseguer-general}\auind{Meseguer, J.}.

\subsection[Logical vs.\ Denotational]
{Logical Semantics vs.\ Denotational Semantics}
\label{sec:logical-denotational}

\subind{semantics!logical vs.\ denotational|(} \subind{denotational
semantics|(}\subind{semantics!denotational|(} Roughly, denotational
semantics \cite{Scott,Scott-Strachey,Stoy}\auind{Scott,
D.}\auind{Strachey, C.}\auind{Stoy, J. E.} takes the meaning of a
program to be an abstract description of its input/output behavior,
where inputs and outputs are uninterpreted tokens. Denotational
semantics assigns to each program a unique value carrying that
meaning. One problem of denotational semantics is how to deal with
observable computational behavior, such as nontermination, that does
not produce output tokens in the concrete sense. This problem was
solved by expanding the domains of input and output, as well as the
domains of program meanings, to partially ordered sets (usually
chain-complete partial orderings \cite{Markowsky}\auind{Markowsky, G.}
or lattices \cite{Scott-lattice}\auind{Scott, D.}) containing objects
representing abstract computational behaviors, not all of which
produce tokens as output \cite{Reynolds,Scott-domain}.
\auind{Reynolds, J. C.}\auind{Scott, D.}
In practice, the definition of appropriate domains is often the most
challenging task in creating a denotational semantic description of a
programming language, and {\em domain theory\/}\subind{domain theory}
has become a definite specialty in theoretical computer science
\cite{Schmidt,Stoy,Zhang,Gunter,Winksel}.
\auind{Schmidt, D. A.}\auind{Stoy, J. E.}\auind{Zhang, G.-Q.}
\auind{Winksel, G.}\auind{Gunter, C. A.}

The denotational approach provides a useful tool for characterizing
what a particular type of implementation actually does, but it does
not give any intuitive basis for discussing what an implementation
{\em ought\/} to do. Logical semantics, on the other hand, begins with
an interpretation of input and output. It does not directly address
techniques for analyzing the behavior of programs---that is left to a
metalanguage. But it {\em does\/} provide an intuitive basis for
distinguishing logically reasonable behaviors from other behaviors.

For example, denotational semantics for functional languages was
initially defined using eager evaluation
\cite{Backus-turing}\auind{Backus, J.} The domains that were used to define
eager evaluation are not rich enough to represent lazy evaluation. In
fact the definition of domains for lazy evaluation
\cite{Winksel}\auind{Winksel, G.}
posed difficult technical problems, causing resistance
to the use of lazy evaluation.
Denotational semantics for lazy evaluation matured long after the idea
had been implemented, and informal evidence for its utility had been
presented. \cite{Friedman-Wise,Henderson-Morris}\auind{Friedman,
D.}\auind{Wise, D.} \auind{Henderson, P.}\auind{Morris, J. H.}
Logical semantics for equational programming, on the other hand, {\em
requires\/} lazy evaluation for completeness, and the demand for
lazy evaluation from this point of view precedes its invention as a
programming tool---at latest it goes back to
\cite{O'Donnell-Springer}\auind{O'Donnell, M. J.} and the essential
roots are already there in work on combinatory logic and the lambda
calculus \cite{Curry-Feys}\auind{Curry, H. B.}\auind{Feys, R.}. Once
lazy evaluation was explained denotationally, that explanation became
a very useful tool for analysis and for deriving implementations. In
general logical semantics predicts and prescribes useful techniques,
while denotational semantics explains and analyzes them.
\subind{semantics!logical vs.\ denotational|)} \subind{denotational
  semantics|)}\subind{semantics!denotational|)}

\subsection[Logical vs.\ Algebraic]
{Logical Semantics vs.\ Initial/Final-Algebra and Herbrand Semantics} 

\subind{semantics!logical vs.\ algebraic|(}
\subind{algebraic semantics|(}\subind{semantics!algebraic|(}
Semantics that use initial or final algebras or Herbrand
models \cite{Guttag-Horning,ADJ,Meseguer-Goguen}
\auind{Guttag, J. V.}\auind{Horning, J. J.}\auind{Meseguer, J.}
\auind{Goguen, J. A.}\auind{Thatcher, J.}\auind{Wagner, E.}
\subind{Herbrand model}\subind{semantics!Herbrand} to represent the meanings of
programs provide systematic techniques for deriving denotational-like
semantics from logical semantics. Logical semantics determines a large
class of models consistent with a given program. Algebraic semantic
techniques construct a single model, depending on the language in
which output is expressed as well as the given program, whose output
theory is the same as that of the class of models given by logical
semantics. This single model can be used for the same sorts of
analysis as denotational semantics (although it is not always based on
a lattice or chain-complete partial ordering). Such single-model
semantics must be reconsidered whenever the output language expands,
since in the larger language the theory of the single model may {\em
not\/} be the same as the theory of the class of models consistent
with the program.

For example, consider a language (based on ideas from
Lucid \cite{Ashcroft-Wadge-nonprocedural}\auind{Ashcroft, E.}
\auind{Wadge, W.}) with symbols $\cons$, $\first$, $\more$, $a$, $b$,
satisfying the equations
$$\begin{array}{rcl}
\first(\cons(x,y)) & \formeq & \first(x) \\
\first(a) & \formeq & a \\
\first(b) & \formeq & b \\
\more(\cons(x,y)) & \formeq & y \\
\more(a) & \formeq & a \\
\more(b) & \formeq & b
\end{array}$$

Assume that only the symbols $a$ and $b$ are allowed as output---that
is, we are only interested in deriving equations of the forms
\mbox{$s\formeq a$} and \mbox{$t\formeq b$}, where $s$
and $t$ are arbitrary input terms. Algebraic semantic techniques
typically interpret this system over a universe of infinite flat
(i.e., not nested) lists with elements from the set \mbox{$\{a,b\}$},
where after some finite prefix, all elements of the list are the same.
\mbox{$\cons(s,t)$} is interpreted as the list beginning with
the first element of $s$, followed by all the elements of
$t$. In this algebraic interpretation,
\mbox{$\cons(\cons(a,b),b)\formeq\cons(a,b)$} and
\mbox{$\cons(b,\cons(a,a))\formeq\cons(b,a)$} hold, although neither
is a semantic consequence of the given equations. If, however, we add
the conventional symbols $\car$ and $\cdr$, and define them by the
equations
$$\begin{array}{rcl}
\car(\cons(x,y)) & \formeq & x \\
\cdr(\cons(x,y)) & \formeq & y
\end{array}$$
then we must expand the universe of the algebraic interpretation to
the universe of binary trees with leaves marked $a$ and $b$. There is
no way to define the functions $\car$ and $\cdr$ in the flat list
model so that they satisfy the new equations. If we take the full
equational theory of the flat list model, and add the defining
equations for $\car$ and $\cdr$, then the resulting theory
trivializes. Every two terms $s$ and $t$ are equal by the
derivation
\begin{eqnarray*}
s & \formeq & \cdr(\car(\cons(\cons(a,s),b))) \\
 & \formeq & \cdr(\car(\cons(a,b))) \\
 & \formeq & \cdr(\car(\cons(\cons(a,t),b))) \\
 & \formeq & t
\end{eqnarray*}
Of course, nobody would apply algebraic semantics in this way---taking
the model for a smaller language and trying to interpret new function
symbols in the same universe. But, what the example shows is that an
algebraic model of a given system of equations may not preserve all
of the relevant information about the behavior of those equations in
extended languages. The set of models associated with a system of
equations by logical semantics is much more robust, and carries enough
information to perform extensions such as the example above.

In general, algebraic semantic techniques, based on initial models,
final models, and Herbrand universes, provide useful tools for
determining, in a given program, the minimum amount of information
that a data structure must carry in order to support the computational
needs of that program. They do {\em not,} and are not intended to,
represent the inherent information given by the formulae in the
program, independently of a particular definition of the computational
inputs and outputs that the program may operate on.
\subind{semantics!logical vs.\ algebraic|)}
\subind{algebraic semantics|)}\subind{semantics!algebraic|)}
\subind{semantics!uses|)}