Received: from relay.cs.ruu.nl by moose.cs.indiana.edu
	(8.7.1/IUCS.1.39) id EAA29771; Tue, 23 Jan 1996 04:53:16 -0500 (EST)
Received: from orff.cs.ruu.nl (orff.cs.ruu.nl [131.211.80.234]) by relay.cs.ruu.nl (8.7.3/8.7.3/UU-CS) with ESMTP id KAA12581 for <itallc96@cs.indiana.edu>; Tue, 23 Jan 1996 10:14:13 +0100 (MET)
From: Wiebe van der Hoek <wiebe@cs.ruu.nl>
Received: (wiebe@localhost) by orff.cs.ruu.nl (8.6.12/8.6.12/ehk) id KAA17685 for itallc96@cs.indiana.edu; Tue, 23 Jan 1996 10:14:12 +0100
Message-Id: <199601230914.KAA17685@orff.cs.ruu.nl>
Subject: no subject (file transmission)
To: itallc96@cs.indiana.edu
Date: Tue, 23 Jan 1996 10:14:11 +0100 (MET)
X-Mailer: ELM [version 2.4 PL25]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Status: RO

%Dear italcc-organizers,

% a bit late, I admit, we like to submit our paper "Interleaved
%Contractino to itallc96. We had some permission for delay by
%larry mos, and I hope even this long delay will not be a big
% problem. Anyway, if you think it is too late in the meanwhile,
% I would understand too.

%Kind regards, Wiebe van der Hoek




%%
%% `Interleaved contractions' by Wiebe van der Hoek and Maarten de Rijke
%%
\documentstyle[11pt]{article}

\makeatletter
\newtheorem{dfi}{Definition}
\newtheorem{cvt}[dfi]{Convention}
\newtheorem{corollary}[dfi]{Corollary}
\newtheorem{lemma}[dfi]{Lemma}
\newtheorem{observation}[dfi]{Observation}
\newtheorem{proposition}[dfi]{Proposition}
\newtheorem{qst}[dfi]{Question}
\newtheorem{theorem}[dfi]{Theorem}
\newenvironment{convention}{\begin{cvt}\rm}{\end{cvt}}
\newenvironment{definition}{\begin{dfi}\rm}{\end{dfi}}
\newenvironment{question}{\begin{qst}\rm}{\end{qst}}

\newcommand{\twovector}[2]{\left(\begin{array}{c}
   {#1} \\
   {#2}
  \end{array}\right)}

\newcommand{\threevector}[3]{\left(\begin{array}{c}
   {#1} \\
   {#2} \\
   {#3}
  \end{array}\right)}

\newcommand{\Cn}{{\rm Cn}}
\newcommand{\Th}{{\rm Th}}


%%% Proof environment
\newenvironment{proof}{\proof}{\endproof}

\def\proof{\followon{Proof}}
\def\endproof{\ifSuppressEndOfProof\global\SuppressEndOfProoffalse
  \else\xqed\fi\endfollowon}
\def\followon#1{\trivlist\item[\hskip\labelsep{\it#1.}]}
\def\endfollowon{\endtrivlist}

% push end of proof to the right for a bit
\def\pushright#1{{\parfillskip=0pt\widowpenalty=10000
\displaywidowpenalty=10000\finalhyphendemerits=0\leavevmode\unskip
\nobreak\penalty50{#1}\hskip.2em\null\hfill \ \par}}

% command to force early end of proof marker. This is used if the end
% of proof marker would otherwise come out in the wrong place.
\def\qed{\markendofproof\global\SuppressEndOfProoftrue}
\newif\ifSuppressEndOfProof\SuppressEndOfProoffalse
\def\xqed{\pushright\markendofproof}
\def\markendofproof{ \ \ \ \mbox{$\dashv$}}
%%% End of proof environment


%%% itemlist environment
\newbox\itembox
\def\itemlistlabel#1{#1\hfill}
\def\itemlist#1{\setbox\itembox=\hbox{#1}%
                \list{}{\labelwidth\wd\itembox
                             \leftmargin\labelwidth
                             \advance\leftmargin by\itemindent
                             \advance\leftmargin by\labelsep
                             \let\makelabel\itemlistlabel}}
\let\enditemlist\endlist

%%% miscellaneous
\newcommand{\Con}[3]{(#1 \sim \vec{#2}) \propto #3}
\newcommand{\ConTphiS}{\Con{T}{\phi}{S}}
\newcommand{\vph}{\vec{\phi}}
\newcommand{\vps}{\vec{\psi}}

\mathchardef\Gamma="0100
\mathchardef\Delta="0101
\mathchardef\Theta="0102
\mathchardef\Lambda="0103
\mathchardef\Xi="0104
\mathchardef\Pi="0105
\mathchardef\Sigma="0106
\mathchardef\Upsilon="0107
\mathchardef\Phi="0108
\mathchardef\Psi="0109
\mathchardef\Omega="010A

%%% page size etc
%
%---------------------------------------------------------------------
% This is A4.sty in text format. %
% ---------------------------------------------------------------------
% This file is based on the document style options A4 and A4wide
% that can be found in the Rochester style archive.
% These files were written by
%     John Pavel,         May  1987,    `a4' document style option.
%     Jean-Francois Lamy, July 1986,    `A4wide' document style option.
%
% In the near future, this document style option will be modified,
% especially for use with ten point typefaces.
%
% Version 0.1: 28 Mar 89
%              combined A4.sty and A4wide.sty from Rochester archive
%         0.2: 9 Jun 89
%              decreased \textwidth for 10pt and 11pt
%
% Editor     : Nico Poppelier
%
%         0.3: 28 Jul 89
%              decreased \textwidth for 11pt and 12pt
%              modified the margins for twodsided printing so that
%              text is printed in the same place on both pages
%              modified marginparwidth's to fit on the paper
%              modified the comments
%
% Editor     : Johannes Braams
% ---------------------------------------------------------------------
%
%
% First, redefine the \textheight and \topmargin
% for A4 paper, as opposed to US paper.
%
% \textheight is the height of text (including footnotes and figures,
% excluding running head and foot).
%
% Adjusting \textheight will adjust position of the bottom of the page.
% Must preserve `(\textheight - \topskip) divides \baselineskip'.
% \topskip always appears to be 10pt.
%
% Following Lamport's change to other style files on 24 Jun 86,
% changed to explicitly compute \textheight to avoid roundoff.
% The value of the multiplier was calculated as the floor of the old
% \textheight minus \topskip, divided by \baselineskip for
% \normalsize.
%
%
\topmargin 0 pt     % Nominal distance from top of paper to top of page
\ifcase \@ptsize
    % modifications for 10 pt
    \textheight 53\baselineskip
\or % modifications for 11 pt
    \textheight 46\baselineskip
\or % modifications for 12 pt
    \textheight 42\baselineskip
\fi
\advance\textheight by \topskip
%
%
% Now redefines the margins so that they are more in line with
% what we are used to see.
%
    \textwidth      15 cm    % Width of text line.
  \if@twoside
    \oddsidemargin  5 mm % Left margin on odd-numbered pages.
    \evensidemargin 5 mm % Left margin on even-numbered pages.
    \marginparwidth 0.90in    % Width of marginal notes.
  \else
    \oddsidemargin  5 mm % Note that \oddsidemargin = \evensidemargin
    \evensidemargin 5 mm %
    \marginparwidth 1.00in
  \fi

\makeatother


\title{Interleaved Contractions}
\author{Wiebe van der Hoek$^1$ and Maarten de Rijke$^2$\\[1.5ex]
\large $^1$~Dept. of Computer Science, Utrecht University\\
\large P.O.\ Box 80089, 3508 TB Utrecht, the Netherlands \\
{\large\tt wiebe@cs.ruu.nl} \\
{\large $^2$~Dept. of Computer Science, University of Warwick} \\
{\large Coventry CV4 7AL} \\
{\large\tt mdr@dcs.warwick.ac.uk}\\[2ex]
%
{\bf The corresponding author is Wiebe van der Hoek}}
\date{January 1996}

\begin{document}
\maketitle
\begin{abstract}
\noindent%
We study an approach to concurrent contractions, that is,
to simultaneous contractions performed by multiple agents.
Using ideas from the semantics of programming we adopt an interleaved
approach to reason about concurrent contractions. Although many of the
notions from the traditional G\"{a}rdenfors approach transfer to this 
setting, our approach also forces us to depart from the AGM framework in
important ways. We present both laws describing rational concurrent 
contractions, and a construction that satisfies these laws.
\end{abstract}


\section{Introduction}
In real life concurrent accessing of data is the rule.  Multiple 
agents are working on the same theory, and multiple copies of some data are 
kept in different locations.  Typical examples include scientific research 
or writing a joint-publication, and practical applications vary from 
networks of personal computers and workstations sharing some common 
information to widely distributed applications such as automatic 
teller machines. The primary advantage of concurrent theory change as
opposed to single agent theory change is the ability to share, access
and engineer data in an efficient manner. The primary disadvantage is the
added complexity required to ensure proper coordination between the agents
taking part.

In a multi-agent setting, managing a belief set is a {\em concurrent\/} 
task: not only may several agents {\em retrieve\/} information from one and 
the same source,
but it may also be the case that multiple agents have permission 
to {\em alter\/} a database (the flight booking procedures are a typical 
example here).  What are sensible strategies for conflict resolution in case 
inconsistency strikes? The task of maintaining consistency in 
the setting of multi-agent theory change is more complex than in the 
single agent case, if only because of the many possibilities that become 
visible.

This abstract is part of a larger project on concurrent theory change
(see \cite{hoek:conc95}). Its purpose is to demonstrate that concurrent 
theory change forms an interesting extension of the traditional G\"ardenfors 
style approach towards theory change, one that has many faces and that calls 
for new 
tools.  Here we will confine ourselves to the simplest case in which a number 
of agents have access to shared data.  The data are changed via contractions, 
which may in principle be proposed by any one of the agents.  We will 
explore some of the options and problems that present themselves. A 
central question of this abstract is: assuming that multiple agents, each 
guided by a familiar set of rationality postulates, propose or 
perform (single agent) contractions for a shared theory, --- what are the 
laws governing the global contractions?

The rest of the abstract is organized as follows. In Section~2 we briefly 
outline the general set-up. Section~3 contains an informal discussion of 
concurrent contractions, and Section~4 recalls some facts from the standard 
G\"ardenfors framework. Then, in Sections~5, 6 and~7 we present our formal 
approach to concurrent contractions, based on the idea of interleaving. We 
conclude the abstract with comments and suggestions for further work in 
Section~8.


 

\section{General Set-up}
There have been many proposals to alter or extend the basic 
Alchourr\'on, G\"ardenfors, Makinson (AGM) framework 
of theory change (see \cite{gard:beli92} for an overview), but most of the 
literature in the AGM tradition focuses on a single agent changing a theory 
as she receives new information.  The actions of this solitary agent are 
usually specified in terms of functional input/output behavior:
\begin{equation}
(T,\phi)\mapsto T',
\label{specify-tc}
\end{equation}
where the input consists of a collection of sentences $T$ (the 
material to be changed) and a sentence $\phi$ (the newly received 
information), and the output is a collection of sentences $T'$ (the result 
of the cognitive action).  Traditionally, three forms of 
theory change are considered: {\em expansions\/}, where we add 
$\phi$ to $T$ and close under logical consequence; {\em contractions\/}, 
where we remove $\phi$ from $T$ while preserving as much of $T$ as 
possible; and {\em revisions\/}, where we add $\phi$ to $T$ while 
maintainine or restoring consistency.  
In this abstract we change the format given in (\ref{specify-tc}), and 
consider concurrent contractions that are specified by expressions of the 
form
\begin{equation}
T\sim\threevector{\phi_1}{\vdots}{\phi_n},
\label{specify-cc}
\end{equation}\noindent%
or $T\sim\vec{\phi}$, where $T$ is as before, and 
$\vec{\phi}$ is a vector of formulas to be contracted from $T$; $\sim$ is 
the concurrent contraction action whose principles we want to understand.  
The basic assumption here is that there are $n$ agents $A_1$, \ldots, 
$A_n$, each of whom proposes or performs a contraction of $T$ in accordance 
with her own contraction operation.  That is, $A_1$ proposes or performs a 
contraction of $T$ by $\phi_1$, \ldots, $A_n$ proposes or performs a 
contraction of $T$ by $\phi_n$, where each agent $A_i$ has her own 
contraction operation $-_i$.  The expression in (\ref{specify-cc}) 
denotes the result(s) of an operation on $T$ that is somehow 
composed of contractions of $T$ by $\phi_1$, 
\ldots, $\phi_n$ performed by, respectively, $A_1$, \ldots, $A_n$ using 
their respective contraction operations $-_1$, \ldots, $-_n$.  The key 
questions we address are:

\begin{itemize}
\renewcommand{\itemsep}{-2pt}
\item How can we model concurrent contractions?
\item Which laws govern the concurrent contraction operation $\sim$?
\item How can $\sim$ be understood in terms of the single agent operations
  $-_1$, \ldots, $-_n$?
\end{itemize}
Below we will explore concurrent contractions.  
We leave the much more complicated (and realistic) case of {\em 
heterogeneous\/}
concurrent theory change in which multi-agent contractions, revisions and 
expansions may take place concurrently to later publications.




\section{Why contract concurrently?}
Before proceeding we give an informal discussion of concurrent 
contractions.  Our basic picture is one where $n$ agents $A_1$, \ldots, 
$A_n$ simultaneously want to remove information from a given background 
theory $T$, that is: each agent proposes or performs a contraction, 
using her private contraction operation.  

To give an example of concurrent theory change at work, one can think of a 
patient's record in a medical database.  Various agents contribute to the 
theory contained in the database: a family doctor's report,
various laboratories with their test results, specialists with
further information\ldots .  Clearly, it is important that consistency be 
preserved.  One may conceptualize this is by personify 
consistency checking in terms of a checker that performs consistency checks 
at certain discrete intervals.  If the checker detects an inconsistency in 
the shared theory, she rings the alarm bell, asking the agents to suggest 
contractions that will help remove the inconsistency.  The agents then 
perform or suggest a contraction.  Having different areas of expertise,
the agents are likely to base their suggested contractions 
on different notions of which information is more reliable (or 
`epistemically entrenched') than other.  In other words, when agents 
suggest a contraction for the shared theory they suggest both {\em which\/} 
information should be given up, and {\em how\/} this should be done in 
their opinion.  Therefore, the global change that is to be made to the 
theory is in general composed out of a finite number of `private' contractions
being performed concurrently.

In the special case where all agents employ the same contraction function, 
there is a clear connection with the {\em multiple contractions\/} proposed
by Fuhrmann and Hansson~\cite{fuhr:surv94}, and with forms of {\em iterated 
belief change\/} that have recently been described by Lehmann and others
(see~\cite{lehm:beli95}).

Ideas related to concurrent contraction also appear in
non-epistemic settings. For example,
co-authoring and joint research are processes in which concurrent 
contractions occur frequently.  They seem especially appropriate when bugs 
or inconsistencies are discovered in cases where agents have sole 
responsibilities for certain parts of the work, and each author can perform 
contractions on the parts for which she holds responsibility.  And of 
course, in concurrent databases concurrent transactions occur all the time.  
It is difficult, however, to find pure cases of concurrent contractions 
that are substantially different from the above ones.


\section{Laws and models for single agent contractions}
\label{section:preliminaries}

In this section we describe the laws governing the contraction
operations of individual agents taking part in a concurrent contraction;
as explained above, we assume that each agent comes equipped with her
own contraction function.  We start with some technical preliminaries.

Our background language is simply propositional logic, equipped with a
consequence operator $\Cn$ that satisfies all the usual properties.
A {\em theory\/} is a set of formulas $T$ that is closed under $\Cn$;
a {\em belief base\/} $K$ is a set of formulas that needs not be
a theory. In the AGM tradition there are two ways of reasoning about 
contraction functions, a {\em syntacic\/} way which specifies postulates that
reasonable contraction functions should satisfy, and a {\em semantic\/}
way that defines contractions functions obeying those laws.  Here's a list 
of the standard AGM postulates for contraction.

\begin{description}
\renewcommand{\itemsep}{-2pt}
\item[{\rm $T-\phi$ is a theory (logically closed) whenever $T$ is}]
  \ \hfill (Closure)
\item[{\rm $T-\phi\subseteq T$}]
  \ \hfill (Inclusion)
\item[{\rm If $\phi\notin T$, then $T-\phi=T$}]
  \ \hfill (Vacuity)
\item[{\rm If $\not\vdash\phi$, then $\phi\notin T-\phi$}]
  \ \hfill (Success)
\item[{\rm If $\phi\in T$, then $T\subseteq \Cn((T-\phi)\cup\phi)$}]
  \ \hfill (Recovery)
\item[{\rm If $\vdash \phi\leftrightarrow\psi$ then $T-\phi=T-\psi$}]
  \ \hfill (Extensionality)
\end{description}
We refer the reader to \cite{gard:know88,gard:beli92} for 
a discussion.  As Hansson~\cite{hans:reve93} points out, the above laws 
constrain how contraction functions $-$ should operate on a single,
fixed theory $T$. But when $n$ agents each come up with a formula $\phi_i$ 
to be contracted from a theory $T$, they should not
only provide the system with a contraction function $-_i$,
but, since the actual implementation of $T \sim \vec{\phi}$ may
deal with several `intermediate' results $T'$ from wich still some of the
$\phi_i$'s have to be contracted, their contraction functions
should indicate how to contract $\phi_i$ from arbitrary theories.

Hansson~\cite{hans:reve93} gives a formal account of contraction 
functions able to deal with aribitrary theories.  His approach is formulated 
in terms of belief bases $K$ rather than theories $T$, and he moreover allows 
for contractions with {\em sets\/} of formulas rather than single formulas.  
We reformulate Hansson's original postulates for the `base/set' case for 
the `theory/formula' case.

\begin{definition} {\bf (Postulates for single agent contraction)}
\label{def:post}
We propose the following postulates for a single agent contraction function
$-$ that is defined for any theory $T$ and formula $\phi$:
\begin{description}
\renewcommand{\itemsep}{-2pt}
\item[{\rm $T-\phi$ is a theory (logically closed) whenever $T$ is}]
  \ \hfill (Closure)
\item[{\rm $T-\phi\subseteq T$}]
  \ \hfill (Inclusion)
\item[{\rm If $\psi\in T\setminus (T-\phi)$}] then there exists
  $T'$ with $T-\phi\subseteq T'\subseteq T$, $T'\not\vdash\phi$,
  but $T',\psi\vdash \phi$
  \ \hfill (Relevance)
\item[{\rm If $T' \vdash \phi\leftrightarrow\psi$ for all subtheories
$T' \subseteq T$, then $T-\phi=T-\psi$}]
  \ \hfill (Uniformity)
\item[{\rm If $\not\vdash\phi$, then $\phi\notin T-\phi$}]
  \ \hfill (Success)
\end{description}
\end{definition}
Relevance ensures that if a formula $\psi$ is excluded 
from $T$ when $\phi$ is rejected, then $\psi$ plays a role in the fact that 
$T$ implies $\phi$.  Whereas Success ensures that formulas that should be 
given up are in fact given up, Relevance blocks the deletion of formulas 
that need not be deleted.  Uniformity ensures that the result of 
contracting $T$ with $\phi$ depends only on the subsets of $T$ that imply 
$\phi$; if all subsets derive a given formula $\phi$ iff they derive 
$\psi$, then contracting with either $\phi$ or $\psi$ produces the same 
result.  Observe that Vacuity is derivable from Inclusion and Relevance.

% agents want to refrain from actions.  The next proposition shows how we can 
% mimick this situation.
% 
% \begin{proposition}
% If a contraction function $-$ satisfies the postulates of 
% Definition~\ref{def:post}, then, for any theory $T$ and tautology $\top$, 
% we have $T - \top = T$.
% \end{proposition}
% 
The best known model of a contraction function in the AGM theory
is {\em partial meet contraction\/}.
It is defined as follows. Let $T\perp \phi$ denote the set of maximal
subsets of $T$ that fail to imply $\phi$. A {\em one-place selection
function\/} for $T$ is a function $s$ such that for all formulas $\phi$, 
if $T\perp \phi$ is non-empty, then $s(T\perp\phi)$ is a non-empty subset 
of $T\perp\phi$. When $T\perp\phi$ is empty, $s(T\perp\phi)=\{T\}$. Then,
an operation $-$ on a theory $T$ is a partial meet contraction if
$T-\phi$ is the intersection of the selected maximal subsets of $T$
that fail to imply $\phi$: 
$T-\phi=\bigcap s(T\perp\phi)$.

One-place selection functions are specific for a particular theory;
if $s$ is a one-place selection function for $T$, and $T\neq
T'$, then $s$ is not a one-place selection function for $T'$ (see Hansson
\cite{hans:reve93}).  Selection functions that work for arbitrary theories
are obtained by extending them with an additional argument; we 
assume that each agent $i$ is equipped with a two-placed
selection function $s$, where, for each theory $T$ and set of theories $(S
\perp \psi)$, we have $s(T, (S \perp \psi))$ $\subseteq (S \perp \psi)$.

The following result links up the postulates for $-$ with two-placed 
contraction functions.

\begin{theorem}
\label{thm:char}
A single agent contraction function $-$ satisfies the postulates of 
Definition~\ref{def:post} iff there exists a two-placed selection
function $s$ with $T - \phi = \bigcap s(T, (T\perp \phi))$,
for any theory $T$ and formula $\phi$.
\end{theorem}
A proof is omitted due to space limitations.
We call a selection function {\em unified\/} if 
if $(S \perp \psi) = (U \perp \chi)$ implies that 
$\bigcap s(T, (S \perp \psi)) = \bigcap s(T', (U \perp \chi))$.
That is, the common parts of the selections should agree, whenever possible.
Theorem~\ref{thm:char} can be strengthened to:

\begin{theorem}
\label{thm:unif}
A single agent contraction function $-$ satisfies the postulates of 
Definition~\ref{def:post} iff there exists a two-placed 
{\em unified} selection function $s$ with
$T - \phi = \bigcap s(T, (T\perp \phi))$,
for any theory $T$ and formula~$\phi$.
\end{theorem}
Again, the proof is omitted because of lack of space.
In the sequel, we will assume that selection functions are unified, and
we will often suppress their first argument.



\section{From sequential to interleaved contractions}
\label{section:sequential-to-interleaved}
In many models of situations in which multiple agents need to access shared 
resources, one finds a reduction to a sequential, non-deterministic scheme.  
Our model of concurrent contractions will be based on the same idea. 
In principle the actions of multiple agents performing a 
their individual contractions on a single theory may 
overlap in arbitrary ways.  But what does 
it mean for an agent $i$ to start a contraction {\em while another agent 
$j$ is still performing her contraction\/}? To what should $i$ apply her 
selection function? What should she act on, if not on the outcome of $j$'s 
actions? Our answer is that to perform a concurrent contraction one should 
execute the individual single agent contractions one at a time.  
Thus, a single agent contraction should be viewed as an atomic transition
during which the other agents are inactive. Hence, rather than 
input/output pairs of theories, {\em sequences\/} of atomic single agent
actions should be considered, and 
we should describe properties of concurrent contractions
that hold for some or all such sequences.

The situation is reminiscent of the concurrent execution of 
independent programs on a single processor, and in particular, of the 
{\em interleaving\/} model of such computations (see e.g.\ \cite{bena:prin90}).
By taking an interleaved approach to multi-agent contractions, it turns
out that new ways of thinking about theory change are called for.
For a start, as we turn to sequences of single agent contractions, we
have to give up the idea of concurrent contractions
as functions,  for, in general, even singleton contractions
are not commutative, that is: the identity
$(T-\phi_1)-\phi_2=(T-\phi_2)-\phi_1$
is not valid (see \cite{hans:reve93} for a counterexample).  
We also have to abandon the idea that contractions
can be specified in terms of preconditions and postconditions.
Instead, we need to be able to talk about intermediate stages of 
a concurrent contraction, as these clearly have internal structure
in the interleaved approach.
Below we present postulates and a model for interleaved contractions
that allow us to describe and classify properties of
sequences of single agent contractions.



\section{Laws for interleaved contractions}
\label{sec:laws}
In this section we present a list of postulates that any reasonable
operation of interleaved contraction should satisfy. We first need
some notation.  Let $\vph$ and $\vps$ be vectors of formulas of length $n$. 
We write $\vph \equiv \vps$ for `for all $i \leq n$: $\vdash \phi_i 
\leftrightarrow \psi_i$,'
and for a set of formulas $Z$, $\vph \equiv_Z \vps$ means that for
all $i \leq n$: $Z \vdash \phi_i \leftrightarrow \psi_i$.
Special vectors are $\vec{\top}$ and $\vec{\bot}$, consisting only of
the formulas $\top$ and $\bot$, respectively;
$\vph\,[\chi/\phi_i]$ denotes the result of replacing the $i$-th
component $\phi_i$ by $\chi$. We write $T-\vec{\phi}\propto S$ for
`$S$ is a result of concurrently contracting $T$ with $\vec{\phi}$.'
Finally, a {\em concurrent contraction function\/} is a function
that produces a set of theories on input a theory $T$ and a vector 
$\vec{\phi}$,


\begin{definition} {\bf (Basic postulates for interleaved contractions)} \
\label{mdr:def-basic-postulates}
Let $T$ be a set of formulas, and let $n$ be a natural number (the number
of agents taking part). Then $\vph$ is a sequence of formulas of length
$n$, and $-_i$ denotes agent $i$'s individual contraction function. We 
assume that each $-_i$ satisfies the postulates for two-placed contraction
given in Definition~\ref{def:post}.
\begin{description}
\renewcommand{\itemsep}{-2pt}
\item[{\rm If $T$ is a theory and $\ConTphiS$, then $S$ is also a theory}]
  \ \hfill (C-closure)
\item[{\rm If $\ConTphiS$ then $S \subseteq T$}]
  \ \hfill (C-inclusion)
\item[{\rm Suppose $\ConTphiS$ and $\psi \not \in S$, $\psi \in T$.}] Then
  there are $T'$ and $i \leq n$ such \ \hfill (C-relevance)\\
  that $S \subseteq T' \subseteq T$,
  $T' \not \vdash \phi_i$, and $T', \psi \vdash \phi_i$
\item[{\rm If $\vph \equiv_{T'} \vps$ for all 
  subtheories $T' \subseteq T$ then $\ConTphiS \mbox{ iff } =
  \Con{T}{\psi}{S}$}]
  \ \hfill (C-uniformity)
\item[{\rm For all $i \leq n$, if $\not\vdash\phi_i$ and $\ConTphiS$,
  then $\phi_i\notin S$}]
  \ \hfill (C-success)
\item[{\rm If for all $j \not = i$, we have $\phi_j = \top,$}]
  then $\ConTphiS$  iff $S = T -_i \phi_i$
  \ \hfill (Solo)
\end{description}
\end{definition}

C-closure and C-inclusion are straightforward concurrent versions of 
their single agent counterparts.
Concurrent Relevance says that for every formula 
$\psi$ that is given up in a concurrent contraction from $T$, there is an 
agent that is `responsible' for this removal; according to the 
individual obedience to Relevance, this agent can determine a part of $T$ 
from which the formula he proposed for contraction has indeed been removed, 
and in the process of doing this, $\psi$ had to be given up.  
C-uniformity says that if no subtheory $T'$ of $T$ can 
distinguish any component $\phi_i$ of $\vph$ from the corresponding 
component $\psi_i$ of $\vps$, then concurrently contracting $\vph$ from $T$ 
cannot be distinguished from concurrently contracting $\vps$ from $T$.  
This uniformity postulate implies the following condition 
of C-extensionality:
\begin{description}
\item[{\rm If $\vph \equiv \vps$ then $\ConTphiS \mbox{ iff } =
\Con{T}{\psi}{S}$}]
  \ \hfill (C-extensionality)
\end{description}
It guarantees that only the {\em content\/} of the individual 's 
proposal for contraction matters, not the actual {\em form\/}.  
C-success guarantees that, as long as an agent does not 
propose to contract a tautology, her request for contraction will have been 
granted in each of the possible results.  Thus, whereas C-relevance says 
that each formula that is given up in a concurrent contraction should be 
due to one of the agents, C-success guarantees that all of the agents' 
wishes will be met as far as they are reasonable.
Finally, the Solo postulate shows that interleaved contractions really builds 
on the individual contraction strategies: when only one agent comes up with 
a non-trivial formula to be removed, it will be her strategy 
that determines the result of the concurrent contraction.

The postulates in Definition~\ref{mdr:def-basic-postulates} 
provide no means to reason about possible `intermediate' results of
interleaved contractions,
and they certainly don't impose the condition that the concurrent
contraction process can be unravelled into successive single 
agent contractions.


\begin{description} 
\label{des:composition}
\item[{$\ConTphiS \Rightarrow$}] $\left\{\begin{minipage}[c]{7cm}
    {\em either\/} $T = S$  and $\vph \equiv \vec{\top}$ \\
    {\em or\/} there exist  $S'$ and $i$ with
    $i \leq n$ and $S \subseteq S' \subseteq T$ such that
    $\phi_i \not \equiv \top$,  
    $S' = T -_i \phi_i$ and  $\Con{S'}{\psi}{S}$,
    where $\vps = \vph[\top/\phi_i]$
    \end{minipage}\right.$
    \phantom{} \hfill(Decomposition)
\item[{$\ConTphiS \Leftarrow$}] $\left\{\begin{minipage}[c]{7cm}
    {\em either\/} $T = S$ and $\vph \equiv \vec{\top}$ \\
    {\em or\/} there exist  $S'$ and $i$ with
    $i \leq n$ and $S \subseteq S' \subseteq T$ such that
    $\phi_i \not \equiv \top$,  
    $S' = T -_i \phi_i$ and  $\Con{S'}{\psi}{S}$,
    where $\vps = \vph[\top/\phi_i]$
    \end{minipage}\right.$
\phantom{hm} \hfill (Composition)
\end{description}
%
Decomposition says that concurrently contracting with $\vec{\top}$
is a void action and that a concurrent contraction with 
$\vec{\phi} \not = \vec{\top}$ can be decomposed in 
an individual contraction $-_i$ followed by another, yet simpler,
concurrent contraction. Conversely, Composition states that if one
recursively unravels a concurrent contraction
$T \sim \vec{\phi}$ into an individual
contraction $T -_i \phi_i$ followed by a concurrent contraction
of a vector $\vec{\psi}$ (obtained from $\vec{\phi}$) from 
the theory $(T -_i \phi_i)$, one ends up with a theory $S$ that will be
a result of the initial concurrent contraction. 
Notice that the Solo postulate is a consequence of Decomposition.
If we think about interleaving contractions in an algorithmic way,
we can view the Composition and Decomposition postulates as halting
criteria: to contract $\vec{\phi}$ from $T$, try to turn all components 
of $\vec{\phi}$ into the formula $\top$ by successively contracting
with $\phi_i$ after another until $\vec{\phi}$ equals $\vec{\top}$.

\begin{theorem}
\label{thm:postimpliesCpost}
Suppose that a set of individual contraction functions $-_i$ and a
concurrent contraction $\sim$ are connected via 
the Decomposition and Composition laws.
If all the $-_i$'s satisfy the postulates from
Definition \ref{def:post},
then $\sim$ satisfies all the Concurrent postulates 
from Definition~\ref{mdr:def-basic-postulates}.
\end{theorem}

Theorem~\ref{thm:postimpliesCpost} expresses a {\em transfer\/} property:
if we define a concurrent contraction $\sim$
via Composition and Decomposition using individual contractions
$-_i$, we get the rationality postulates for $\sim$
if we impose rationality postulates on all the $-_i$'s. 
Theorem \ref{thm:Cpostimpliespost} expresses a {\em projection\/} principle
going in the converse direction.

\begin{theorem}
\label{thm:Cpostimpliespost}
Suppose that a set of individual contraction functions $-_i$ and a
concurrent contraction $\sim$ are connected via
the Decomposition and Composition laws.
If  $\sim$ satisfies the Concurrent postulates
from Definition~\ref{mdr:def-basic-postulates},
then all the $-_i$'s satisfy the postulates from Definition~\ref{def:post}.
\end{theorem} 

Combining the above two theorems we see that the Composition and Decomposition
postulates propperly link individual and concurrent contractions together: 
postulates for one operation are guaranteed by imposing them on the other.
Having observed that Composition plus Decomposition guarantees an `equivalence' 
between
the $-_i$ postulates and the postulates for $\sim$, we do not know yet 
whether a
converse is also true, i.e, whether `equivalence' between the two types of
postulates implies that the concurrent contraction function can be defined
in terms of Composition and Decomposition. 



\newcommand{\state}[1]{{\sf #1}}

\section{Models for interleaved contractions}
\label{section:reasoning-about-interleaving}

Let $n>1$ be the number of agents. We assume that for each $i$,
agent $i$'s contraction function is defined using a selection function
$s_i$, as outlined in Section~\ref{section:preliminaries}.
The models we are about to define are called selection systems; they are 
based on the selection functions contributed by the individual agents.  
Roughly, a selection system is a collection of compositions of single agent 
selection functions that satisfies certain constraints.

A {\em selection system\/} $({\cal S}, {\cal T}, \state{s}_0)$, intended to 
represent interleaved contractions, is given by the following components:
\begin{itemize}
\renewcommand{\itemsep}{-2pt}
\item  ${\cal S}$, a finite set of states. Each state $\state{s}$ is
  labeled with a theory $\Th(\state{s})$. These are the theories
  that the theory of the {\em initial state\/} $\Th(\state{s}_0)$ can
  evolve into by applying sequences of single agent contractions.
  Two states may be labeled with the same theory.
	
\item  ${\cal T}$, a finite set of single agent selections. Each such 
  selection is defined as a function $
  \state{s}\mathrel{\smash{\stackrel{s_i}{\longrightarrow}}} \state{s}'$
  that maps the theory $\Th(\state{s})$ into the theory $\Th(\state{s}')$
  by contracting $\Th(\state{s})$ with $\phi$ using agent $i$'s selection
  function $s_i$ ($1\leq i\leq n$):
  $\Th(\state{s})\mapsto s_i(\Th(\state{s})\bot_i, \phi_i)=\Th(\state{s}')$.
  Here $\state{s}'$ is called a {\em successor\/}
  (or $-_i\phi$-{\em successor\/}) of $\state{s}$. For technical reasons
  we will assume that all successor steps are irreflexive:
  if $\state{s}\mathrel{\smash{\stackrel{-_i\phi}{\longrightarrow}}}\state{s}'$
  then $\state{s}\neq \state{s}'$.
\end{itemize}
A state $\state{s}\in {\cal S}$ is {\em terminal\/} if it has no 
successors.  A {\em choice sequence\/} of a selection system $({\cal 
S},{\cal T}, \state{s}_0)$ is a sequence $\sigma\,:\, \state{s}_1,\ldots, 
\state{s}_m$ satisfying the following requirements. First,
the {\em Initiation\/} requirement says  the state $\state{s}_1$ is the 
initial state of the selection system, that is $\state{s}_1=\state{s}_0$.
Second, the {\em Consecution\/} requirement says that for each pair of 
consecutive states $\state{s}_j$, $\state{s}_{j+1}\in \sigma$ there is a 
selection $s_i$ such that 
$\state{s}_j\mathrel{\smash{\stackrel{s_i}{\longrightarrow}}}\state{s}_{j+1}$.
(Observe that two states may be connected by multiple transitions.)
Finally, the {\em Termination\/} requirement says that the final state 
$\state{s}_m$ is a terminal state.

A {\em prefix\/} is a sequence $\state{s}_1$, \ldots, $\state{s}_k$ satisfying
the requirements of initiation and consecution, but not necessarily of 
termination. The {\em length\/} of a prefix is its number of states.

Let $T$ be a theory, $n$ the number of agents, and $\phi_1$, \ldots, 
$\phi_n$ a sequence of formulas.  Our next aim is to determine what it 
means for a selection system ${\bf T}=({\cal S}, {\cal T}, 
\state{s}_0)$ to model or represent the interleaved contraction 
$T\sim(\phi_1$, \ldots, $\phi_n)$. We will impose the 
three constraints.
First, the {\em Start\/} constraint says that 
$\Th(\state{s}_0)$, the theory of the initial state, should equal $T$.
Second, the {\em Tightness\/} constraint requires that
for every choice sequence $\sigma$ in {\bf T} and every $i\leq n$ there
exists at most one pair of consecutive states $\state{s}_j$, 
$\state{s}_{j+1}$ in $\sigma$ such that
$\state{s}_j\mathrel{\smash{\stackrel{s_i}{\longrightarrow}}}\state{s}_{j+1}$.
The tightness property says that no attempt is made to carry out a
single agent contraction in $T\sim\vec{\phi}$ twice. Third, the
{\em Fairness\/} constraint says that
for every choice sequence $\sigma$ in {\bf T} and every $i\leq n$ there is a
consecutive pair $\state{s}_j$, $\state{s}_{j+1}$ in $\sigma$ such that
$\state{s}_j\mathrel{\smash{\stackrel{s_i}{\longrightarrow}}}\state{s}_{j+1}$.
holds. The fairness property expresses that
every single agent contraction in $T\sim\vec{\phi}$ will be carried out.

Let ${\bf S}=({\cal S}, {\cal T}, \state{s}_0)$ be a selection system.  
{\bf S} is called a {\em model\/} for $T\sim\vec{\phi}$ if it satisfies the 
starting, tightness and fairness conditions for $T\sim\vec{\phi}$.  
% A model 
% {\bf S} for $T\sim\vec{\phi}$ is called {\em full\/} if every possible 
% sequence of single agent contractions from $T\sim\vec{\phi}$ occurs as a 
% prefix.  
Given a model ${\bf S}=({\cal S}, {\cal T}, \state{s}_0)$ for 
$T\sim\vec{\phi}$, a {\em proper choice sequence\/} of 
$T\sim\vec{\phi}$ is simply a choice sequence in {\bf S}.
What this definition boils down to is that we view interleaved
contractions as generators of proper choice sequences.  
% Thus, to compare 
% interleaved contractions we need to compare the proper choice sequences they 
% generate.  This should be contrasted with the way standard AGM contractions 
% are compared: as sets of input/output pairs.

To be able to express the connection between concurrent contraction 
functions and selection systems, we say that a contraction function $\sim$
{\em generates a full selection system for $T$ and $\phi$\/} if there
are single agent selection functions $s_1$, \ldots, $s_n$ such
that $-_j$ is defined in terms of $s_j$ ($1\leq j\leq n$), and for
all $S$ such that $T\sim\vec{\phi}\propto S$ there exists a 
sequence $S_0$, \ldots, $S_n$ such that $S_0=T$, $S_{i+1}=s_{i+1}(S_i,
(S_i\perp \phi_{\pi(i)}))$, where $\pi$ is a permutation $\{1,\ldots, n\}$, 
and $S_n=S$.


\begin{theorem}
Let $\sim$ be a concurrent contraction function, and suppose that
$\sim$ and $-_i$ are related via the Composition and Decomposition
laws from Section~6. Then $\sim$ satisfies the C-postulates from
Definition~4 iff, for every theory $T$ and vector of formulas $\vec{\phi}$,
$\sim$ generates a full selection system for $T$ and $\phi$.
\end{theorem}




\section{Concluding remarks}
We have shown that concurrent contractions are well-behaved in that
they satisfy a set of fairly transparent rationality postulates ---
on the assumption that all the underlying single agents  contract
in a rational way, and that concurrency is modelled in an 
interleaving manner.

In our ongoing work we consider alternative models for interleaved
contractions called {\em entrenchment systems\/} that are based
on compositions of single agent entrechment relations. One can prove
a representation result to the effect that every selection system
can be represented as an entrenchment system, and vice versa, that
gives rise to the same concurrent contraction function.



\paragraph*{Acknowledgments.}
Wiebe van der Hoek was partially support\-ed by ES\-PRIT III BRWG project No.\ 
8319 `ModelAge'.

\begin{thebibliography}{10}
\renewcommand{\itemsep}{-2pt}

\bibitem{alch:logi85}
C.E. Alchourr\'on, P.~G\"ardenfors, and D.~Makinson.
\newblock On the logic of theory change: partial meet contraction and revision
  functions.
\newblock {\em Journal of Symbolic Logic}, 50:510--530, 1985.

\bibitem{bena:prin90}
M.~Ben-Ari.
\newblock {\em Principles of Concurrent and Distributed Programming}.
\newblock Prentice Hall, 1990.

\bibitem{fuhr:surv94}
A.~Fuhrmann and S.-O. Hansson.
\newblock A survey of multiple contractions.
\newblock {\em Journal of Logic, Language and Information}, 3:39--75, 1994.

\bibitem{gard:know88}
P.~G\"ardenfors.
\newblock {\em Knowledge in Flux}.
\newblock The MIT Press, 1988.

\bibitem{gard:beli92}
P.~G\"{a}rdenfors and H.~Rott.
\newblock Belief revision.
\newblock In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, eds, {\em
  Handbook of Logic in AI and Logic Programming, Vol IV}, Oxford
  University Press, 1992.

\bibitem{hans:reve93}
S.O. Hansson.
\newblock Reversing the {L}evi identity.
\newblock {\em Journal of Philosophical Logic}, 22:637--669, 1993.

\bibitem{hoek:conc95}
W.~van~der Hoek and M.~de Rijke.
\newblock Concurrent theory change.
\newblock CWI, Amsterdam, 1995.

\bibitem{lehm:beli95}
D.~Lehmann.
\newblock Belief revision, revised.
\newblock In {\em Proceedings IJCAI 95}, 1995.
 
\bibitem{lind:epis91}
S.~Lindstr{\"{o}}m and W.~Rabinowicz.
\newblock Epistemic entrenchment with incomparabilities and relational belief
  revision.
\newblock In A.~Fuhrmann and M.~Morreau, eds, {\em The Logic of Theory
  Change}, Springer, 1991.

\bibitem{maki:howt85}
D.~Makinson.
\newblock How to give it up: A survey of some formal aspects of the logic of
  theory change.
\newblock {\em Synthese}, 62:347--363, 1985.

\end{thebibliography}


\end{document}


