\chapter{Transaction Logic Programming}
Transaction Logic was designed as a general logic capable of solving
a wide range of update-related problems. It supports a wide variety
of functionality in several areas. The functionality includes database
queries and views, unification and rule-base inference, updating of
information, serial execution, and non-deterministism. This chapter
outlines the general semantics of Transaction Logic. A complete
development can be found in [$BK95$].
\section{Overview of Transaction Logic Programming}
From the user's point of view, using \TR is very similar to using
Prolog or using a relational database system. Users can specify rules,
ask queries, or perform updates. Each of these transactions can be viewed
as a query with possible side effects on the database. Unfortunately,
updates in Prolog are not logical. If the execution fails after an update
is performed, the update cannot be undone. So, although executions in
Prolog can be backtracked, the database does not roll back to its
initial state if updates are involved. In other words, database consistency
cannot be guaranteed if transactions fail.
\section{Syntax}
Transaction Logic extends first-order logic with a single binary
operator, $\otimes$ , called {\em serial conjunction}. It is used to
compose transactions and formulate queries. Informally, the formula,
$a \otimes b$, means ``First execute transaction a, and then execute transaction
b.'' It has a dual operator called {\em serial disjunction}, $\oplus$ , defined
by the equivalence $a \oplus\ b = \neg (\neg b \otimes\ \neg a)$.
Formally, transaction formulas are defined recursively as follows:
\begin{enumerate}
\item An atomic transaction formula is an expression of the form
$p(t_{1}, \ldots ,t_{n})$, where $p$ is a predicate symbol, and
$t_{1}, \ldots ,t_{n}$ are function terms as in first-order logic.
\item If $\phi$ and $\psi$ are transaction formulas, then so are the
following expressions:
\begin{itemize}
\item $\phi \vee \psi , \ \phi \wedge \psi , \ \phi \otimes \psi ,
\ \phi \oplus \psi , and \ \neg \phi $.
\item ($\forall$ X)$\phi$ and \ ($\exists$ X)$\phi$ ,
where X is a variable.
\end{itemize}
\end{enumerate}
\section{Elementary Operations}
Transaction Logic comes with a parameter: a pair of
oracles, called the {\em data oracle} and the {\em transition oracle}, which
specify elementary database operations. The data oracle specifies
a set of primitive database queries, and the transaction oracle
specifies a set of primitive database updates. These oracles are not
fixed because any pair of oracles can be ``plugged into'' a \TR theory.
The data oracle specifies the semantics of states. It is a
mapping, $O^{d}$, from state identifiers to sets of first-order formulas.
On the other hand, the state transition oracle, $O^{t}$,
defines elementary state transitions. It is a function that maps pairs
of database states into sets of ground atomic formulas, or elementary
transitions. For a relational database, a state {\bf D} is a set of ground
atomic formulas, and $O^{d}({\bf D}) = {\bf D}$. The insertion and deletion
of atoms with predicate symbol $p$ is represented by the predicates $p.ins$
and $p.del$, respectively. Formally, a transition oracle for these updates
is defined as follows: $p.ins(x) \in O^{t}({\bf D_1},{\bf D_2})$
iff ${\bf D_2} = {\bf D_1} \cup {p(x)}$
and $p.del(x) \in O^{t}({\bf D_1},{\bf D_2})$ iff ${\bf D_2} = {\bf D_1}
- {p(x)}$. More examples of oracles can be found in [$BK95$].
\section{Serial-Horn Transaction Logic Program}
Transaction Logic has a Horn-like fragment that allows users to program
transactions by rule definitions. A serial-Horn \TR program consists of
2 parts: transaction base, and database.
\begin{itemize}
\item The transaction base is a finite set of serial Horn rules
specifying user-defined transactions.
\item The database is a set of first-order logic formulas. It is
updatable by the transaction base.
\end{itemize}
A serial Horn rule is a transaction formula of the form $p \leftarrow
\phi$ , where $p$ is an atomic formula and $\phi$ is a serial goal
(a transaction formula of the form $b_1 \otimes\ b_2 \otimes\ \cdots\
\otimes\ b_n$, where each $b_i$ is an atomic formula, and
$n \geq 0$). As in classical logic, it is equivalent to $p \vee \neg \phi$,
and it means ``to execute $p$, it is sufficient to execute $\phi$''.
This interpretation provides a subroutine facility for \TR, and allows
us to write transaction programs. Like Horn-clause logic, in the rule
$p(X_1,X_2, \ldots ,X_n) \leftarrow \phi$, the symbol $p$ acts as the
transaction name, and the arguments $X_1, \ldots , X_n$ act as the input
parameters, and $\phi$ is the transaction definition.
\section{Model Theory}
The formal semantics of \TR is based on states and transaction execution
paths. The set of states is a set of first-order classical formulas which
comes from the data and transition oracle. A transaction
execution path is a finite sequence of states. When a transaction
is executed, the database may change, from an initial state, through
some number of intermediate states, to a final state. A path is any of
such finite sequence of states. In \TR, truth of an execution is defined
on paths, not states. For example, $ins:a\; \otimes\; ins:b$ is not equivalent
to $ins:b\; \otimes\; ins:a$ because their execution paths,
$< D,\ D+\{ a \},\ D+\{ a,b\} >$ and $< D,\ D+\{ b\},\ D+\{ a,b\} >$ are
not the same.
\newtheorem{axiom}{Definition}[section]
In general, if the path has length 1, then the transaction is a query; if
the path has length 2, then the transaction is an elementary update;
and if the path has length greater than 2, then the transaction is a
composite update. The path structure distinguishes a state s from the
path $~~$ of length 1. The state s represents the formulas stored in
the database, and the path $~~~~$ represents formulas derived by combining
the database and the transaction base. The path structure is defined here:
\begin{axiom}
(Path Structure)
{\em Let $L$ be a language of \TR with set of function symbols $F$. A path
structure, $M$, over $L$ is a triple $~~__$ where $U$ is the
domain of $M$, $I_F$ is an interpretation of function symbols in $L$, and
$I_{path}$ is a mapping that assigns a first-order semantic structure to a
path.}
\end{axiom}
The truth or falsity of a transaction formula is evaluated from on paths
of a structure, as follows:
\begin{axiom}
(Satisfaction)
{\em Let $M = ____$ be a path structure, let $\pi$ be an
arbitrary path, and let v be a variable assignment (i.e., a mapping
$V \mapsto\ U$, which takes a variable as input, and returns a domain element
as output). Then:
\begin{enumerate}
\item $M, \pi \models_v p(t_1, \ldots , t_n)\; $ if and only if
$\; I_{path}\models^c_v p(t_1, \ldots , t_n)$, for any atomic formula
$p(t_1, \ldots , t_n)$, where ``$\models^c_v$'' denotes classical
satisfication in first-order predicate calculus.
\item $M, \pi\ \models_v \neg \phi\; $ if and only if it is not the case
that $\; M, \pi \models_v \phi$.
\item $M, \pi\ \models_v \phi \wedge \psi\; $ if and only if
$\; M, \pi\ \models_v \phi$ and $M, \pi\ \models_v \psi$.
\item $M, \pi\ \models_v \phi \vee \psi\; $ if and only if
$\ M, \pi\ \models_v \phi\; $ or $\; M, \pi\ \models_v \psi$.
\item $M, \pi\ \models_v \phi \otimes \psi\; $ if and only if
$\; M, \pi_1\ \models_v \phi\; $ and $\; M, \pi_2\ \models_v \psi\; $
for some split\footnote{
$\pi_1 \circ \pi_2$ is a split of path $\pi$ if and only if
$\pi =\; <{\bf D_1, \ldots ,D_n}>$,
$\pi_1 =\; <{\bf D_1, \ldots ,D_i}>$ and
\mbox{$\pi_2 =\; <{\bf D_i, \ldots , D_n}>$} for some $i\ (1 \leq i \leq n)$.}
\ $\pi_1 \circ \pi_2$ of path $\pi$.
\item $M, \pi\ \models_v (\forall X) \phi\; $ if and only if
$\; M, \pi\ \models_{\mu} \pi\; $ for every variable assignment $\mu$
that agrees with v everywhere except X.
\item $M, \pi\ \models_v (\exists X) \phi\; $ if and only if
$\; M, \pi\ \models_{\mu} \pi\; $ for some variable assignment $\mu$
that agrees with v everywhere except X.
\end{enumerate}
}
\end{axiom}
A model, M, of a \TRR -formula $\phi$ is a path structure such that
$\; M \models\ \phi\; $ if and only if $\; M, \pi\ \models\ \phi\; $\ for every
path $\pi$. A path structure is a model of a set of
formulas if and only if it is a model of every formulas in the set.
Further details of the model theory can be found in [$BK95$].
\section{Execution Entailment}
Let P be a transaction base. Let $\phi$ be a transaction formula, and
let $D_0,\ D_1,\ \ldots ,\ D_n$ be a sequence of databases states. Then,
the following statement
\[ P,\ D_0,\ D_1,\ \ldots ,\ D_n \models\ \phi \]
is true if and only if $\; M, \models\ \phi\ $
for every model $M$ of $P$.
\\
\\
For any transaction base $P$, any sequence of database states $D_0,\ \ldots,\
D_n$, and any transaction formulas $\alpha$\ and $\beta$, the following
are properties of execution entailment:
\begin{enumerate}
\item If $P,\ D_0,\ \ldots ,\ D_n \models\ \alpha\ $ and
$P,\ D_0,\ \ldots ,\ D_n \models\ \beta$\ then
$P,\ D_0,\ \ldots ,\ D_n \models\ \alpha\ \vee\ \beta$.
\item If $P,\ D_0,\ \ldots ,\ D_i \models\ \alpha\ $ and
$P,\ D_i,\ \ldots ,\ D_j \models\ \beta$\ then
$P,\ D_0,\ \ldots ,\ D_j \models\ \alpha\ \otimes\ \beta$ .
\item If $\alpha \leftarrow\ \beta$\ is in P,
$D_0,\ \ldots ,\ D_n \models \beta\ $ then
$D_0,\ \ldots ,\ D_n \models \alpha\ $ .
\item If $O^t(D_0,\ D_1) \models^c \alpha\ $ then $P,\ D_0,\ D_1 \models\
\alpha$ .
\item If $O^d(D_0) \models^c \alpha\ $ then $P,\ D_0 \models\ \alpha$ .
\end{enumerate}
In 4 and 5, $\alpha$\ is a first-order formula and ``$\models^c$''denodes
classical entailment.
__