\documentstyle{llncs}

\newstytheorem{algorithm}{\bf}{\rm}[theorem]{Algorithm}
\renewcommand{\labelenumi}{(\roman{enumi})}
\newcommand{\crossbox}{ \Box \! \! \! \! \! \! \times}
\newcommand{\disunion}{\stackrel{\cdot}{\cup}}

\title{Identification, Genericity and Consistency in Object-Oriented Databases\thanks{This work has been supported in part by research grants
from the E.E.C. Basic Research Action 3070 FIDE: ``Formally Integrated Data
Environments''.}}

\author{Klaus--Dieter Schewe, Joachim W. Schmidt, Ingrid Wetzel}

\institute{University of Hamburg, Dept. of Computer Science,\\Vogt-K\"olln-Str. 30, D-W-2000 Hamburg 54}

\begin{document}

\maketitle

\begin{abstract}

\noindent
It is claimed that object-oriented databases overcome many of the limitations of the relational data model especially by generalizing the notion of object identification. A clear distinction between objects and values turns out to be essential for the object-oriented approach whereas the relational model is based exclusively on values. Since, however, value uniqueness within scopes is a quite natural constraint for a wide class of applications, identification by value is also of interest for object-oriented datamodels.

Hence, in this paper we concentrate on those classes where the extents are completely representable by values. We formalize some basic concepts of object-oriented databases and show that the finiteness of a database and the existence of finitely representable recursive types are sufficient to decide {\em value-representability}. 

Another advantage of the relational approach is the existence of structurally determined {\em canonical update operations}. We show that this property can be carried over to object-oriented datamodels iff classes are value-representable. Moreover, in this case {\em database consistency} with respect to implicitly specified referential and inclusion constraints will be automatically preserved.

\end{abstract}

\section{Introduction}

The success of the relational data model is due certainly to the existence of
simple query and update-languages whereas its
modelling power is often criticized for its limitations
\cite{abiteboul,oo-manifesto,beeri,bk}. Novel data modelling constructs are
required by advanced database applications and it is claimed that
object-oriented databases will satisfy a much wider range of demands
\cite{albano,oo-manifesto,o2,exodus,vision,iris,orion,gemstone}.
However, in contrast to the relational model where a commonly accepted theory existed very early on, there is not yet a generally accepted object-oriented
data model.

Object-oriented databases are based on a clear
distinction between {\em values} and {\em objects} \cite{beeri2}. A value is
identified by itself whereas an object has an identity independent of its
value. This object identity is usually
encoded by object identifiers \cite{abiteboul,oidquery,oid86}. The identifier
of an object is immutable during the object's lifetime; the object's value is
in general assumed to be mutable. Identifiers can be used to model
relationships naturally by references between objects. This facilitates sharing and cyclicity.

In contrast to the relational model where identification is modelled by
keys, object identifiers are system-provided and hence do not have a meaning
for the user. Consequently, they have to be hidden from the user. 

Values can be classified into types and objects can be grouped into classes.
Roughly speaking, a type defines a fixed set of values and a class defines a finite collection of
objects with the same structure. The content of a class varies over time. The
dynamics of an object-oriented database is defined by methods associated
with objects (classes).

Our intent here is not to describe a concrete object-oriented database
language. Instead we study whether equality of identifiers can be derived from the
equality of values. In the literature the notion of ``deep'' equality has
been introduced for objects with equal values and references to
objects that are also ``deeply'' equal. This recursive definition becomes
interesting in the case of cyclic references.

Therefore, we introduce {\em functional constraints} on classes, in particular
{\em uniqueness constraints}, which express equality on identifiers as a consequence
of the equality of some values or references. On this basis we can
address the following problems:

\begin{itemize}

\item How to characterize those classes that are completely representable
(and hence also identifiable) by values?

\item How to characterize those classes for which canonical update operations
can be derived? 

\item How to define canonical update operations that enforce integrity with
respect to inclusion and to functional and referential constraints as
mentioned above?

\end{itemize}

Our approach to the first and the second of these problems have been reported in \cite{rostock} in a more informal way. In this paper we show that the finiteness of a database and the existence of finitely representable recursive types are sufficient to decide value-representability. 
Moreover, in the case of value-representability, we can derive canonical update operations that enforce consistency with respect to all implicit referential and inclusion constraints.

The remainder of the paper is organized as follows. In Section \ref{fundamentals} we first introduce concepts of OODBs informally. For their formalization we introduce in Section \ref{types} an algebraic framework for type specifications similar
to \cite{bk}. The possibility of defining parameterized types enables us to formally define classes with implicit referential and inclusion
constraints plus additional user-defined functional constraints. This will be done in Section \ref{structure}.

In Section \ref{value-rep} we define formally the notions of
value-representability and value-definability of a class and analyse the referential structure of a given schema. We
derive sufficient conditions for value-representability.

Section \ref{generic} discusses the problem of canonical update operations. It
consists of the results on the definability of such operations and their
relation to consistency. We conclude with a short summary and outlook.

\section{The Structure of Object-Oriented Databases} \label{fundamentals}

In our approach to OODBs each object $o$ consists of a unique identifier $id$, a set
of (type-, value-)pairs $( T_i , v_i )$, a set of (reference-, object-)pairs $(
ref_j , o_j )$ and a set of methods $meth_k$. We assume all identifiers $id$ to belong to unique given set $ID$. Types represent immutable sets of values. They can be defined algebraically similar to
\cite{bk}. Type constructors can be defined analogously by parameterized types. These can be used to build complex types by nesting and recursive types. We assume that the set $ID$ of possible object identifiers is also a type. Then an instantiation of a parameterized type defines a structure
that represents a combination of values and references, where references are expressed by the occurrence of a value of type $ID$.

Objects can be grouped into
classes with some structure built from values and references. Furthermore, we may associate
methods and constraints with each class. This means of structure building involves implicit {\em referential
constraints}. Inheritance on classes is given by IsA-relations, i.e. by set inclusion on object identifiers. Moreover we introduce subtyping and formalize this by the definition of a continuous function from a subtype to a supertype. The relation between subtyping and inheritance is given by an {\em inclusion constraint} on classes.

\begin{example} \label{bsp-informal}

Let us look at a university application, where the objects are persons or departments. Let ($\cdot$), \{$\cdot$\} and [$\cdot$] denote type constructors for (tagged) tuples, finite sets and lists respectively. Let PERSON, DEPARTMENT, PROFESSOR and STUDENT be types such that STUDENT and PROFESSOR are subtypes of PERSON. The type specifications will be given elsewhere. Then we need the following four class definitions (omitting additional constraints):\\

\noindent
PersonC = {\tt structure} PERSON {\tt end}

\noindent
ProfessorC = {\tt IsA} PersonC \\
\indent {\tt structure} ( prof : PROFESSOR , fac : DepartmentC ) {\tt end}

\noindent
DepartmentC = {\tt structure} ( fac : DEPARTMENT , head : ProfessorC ) {\tt end}

\noindent
StudentC = {\tt IsA} PersonC \\
\indent {\tt structure} ( stud : STUDENT , major : DepartmentC , minor : DepartmentC , \\
\hspace*{25pt} supervisors : \{ ( fac : DepartmentC , prof : [ sup : ProfessorC ] ) \} ) {\tt end}\\

\noindent
Note that we used names for the references. In this example an object $o$ in the class ProfessorC is given by $(i,(v,j))$, where $i :: ID$ is the oid of $o$, $v$ is a value of type PROFESSOR and $j :: ID$ is the oid of an object $o^\prime$ in the class DepartmentC. Moreover, $o$ also belongs to the class PersonC and is represented there by $(i,w)$, where the subtype function $f : \mbox{PROFESSOR} \rightarrow \mbox{PERSON}$ satisfies $f(v) = w$. \qed

\end{example}

\section{Type Specifications} \label{types}

Our approach to types is an algebraic one similar to \cite{bk}. In general a type is specified by a collection of constructors, selectors and other functions -- the signature of the type -- and axioms defined by universal Horn formulae. Now let $N_P$, $N_T$, $N_C$, $N_R$, $N_F$, $N_M$ and $V$ denote
arbitrary pairwise disjoint, countably infinite sets representing a reservoir of
parameter-, type-, class-, reference-, function-, method- and variable-names
respectively.

\begin{definition} \label{def-signature}

\ A {\em type signature} $\Sigma$ consists of a type name $t \in N_T$, a finite set of supertype-/function-pairs $T \subseteq N_T \times N_F$, a
finite set of parameters $P \subseteq N_P$, a finite set of base types $B
\subseteq N_T$ and pairwise disjoint finite sets $C, \, S, \, F \subseteq
N_F$ of constructors, selectors and functions such that there exist
predefined arities $ar(c) \in (P \cup B^* \cup \{ t \} )^* \times \{ t \}$,
$ar(s) \in \{ t \} \times (P \cup B^* \cup \{ t \} )$ and
$ar(f) \in (P \cup B^* \cup \{ t \} )^* \times (P \cup B^* \cup \{ t \} )$ for
each $c \in C$, $s \in S$ and $f \in F$.

\end{definition}

\noindent
We write $f : t \rightarrow t^\prime$ to denote a {\em supertype-/function-pair} $(t^\prime,f) \in T$.
We write $c : t_1 \times \ldots \times t_n \rightarrow t$ to denote a {\em
constructor} of arity $(t_1 \ldots t_n , t )$, $s : t \rightarrow t^\prime$
to denote a {\em selector} of arity $( t , t^\prime )$ and
$f : t_1 \times \ldots \times t_n \rightarrow t^\prime$ to denote a {\em
function} of arity $(t_1 \ldots t_n , t^\prime )$. If $t_i = b_i^0 \ldots b_i^m \in B^*$, we write $b_i^0 ( b_i^1 \ldots b_i^m )$. We call ${\cal S} = P
\cup B \cup \{ t \} $ the set of {\em sorts} of the signature $\Sigma$. 

\begin{definition} \label{type}

\ A {\em type declaration} consists of a type signature $\Sigma$ with type
name $t$ such that there exists a type declaration for each $b \in B - \{ t \}$ and
a set $Ax$ of Horn formulae over $\Sigma$. Moreover, if $b_i^0 ( b_i^1 \ldots b_i^m )$ with $b_i^j \in B$ occurs within a constructor, selector or function, then $b_i^0$ must have been declared as a parameterized type with $m$ parameters. We say that $( \Sigma , Ax )$
defines the {\em parameterized type} $t ( \alpha_1 , \ldots , \alpha_n )$,
iff $P = \{ \alpha_1 , \ldots , \alpha_n \} \neq \emptyset$ or the {\em proper
type} $t$ respectively.\\
A {\em type} $t$ is defined either by a type declaration or by mutually recursive equations involving $t$ as a variable.

\end{definition}

\noindent
The semantics of a type is given by term generated algebras that are quotients of the term algebra defined by the constructors. Functions are considered to define additional structure
via operations and functions on these algebras. Subtyping is modelled by the use of a continous function taking the subtype to the supertype. Recursive types are fixpoints of functors.

\begin{example} \label{bsp-types}

\ Assume the types NAT, PERSONNAME and ADDRESS to be defined elsewhere. Then a proper type PERSON as used in Example \ref{bsp-informal} can be defined as follows:\\

\noindent
PERSON == \\
\indent {\tt BasedOn} NAT ; PERSONNAME ; ADDRESS ;\\
\indent  {\tt Constructors} \\
\hspace*{25pt} Person : NAT $\times$ PERSONNAME $\times$ ADDRESS $\rightarrow$ PERSON ;\\
\indent {\tt Selectors} \\
\hspace*{25pt} PersonIdentityNo : PERSON $\rightarrow$ NAT ;\\
\hspace*{25pt} Name : PERSON $\rightarrow$ PERSONNAME ;\\
\hspace*{25pt} Address : PERSON $\rightarrow$ ADDRESS ;\\
\indent {\tt Axioms} \\
\hspace*{25pt} {\tt With} P :: PERSON : \\
\hspace*{50pt} Person(PersonIdentityNo(P),Name(P),Address(P)) = P ;\\
\hspace*{25pt} {\tt With} N :: NAT , PN :: PERSONNAME , A :: ADDRESS :\\
\hspace*{50pt} PersonIdentityNo(Person(N,PN,A)) = N;\\
\hspace*{25pt} {\tt With} N :: NAT , PN :: PERSONNAME , A :: ADDRESS :\\
\hspace*{50pt} Name(Person(N,PN,A)) = PN;\\
\hspace*{25pt} {\tt With} N :: NAT , PN :: PERSONNAME , A :: ADDRESS :\\
\hspace*{50pt} Address(Person(N,PN,A)) = A;\\
{\tt End} PERSON \qed

\end{example}

In \cite{iwsds} we presented the parameterized type $FSETS(\alpha)$ denoting finite sets with elements of type $\alpha$. On this basis, it is easy to define $PFUN(\alpha,\beta)$, the type of partial functions (with finite domain) from $\alpha$ to $\beta$.

So far we use only single-sorted algebras, but the extension to many-sorted and order-sorted algebras is straightforward. Moreover, each value of a given type can be expressed by a closed constructor term. In the case of recursive types this term is a {\em rational tree}.

\section{The Concept of a Class in Object-Oriented Databases} \label{structure}

Our approach to OODBs distinguishes between values grouped into types and objects grouped into classes. The extent of classes varies over time, whereas types are immutable. Relationships between classes are represented by references together with referential constraints on the object identifiers involved. Moreover, each class is accompanied by a collection of methods, but methods will be postponed to Section \ref{generic}.

Throughout the rest of the paper we assume a proper identifier type $ID$ to
be defined such that only the trivial type $\bot$ is a supertype of $ID$. A type $T$ without any occurrence of $ID$ will be called a {\em value type}.

Each object in a class consists of an identifier, a collection of values and references to objects in other classes. Identifiers can be represented using the unique identifier type $ID$. Values and references can be combined into a representation type, where each occurence of $ID$ denotes references to some other classes. Therefore, we may define the structure of a class using parameterized types.

\begin{definition} \label{structure-expression}

\begin{enumerate}

\item Let $t$ be a value type with parameters $\alpha_1 , \ldots , \alpha_n$. Let $r_1 , \ldots , r_n \in N_R$ be distinct reference names and $C_1 , \ldots , C_n \in N_C$ be class names. The expression derived from $t$ by replacing each $\alpha_i$ in $t$ by $r_i : C_i$ for $i = 1 , \ldots , n$ is called a {\em structure expression}.

\item A {\em class} consists of a class name $C \in N_C$, a structure expression $S$, a list of superclasses $D_1 , \ldots , D_m$ and a list of constraints ${\cal I}_1 , \ldots , {\cal I}_k $. We call $r_i$ the {\em reference} named $r_i$ from class $C$ to class $C_i$. The type derived from $S$ by replacing each reference $r_i : C_i$ by the type $ID$ is called the {\em representation type} $T_C$ of the class $C$.

\end{enumerate}

\end{definition}

\noindent
In general a class may be considered as a variable $C$ of type $PFUN(ID,T_C)$. However, the introduction of classes is associated inevitably with the introduction of constraints. In object-oriented databases we want to be able to model inheritance between classes, which leads to some kind of {\em inclusion constraint}. Modelling relationships between classes via references leads to the introduction of {\em referential constraints}. Moreover, generalizing the well known key constraints from the relational theory will give us {\em uniqueness constraints} on classes. 

\begin{definition} \label{constraint}

\ Let $C$, $C^\prime$ be classes of representation types $T_C$ and $T_{C^\prime}$ respectively. Let $i,j$ be of type $ID$ and $v,w$ be of type $T_C$.

\begin{enumerate}

\item A {\em referential constraint} on $C$ and $C^\prime$ has the form

\[ Pair(i,v) \in C \, \wedge \, o(v,j) = true \; \Rightarrow \; j \in dom(C^\prime) \, , \]

\noindent
where $o : T_C \times ID \rightarrow BOOL$ is a function.

\item An {\em inclusion constraint} on $C$ and $C^\prime$ has the form

\[ Pair(i,v) \in C \; \Rightarrow \; Pair(i,f(v)) \in C^\prime \, , \]

\noindent
where $f : T_C \rightarrow T_{C^\prime}$ is a subtype function provided such an $f$ exists. Otherwise it is simply

\[ i \in dom(C) \Rightarrow i \in dom(C^\prime) \]

\item A {\em uniqueness constraint} on $C$ has the form

\[ Pair(i,v) \in C \wedge  Pair(j,w) \in C \wedge f(v) = f(w) \; \Rightarrow \; i = j \; , \]

\noindent
where $f : T_C \rightarrow T$ is a subtype function.

\end{enumerate}

\end{definition}

\noindent
Each reference in the structure expression $S$ of a class $C$ gives rise to an implicit referential constraint. Each superclass $D$ of a class $C$ defines an implicit inclusion constraint. Moreover, arbitrary constraints may be added as explicit constraints, but for the purpose of this paper we concentrate on uniqueness constraints.

\begin{example} \label{bsp-class}

\ Let $f : PAIR(PERSON,ID) \rightarrow PAIR(NAT,ID)$ be a subtype function defined by the axiom\\
\indent {\tt With} P :: PERSON , I :: ID : f(Pair(P,I)) = Pair(PersonIdentityNo(P),I) .\\
\noindent
Then a class named {\sc MarriedPersonC} may be defined as follows:\\

\noindent
{\sc MarriedPersonC} == {\tt IsA} {\sc PersonC}\\
\indent {\tt Structure} \ PAIR( PERSON , spouse : {\sc MarriedPersonC})\\
\indent {\tt Constraints} \ {\tt With} I,J :: ID , V,W :: PAIR(PERSON,ID) :\\
\hspace*{25pt} Pair(I,V) $\in$ {\sc MarriedPersonC} $\wedge$ Pair(J,W) $\in$ {\sc MarriedPersonC} $\wedge$\\
\hspace*{35pt} f(V) = f(W) $\; \Rightarrow \; $  I = J\\
{\tt End} \ {\sc MarriedPersonC} \qed

\end{example}

\begin{definition} \label{schema}

\begin{enumerate}

\item A {\em schema} $\cal S$ is a finite collection of classes $C_1 , \ldots , C_n$ closed under references and superclasses.

\item An {\em instance} $\cal D$ of a schema $\cal S$ assigns to each class $C$ a value ${\cal D} (C)$ of type $PFUN(ID,T_C)$ such that all implicit and explicit constraints on $\cal S$ are satisfied.

\end{enumerate}

\end{definition}

\section{Object Identification and Value-Representation} \label{value-rep}

According to our definitions two objects in a class $C$ are identical iff they have the same identifier. By the use of constraints, especially uniqueness constraints, we could restrict this notion of equality.

The goal of this section is the characterization of those classes, the objects in which are completely representable by values, i.e. we could drop the object identifiers and replace references by values of the referred object. We shall see in Section \ref{generic} that in case of value-representable classes we are able to preserve an important advantage of relational databases, i.e. the existence of structurally determined update operations.

\begin{definition} \label{value-repr}

\ Let $C$ be a class in a schema $\cal S$ with representation type $T_C$.

\begin{enumerate}

\item $C$ is called {\em value-identifiable} iff there exists a proper value type $I_C$ such that for all instances $\cal D$ of $\cal S$ there is a function $c: T_C \rightarrow I_C$ such that the uniqueness constraint on $C$ defined by $c$ holds for $\cal D$.

\item $C$ is called {\em value-representable} iff there exists a proper value type $V_C$ such that for all instances $\cal D$ of $\cal S$ there is a function $c: T_C \rightarrow V_C$ such that for $\cal D$

\begin{enumerate}

\item the uniqueness constraint on $C$ defined by $c$ holds and

\item for each uniqueness constraint on $C$ defined by some function $c^\prime: T_C \rightarrow V_C^\prime$ with proper value type $V_C^\prime$ there exists a function $c^\prime{}^\prime: V_C \rightarrow V_C^\prime$ that is unique on $c(codom_{\cal D}(C))$ with $c^\prime = c^\prime{}^\prime \circ c$.

\end{enumerate}

\end{enumerate}

\end{definition}

\noindent
It is easy to see that each value-representable class $C$ is also value-identifiable. Moreover, the {\em value-representation type} $V_C$ in definition \ref{value-repr} is unique up to isomorphism.

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$. Then $C$ is value-representable iff $C$ is value-identifiable and $C_i$ is value-representable for all references $r_i : C_i$ in the structure expression $S$.

\end{theorem}

\begin{proof}

This follows directly from the definitions. \qed

\end{proof}

\subsection{Value-Representability in the Case of Acyclic Reference Graphs} \label{vrep-simple}

Since value-representability is defined by the existence of a certain proper value type, it is hard to decide, whether an arbitrary class is value-representable or not. In case of simple classes the problem is easier, since we only have to deal with uniqueness and value constraints. In this case it is helpful to analyse the reference structure of the class. Hence the following graph-theoretic definitions.

\begin{definition}  \label{ref-graph}

The {\em reference graph} of a class $C$ in a schema $\cal S$ is the smallest labelled graph $G_{rep} = (V,E,l)$ satisfying:

\begin{enumerate}

\item There exists a vertex $v_C \in V$ with $l(v_C) = \{ t , C \}$, where $t$ is the top-level type in the structure expression $S$ of $C$.

\item For each proper occurrence of a type $t \neq ID$ in $T_C$ there exists a unique vertex $v_t \in V$ with $l(v_t) = \{ t \}$.

\item For each reference $r_i : C_i$ in the structure expression $S$ of $C$ the reference graph $G_{ref}^i$ is a subgraph of $G_{ref}$.

\item For each vertex $v_t$ or $v_C$ corresponding to $t ( x_1 , \ldots , x_n )$ in $S$ there exist unique edges $e_t^{(i)}$ from $v_t$ or $v_C$ respectively to $v_{t_i}$ in case $x_i$ is the type $t_i$ or to $v_{C_i}$ in case $x_i$ is the reference $r_i : C_i$. In the first case $l(e_t^{(i)}) = \{ S_i \}$, where $S_i$ is the corresponding selector name; in the latter case the label is $\{ S_i , r_i \}$.

\end{enumerate}

\end{definition}

\begin{definition} \label{id-graph}

\ Let ${\cal S} = \{ C_1 , \ldots , C_n \}$ be a schema. Let ${\cal S}^\prime = \{ C_1^\prime , \ldots , C_n^\prime \}$ be another schema such that for all $i$ either $T_{C_i}^\prime = T_{C_i}$ holds or there exists a uniqueness constraint on $C_i$ defined by some $c_i: T_{C_i} \rightarrow T_{C_i^\prime}$. Then an {\em identification graph} $G_{id}$ of the class $C_i$ is obtained from the reference graph of $C_i^\prime$ by changing each label $C_j^\prime$ to $C_j$.

\end{definition}

\begin{example} \label{bsp-graph}

\ Let {\sc MarriedPersonC} be defined as in Example \ref{bsp-class}. Then the reference graph and the identification graph with respect to the uniqueness constraint of this class are shown in Figure \ref{fig-graph}. \qed

\begin{figure}
\setlength{\unitlength}{1cm}

\begin{picture}(12.8,3.5)
\thicklines

\put(3.0,0.5){\circle{0.5}}
\put(3.0,2.5){\circle{0.5}}
\put(3.0,2.25){\vector(0,-1){1.5}}
\put(4.25,2.5){\oval(1,1)[r]}
\put(4.25,3){\vector(-2,-1){1}}
\put(4.25,2){\line(-2,1){1}}
\put(0,3){\{ PAIR , {\sc MarriedPersonC} \} }
\put(0.5,0.45){\{ PERSON \} }
\put(1.7,1.5){\{ first \} }
\put(3.5,1.7){\{ second , spouse \} }

\put(9.5,0.5){\circle{0.5}}
\put(9.5,2.5){\circle{0.5}}
\put(9.5,2.25){\vector(0,-1){1.5}}
\put(10.75,2.5){\oval(1,1)[r]}
\put(10.75,3){\vector(-2,-1){1}}
\put(10.75,2){\line(-2,1){1}}
\put(5.75,3){\{ PAIR , {\sc MarriedPersonC} \} }
\put(7.75,0.45){\{ NAT \} }
\put(7.85,1.5){\{ first \} }
\put(10.0,1.7){\{ second , spouse \} }

\end{picture}
\caption{\label{fig-graph} The reference graph and identification graph of class {\sc MarriedPersonC}}
\end{figure}

\end{example}

\begin{theorem} \label{graph-char}

\ Let $C$ be a class in a schema $\cal S$ with acyclic reference graph $G_{ref}$ such that there exist uniqueness constraints for $C$ and each $C_i$ such that $C_i$ occurs as a label in $G_{ref}$. Then $C$ is value-representable.

\end{theorem}

\begin{proof}

\ We use induction on the maximum length of a path in $G_{ref}$. If there are no references in the structure expression $S$ of $C$ the type $T_C$ is a proper value type. Since there exists a uniqueness constraint on $C$, the identity function $id$ on $T_C$ also defines a uniqueness constraint. Hence $V_C = T_C$ satisfies the requirements of Definition \ref{value-repr}.

If there are references $r_i : C_i$ in the structure expression $S$ of $C$, then the induction hypothesis holds for each such $C_i$, because $G_{ref}$ is acyclic. Let $V_C$ result from $S$ by replacing each $r_i : C_i$ by $V_{C_i}$. Then $V_C$ satisfies the requirements of Definition \ref{value-repr}. \qed

\end{proof}

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exist an acyclic identification graph $G_{id}$ and uniqueness constraints for $C$ and each $C_i$ occuring as a label in $G_{id}$. Then $C$ is value-identifiable.

\end{theorem}

\begin{proof}

\ The proof is analogous to that of Theorem \ref{graph-char} \qed

\end{proof}

\begin{theorem} \label{simple-char}

\ Let $C$ be a class with acyclic reference graph in a schema $\cal S$. Then the value-representability of $C$ is decidable.

\end{theorem}

\begin{proof}

\ So far the only explicit constraints in our model are uniqueness constraints. According to Definition \ref{constraint} equality of identifiers occurs only as a positive literal in such constraints. Therefore, it is impossible to derive a uniqueness constraint for a class $C$ that has not one a priori. Theorem \ref{graph-char} implies that value-representability can be decided by checking the existence of uniqueness constraints in the class definitions. \qed

\end{proof}

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exist an acyclic identification graph. Then the value-identifiability of $C$ is decidable.

\end{theorem}

\begin{proof}

\ The proof is analogous to that of Theorem \ref{simple-char}. \qed

\end{proof}

\subsection{Computation of Value Representation Types}

We want to address the more general case where cyclic references may occur in the schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. In this case a simple induction argument as in the proof of Theorem \ref{graph-char} is not applicable. So we take another approach. We define algorithms to compute types $V_C$ and $I_C$ that turn out to be proper value types under certain conditions. In the next subsection we then show that these types are the value representation type and the value identification type required by Definition \ref{value-repr}.

\begin{algorithm} \label{alg-vc}

Let $G(C_i) = T_{C_i}$ provided there exists a uniqueness constraint on $C_i$, otherwise let $G(C_i)$ be undefined. If $ID$ occurs in some $G(C_i)$ corresponding to $r_j : C_j$ ($j \neq i$), we write $ID_j$.

Then iterate as long as possible using the following rules: 

\begin{enumerate}

\item If $G(C_j)$ is a proper value type and $ID_j$ occurs in some $G(C_i)$ ($j \neq i$), then replace this corresponding $ID_j$ in $G(C_i)$ by $G(C_j)$.

\item If $ID_i$ occurs in some $G(C_i)$, then let $G(C_i)$ be recursively defined by $G(C_i) == S_i$, where $S_i$ is the result of replacing $ID_i$ in $G(C_i)$ by the type name $G(C_i)$.

\end{enumerate}

\noindent
This iteration terminates, since there exists only a finite collection of classes. If these rules are no longer applicable, replace each remaining occurrence of $ID_j$ in $G(C_i)$ by the type name $G(C_j)$ provided $G(C_j)$ is defined. \qed

\end{algorithm}

\noindent
Note that the the algorithm computes (mutually) recursive types.
Now we give a sufficient condition for the result of Algorithm \ref{alg-vc} to be a proper value type.

\begin{lemma} \label{lemma-vc}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in the reference graph $G_{ref}$ of $C$. Let $V_C$ be the type $G(C)$ computed by Algorithm \ref{alg-vc}. Then $V_C$ is a proper value type.

\end{lemma}

\begin{proof}

\ Suppose $V_C$ were not a proper value type. Then there exists at least one occurrence of $ID$ in $V_C$. This corresponds to a class $C_i$ without uniqueness constraint occurring as a label in $G_{ref}$, hence contradicts the assumption of the lemma. \qed

\end{proof}

\begin{algorithm} \label{alg-ic} 

Let $F(C_i) = T_i$ provided there exists a uniqueness constraint on $C_i$ defined by $c_i: T_{C_i} \rightarrow T_i$, otherwise let $F(C_i)$ be undefined. If $ID$ occurs in some $F(C_i)$ corresponding to $r_j : C_j$ ($j \neq i$), we write $ID_j$.

Then iterate as long as possible using the following rules: 

\begin{enumerate}

\item If $F(C_j)$ is a proper value type and $ID_j$ occurs in some $F(C_i)$ ($j \neq i$), then replace this corresponding $ID_j$ in $F(C_i)$ by $F(C_j)$.

\item If $ID_i$ occurs in some $F(C_i)$, then let $F(C_i)$ be recursively defined by $F(C_i) == S_i$, where $S_i$ is the result of replacing $ID_i$ in $F(C_i)$ by the type name $F(C_i)$.

\end{enumerate}

\noindent
This iteration terminates, since there exists only a finite collection of classes. If these rules are no longer applicable, replace each remaining occurrence of $ID_j$ in $F(C_i)$ by the type name $F(C_j)$ provided $F(C_j)$ is defined. \qed

\end{algorithm}

\begin{lemma} \label{lemma-ic}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in some identification graph $G_{id}$ of $C$. Let $I_C$ be the type $F(C)$ computed by Algorithm \ref{alg-ic} with respect to the uniqueness constraints used in the definition of $G_{id}$. Then $I_C$ is a proper value type.

\end{lemma}

\begin{proof}

The proof is analogous to that of Lemma \ref{lemma-vc}. \qed

\end{proof}

\subsection{The Finiteness Property} \label{finiteness}

Let us now address the general case. The basic idea is that there is always only a finite number of objects in a database. Assuming the database being consistent with respect to inclusion and referential constraints yields that there can not exist infinite cyclic references. This will be expressed by the {\em finiteness property}.
We show that this property implies the decidability of value-representability provided the type system allows recursive types to be defined in such a way that all their values are finitely representable, i.e. representable as rational trees. Note that the type specifications introduced in Section \ref{types} satisfy this property.

\begin{definition} \label{cycle}

\ Let $C$ be a class in a schema $\cal S$ and let $g_{k,l}$ denote a path in $G_{ref}$ from $v_{C_k}$ to $v_{C_l}$ provided there is a reference $r_l : C_l$ in the structure expression of $C_k$. Then a {\em cycle} in $G_{ref}$ is a sequence $g_{0,1} \cdots g_{n-1,n}$ with $C_0 = C_n$ and $C_k \neq C_l$ otherwise.

\end{definition}

\noindent
Note that we use paths instead of edges, because the edges in $G_{ref}$ do not always correspond to references.
According to our definition of a class there exists a referential constraint on $C_k$, $C_l$ defined by $o_{k,l} : T_{C_k} \times ID \rightarrow BOOL$ corresponding to $g_{k,l}$. Therefore, to each cycle there exists a corresponding sequence of functions $o_{0,1} \cdots o_{n-1,n}$. This can be used as follows to define a function $cyc: ID \times ID \rightarrow BOOL$ corresponding to a cycle in $G_{ref}$.

\begin{definition} \label{cycle-rel}

\ Let $C$ be a class in a schema $\cal S$ and let $g_{0,1} \cdots g_{n-1,n}$ be a cycle in $G_{ref}$. The corresponding {\em cycle relation} $cyc: ID \times ID \rightarrow BOOL$ is defined by $cyc(i,j) = true$ iff there exists a sequence $i = i_0 , i_1 , \ldots , i_n = j$ ($n \neq 0$) such that $( i_l , v_l ) \in C_l$ and $o_{l,l+1} ( i_{l+1} , v_l ) = true$ for all $l = 0 , \ldots , n-1$.

\end{definition}

\noindent
Given a cycle relation $cyc$, let $cyc^m$ the $m$-th power of $cyc$.

\begin{lemma} \label{fin-ass}

\ Let $C$ be a class in a schema $\cal S$. Then $C$ satisfies the finiteness property, i.e. for each instance $\cal D$ of $\cal S$ and for each cycle in $G_{ref}$ the corresponding cycle relation $cyc$ satisfies

\[ \forall i \in dom(C) . \, \exists n . \, \forall j \in dom(C) . \, \exists m < n . \; ( \, cyc^n(i,j) = true \, \Rightarrow \, cyc^m(i,j) = true \, ) \; . \]

\end{lemma}

\begin{proof}

Suppose the finiteness property were not satisfied. Then there exist an instance $\cal D$, a cycle relation $cyc$ and an object identifier $i_0$ such that

\[ \forall n . \, \exists j \in dom(C) . \, \forall m < n . \; ( \, cyc^n(i_0,j) = true \, \wedge \, cyc^m(i_0,j) = false \, ) \]

\noindent
holds. Let such a $j$ corresponding to $n > 0$ be $i_n$. Then the elements $i_0 , i_1 , i_2 , \ldots$ are pairwise distinct. Hence there would be infinitely many objects in $\cal D$ contradicting the finiteness of a database. \qed

\end{proof}

\begin{lemma} \label{lemma2-vc}

\ Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then $\cal D$ satisfies at each stage of Algorithm \ref{alg-vc} uniqueness constraints for all $i = 1 , \ldots , n$ defined by some $c_i : T_{C_i} \rightarrow G(C_i)$.

\end{lemma}

\begin{proof}

It is sufficient to show that whenever a rule is applied replacing $G(C_i)$ by $G(C_i)^\prime$, then $G(C_i)^\prime$ also defines a uniqueness constraint on $C_i$.

Suppose that $Pair(i,v) \in C_i$ holds in $\cal D$. Since it is possible to apply a rule to $G(C_i)$, there exists at least one value $j :: ID$ occurring in $c_i(v)$. Replacing $ID_j$ in $G(C_i)$ corresponds to replacing $j$ by some value $v_j :: G(C_j)$. Because of the finiteness property such a value must exist. Moreover, due to the uniqueness constraint defined by $c_j$ the function $f : G(C_i) \rightarrow G(C_i)^\prime$ representing this replacement must be injective on $c_i(codom_{\cal D}(C_i))$. Hence, $c_i^\prime = f \circ c_i$ defines a uniqueness constraint on $C_i$. \qed

\end{proof}

\begin{lemma} \label{lemma2-ic}

\ Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then $\cal D$ satisfies at each stage of Algorithm \ref{alg-ic} uniqueness constraints for all $i = 1 , \ldots , n$ defined by some $c_i^\prime : T_{C_i} \rightarrow F(C_i)$.

\end{lemma}

\begin{proof}

The proof is analogous to the proof of Lemma \ref{lemma2-vc}. \qed

\end{proof}

\begin{lemma} \label{lemma-vc-ic}

Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then at each stage of the algorithms \ref{alg-vc} and \ref{alg-ic} for all $i = 1 , \ldots , n$ there exists a function $\bar{c}_i : G(C_i) \rightarrow F(C_i)$ that is unique on $c_i(codom_{\cal D}(C_i))$ with $c_i^\prime = \bar{c}_i \circ c_i$.

\end{lemma}

\begin{proof}

As in the proof of Lemma \ref{lemma2-vc} it is sufficient to show that the required property is preserved by the application of a rule from Algorithm \ref{alg-vc} or \ref{alg-ic}. Therefore, let $\bar{c}_i$ satisfy the required property and let $g : G(C_i) \rightarrow G(C_i)^\prime$ and $f : F(C_i) \rightarrow F(C_i)^\prime$ be functions corresponding to the application of a rule to $G(C_i)$ and $F(C_i)$ respectively. Such functions were constructed in the proofs of Lemma \ref{lemma2-vc} and Lemma \ref{lemma2-ic} respectively. 

Then $f \circ \bar{c}_i$ satisfies the required property with respect to the application of $f$. In the case of applying $g$ we know that $g$ is injective on $c_i(codom_{\cal D}(C_i))$. Let $h : G(C_i)^\prime \rightarrow G(C_i)$ be any continuation of $g^{-1} : g(c_i(codom_{\cal D}(C_i))) \rightarrow G(C_i)$. Then $\bar{c}_i \circ h$ satisfies the required property. \qed

\end{proof}

\begin{theorem} \label{vc-theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in the reference graph $G_{ref}$ of $C$. Let $V_C$ be the type $G(C)$ computed by Algorithm \ref{alg-vc}. Then $C$ is value-representable with value representation type $V_C$.

\end{theorem}

\begin{proof}

\ $V_C$ is a proper value type by Lemma \ref{lemma-vc}. From Lemma \ref{lemma2-vc} it follows that if $\cal D$ is an instance of $\cal S$, then there exists a function $c : T_C \rightarrow V_C$ such that the uniqueness constraint defined by $c$ holds for $\cal D$. 

If $V_C^\prime$ is another proper value type and $\cal D$ satisfies a uniqueness constraint defined by $c^\prime : T_C \rightarrow V_C^\prime$, then $V_C^\prime$ is some value-identification type $I_C$. Hence by Lemma \ref{lemma-vc-ic} there exists a function $c^\prime{}^\prime : V_C \rightarrow V_C^\prime$ that is unique on $c(codom_{\cal D}(C))$ with $c^\prime = c^\prime{}^\prime \circ c$. This proves the lemma. \qed

\end{proof}

\begin{theorem} \label{ic-theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in some identification graph $G_{id}$ of $C$. Let $I_C$ be the type $F(C)$ computed by Algorithm \ref{alg-ic} with respect to the uniqueness constraints used in the definition of $G_{id}$. Then $C$ is value-identifiable with value identification type $I_C$.

\end{theorem}

\begin{proof}

The proof is analogous to that of Theorem \ref{vc-theorem}. \qed

\end{proof}

\begin{theorem} \label{fin-theorem}

\ Let $C$ be a class in a schema $\cal S$. Then the value-representability and the value-identifiability of $C$ are decidable.

\end{theorem}

\begin{proof}

The proof is analogous to that of Theorem \ref{simple-char}. \qed

\end{proof}

\section{Existence and Consistency of Generic Update Operations} \label{generic}

{\em Methods} are used to specify the dynamics of an object-oriented database. Here, we do not want to give a concrete language for methods. In general methods can be specified in the style of Dijkstra focussing on deterministic operations \cite{iwsds}.

In this paper we are only interested in {\em canonical update operations}, i.e. we want to associate with each class $C$ in a schema $\cal S$ {\em methods} for {\em insertion}, {\em deletion}\/ and {\em update}\/ on single objects. These operations should be consistent with respect to the constraints in $\cal S$. Thus, they are sufficient to express the creation, deletion and change of objects including the migration between classes. However, we would like to regard these operations as being ``generic'' in the sense of polymorphic functions, since insert, delete and update should be defined for each class. The problem is that the input-type and the body of these operations require information from the schema. This leads to polymorphism with respect to meta-types. For the purpose of this paper we do not discuss this problem.

\subsection{Canonical Update Operations}

The requirement that object-identifiers have to be hidden from the user imposes the restriction on canonical update operations to be value-defined in the sense that the identifier of a new object has to be chosen by the system whereas all input- and output-data have to be values of proper value types.

We now formally define canonical update operations. For this purpose regard an instance $\cal D$ of a schema $\cal S$ as a set of objects. For each recursively defined type $T$ let $\bar{T}$ denote by replacing each occurrence of a recursive type $T^\prime$ in $T$ by $UNION(T^\prime,ID)$.

\begin{definition} \label{generic-upd}

Let C be a class in a schema $\cal S$. {\em Canonical update operations} on $C$ are $insert_C$, $delete_C$ and $update_C$ satisfying the following properties:

\begin{enumerate}

\item Their input types are proper value types; their output type is the trivial type $\bot$.

\item In the case of $insert$ applied to an instance $\cal D$ there exists a distinguished object $o :: PAIR(ID,T_C)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime$ with $o \in {\cal D}^\prime$ and ${\cal D} \subseteq {\cal D}^\prime$ hold and

\item if $\bar{\cal D}$ is any instance with ${\cal D} \subseteq \bar{\cal D}$ and $o \in \bar{\cal D}$, then ${\cal D}^\prime \subseteq \bar{\cal D}$.

\end{enumerate}

\item In the case of $delete$ applied to an instance $\cal D$ there exists a distinguished object $o :: PAIR(ID,T_C)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime$ with $o \not\in {\cal D}^\prime$ and ${\cal D}^\prime \subseteq {\cal D}$ hold and

\item if $\bar{\cal D}$ is any instance with $\bar{\cal D} \subseteq {\cal D}$ and $o \not\in \bar{\cal D}$, then $\bar{\cal D} \subseteq {\cal D}^\prime$.

\end{enumerate}

\item In the case of $update$ applied to an instance ${\cal D} = {\cal D}_1 \disunion {\cal D}_2$, where ${\cal D}_2 = \{ o \}$ if $o \neq o^\prime$ and ${\cal D}_2 = \emptyset$ otherwise there exist distinguished objects $o,o^\prime :: PAIR(ID,T_C)$ with $o = Pair(i,v)$ and $o^\prime = Pair(i,v^\prime)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime = {\cal D}_1 \disunion {\cal D}_2^\prime$ with ${\cal D}_2 \cap {\cal D}_2^\prime = \emptyset$,

\item $o \in {\cal D}$, $o^\prime \in {\cal D}^\prime$,

\item if $\bar{\cal D}$ is any instance with ${\cal D}_1 \subseteq \bar{\cal D}$ and $o^\prime \in \bar{\cal D}$, then ${\cal D}^\prime \subseteq \bar{\cal D}$.

\end{enumerate}

\end{enumerate}

\noindent
{\em Quasi-canonical update operations} on $C$ are $insert_C^\prime$, $delete_C^\prime$ and $update_C^\prime$ defined analogously with the only difference of their output type being $ID$ and their input-type being $\bar{T}$ for some value-type $T$.

\end{definition}

\noindent
Note that this definition of canonical update operations includes the consistency with respect to the implicit and explicit constraints on $\cal S$. We show that value-representability is sufficient for the existence and uniqueness of such operations. We use a guarded command notation as in \cite{iwsds} for these update operations.

\begin{lemma} \label{lemma28}

\ Let $C$ be a class in a schema $\cal S$ such that there exist quasi-canonical update operations on $C$. Then also canonical update operations exist on $C$.

\end{lemma}

\begin{proof}

\ In the case of {\em insert} define $insert_C (V :: V_C) == I \leftarrow insert_C^\prime (V)$, i.e. call the corresponding quasi-canonical operation and ignore its output. The same argument applies to {\em delete} and {\em update}. \qed

\end{proof}

\subsection{Existence of Canonical Updates in the Case of Value-Representability}
Our next goal is to reduce the existence problem of quasi-canonical update operations to schemata without IsA relations.

\begin{lemma} \label{lemma29}

Let $C$, $D$ be value-representable classes in a schema $\cal S$ such that $C$ is a subclass of $D$ with subtype function $g : T_C \rightarrow T_D$. Then there exists a function $h : V_C \rightarrow V_D$ such that for each instance $\cal D$ of $\cal S$ with corresponding functions $c : T_C \rightarrow V_C$ and $d : T_D \rightarrow V_D$ we have $h(c(v)) = d(g(v))$ for all $v \in codom_{\cal D}(C)$.

\end{lemma}

\begin{proof}

\ By Definition \ref{value-repr} $c$ is injective on $codom_{\cal D}(C)$, hence any continuation $h$ of $d \circ g \circ c^{-1}$ satisfies the required property.

It remains to show that $h$ does not depend on $\cal D$. Suppose ${\cal D}_1$, ${\cal D}_2$ are two instances such that $w = c_1(v_1) = c_2(v_2) \in V_C$, where $c_1 ,d_1, h_1$ correspond to ${\cal D}_1$ and $c_2 ,d_2, h_2$ correspond to ${\cal D}_2$. Then there exists a permutation $\pi$ on $ID$ such that $v_2 = \pi(v_1)$. We may extend $\pi$ to a permutation on any type. Since $ID$ has no non-trivial supertype, $g$ permutes with $\pi$, hence $g(v_2) = \pi(g(v_1))$. From Definition \ref{value-repr} it follows $d_2(g(v_2)) = d_1(g(v_1))$, i.e. $h_2(w) = h_1(w)$. \qed

\end{proof}

\noindent
In the following let ${\cal S}_0$ be a schema derived from a schema $\cal S$ by omitting all IsA relations.

\begin{lemma} \label{lemma30}

\ Let $C$ be a value-representable class in $\cal S$ such that all its superclasses $D_1 \ldots D_n$ are also value-representable. Then quasi-canonical update operations exist on $C$ in $\cal S$ iff they exist on $C$ and all $D_i$ in ${\cal S}_0$.

\end{lemma}

\begin{proof}

\ By Theorem \ref{vc-theorem} the value-representation type $V_C$ is the result of Algorithm \ref{alg-vc}, hence $V_C$ does not depend on the inclusion constraints of $\cal S$. Then we have
\begin{eqnarray*} 
&& I :: ID \, \leftarrow \, insert_C^\prime(V :: V_C) == \\
&& \hspace*{20pt} I \leftarrow insert_{D_1}^\prime(h_1(V)) ; \ldots ; I \leftarrow insert_{D_n}^\prime(h_n(V)) ; I \leftarrow insert_C^0(V) \; \; \; ,
\end{eqnarray*}
\noindent
where $h_i : V_C \rightarrow V_{D_i}$ is the function of Lemma \ref{lemma29} and $insert_C^0$ denotes a quasi-canonical insert on $C$ in ${\cal S}_0$. Hence in this case the result for the {\em insert} follows by structural induction on the IsA-hierarchy.

If the subtype function $g$ required in Lemma \ref{lemma29} does not exist for some superclass $D$ then simply add $V_D$ to the input type. We omit the details for this case.

The arguments for {\em delete}\/ and {\em update}\/ are analogous. \qed

\end{proof}

\noindent
Now assume the existence of a global operation $NewId$ that produces a fresh identifier $I :: ID$.

\begin{lemma} \label{lemma31}

\ Let $C$ be a value-representable class in ${\cal S}_0$. Then there exist unique quasi-canonical update operations on $C$.

\end{lemma}

\begin{proof}

\ Let $r_i : C_i$ ($i = 1 \ldots n$) denote the references in the structure expression of $C$. If $V$ be a value of type $\bar{V_C}$, then there exist values $V_{i,j} :: \bar{V_{C_i}}$ ($i = 1 \ldots n , j = 1 \ldots k_i$) occurring in $V$. Let $\bar{V} = \{ V_{i,j} / J_{i,j} \mid i = 1 \ldots n , j = 1 \ldots k_i \} . V$ denote the value of type $T_C$ that results from replacing each $V_{i,j}$ by some $J_{i,j} :: ID$. Moreover, for $I :: ID$ let 
\[ V_{i,j}^{(I)} = \left \{ \begin{array}{ccl}
\{ V / I \} . V_{i,j} && \mbox{if } V \mbox{ occurs in } V_{i,j}\\
V_{i,j} && \mbox{else} \end{array} \right . \]
Then the quasi-canonical insert operation can be defined as follows: 
\begin{eqnarray*}
&& I :: ID \leftarrow insert_C^\prime ( V :: \bar{V_C} ) \, == \\
&& IF \; \exists \, I^\prime :: ID \, , \, V^\prime :: T_C . \; ( Pair(I^\prime,V^\prime) \in C \, \wedge \, c(V^\prime) = V ) \\
&& THEN \; I := I^\prime\\
&& ELSE \; I \leftarrow NewId \: ; \: J_{1,1} \leftarrow insert_{C_1}^\prime (V_{1,1}^{(I)}) \, ; \, \ldots \, ; \, J_{n,k_n} \leftarrow insert_{C_n}^\prime (V_{n,k_n}^{(I)}) \, ; \\
&& \hspace*{45pt} C := C \cup \{ Pair(I,\bar{V}) \}\\
&& FI
\end{eqnarray*} 
\noindent
It remains to show that this operation is indeed quasi-canonical. Apply the operation to some instance $\cal D$. If there already exists some object $o = Pair(I^\prime,V^\prime)$ in $C$ with $c(V^\prime) = V$, the result is ${\cal D}^\prime = {\cal D}$ and the requirements of Definition \ref{generic-upd} are trivially satisfied. Otherwise let the distinguished object be $o = Pair(I,\bar{V})$. If $\bar{\cal D}$ is an instance with ${\cal D} \subseteq \bar{\cal D}$ and $o \in \bar{\cal D}$, we have $J_{i,j} \in dom(C_i)$ for all $i = 1 \ldots n$, $j = 1 \ldots k_i$, since $\bar{\cal D}$ satisfies the referential constraints. Hence $\bar{\cal D}$ contains the distinguished objects corresponding to the involved quasi-canonical operations $insert_{C_i}^\prime$.. By induction on the length of call-sequences ${\cal D}_{i,j} \subseteq \bar{\cal D}$ for all $i = 1 \ldots n$, $j = 1 \ldots k_i$, where ${\cal D}_{i,j}$ is the result of $J_{i,j} \leftarrow insert_{C_i}^\prime(V_{i,j}^{(I)})$. Hence ${\cal D}^\prime = \b
igcup\limits_{i,j} {\cal D}_{i,j} \, \cup \, \{ o \} \subseteq \bar{\cal D}$. The uniqueness follows from the uniqueness of $V_C$.

The definitions and proofs for {\em delete}\/ and {\em update}\/ are analogous. \qed

\end{proof}

\begin{theorem} \label{theo-vdef}

\ Let $C$ be a value-representable class in a schema $\cal S$ such that all its superclasses are also value-representable. Then there exist unique canonical update operations on $C$.

\end{theorem}

\begin{proof}

\ By Lemma \ref{lemma28} and Lemma \ref{lemma30} it is sufficient to show the existence of quasi-canonical update operations on $C$ and all its superclasses in the schema ${\cal S}_0$. This follows from Lemma \ref{lemma31}. \qed

\end{proof}

\section{Conclusion} \label{conc}

In this paper we introduce a structural object-oriented datamodel with a clear distinction between types and classes. Types are algebraically specified such that each value of a type is finitely representable. This can be exploited to define constraints on a schema in a uniform way. Moreover, parameterized type declarations and a unique object identifier type can be used to represent classes by a partial function type. 

An advantage of the uniform type and constraint declarations is the possibility to study alternatives for the representation of objects. Our main interest are objects that could also be represented without using abstract object identifiers. We call them value-representable. Due to the finiteness of a database value-representability is decidable if uniqueness constraints are the only explicit constraints. Moreover, we show that value-representability is sufficient for the existence of unique structurally determined canonical update operations that enforce implicit referential and inclusion constraints.  

This constitutes the basis of a behavioural object-oriented datamodel. Therefore, the next steps will be to extend the outlined approach to a complete formal object-oriented datamodel including a complete query language, views and transactions.

\begin{thebibliography}{12}

\bibitem{abiteboul} S.~Abiteboul: {\it Towards a deductive object-oriented database language}, Data \& Knowledge Engineering, vol. 5, 1990, pp. 263 -- 287

\bibitem{oidquery} S.~Abiteboul, P. Kanellakis: {\it Object Identity as a Query Language Primitive}, in Proc. SIGMOD, Portland Oregon, 1989, pp. 159 -- 173

% \bibitem[AGO91]{albano1} A.~Albano, G.~Ghelli, R.~Orsini: {\it Objects and Classes for a Database Programming 
% Language}, FIDE technical report 91/16, 1991

\bibitem{albano} A.~Albano, G.~Ghelli, R.~Orsini: {\it A Relationship Mechanism for a Strongly Typed Object-Oriented Database Programming Language}, in A.~Sernadas (Ed.): {\it Proc. VLDB 91}, Barcelona 1991

% \bibitem[AlTh90]{key}
% S. Al Fedaghi, B. Thalheim: {\it Fundamentals of databases - The key concept},
% submitted for publication, 1990

\bibitem{oo-manifesto} M.~Atkinson, F.~Bancilhon, D.~DeWitt, K.~Dittrich, S.~Zdonik: {\it The Object-Oriented Database System Manifesto}, Proc. 1st DOOD, Kyoto 1989

\bibitem{o2} F.~Bancilhon, G.~Barbedette, V.~Benzaken, C.~Delobel, S.~Gamerman, C.~L{\'e}cluse, P.~Pfeffer, P.~Richard, F.~Velez: {\it The Design and Implementation of O$_2$, an Object-Oriented Database System}, Proc. of the ooDBS II workshop, Bad M{\"u}nster, FRG, September 1988

\bibitem{beeri2} C.~Beeri: {\it Formal Models for Object-Oriented 
Databases}, Proc. 1st DOOD 1989, pp. 370 -- 395

\bibitem{beeri} C.~Beeri: {\it A formal approach to object-oriented databases}, Data and Knowledge Engineering, vol. 5 (4), 1990, pp. 353 -- 382

\bibitem{bk} C.~Beeri, Y.~Kornatzky: {\it Algebraic Optimization of Object-Oriented Query Languages},
in S.~Abiteboul, P.~C.~Kanellakis (Eds.): Proceedings of ICDT 90, Springer LNCS 470, pp. 72 -- 88

% \bibitem[Broy85]{broy} M. Broy: {\it Algebraic Characterization of Models for $\lambda$-Calculus}, Passau University, % report MIP -- 8507, 1985

% \bibitem[BrWe87]{wegner} K.~B.~Bruce, P.~Wegner: {\it An Algebraic Model of
% Subtype and Inheritance}, in F.~Bancilhon, P.~Buneman (Eds.): {\it Workshop
% on Database Programming Languages}, Roscoff, France, September 1987

\bibitem{exodus} M.~Carey, D.~DeWitt, S.~Vandenberg: {\it A Data Model and Query Language for EXODUS}, Proc. ACM SIGMOD 88

\bibitem{vision} M.~Caruso, E.~Sciore: {\it The VISION Object-Oriented Database Management System}, Proc. of the Workshop on Database Programming Languages, Roscoff, France, September 1987

% \bibitem[DiSc89]{dij}
% E. W. Dijkstra, C. S. Scholten: {\it Predicate Calculus and Program Semantics},
% Springer-Verlag, 1989

% \bibitem[EGL89]{lipeck} H.-D. Ehrich, M.~Gogolla, U.~Lipeck: {\it Algebraische Spezifikation abstrakter Datentypen}, % Teubner-Verlag, 1989

% \bibitem[EhSe91]{ehrich} H.-D.~Ehrich, A.~Sernadas: {\it Fundamental Object Concepts and Constructors}, in G.~Saake, % A.~Sernadas (Eds.): Information Systems -- Correctness and Reusability, TU Braunschweig, Informatik Berichte 91-03, 
% 1991

% \bibitem[EhMa85]{ehma} H. Ehrig, B. Mahr: {\it Fundamentals of Algebraic Specification}, vol.1, Springer 1985

\bibitem{iris} D.~Fishman, D.~Beech, H.~Cate, E.~Chow et al.: {\it IRIS: An Object-Oriented Database Management System}, ACM ToIS, vol. 5(1), January 1987

% \bibitem[GKS91]{gottlob} G.~Gottlob, G.~Kappel, M.~Schrefl: {\it Semantics of Object-Oriented Data Models -- The 
% Evolving Algebra Approach}, in J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation
% Information  Systems Technology, Springer LNCS, vol. 504, 1991

% \bibitem[HeSa91]{heuer} A.~Heuer, P.~Sander: {\it Classifying Object-Oriented 
% Results in a Class/Type Lattice}, in B.~Thalheim et al. (Ed.): {\it 
% Proceedings MFDBS 91}, Springer LNCS 495, pp. 14 -- 28

\bibitem{oid86} S. Khoshafian, G. Copeland: {\it Object Identity}, 
Proc. 1st Int. Conf. on OOPSLA, Portland, Oregon, 1986

\bibitem{orion} W.~Kim, N.~Ballou, J.~Banerjee, H.~T.~Chou, J.~Garza, D.~Woelk: {\it Integrating an Object-Oriented Programming System with a Database System}, in Proc. OOPSLA 1988

% \bibitem[LoSc87]{lockemann} P.~Lockemann, J.~W.~Schmidt: {\it Datenbankhandbuch}, Springer, 1987

\bibitem{gemstone} D.~Maier, J.~Stein, A.~Ottis, A.~Purdy: {\it Development of an Object-Oriented DBMS}, OOPSLA, September 1986

% \bibitem{nelson} G.~Nelson: {\it A Generalization of Dijkstra's Calculus}, ACM TOPLAS, vol. 11 (4), October 
% 1989, pp. 517 -- 561

% \bibitem[Oho90]{ohori} A. Ohori: {\it Representing Object Identity in a Pure Functional Language}, Proc. ICDT 90, 
% Springer LNCS, pp. 41 -- 55

% \bibitem[SaJu91]{saake} G. Saake, R. Jungclaus: {\it Specification of Database Applications in the TROLL Language}, 
% in Proc. Int. Workshop on the Specification of Database Systems, Glasgow, 1991

% \bibitem[SSW$^+$91]{fide}
% K.-D.~Schewe, J.~W.~Schmidt, I.~Wetzel, N.~Bidoit, D.~Castelli, C.~Meghini: 
% {\it Abstract Machines Revisited}, FIDE technical report 1991/11

\bibitem{rostock}
K.-D.~Schewe, B.~Thalheim, I.~Wetzel, J.~W.~Schmidt: {\it Extensible Safe Object-Oriented Design of Database Applications}, University of Rostock, Technical report, September 1991 

\bibitem{iwsds} K.-D.~Schewe, I.~Wetzel, J.~W.~Schmidt: {\it Towards a Structured Specification Language for Database Applications}, in Proc. Int. Workshop on the Specification of Database Systems, Glasgow, Springer WICS 1991

% \bibitem[ScSc90]{schekscholl} M. H. Scholl, H.-J. Schek: {\it A Relational Object Model}, in Proc. ICDT 90, Springer 
% LNCS, pp. 89 -- 105

% \bibitem[ShZd89]{shaw} G. M. Shaw, S. B. Zdonik: {\it An Object-Oriented Query-Algebra}, IEEE Data Engineering, vol. 
% 12 (3), 1989, pp. 29 -- 36

% \bibitem{tha88} B.~Thalheim: {\it Dependencies in Relational Databases}, Teubner Leipzig, 1988

% \bibitem[Tha91]{herm} B.~Thalheim: {\it The Higher-Order Entity-Relationship
% Model}, in J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation
% Information  Systems Technology, Springer LNCS, vol. 504, 1991

\end{thebibliography}

\end{document}
