\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 $<s>$ of length 1. The state s represents the formulas stored in 
the database, and the path $<s>$ 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 $<U, I_F , I_{path} >$ 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 = <U, I_F, I_{path}>$ 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, <D_0,\ D_1,\ \ldots ,\  D_n> \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.
