Database Reference
In-Depth Information
7
Operational Semantics for Database Mappings
7.1
Introduction to Semantics of Process-Programming
Languages
In computer science, the process calculi (or process algebras) are a diverse fam-
ily of related approaches to formally modeling concurrent systems. Process calculi
provide a tool for the high-level description of interactions, communications, and
synchronization between a collection of independent processes. They also provide
algebraic laws that allow process descriptions to be manipulated and analyzed, and
permit formal reasoning about equivalences between processes (e.g., using bisimu-
lation). Leading examples of process calculi include Milner's Calculus of Commu-
nicating Systems (CCS) [
34
] and Hoare's theory of Communicating Sequential Pro-
cesses (CCP) [
18
]. Both of them share the premise that the meaning of a process is
fully determined by a synchronization tree, namely, a rooted, unordered tree whose
edges are labeled with symbols denoting basic actions (or events). These trees are
typically specified by a Structural Operational Semantics (SOS) [
35
] and so are, in
fact, recursively enumerated trees. Two CCS process are distinguished according to
an interactive game-like protocol called bisimulation, so that indistinguishable CCS
processes are said to be bisimilar. Both CCS and CSP have the so-called silent ac-
tions, which in our case do not exist (basic actions are a set of relations obtained by
computation of queries over non-empty models of database schemas), so that in the
absence of silent action, and in the finitely branching processes (in database map-
ping systems, the number of inter-schema mappings from a given database schema
toward another database schemas is always finite) we obtain the so-called Structural
Operational Semantics with Guarded recursion (GSOS) in [
7
]. In GSOS, we have
that bisimulation corresponds to the congruence w.r.t. all operations of CCS (here
we will use only the parallel binary composition '
' and action prefixing unary op-
erations '
a.
_' described in what follows), and Milner has argued extensively that in
this case bisimulation yields the finest appropriate notion of the behavior of concur-
rent processes based on synchronization trees.
