\documentstyle[nlpbbl,lingmacros]{jnlp_e_b5}

\newtheorem{DEF}{}
\newtheorem{PROP}{}
\newtheorem{LEM}[]{}
\newtheorem{Cor}[]{}
\newtheorem{Th}[]{}
\newtheorem{EX}{}
\newcommand{\force}{}
\newcommand{\forces}{}
\newcommand{\Iff}{}
\newcommand{\To}{}
\newcommand{\lden}{}
\newcommand{\rden}{}
\newcommand{\K}{}
\newenvironment{BOX}[1]{}{}
\newenvironment{BOX2}[1]{}{}
\newcounter{sen}
\newcounter{sen2}
\setcounter{sen}{1}
\newenvironment{SEN}{}{}
\newenvironment{SEN2}{}{}

\setcounter{page}{93}
\setcounter{巻数}{6}
\setcounter{号数}{4}
\setcounter{年}{1999}
\setcounter{月}{7}
\受付{October}{9}{1997}
\再受付{July}{9}{1998}
\採録{March}{4}{1999}

\setcounter{secnumdepth}{2}

\title{}
\author{}
\jkeywords{}

\etitle{Formal Semantics of Dialogues\\Based on Belief Sharing\\and Observational Equivalence of Dialogues}

\eauthor{Norihiro Ogata\affiref{UMIST}} 

\headauthor{Ogata}
\headtitle{Formal Semantics of Dialogues}

\affilabel{UMIST}	
	  {Osaka University, Dept. of Language and Culture}
	  {Osaka University, Dept. of Language and Culture}

\eabstract{
This paper shows that there is a direct connection between dialogues and belief sharing.
This connection is shown by proving a correspondence between {\it observational equivalence} between dialogues and {\it epistemic bisimulation} between {\it Hyper-Discourse Representation Structures} (Hyper-DRS) constructed from dialogues.
An observational equivalence between dialogues is defined by a kind of similarity of resulting shared beliefs of the dialogues.
The theory of Hyper-DRSs is defined by extending Kamp's {\it Discourse Representation Theory} \cite{KR93}, a formal semantics of discourse or a dynamic semantics, which is exploiting the theory of {\it hypersets} \cite{Acz87,BM96} in order to solve the problem of the definition, formation and revision of circular objects like shared beliefs.
}


\ekeywords{formal semantics, dialogue, belief sharing, hyperset, Hyper-Discourse Representation Structure, observational equivalence}

\begin{document}
\maketitle

\section{Introduction}  
In this paper, we will propose a formal semantics of dialogues, {\it Hyper-Discourse Representation Theory} (henceforth {\it Hyper-DRT}) based on a view of dialogues as {\it processes of formation and revision of shared belief} between the conversants, which can treat an equivalence relation between dialogues, called the {\it observational equivalence}.
In Hyper-DRT, we will define {\it Hyper-Discourse Representation Structures} (henceforth {\it Hyper-DRS}), an extension of {\it Discourse Representation Structures} \cite{Kam81,KR93}, 
by exploiting the theory of {\it hypersets} or {\it non-wellfounded sets} \cite{Acz87,BM96}.
This allows us to define infinite objects by finite specifications, 
and thus to treat shared beliefs by finite representations.
This finite representability makes it possible to form or revise infinite objects like shared beliefs by finite operations.
As a result, we will prove the following three properties of our theory:
\begin{enumerate}
\item[\hspace*{1cm}1)] If a dialogue $\delta$ is well-formed, then its Hyper-DRS verifies that its conversants $A$ and $B$ share the belief $\varphi$ expressed by the moves in the dialogue ({\it Dialogues as shared belief formations and revisions})
\item[\hspace*{1cm}2)] Any part of a dialogue may have information dependent on its context, and its Hyper-DRS verifies this type of information as well. ({\it Dialogues as compositional shared belief revisions})
\item[\hspace*{1cm}3)] Two dialogues can be considered as equivalent processes from the point of view of the shared beliefs which have been formed in each of the dialogue, and their Hyper-DRSs reflect the equivalence. ({\it Dialogues as processes whose identity is definable from the resulting shared beliefs})
\end{enumerate}
The first property means that Hyper-DRT treats dialogues as belief sharing processes, and this is written as $\delta\models S_{A,B}\varphi$ (See definition \ref{Mean}).
The second property means that Hyper-DRT treats dialogues compositionally.
The equivalence mentioned in the third property, we will call {\it observational equivalence}.
Hyper-DRT captures observational equivalence of dialogues by {\it epistemic bisimulation} between their Hyper-DRSs.
That is, the information represented by Hyper-DRSs captures at least the information defined by the observational equivalence of dialogues.
\par
Section \ref{view} provides, along with the above three points, a discussion of the basic questions: {\it what is a shared belief or belief sharing?}, and  {\it why can dialogues be considered as belief sharing?}
In section \ref{hdrs}, we introduce Hyper-DRT, which consists of the definition of Hyper-DRSs, the definition of the semantics of Hyper-DRSs based on hyperset theory, and the construction algorithm and construction rules of Hyper-DRSs.
Section \ref{hdrs} also contains a discussion of the main properties of Hyper-DRSs which reflect (1)-(3) above.
In section \ref{comp}, we classify formal theories of the semantics of dialogues and compare Hyper-DRT with the other proposals.

\section{Dialogues as Belief Sharings}\label{view}
While both dialogues and other types of discourse can be considered as acts involving the agents' information state transitions, 
the main distinctive property of dialogue is that their resulting informational states of the conversants of a dialogue can be divided into a state {\it shared} between the participants and an {\it unshared} state (i.e., {\it publicized information} and {\it private information}).
Only the former is available for observation based on sequences of linguistic forms used in dialogues (called {\it moves}).
Private information can be inferred from an observation of a conversant's face, attitude, quality of voice, physical state (blood pressure, pulse rate, etc.) and so on, as in lie detector tests, or from the context and the situation.
Therefore, the semantics of dialogues (or {\it sequences of linguistic forms used by a group of agents}) should not be directly associated with the real mental states of conversants (i.e., private information), 
but with publicized information, shared between the conversants as the result of the dialogues.
\par
If the semantics of dialogues in the above sense is related to the information which becomes public in the process of the dialogue, 
the notion of `public information' should be formalized in the semantics.
Public information or shared belief is formalized as an infinite or circular object such that information $p$ is public in the group $C$ if and only if every member of $C$ believes that $p$ and that $p$ is public in $C$, as \cite{Lew69,CM81,Bar89} argued.
Some scholars have already pointed out the connection between natural language use and shared beliefs or mutual beliefs (cf. Definite Reference \cite{CM81}, the {\it Dirty Children Puzzle} or {\it Conway's paradox} \cite{Bar89,FHMV95}), but they mainly argue that shared belief is a part of presuppositions of dialogues.
However, the direct connection between each move of a dialogue and belief sharing has not yet been discussed.
Our main claim in this paper is that the viewpoint of ``dialogues as belief sharing'' provides for a successful semantics of dialogues and that this viewpoint entails that information possessed by an agent becomes public in the group of conversants through the processes of dialogues.\<\footnote{
We will continue to use the term ``belief'' in the sense of information possessed by some agent, which has not to be believed by him/her.}
\par
The notion of dialogues as belief sharing can be factored into three notions: (i) dialogues can be analyzed as shared belief formations/revisions, (ii) dialogues are compositional, and (iii) dialogues are processes whose identity is definable from the resulting shared beliefs.
In section \ref{SBF}, \ref{comp2}, and \ref{wellfound}, we will discuss these points in detail.
\subsection{Dialogues as Shared Belief Formations/Revisions}\label{SBF}
If the notion of ``dialogues as belief sharing'' is useful,
we must explain the fact that a dialogue itself presupposes a shared belief about its language usage, since every instance of language use presupposes shared beliefs about the language and its use.
We can reduce the shared belief about language usage to the problem of language acquisition or of an agent's social adaptation.
However, can dialogues be considered as shared belief formations from square one, ignoring common knowledge about language use?
Our answer is yes.
For example, the information {\it who is the other for each conversant}\<\footnote{
The {\it other} means the interlocutor.
}
 and {\it who/what is the speaker}, namely, information about {\it
mutual identification} in terms of \cite{Ste94}, is deliberately
shared at the opening or turn-exchange phase of a dialogue, as in
(\ref{open}).
\noindent
\eenumsentence{\label{open}
\item Hello?$_A$; Mr. Hurd. It's Professor Clark's secretary, from Paramilitary College.$_B$; oh yes?$_A$ \cite{Ste94}
\footnote{The subscripts, $A$, $B$, $\ldots$, $Max$, $Claire$,$\ldots$, annotated to the moves indicate the utterers of the moves, and `;' indicates the turn-exchange in the sequence of moves.}
\item Hello. Could I speak to Mr. Parker please?$_B$; Who's calling?$_A$; It's Doctor Edgton.$_B$; Um.$_A$ \cite{Ste94}
\item Hello?$_C$; Juddy?$_B$; Yeah.$_C$; Jack Green.$_B$; Hi, Jack.$_C$ \cite{Sacks}
\item Hello, Ronald.$_A$; Yeah.$_B$; My name is Smith.$_A$; Uh-huh.$_B$ \cite{Sacks}
}
The information about mutual identification is among the most basic of shared beliefs.
For example, a part of a dialogue using {\it indexicals} (e.g., I, you, here) may fail because of the lack of sharing of mutual identification, as in the following example.
\enumsentence{\label{Come}
Hey, you.$_A$; Me?$_B$; No.$_A$\label{come3}
}
In (\ref{come3}), first $B$ presupposes the shared belief (\ref{a}):

\enumsentence{\label{a}
$A$ and $B$ share the belief that $A$ believes that the other for $A$ is $B$ and $B$ believes that the other for $B$ is $A$
}
Then, $B$ changes his/her presupposition to the shared belief (\ref{b}):
\enumsentence{\label{b}
$A$ and $B$ share the belief that (\ref{a}) was wrong.
Now (\ref{a}) is right.
}
Therefore, (\ref{Come}) involves a shared belief revision.
\par
Another type of example of shared belief revision by dialogue (cited in \cite{Ste94}) is {\it check moves}, which indicates that the utterer is eager to have the previous words repeated, like {\it What was that?} in (\ref{right3}).
\enumsentence{\label{right3}
The two phonemic cluster. No.$_A$; {\it What, what was that again?}$_B$; The two phonemic cluster. No.$_A$ \cite{Ste94}
}
$B$'s check move deletes $A$'s content from $A$ and $B$'s shared beliefs, but $A$ and $B$ share the belief that $A$ said something.
\par
Therefore, in dialogues, even the shared beliefs that constitute the ground information of the dialogue itself, such as the basis of indexicals or the said content, can change.
\par
We have seen that information about mutual identification which is among the most basic of shared beliefs and the shared beliefs that constitute the ground information of the dialogue are formed or revised in dialogue.
This means that dialogues involve shared belief formations from square one, as long as formation and revision of common knowledge about language use is ignored as a problem irrelevant to dialogue processes.
\subsection{Dialogues as Compositional Shared Belief Revisions}\label{comp2}
In this subsection, we discuss the compositionality of semantics of dialogues and its related problems, in particular, the following three points.
\clearpage
\paragraph{The Technical Problem of Updates of Shared Beliefs}
If we adopt the viewpoint of a dialogue process as a belief sharing,
the process $\pi$ of talking about a proposition $\psi$ can be modeled with the update function $F_{\pi}$ of the presupposed shared belief $S_{A,B}\varphi$
\<\footnote{$S_{A,B}\varphi$ means that $A$ and $B$ share the belief $\varphi$.}
 as follows:
$$F_{\pi}(S_{A,B}\varphi)=S_{A,B}(\varphi\wedge\psi).$$
However, $F_{\pi}$ is a composition of the update function $F_{m_i}$ for each move $m_i$ ($i<n$).
Namely,
$$F_{\pi}=F_{m_0}\circ F_{m_1}\circ \ldots \circ F_{m_{n-1}}.$$
This means that the definition of $F_{m_i}$ is problematic.
For example, while dialogue (\ref{dia1}a) can be modeled as the function $F_{(\ref{dia1}a)}$,
\eenumsentence{\label{dia1}
\item Do you have the three of spades?$_A$; Yes.$_B$
\item $F_{(\ref{dia1}a)}(S_{A,B}\varphi)=F_{A:do\_you\_have\_3\spadesuit?}\circ F_{B:yes}(S_{A,B}\varphi)$\\ $=S_{A,B}(\varphi\wedge have(B,3\spadesuit))$
}
we still need to define $F_{A:do\_you\_have\_3\spadesuit?}$ and $F_{B:yes}$.
We can easily define any total dialogue $\pi$ as the update function $F_{\pi}$ of shared belief, but the update function $F_{m}$ of each move $m$ is not a direct update function of shared beliefs.
This is a technical problem.
If we associate processes of dialogues with shared beliefs formed in the processes, we should define the meaning of each move in terms of belief sharing.
We will define such a meaning of each move as an update function of a  Hyper-DRS which amounts to a partial model of shared beliefs.
\paragraph{The Semantic Dependency of Moves on their Adjacent Moves}\label{adj}
The information content of a move is not completely determined by the move itself.
It depends on the adjacent moves.
(\ref{Huh2}) shows that {\it Huh?} must have a previous move.
\eenumsentence{\label{Huh2}
\item I have the three of spades.$_A$;Huh?$_B$
\item I have the three of spades.$_A$;Huh?$_B$;Huh?$_A$
\item *Huh?$_B$
\item *Huh?$_B$;Huh?$_A$
}
Furthermore, (\ref{Huh3}) shows that {\it Huh?} deletes the content of the previous move, since (\ref{Huh3}a) have the same informational content as (\ref{Huh3}c).
The deletion is not total, but partial, since using {\it Huh?} creates the expectation that the next utterance will have the same content as the one that provoked the {\it Huh?}.
\eenumsentence{\label{Huh3}
\item I have the three of spades.$_A$;Huh?$_B$;I have the three of spades.$_A$;
\item *I have the three of spades.$_A$;Huh?$_B$;I have the four of spades.$_A$;
\item I have the three of spades.$_A$
}
Although these examples only describe properties of {\it Huh?}, they do show the possibility of a semantic dependency of moves on their adjacent moves.
Therefore, the semantics of moves or dialogues must treat their dependence on the context (i.e., the state of the shared belief).

\paragraph{Well-definedness of Shared Beliefs and (Non-)Well-foundedness of Dialogues}\label{wellfound}
The notion of shared beliefs can be defined formally in many ways as in \cite{Bar89} and \cite{FHMV95}, but there is still the question of the relevance of such a formal definition of shared beliefs to the semantics of dialogues.
One of the properties of dialogues, {\it the finiteness of acknowledgements}, requires the well-definedness of the notion of shared beliefs.
Normal dialogues finish in finite moves.
In particular, as in (\ref{d3}), a reply is achieved by one or a few moves.
\eenumsentence{
\item I have the three of spades.$_A$; Uh-huh.$_B$\label{d3}
\item $\ast$I have the three of spades.$_A$; Uh-huh.$_B$; Uh-huh.$_A$; Uh-huh.$_B$,...\label{d4}
\item I have the three of spades.$_A$; Huh?$_B$; Huh?$_A$; Huh?$_B$,...\label{d5}
}
However, if an acknowledgement move can only acknowledge the previous move, and every move must be acknowledged, then every acknowledgement also needs its own acknowledgement.
This would lead to dialogues like (\ref{d4}) that can't terminate in finite many moves.
Even if an acknowledgement carries the information that the speaker shares the belief that was just expressed, that belief also needs to be shared and this leads right back to infinite dialogues.
\par
If shared beliefs are formalized as in \cite{Bar89} and \cite{FHMV95}, shared beliefs satisfy, at least, the {\it Fixed Point Axiom} (\ref{FPA1}) and the {\it Induction Rule} (\ref{FPA2}).
\eenumsentence{\label{FPA}
\item $S_{A,B}\varphi\equiv Bel(A,S_{A,B}\varphi\wedge \varphi)\wedge Bel(B,S_{A,B}\varphi\wedge \varphi)$,\label{FPA1}
\item $\varphi\to Bel(A,\varphi\wedge \psi)\wedge Bel(B,\varphi\wedge\psi)$ implies $\varphi\to S_{A,B}\psi$.\label{FPA2}
}
Under the assumption that these axioms hold, if $A$ and $B$ share belief $p$ at a move, then $A$ and $B$ share $A$ and $B$'s shared belief of $p$.
This implies that it is not necessary that either agent acknowledges an  acknowledgement.
Therefore, the problem of the infinity of acknowledgements is avoided, and the necessity of the well-definedness of shared beliefs is shown.
The Semantics of dialogues must be able to distinguish the relevant public information from the other information, and to define it as a well-defined shared belief in the sense that it satisfies the axioms of shared beliefs.
\clearpage
\subsection{Dialogues as Processes whose Identity is definable from the Resulting Shared Beliefs}
The relation between dialogues and shared beliefs allows for a notion of equivalence of dialogues as processes based on identification of the shared beliefs that they give rise to.
For example, in dialogues
 `Do you have the three of spades?$_A$;Yes.$_B$' and `I have the three of spades.$_B$; Uh-huh.$_A$', the same information `B believes that B has the three of spades' becomes public between agents A and B, even if B tells a lie and A knows that.
We say that these two dialogues are {\it observationally equivalent}.
This equivalence does not concern the private information which each of the conversants really has, but the public or observable (in the above sense) information between them.\<\footnote{
However, this does not mean an exclusion of the attribution of the informational content of an utterance to its utterer, say $a$.
Undoubtedly, an utterance of content $p$ has such information, say $Bel(a,p)$.
This informational content is not intended to mean that $a$ believes $p$,
but intended to mean that informational content $p$ can be attributed to $a$.
That is, whatever $a$ believes, $a$'s utterance $p$ has information $Bel(a,p)$.}
In this section, we will consider three classes of observationally equivalent dialogues\<\footnote{
Other important classes of subdialogues include: subdialogues on turn-taking and subdialogues on closing.
}: 
\paragraph{Openings of Dialogues as Sharing `Other'} 
\eenumsentence{\label{hello}
\item Hi, Claire.$_A$; Hi, Max$_B$.
\item Hello?$_A$; Max?$_B$; Yeah.$_A$; (it's) Claire.$_B$; Hi, Claire.$_A$
\item Hello, Claire.$_A$; Yeah.$_B$; My name is Max.$_A$; Uh-huh.$_B$
}
Dialogues (\ref{hello}a-c) are observationally equivalent, since as the result of each dialogue $A$ and $B$ have shared the belief of their mutual identification.
We define Max and Clare's mutual identification as the shared belief whose content is expressed by the following formulas:
\begin{itemize}
\item[(i)] $Bel(A,Other(x)),Bel(B,Other(y)),$
\item[(ii)] $Max(y),Claire(x),$
\item[(iii)] $Anch(x,B),Anch(y,B),$
\end{itemize}
where $Other(x)$ means that `$x$ is the other who someone talks with,'
$Name(x)$ means that `$x$ is named as $Name$,'
and $Anch(x,B)$ means that `$x$ is anchored to $B$.'
Formulas (i-iii) express that they have recognized each other.
These propositions play the role of the basis (i.e., the common ground) of what the indexicals `me (I)' and `you' mean.
Therefore, the opening phases of dialogues form the basic shared belief.
Conversely, this kind of shared belief is normally established in the opening phase of a dialogue.
\paragraph{Subdialogues on formed shared beliefs} 
According to \cite{Ste94}, {\it follow-ups moves} ratify the response moves just previously uttered by the other, and, in particular, in (\ref{right}) {\it Right} serves as a confirmation of a {\it mutual agreement}.
\enumsentence{\label{right}
Shall we keep those brackets as they are?$_A$; Yes.$_B$; {\it Right}.$_A$
}
{\it Re-opener moves} can also be used to {\it double-check an agreement}, as {\it Right?} in (\ref{right2}).
\enumsentence{\label{right2}
A: Would twelve o'clock be okay?; B: Lovely.; A: {\it Right?}; B: Yes.
}
In particular, dialogues (\ref{right}-\ref{right2}) contain subdialogues on the shared beliefs which are formed just at the previous moves.
A dialogue that contains such a subdialogue \mbox{is observationally} equivalent to a dialogue without such a subdialogue.
For example, dialogues (\ref{rightyes}a-b) are observationally equivalent in the sense that $A$ and $B$'s shared belief is (\ref{rightyes2}) in each dialogue.
\eenumsentence{\label{rightyes}
\item Do you have the three of spades?$_A$; Yes.$_B$; {\it Really?}$_A$; Yes.$_B$
\item Do you have the three of spades?$_A$; Yes.$_B$
}
\enumsentence{\label{rightyes2}
$Bel(B,have(B,3\spadesuit))$.
}
\paragraph{Subdialogues for repairing}
Another kind of subdialogue is {\it repairs}.
Dialogue (\ref{havecar}a) with the subdialogue for repairing `Have the three of spades?$_B$; Yes.$_A$' and dialogue (\ref{havecar}b) without it are observationally equivalent in the sense that $A$ and $B$ share the belief (\ref{rightyes2}).
\eenumsentence{\label{havecar}
\item Do you have the three of spades?$_A$; Have the three of spades?$_B$; Yes.$_A$; Yes.$_B$
\item Do you have the three of spades?$_A$; Yes.$_B$
}
Therefore, a semantics of dialogues which associates processes of dialogues with shared beliefs formed in the processes, 
can define an equivalence without considering the real mental states of conversants, 
by considering the shared beliefs which can be learned from mere {\it observation of dialogue processes}, i.e., observational equivalence of dialogues.
\par
Thus, our problem here is how to formalize the information sharing in dialogues so as to reflect observational equivalence of the dialogues.
\section{Hyper-Discourse Representation Theory}\label{hdrs}
We now turn to {\it Hyper-Discourse Representation Theory} ({\it Hyper-DRT}).
Section \ref{theo} introduces the theoretical background of modeling shared beliefs in {\it Situation Theory}.
Section \ref{Def} provides the definitions of Hyper-DRSs and their semantics based on the Situation-Theoretic modeling of shared beliefs.
Section \ref{Cons} provides the Construction Algorithm and the Construction Rules for constructing Hyper-DRSs from dialogues.
Section \ref{Prop} discusses the main properties of Hyper-DRT which model the basic properties of ``dialogues as belief sharing.''
\clearpage
\subsection{Situation Theoretic Modeling of Shared Beliefs}\label{theo}
The theory presented in this paper is basically an extension of \cite{BE87}.
The following paragraphs provide a brief introduction to this framework.
\paragraph{Situation Theory}
{\it Situation Theory} \cite{BP83,BE87,Bar89} is a model-theoretic framework of informational content.
In Situation Theory, the informational content of an expression is identified as a set-theoretic object.
\par
Let $\{H,Bel\}\cup AG\cup CARD\cup \{1,0\}\cup\{type,ofType\}$ be a set of atoms, where 
\begin{itemize}
\item $H$ and $Bel$ are relations which mean having and believing respectively,
\item $AG=\{Max,Claire\}$ be a set of agents,
\item $CARD=\{2\spadesuit,...,A\heartsuit\}$ be a set of cards,
\item $\{1,0\}$ be a set of polarities.
\end{itemize}
A {\it state of affairs} $\sigma$ is a tuple such as $((H,(a,c)),i)$ ($a$'s (not) having $c$), or $((Bel,(a,s)),i)$ ($a$'s (not) believing $p$), written $(H,a,c;i)$, $(Bel,a,s;i)$ respectively, for convenience's sake, where $a\in AG$, $c\in CARD$, $i\in \{1,0\}$, and $s$ is a situation.
Let $SOA$ be the set of states of affairs.
If $s\subseteq SOA$, then $s$ is a {\it situation}.
Let $SIT$ be the set of situations.
A {\it type} $T$ is a tuple $(type,\sigma)$, written $[\sigma]$, where $\sigma\in SOA$.
Let $TYPE$ be the set of types.
A {\it proposition}\<\footnote{
Strictly speaking, these propositions are called {\it Austinean} \cite{BE87,Bar89}.}
is a tuple $(ofType,s,T)$ ($s$ is of type $T$), written $(s:T)$, where $s\in SIT$ and $T\in TYPE$.
The class $\{(H,x,c;i)|x\in A, c\in CARD,i\in\{1,0\}\}\cup \{(n,x;i)|,n\in\{Max,Claire,Other,Self\},x\in A,i\in\{1,0\}\}$ is called $BSOA$ ({\it basic state of affairs}).
A proposition $(s:[\sigma])$ is said to be true if $\sigma\in s$.
\paragraph{Hypersets and Circular Objects}
A {\it hyperset} or {\it non-well-founded set} \cite{Acz87} is an object in the {\it hyper-universe} constructed by the axioms of a set theory with a new axiom, the {\it Anti-Foundation Axiom} (henceforth $AFA$) replacing the {\it Foundation Axiom}.
Therefore, a hyperset $x$ can be {\it circular}, i.e., $x\in \ldots \in x$ or {\it non-grounded}, i.e., there is an infinite sequence of distinct objects, starting with $x$, each a constituent of the next: $\ldots \in x''\in x'\in x$.
Any hyperset can be regarded as a unique solution to an equational system of sets.
For example, if $x$ has the two constituents $x$ and $a$, i.e., $x,a\in x$, then $x$ can be regarded as a unique solution to $x=\{x,a\}$.
The $AFA$ guarantees the existence of a unique solution to such equational systems of sets.
\par
More formally, given a set of atoms ${\cal U}$, an equational system of sets ${\cal E}$ is defined as the triple $(X,A,e)$, consisting of a set $X\subseteq {\cal U}$, a set $A$ disjoint from $X$, and a function $e:X\to pow(X\cup A)$.
For example, $x=\{x,a\}$ is defined as $(\{x\},\{a\},\{(x,\{x,a\})\})$.
A solution to ${\cal E}$ is a function $\theta$ with domain $X$ satisfying $\theta(x)=\{\theta(y)|y\in e(x)\cap X\}\cup e(x)\cap A$ for each $x\in X$.
For example, the solution $\theta$ of the above example is defined as satisfying $\theta(x)=\{\theta(x),a\}$.\<\footnote{
Such a definition is called a {\it corecursive definition} \cite{BM96}.}
The $AFA$ is formulated as ``{\it every equational system of sets has a unique solution} $\theta$.''\<\footnote{
\cite{BE87} and \cite{Bar89} apply this hyperset theory to the construction of {\it circular propositions}.
For example, the so-called {\it liar sentences}, e.g., (a): (a) is false, 
are regarded as expressing a proposition $(s:[Tr,p;0])$ for a situation $s$ where each sentence is used, and $p$ a solution to $p=(s:[Tr,p;0])$.
Standard semantic theories can only treat liar sentences as having undefined semantics.
}
\paragraph{Modeling Shared Beliefs}
{\it Shared beliefs} or {\it mutual beliefs} are considered as circular objects in Situation Theory.
\cite{Bar89} compares three approaches to modeling of shared beliefs, and two of them ((ii) and (iii)) are defined by non-well-founded sets, while one ((i)) is an infinite set.
For example, the shared belief $b_s$ shared between $a$ and $b$ that $a$'s having the three of spades at situation $s$ is defined in each approach as follows:
\begin{itemize}
\item [(i)] the Iterate: 
$s_I=\bigcup_{\alpha<\omega}s_{\alpha}$, where $s_{\alpha+1}=\{(Bel,a,s_{\alpha};1),(Bel,a,s_{\alpha};1)\}$, and $s_0=\{(H,a,3\spadesuit;1)\}$;
\item [(ii)] the Fixed Point: 
$s_F=\{(Bel,a,\{(H,a,3\spadesuit;1)\}\cup s_F;1),(Bel,a,\{(H,a,3\spadesuit;1)\}\cup s_F;1)\},$;
\item [(iii)] the Shared-Situation: $s_S=\{(Bel,a,s_S;1),(Bel,b,s_S;1),(H,a,3\spadesuit;1)\}$.\<\footnote{
\cite{BE87} proposes a slightly different formalization as the solution of the equation $x=(s:[[H,a,3\spadesuit;1]\wedge [Bel,a,x;1]\wedge [Bel,b,x;1]]).$
}
\end{itemize}
We will adopt the Shared-Situation approach here, 
since it formalizes shared beliefs as finite objects, and the Fixed Point approach, which can similarly formalize them as finite objects,
can be considered a distributed belief of the shared belief.
Namely, the Fixed Point situation $s_F$ can be considered the solution to $s_F=\{(Bel,a,t;1),(Bel,a,t;1)\}$, and $t=\{(H,a,3\spadesuit;1)\}\cup s_F$, i.e., 
$t=\{(H,a,3\spadesuit;1),(Bel,a,t;1),(Bel,a,t;1)\}$.
Therefore, $s_F=\{(Bel,a,s_S;1),(Bel,a,s_S;1)\}$.
Thus, the intrinsic circularity of shared beliefs is expressed by the Shared Situation $s_S$.\<\footnote{
Furthermore we must introduce a notion of coherence of models of shared beliefs to avoid such an {\it incoherent} shared belief as: (i) $A$ and $B$ share the belief that $A$ and $B$ don't share any belief; (ii) $A$ and $B$ share the belief that $A$ and $B$ don't share (ii); and so on \cite{Oga95c}.
For simplicity of the argument here, discussion of this problem is omitted.}
\par
We introduce the notion of an {\it equational system of situations} ($ESS$), 
which is basically an equational system of sets, expressed as a tuple ${\cal E}=(S,A,P,e,s)$, where $S$ is a set of indeterminates, $A$ a set of agents, $P\subseteq BSOA$, $s\in S$ (called the root of ${\cal E}$), $e:S\to \Gamma(P\cup S)$, and 
$\Gamma:x\mapsto \{(Bel,x,s;i)|s\in pow(x),x\in A,i\in\{1,0\}\}\cup BSOA$.
\par
For example, $s_S$ can be considered as a solution to an equational system of situations:\\ 
$(\{s\},\{a,b\},\{(H,a,3\spadesuit;1)\},\{(s,\{(Bel,a,s;1),(Bel,b,s;1),(H,a,3\spadesuit;1)\})\}$.
\par
$s_S$ can be unfolded infinitely as follows:
$$
\begin{BOX}{lcl}
s_S&=&\{(Bel,a,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\\
&&(Bel,b,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\sigma\},\\
&=&\{(Bel,a,\{(Bel,a,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\\
&&(Bel,b,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\sigma\};1),\\
&&(Bel,b,\{(Bel,a,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\\
&&(Bel,b,\{(Bel,a,s_S;1),(Bel,b,s_S;1),\sigma\};1),\sigma\};1)\},\\
&=&\vdots\\
\end{BOX}
$$
This property grasps the essence of shared beliefs, which, in modal logic approaches \cite{FHMV95} to shared beliefs or common knowledge, is axiomatized as the {\it Fixed Point Axiom} (\ref{FPA1}) and the {\it Induction Rule} (\ref{FPA2}).
\subsection{Definitions of Hyper-DRSs and their Semantics}\label{Def}
\begin{DEF}[Definition of Hyper-DRSs]\sl
Let ${\cal A}=\{x_1,\ldots,x_n\}$ be a set of agent indeterminates, $AG$ be a set of agents, $CARD$ be a set of cards, 
${\cal T}$ = $\{K_0,\ldots,K_n\}$ be a set of theory (set of propositions) indeterminates.
A term is defined by $$\varphi::=Other(x)|Anch(x,a)|have(x,c)|Bel(x,K),$$
where $a\in AG$, $c\in CARD$, $K\in {\cal T}$, and $x\in {\cal A}$.
$\Phi$ is the set of terms.
A condition $\phi$ is defined by $$\phi::=\varphi\epsilon^+K|\varphi\epsilon^-K|K_1:=K_2.$$
A Hyper-DRS $\K$ is a set of conditions, which is specified by a tuple
$$(dom(\K),ag(\K),cond(\K),\epsilon^+_{\K},\epsilon^-_{\K},\sigma_{\K},r_{\K}),$$
where 
\begin{itemize}
\item $dom(\K)\subseteq {\cal A}\cup{\cal T}$ is the domain of $\K$, 
\item $ag(\K)\subseteq {\cal A}$ is the set of the conversants, 
\item $cond(\K)$ is a set of terms appearing in $\K$, 
\item $\epsilon^+\subseteq \Phi\times {\cal T}$ means a positive membership and $\epsilon^+\subseteq \Phi\times {\cal T}$ means a negative membership, 
satisfying the condition: $\epsilon^+_{\K}\cap \epsilon^-_{\K}=\emptyset$,
\item $\sigma_{\K}$ means a substitution between theory indeterminates which appear in $\K$, and
\item $r_{\K}\in dom(\K)\cap {\cal T}$ is called the {\it root} of $\K$.
\end{itemize}
\par
A Hyper-DRS $\K$ is complete iff $\forall K\in dom(\K)\cap {\cal T}\forall \tau\in \Phi_{\K}.\tau\epsilon^+ K\mbox{ or }\tau\epsilon^- K$.


Let $\K_1,\K_2$ be Hyper-DRSs.
Then, $\K_1$ is a sub-Hyper-DRS of $\K_2$ (or $\K_2$ is a
super-Hyper-\clearpage \noindent
DRS of $\K_1$), written $\K_1\subseteq \K_2$, iff $dom(\K_1)\subseteq dom(\K_2)$, $ag(\K_1)\subseteq ag(\K_2)$, $cond(\K_1)\subseteq cond(\K_2)$, $r\K_1=r\K_2$, $\epsilon^+_{\K_1}\subseteq\epsilon^+_{\K_2}$, $\epsilon^-_{\K_1}\subseteq\epsilon^-_{\K_2}$, and $\sigma_{\K_1}\subseteq\sigma_{\K_2}$.
\end{DEF}
\begin{DEF}[Semantics of Hyper-DRSs]\sl
Let $\K$ be a Hyper-DRS and ${\cal E}=(X,A,P,e,s)$ an ESS.
$\K$ is true in ${\cal E}$, written ${\cal E}\forces\K$, iff there is an embedding $g:dom(\K)\to X\cup pow(X)$, 
of $\K$ in ${\cal E}$ such that: 
\begin{itemize}
\item[] if $x\in ag(\K)$, then $g(x)\in A$, and if $K\in dom(\K)\cap{\cal T}$, then $g(K)\in X$, 
\item[] if $(\varphi\epsilon^+_{\K}K)$, then $\lden\varphi\rden_g\in e(g(K))$, and if $(\varphi\epsilon^-_{\K}K)$, then $\lden\varphi\rden_g\notin e(g(K))$,
\item[] if $\sigma_{\K}(K)=K'$, then $g(K)=g(K')$, 
\item[] $\lden Other(x)\rden_g=(Other,g(x);1)$, $\lden have(x,c)\rden_g=(H,g(x),c;1)$,\\ $\lden Bel(x,K)\rden_g=(Bel,g(x),g(K);1)$, and $\lden Anch(x,a)\rden_g=(Anch,g(x),a;1)$.
\end{itemize}
\end{DEF}
\par
The equational systems are adopted for the following reasons: 
\begin{itemize}
\item The intrinsic infinity or circularity of shared beliefs can be finitely represented by equa-tional systems, 
e.g., the shared belief of proposition $p$ between agent $A$ and $B$ is represented as a solution of $\{Bel(A,K)\epsilon^+ K,Bel(B,K)\epsilon^+K,p\epsilon^+K\}$; 
\item Equational systems can be updated easily,
e.g., $A$'s belief that $p$, which can be represented as $\{Bel(A,K)\epsilon^+ K,p\epsilon^+ K\}$, can be updated to the shared belief of $p$ between $A$ and $B$ monotonically by adding to it the single condition `$Bel(B,K)\epsilon^+K$';
\item The semantics of $\epsilon^+,\epsilon^-$ are guaranteed by embedding of $\epsilon^+$ and $\epsilon^-$ in equations and inequations, respectively, as the following figure indicates: 
$$
\begin{BOX}{l}
p_0\epsilon^+K,p_1\epsilon^+K,q_0\epsilon^-K\\
\end{BOX}
\stackrel{embed\; in}{\Longrightarrow}
\begin{BOX2}{l}
\{p_0,p_1,\ldots,p_n\}=K\\
\end{BOX2}
$$
\par
Therefore, they can give a meaning to the intermediate state in each move.
\item Even if a Hyper-DRS is not true (or has no solution), it represents some information.
Therefore, a Hyper-DRS can represent information expressed by each move and can solve the {\it compositionality problem of the semantics of dialogue}.
Furthermore, a Hyper-DRS can represent information even in failed dialogues or abnormal dialogues, although such a Hyper-DRS has no model.
On this point, Hyper-DRSs are more appropriate for treating dialogues than any direct model of dynamic semantics.
\end{itemize}
\subsection{Constructing Hyper-DRS from Dialogues}\label{Cons}
Discourse Representation Theory \cite{KR93} has a Construction Algorithm and Construction Rules for DRSs.
We propose a Construction Algorithm and Construction Rules of Hyper-DRSs as follows.
This formalization relies on the framework of \cite{KR93} regarding
Construction Rules for intra-sentential constituents.
\clearpage
\renewcommand{\arraystretch}{}
\small
\begin{center}
\begin{tabular}{||p{1.8cm}p{11.5cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf Hyper-DRS Construction Algorithm}} \\
\hline
{\bf Inputs:} & a dialogue $m_1;\ldots;m_i;m_{i+1};\ldots;m_n$\\
& the empty Hyper-DRS $\K$, i.e., $dom(\K)=\{K_0\}$, $ag(\K)=$ \o,
$cond(\K)=$ \o, $\epsilon^+,\epsilon^-=$ \o, and $K_0=r_{\K}$.\\
& the empty stack of discourse referents $S=\Lambda$\\
\multicolumn{2}{||l||}{{\bf For} $i=0,\ldots,n$} \\
& $cond(\K):=cond(\K)\cup \{[m_i^{\ast}]_A\}$, where $[m_i^{\ast}]$ is the syntactic analysis of move $m_i$ and $A$ its utterer;\\
& Until $cond(\K)$ contains only irreducible conditions, keep on applying construction rules to each reducible condition $\varphi\in cond(\K)$;\\
\hline
\hline
\end{tabular}
\end{center}
\normalsize
A Construction Rule for a Hyper-DRS is of the form of $(\frac{\Gamma}{\Delta},\alpha S)$, read `change $\Gamma$ to $\Delta$,' where $\Gamma,\Delta$ are conditions of a Hyper-DRS, $S$ a stack of discourse referents, and $\alpha$ an operation of $S$ (to push a discourse referent to $S$ or to pop the top of $S$).
$\uplus$ means disjoint union.
\par
\vspace{2mm}
The following Construction Rules are for typical conversational moves.
\small
\begin{center}
\begin{tabular}{||p{11.8cm}p{1.5cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Initial Greeting}} \\
\hline
{\footnotesize \hspace*{-6pt}$\begin{array}{c}\Gamma\uplus\{[\alpha]_A\}\\ 
\overline{\Gamma\uplus\{Bel(x,K_0)\epsilon^+K_0,Bel(x,K')\epsilon^+K_0,Other(y)\epsilon^+K',Anch(x,A)\epsilon^+K_0,Bel(y,K_0)\epsilon^+K}\}\end{array}$}& \hspace{-3mm}$push(K,S)$\\
where $\alpha\in 1Greet$, $K_0\in dom(\Gamma)$, $K,K'\notin dom(\Gamma), x,y\notin ag(\Gamma)$, $K_0=r_{\Gamma}$ &\\
\hline
\hline
\end{tabular}
\end{center}
\small
$1Greet$ consists of `Hi', `Hello' etc. with the proper intonation for an initial greeting, expressed by `?'.
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Secondary Greeting}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha]_A\}\\ 
\overline{\Gamma\uplus\{Bel(y,K')\epsilon^+K, Other(x)\epsilon^+K', Anch(y,A)\epsilon^+K},K:=K_0\}\end{array}$ & $pop(S)$ \\
where $\alpha\in 2Greet$, $K=top(S)$, 
$(Bel(x,K)\epsilon^+K_0), (Other(y)\epsilon^+K)\in \Gamma$, $K_0,K,K'\in dom(\Gamma)$, $x,y\in ag(\Gamma)$, $K_0=r_{\Gamma}$ &\\
\hline
\hline
\end{tabular}
\end{center}
$2Greet$ consists of `Hi', `Hello' etc. with the proper intonation for secondary greetings.
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Assertion}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha.]_A\}\\ 
\overline{\Gamma\uplus\{Bel(x,K)\epsilon^+K', [\alpha]\epsilon^+K}\}\end{array}$ & $push(K',S)$ \\
where $(Anch(x,A)\epsilon^+K_0)\in \Gamma$, $K_0\in dom(\Gamma)$, $x\in ag(\Gamma)$, $K_0=r_{\Gamma}$, $K,K'\notin dom(\Gamma)$ &\\
\hline
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Acknowledgement to Assertion}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha.]_A\}\\ 
\overline{\Gamma\uplus\{K':=K_0}\}\end{array}$ & $pop(S)$ \\
where $\alpha\in Ack$, $(Anch(x,A)\epsilon^+K_0),(Bel(x,K)\epsilon^+K')\in \Gamma$, $K_0,K,K'\in dom(\Gamma)$, $K'=top(S)$, $x\in ag(\Gamma)$, $K_0=r_{\Gamma}$ &\\
\hline
\hline
\end{tabular}
\end{center}
$Ack$ consists of `Uh-huh', `Yeah', `Hum', and so on.
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Question}
\<\footnotemark
} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha?]_A\}\\ 
\overline{\Gamma\uplus\{Bel(y,K)\epsilon^+K', [\alpha]\epsilon^+K}\}\end{array}$ & $push(K',S)$ \\
where $(Anch(x,A)\epsilon^+K_0),(Bel(x,K'')\epsilon^+K_0),(Other(y)\epsilon^+K'')\in \Gamma$, $K_0,K''\in dom(\Gamma)$, $x,y\in ag(\Gamma)$, $K_0=r_{\Gamma}$, $K,K'\notin dom(\Gamma)$ &\\
\hline
\hline
\end{tabular}
\end{center}
\footnotetext{
This is similar to Hintikka's semantics (cf. \cite{HS97}) of questions, since it involves the other's epistemic operator.
However, the difference from Hintikka's semantics is that the goal of the question is not the proof of the proposition with the other's  epistemic operator,
but sharing the proposition in our semantics.
On the other hand, the standard formal semantics of questions is based on a possible world semantics by \cite{GS97} as follows.
$$\lden ?\varphi\rden^{{\cal M}}=\{\{w'\in W|w\in\lden\varphi\rden^{{\cal M}}\Iff w'\in\lden\varphi\rden^{{\cal M}}\}|w\in W\}$$
In this semantics, epistemic operators are not used.
}
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Assent to Positive Question}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha.]_A\}\\ 
\overline{\Gamma\uplus\{K':=K_0}\}\end{array}$ & $pop(S)$ \\
where $\alpha\in Asn$, $(Anch(x,A)\epsilon^+K_0),(Bel(x,K)\epsilon^+K')\in \Gamma$, $K_0,K,K'\in dom(\Gamma)$, $K'=top(S)$, $x\in ag(\Gamma)$, $K_0=r_{\Gamma}$ &\\
\hline
\hline
\end{tabular}
\end{center}
$Asn$ consists of `Yes', `Yeah', and so on.
\vspace{3mm}
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Repetitive Question}} \\
\hline
{\footnotesize $\begin{array}{c}\Gamma\uplus\{[\alpha??]_A\}\\ 
\overline{\Gamma\uplus\{Bel(y,K_2)\epsilon^+K, 
Bel(x,K_2)\epsilon^+K_2,
Bel(y,K_2)\epsilon^+K_2,
Bel(y,K_1)\epsilon^+K_2,
[\alpha]\epsilon^+K_1}\}\end{array}$} & $push(K,S)$\\
where $(Anch(x,A)\epsilon^+K_0),(Bel(x,K'')\epsilon^+K_0),(Other(y)\epsilon^+K'')\in \Gamma$, $K_0,K''\in dom(\Gamma)$, $x,y\in ag(\Gamma)$, $K_0=r_{\Gamma}$, $K_1,K_2,K\notin dom(\Gamma)$ &\\
\hline
\hline
\end{tabular}
\end{center}
`??' expresses the proper intonation for repetitive questions.
\vspace{3mm}
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Repetitive Requirement}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha]_A\}\\ 
\overline{(\Gamma-\Delta[K'])\uplus\{K:=K_0}\}\end{array}$ & $pop(S)$ \\
where $\alpha\in RR$, $\Delta[K']=\{p\in\Gamma|\exists \varphi.p=(\varphi\epsilon^+K')\}$, $(Bel(z,K')\epsilon^+K)\in \Gamma$, $K=top(S)$, $K_0,K,K'\in dom(\Gamma)$, $z\in ag(\Gamma)$, $K_0=r_{\Gamma}$ &\\
\hline
\hline
\end{tabular}
\end{center}
$RR$ consists of `Huh?', `What?, `Pardon?' and so on.
\vspace{3mm}
\begin{center}
\begin{tabular}{||p{11.5cm}p{1.8cm}||}
\hline
\hline
\multicolumn{2}{||l||}{{\bf CR.Reopener}} \\
\hline
$\begin{array}{c}\Gamma\uplus\{[\alpha]_A\}\\ 
\overline{(\Gamma)\uplus\{Bel(y,K_0)\epsilon^+K}\}\end{array}$ & $push(K,S)$ \\
where $\alpha\in Reo$, $Anch(y,A)\epsilon^+K_0\in \Gamma$, $K=top(S)$, $K_0\in dom(\Gamma)$, $y\in ag(\Gamma)$, $K_0=r_{\Gamma}$, $K\notin dom(\Gamma)$ &\\
\hline
\hline
\end{tabular}
\end{center}
$Reo$ consists of `Really?', and so on.

\clearpage
\normalsize
Table \ref{tab} is a brief explanation of these Construction Rules.
It shows the transition of Hyper-DRSs for four observationally equivalent dialogues, where the left part of each column gives the stack for each state.
$Bel(A,p)\epsilon^+K$ is an abbreviation of `$Bel(A,K')\epsilon^+K,p\epsilon^+ K'$', and $S_{A,B}\{p_1,...,p_n\}$ is an abbreviation of `$Bel(A,K')\epsilon^+K$, $Bel(B,K')\epsilon^+K$, $p_1,...,p_n\epsilon^+K'$.'
The resulting states are ones after each dialogue.\<\footnote{
These states also include shared beliefs established in the opening of the dialogue.
}
\begin{table}[h]
\footnotesize
\tabcolsep=5pt
\begin{tabular}{||l|l|l|l||}
\hline
\hline
\multicolumn{4}{||c||}{{\small {\bf Dialogues}}} \\
\hline
p?$_B$;Yes.$_A$ & p?$_B$;p??$_A$;Yes.$_B$;Yes.$_A$ & p?$_B$;Yes.$_A$;Really?$_B$;Yes.$_A$ & p?$_B$;Huh?$_A$;p?$_B$;Yes.$_A$\\
\hline
\hline
\multicolumn{4}{||c||}{{\small {\bf Hyper-DRS transitions in each dialogue}}} \\
\hline
$K: Bel(A,p)\epsilon^+K$ & $K:Bel(A,p)\epsilon^+K$ & $K:Bel(A,p)\epsilon^+K$& $K:Bel(A,p)\epsilon^+K$ \\
\hline
$\Lambda:K:=K_0$ & $K',K:$ & $\Lambda:K:=K_0$& $K_1:Bel(A,K_1)\epsilon^+K$, \\
 & $Bel(A,S_{A,B}\{Bel(A,p)\})\epsilon^+K'$ & & $K:=K_0$\\
\hline
 & $K: K':=K_0$ & $K': Bel(A,K_0)\epsilon^+ K'$& $K': Bel(A,K_2)\epsilon^+K'$, \\
 &  & & $p\epsilon^+K_2$, $K_2:=K_1$\\
\hline
 & $\Lambda: K:=K_0$ & $\Lambda: K':=K_0$ & $\Lambda: K':=K_0$\\
\hline
\hline
\multicolumn{4}{||c||}{{\small {\bf Resulting Hyper-DRSs after opening and each dialogue}}} \\
\hline
$S_{A,B}\{Bel(A,p)\}$ & $S_{A,B}\{Bel(A,p),$ & $S_{A,B}\{Bel(A,p)\}$ & $S_{A,B}\{Bel(A,p)\}$ \\ 
& $Bel(A,S_{A,B}\{Bel(A,p)\})\}$ & & \\
\hline
\hline
\end{tabular}
\vspace{2mm}
\caption{Transitions and resulting Hyper-DRSs of four dialogues}\label{tab}
\end{table}
\normalsize
\tabcolsep=6pt
\renewcommand{\arraystretch}{}

\vspace{-3mm}
Table \ref{tab} shows that Hyper-DRS construction processes are distinct for the four observationally equivalent dialogues, but their resulting Hyper-DRSs are epistemically bisimilar as defined in the next section.
That is, Hyper-DRT can distinguish each of the dialogues from the others by their construction steps, and can identify them as being the same by an equivalence relation based on circularity.
\subsection{The Main Properties of Hyper-DRT}\label{Prop}
Now we define the relation $\models$ which is a relation between a dialogue or its Hyper-DRS, and a language which describes what the dialogue or Hyper-DRS means.
\begin{DEF}\label{Mean}\sl Let $\delta$ be a dialogue, ${\cal K}$ one of its Hyper-DRSs.\\
\begin{tabular}{rcl}
$K\models_{\K} p$ &$\Iff$ &$p\epsilon^+_{\K} K$, where $p=Other(x),Anch(x,a),have(x,c)$,\\
$K\models_{\K} Bel(x,\varphi)$ & $\Iff$ & there is $K_1$ such that $Bel(x,K_1)\epsilon^+_{\K} K$ and $K_1\models_{\K} \varphi$,\\
$K\models_{\K} \varphi_1\wedge \varphi_2$ & $\Iff$ & $K\models_{\K}\varphi_1\mbox{ and }K\models_{\K}\varphi_2$,\\
$\delta\models\varphi$ & $\Iff$ & $r_{\K}\models_{\K}\varphi$\\
\end{tabular}

\noindent
For $S_{a,b}\varphi$, we can define a special case of the definition of $\models$ such that 
$K\models_{\K} S_{a,b}\varphi$ iff the equation $X=B_a^{\K}(X)\cap B_b^{\K}(X)$ has the non-empty largest solution $Z$ and for all $H\in Z$, $H\models_{\K}\varphi$, where $B_x^{\K}(X)=\{K\in dom(\K)|K'\in X\& Bel(x,K')\epsilon^+_{\K}K\}$.
\end{DEF}
Let us first examine the basic properties of $S_{a,b}\varphi$ in Hyper-DRT.
\begin{LEM}\label{KT}\sl
Every Hyper-DRS $\K$ has a largest solution to $X=B_a^{\K}(X)\cap B_b^{\K}(X)$.
\end{LEM}
{\it Proof.} Let $F$ be a function $X\mapsto B_a^{\K}(X)\cap B_b^{\K}(X)$ for $X\subseteq dom(\K)\cap{\cal T}$.
If $F$ is {\it monotone}, i.e., $Y\subseteq Z\;\To\;F(Y)\subseteq F(Z)$,
$F$ has the greatest fixed point and the least fixed point by the {\it Knaster-Tarski Theorem}\<
\footnote{
The Knaster-Tarski theorem \cite{DP90,Llo87} is as follows:
Let \hspace{3mm}$=(L,\subseteq)$ be a complete lattice and $F:L\to L$ be a monotone function.
Then $F$ has the least fixed point $lfg(F)$ and the greatest fixed point $gfp(F)$.
Furthermore, $lfp(F)=\bigcap\{X|F(X)\subseteq X\}$ and $gfp(F)=\bigcup\{X|X\subseteq F(X)\}$.
}
since $(pow(dom(X)\cap {\cal T}),\subseteq)$ is a complete lattice.
By definition, $B_x^{\K}(Z)\subseteq B_x^{\K}(Z\cup Y)$.
Therefore, $F$ is monotone and has its greatest fixed point,
namely, the largest solution to $X=B_a^{\K}(X)\cap B_b^{\K}(X)$.$\dashv$
\begin{LEM}\label{appro}\sl
Let $S_{a,b}\varphi^{\ast}$ be the infinite approximation by $\wedge$ and $Bel$ of $S_{a,b}\varphi$, defined by induction on ordinals as follows: $S_{a,b}\varphi_{0}=\{\varphi\}$, $S_{a,b}\varphi_{\alpha+1}=Bel(a,S_{a,b}\varphi_{\alpha})\wedge Bel(b,S_{a,b}\varphi_{\alpha})$, and $S_{a,b}\varphi^{\ast}=\bigwedge_{\alpha<\omega}S_{a,b}\varphi_{\alpha}$.
Then,
$K\models_{\K}S_{a,b}\varphi\;\Iff \;K\models_{\K}S_{a,b}\varphi^{\ast}.$\<\footnote{
A similar theorem has already proved in \cite{Lis95}.}
\end{LEM}
{\it Proof.} Using the functions $B_a^{\K}$ and $B_b^{\K}$ and $X^{\ast}=\{K\in dom(\K)|K\models_{\K}S_{a,b}\varphi^{\ast}\}$, the definition of $S_{a,b}\varphi^{\ast}$ is redefined by induction on ordinals as follows:
\begin{eqnarray*}
X_0&=&\{K\in dom(\K)|p\epsilon^+_{\K}K\},\\
X_{\alpha+1}&=&B_a^{\K}(X_{\alpha})\cap B_a^{\K}(X_{\alpha}),\\
X^{\ast}&=&\bigcap_{\alpha<\omega}X_{\alpha}.
\end{eqnarray*}
That is, $X^{\ast}$ is $gfp(F)\cap X_0$ in Lemma \ref{KT}, i.e., the largest solution to $X=B_a^{\K}(X)\cap B_b^{\K}(X)$ by the {\it dual of the Kleene Theorem}\<\footnote{
The Kleene theorem \cite{Llo87} is that $lfp(F)$ of any upward continuous function $F$ over a complete lattice $(L,\bot,\leq)$ is constructed by transfinite induction on ordinals as follows: $F_0=\bot$, $F_{\alpha+1}=F(F_{\alpha})$, $lfp(F)=\bigsqcup_{\alpha<\omega}F_{\alpha}$.},
if $F$ has {\it downward continuity}, i.e., $F(\bigcap_{i\in I}Y_i)=\bigcap_{i\in I}F(Y_i)$,
since $(pow(X_0),\subseteq)$ is a complete lattice.
We only need to show that $F$ is downward continuous.
We have $K'\in Y\cap Y'\; \&\; Bel(x,K')\epsilon^+_{\K}K\; \Iff\; K'\in Y \;\&\; Bel(x,K')\epsilon^+K\; \&\; K'\in Y'$.
So, $F(Y\cap Y')=F(Y)\cap F(Y')$, so, $F$ is downward continuous.$\dashv$
\par
We can show that Hyper-DRSs have the three properties discussed in sections 1 and 2, as in the following theorems of Hyper-DRT.
\begin{LEM}\label{sub}
If $K\models_{\K_1}\varphi$ and $\K_1\subseteq \K_2$, then $K\models_{\K_2}\varphi$.
\end{LEM}
\par
{\it Proof.} Directly from the definition.$\dashv$
\begin{LEM}\label{monotone}
$\delta\models S_{a,b}(\varphi_1\wedge\varphi_2)\To \delta\models S_{a,b}(\varphi_2)$.
\end{LEM}
\par
{\it Proof.} Suppose $\delta\models S_{a,b}(\varphi_1\wedge \varphi_2)$ and $\K$ is a Hyper-DRS of $\delta$.
By definition, 
$r_{\K}\models_{\K} S_{a,b}(\varphi_1\wedge\varphi_2)$,
i.e., $r_{\K}$ is in the largest solution $Z$ to $X=B_a^{\K}(X)\cap B_b^{\K}(X)$ and $r_{\K}\models_{\K}\varphi_1\wedge\varphi_2$.
Therefore, $r_{\K}\models_{\K}\varphi_2$.$\dashv$
\begin{Th}[Dialogues as Compositional Shared Belief Revisions] Let $\delta_1$ and $\delta_2$ be dialogues, and $\delta_1;\delta_2$ the sequential composition of $\delta_1$ and $\delta_2$.
If $\delta_1\models S_{a,b}\varphi_1$ and $\delta_2\models \varphi_2$, then $\delta_1;\delta_2\models S_{a,b}(\varphi_1\wedge\varphi_2)$.
\end{Th}
\par
{\it Proof.} Suppose $\delta_1\models S_{a,b}(\varphi)$, and $\K_1$ is a Hyper-DRS of $\delta_1$, $\K_2$ a Hyper-DRS of $\delta_2$, $\K$ a Hyper-DRS of $\delta_1;\delta_2$.
By definition, 
$r_{\K_1}\models_{\K_1} S_{a,b}(\varphi_1)$,
i.e., $r_{\K_1}$ is in the largest solution $Z$ to $X=B_a^{\K}(X)\cap B_b^{\K}(X)$ and $r_{\K_1}\models_{\K_1} \varphi$.
By the Construction Algorithm and the Construction Rules, $\K_2$ inherits $r_{\K_1}$, i.e., $r_{\K_2}=r_{\K_1}=r_{\K}$ (*).
By the hypothesis and (*), $r_{\K}\models_{\K_2}\varphi_2$.
By the Construction Algorithm, $\K_2\subseteq \K$ (**).
By Lemma \ref{sub} and (**), $r_{\K}\models_{\K} \varphi_1\wedge \varphi_2$.
Therefore, $r_{\K}\models_{\K}S_{a,b}(\varphi_1\wedge\varphi_2)$.$\dashv$
\begin{PROP}[Openings of Dialogues as Mutual Identifications]\label{Form1}
\begin{list}{}{\leftmargin=10mm \labelwidth=30mm}
\item[]
\item [{\it 1.}] $Hi?_B;Hi._A\models S_{A,B}(Bel(A,Other(B))\wedge Bel(B,Other(A)))$,
\item [{\it 2.}] $Hi?_A;Hi._B\models S_{A,B}(Bel(A,Other(B))\wedge Bel(B,Other(A)))$,
\end{list}
\end{PROP}
\par
{\it Verification.} Directly from the Construction Rules and definition \ref{Mean}.$\dashv$
\par
That is, the Construction Rules of Initial Greetings and Secondary Greetings provide sharing of mutual identification for openings of dialogues.
\begin{PROP}[Dialogues as Shared Belief Formations/Revisions]\label{Form2}
\begin{list}{}{\leftmargin=10mm \labelwidth=30mm}
\item[]
\item [{\it 1.}] $Open_{A,B};p._A;Uh-huh._B\models S_{A,B}Bel(A,p')$,
\item [{\it 2.}] $Open_{A,B};p?_B;Yes._A\models S_{A,B}Bel(A,p')$,
\item [{\it 3.}] $Open_{A,B};p?_B;p??_A;yes._B;yes._A\models S_{A,B}Bel(A,p')$,
\item [{\it 4.}] $Open_{A,B};p?_B;yes._A;Really?_B;yes._A\models S_{A,B}Bel(A,p')$,
\item [{\it 5.}] $Open_{A,B};p?_B;Huh?_A;p?_B;Yes._A\models S_{A,B}Bel(A,p')$,
\end{list}
\rm where $p'$ means $p$'s content and $Open_{A,B}$ is one of the dialogues in  Proposition \ref{Form1}.
\end{PROP}
\par
{\it Proof.} Directly from the Construction Algorithm, the Construction Rules and Lemma \ref{monotone}. (See Table \ref{tab})$\dashv$
\paragraph{Dialogues as Processes whose Identity is Definable from the Shared Belief}
We will see that Hyper-DRSs reflect the observational equivalence of dialogues in terms of epsitemic bisimulation of Hyper-DRSs.
Therefore, Hyper-DRSs identify dialogues from the viewpoint of their formed shared beliefs.
\begin{DEF}[Observational Equivalence] Let $\delta_1,\delta_2$ be dialogues.
$$\delta_1\simeq\delta_2\;\Iff\; \forall \varphi(\delta_1\models\varphi\; \Iff\;\delta_2\models\varphi)$$
\end{DEF}
\newcommand{\toA}{}
\newcommand{\toB}{}
\newcommand{\toX}{}
\begin{DEF}[Epistemic Graph] Let $\K$ be a Hyper-DRS.
The {\it epistemic graph} ${\cal G}(\K)$ of $\K$ is a tuple 
$$(G,(\toX)_{x\in ag(\K)},r_{\K},l),$$
where 
$G=dom(\K)\cap {\cal T}$,
$K\toX K'$ iff $Bel(x,K')\epsilon^+K$,
$l:G\to cond(\K)$, $l(K)=\{p|p\epsilon^+K,p\mbox{ is atomic}\}$.
\end{DEF}
\begin{DEF}[Epistemic Bisimulation] Let $\K_1,\K_2$ be Hyper-DRSs.
$\K_1$ and $\K_2$ are {\it epistemically bisimilar}, written $\K_1\equiv \K_2$, iff their epistemic graphs ${\cal G}(\K_1)$ and ${\cal G}(\K_2)$ are bisimilar,
i.e. they satisfy the following conditions:
\begin{itemize}
\item For every $K\in G(\K_1)$ there is $K'\in G(\K_2)$ such that $KRK'$ and $R\in EB(\K_1,\K_2)$,
\item For every $K'\in G(\K_2)$ there is $K\in G(\K_1)$ such that $KRK'$ and $R\in EB(\K_1,\K_2)$,
\end{itemize}
where $R\in EB(\K_1,\K_2)$ is defined as follows:
\begin{itemize}
\item If $KRK'$ and $K\toX H$ then there is $H'$ with $HRH'$ and $K'\toX H'$,
\item If $KRK'$ and $K'\toX H'$ then there is $H$ with $HRH'$ and $K\toX H$,
\item If $KRK'$ then $l(K)=l(K')$.
\end{itemize}
Let $\delta_1,\delta_2$ be dialogues, we will write $\delta_1\equiv \delta_2$ iff $\K(\delta_1)\equiv \K(\delta_2)$ for convenience.
\end{DEF}
\begin{Th}[Epistemic Bisimulation = Observational Equivalence]\label{main}
$$\delta_1\equiv\delta_2\; \Iff\; \delta_1\simeq\delta_2.$$
\end{Th}
\par
{\it Proof}. This proof is similar to Proposition 10.8 of \cite{BM96}, which is that $G$ and $G'$ are bisimilar iff $d[G]=d'[G']$, for labeled graphs $G$ and $G'$, where $d,d'$ are the decoration of $G$ and $G'$ respectively.
Let $\K_1$ and $\K_2$ be a Hyper-DRS of $\delta_1$ and $\delta_2$, respectively.
We only need to show that for every $K\in dom(\K_1)$, $K'\in dom(\K_2)$, there exists $R\in EB(\K_1,\K_2)$ such that $K{\K_1}R K'\; \Iff\; m_{\K_1}(K)=m_{\K_2}(K')$,
where $m_{\K}(x)=\{\varphi|x\models_{\K} \varphi\}$.\\
($\To$) Assume $R\in EB(\K_1,\K_2)$.
We show that $KR K'$ and $K \models_{\K_1}\varphi$ imply $K' \models_{\K_2}\varphi$ by induction on the complexity of $\varphi$.
We will only consider $Bel$ and the atomic case $p$, since the case of $\wedge$ is trivial and the case of $S_{a,b}$ is reducible to $Bel$ by Lemma \ref{appro}.
(i) $\varphi=p$: By definition of $R$, $l(K)=\{p|p\epsilon^+_{\K_1}K\}=l(K')=\{p|p\epsilon^+_{\K_2}K'\}$.
Therefore, $K'\models_{\K_2}p$.
(ii) $\varphi=Bel(x,\psi)$: Assume the following conditions: (a) If $xRx'$ and $x\models_{\K_1}\psi$ then $x'\models_{\K_2}\psi$; (b) $KRK'$; and (c) $K\models_{\K_1}Bel(x,\psi)$.
The following two conditions follow from (c): (d) $H\models_{\K_1}\psi$; (e) $Bel(x,H)\epsilon^+_{\K_1}K$ for some $H\in dom(\K_1)$.
From (c) and (b), the following two conditions follow: (f) $Bel(x,H')\epsilon^+_{\K_2}K'$ and (g) $HRH'$ for some $H'\in dom(\K_2)$.
From (g), (d) and (a), $H'\models_{\K_2}\psi$.
So, $K'\models_{\K_2}Bel(x,\psi)$.\\
($\Leftarrow$) Define $xRx'$ iff $m_{\K_1}(x)=m_{\K_2}(x')$, then we will show $R\in EB(\K_1,\K_2)$.
We only need to show that if $K\models_{\K_1}\varphi$ iff $K'\models_{\K_2}\varphi$, then $KRK'$ and $R\in EB(\K_1,\K_2)$ by induction on the complexity of $\varphi$. 
(i) $\varphi=p$: Assume that $K\models_{\K_1}p$ iff $K'\models_{\K_2}p$.
This satisfies the condition $l(K)=l(K')$.
(ii) $\varphi=Bel(x,\psi)$: Suppose that $K\models_{\K_1}Bel(x,\psi)$ iff $K'\models_{\K_2}Bel(x,\psi)$ and that if $x\models_{\K_1}\psi$ iff $x'\models_{\K_2}$, then $xRx'$ and $R\in EB(\K_1,\K_2)$.
$H\models_{\K_1}\psi$, $Bel(x,H)\epsilon^+_{\K_1}K$, and $H\models_{\K_1}\psi$ for some $H\in dom(\K_1)$ iff 
$H'\models_{\K_2}\psi$, $Bel(x,H')\epsilon^+_{\K_2}K'$, and $H'\models_{\K_2}\psi$ for some $H'\in dom(\K_2)$.
By the induction hypothesis, $HRH'$ and $R\in EB(\K_1,\K_2)$.$\dashv$
\par
The next corollaries show that Hyper-DRT reflects the observational equivalence of some basic fragments of dialogues.
\begin{Cor}
\begin{list}{}{\leftmargin=10mm \labelwidth=30mm}
\item[]
\item [{\it 1.}] $Hi?._A;Hi._B\equiv Hi?_B;Hi._A$,
\item [{\it 2.}] $Open_{A,B};p._A;Uh-huh._B\equiv Open_{A,B};p?_B;Yes._A$,
\item [{\it 3.}] $Open_{A,B};p?_A;yes._B\equiv Open_{A,B};p?_A;p??_B;yes_A;yes_B$\\
$\equiv Open_{A,B};p?_A;yes._B;Really?_A;yes._B \equiv Open_{A,B};p?_A;Huh?_B;p?_A;yes._B$
\end{list}
\end{Cor}
\par
{\it Verification}. Directly from Proposition \ref{Form1}, Proposition \ref{Form2}, and Theorem \ref{main}.
In particular, the Hyper-DRS of dialogue 2 is roughly
$\K=\{Bel(x,K_0)\epsilon^+K_0,$
$Bel(y,K_0)\epsilon^+K_0,$
$Bel(y,K_1)\epsilon^+K_0,$
$Bel(y,K_2)\epsilon^+K_0,$
$Bel(x,K_2)\epsilon^+K_2,$
$Bel(y,K_2)\epsilon^+K_2,$
$Bel(y,K_1)\epsilon^+K_2,$
$p'\epsilon^+K_1\}$, 
which is dif-ferent from the other dialogues of which Hyper-DRS is roughly
$\K'=\{Bel(x,K_0)\epsilon^+K_0,$
$Bel(y,K_0)\epsilon^+K_0,$
$Bel(y,K_1)\epsilon^+K_0,$
$p'\epsilon^+K_1\}$, 
$K'\equiv K$.$\dashv$
\section{Comparison with the Other Formal Semantics}\label{comp}
From the viewpoint of shared beliefs formed in dialogues, we can classify formal theories of the semantics of dialogues into the following four classes: 
\begin{itemize}
\item Non-Belief-Based Semantics: theories containing no formalization of each conversant's non-nested belief,
\item Distributed Belief Semantics: theories containing only formalization of each conversant's non-nested belief, but no formalization of shared beliefs,
\item Shared Belief Semantics: theories containing formalization about shared beliefs but no update mechanism corresponding to processes of dialogues,
\item Belief-Sharing Semantics: theories containing formalization about shared beliefs and an update mechanism of them corresponding to processes of dialogues.
\end{itemize}
\cite{Gei95}'s version of DRT concentrates only on the dynamicity of speech acts in dialogues, and therefore it is a Non-Belief-Based Semantics.
Kamp's (1991) version of DRT\<\footnote{
Kamp analyzes the informational content of an utterance $p$ of a conversant $s$ to another conversant $h$ as:
$Cont(Cont(h,Bel(s,p))\To Bel(h,Bel(s,p)))\To Bel(Cont(h,Bel(s,p))\To Bel(h,Bel(s,p)))$, where $Cont(x,p)$ represents $x$'s contemplation of $p$, `$Cont(x,p)\To Bel(x,p)$' represents $x$'s implicit belief, and the agent of the outermost operator is $s$.
Namely, by an utterance the conversants' cognitive states change to a state with implicit beliefs of the utterance's content.
About shared beliefs, Kamp accounts for the infinite nesting of the shared belief with implicit beliefs and inference.
}, van Eijck and Cepparello's (1994) version of Dynamic Semantics\< \footnote{
For example, given a set of possible worlds $W$, dialogue ``A: p. B: OK.'' has the following denotation
$$
\lden (a:p);(b:ok;\Lambda)\rden(X,Y)=
\left\{
\begin{array}{ll}
(\lden p\rden(X),\lden p\rden(Y)) & \mbox{ if }X=\lden p\rden(X)\\
(\emptyset,\lden p\rden(Y)) & \mbox{ if }X\neq\lden p\rden(X)\\
\end{array}
\right.
$$
where $X\subseteq W$ is $a$'s state, $Y\subseteq W$ is $b$'s state,
and $\lden p\rden(X)=X\cap V(p)$.
Namely, $p$ holds at $a$ and $b$'s result states of the dialogue.
This is not a belief sharing, but shows that the same proposition is distributed over agent $a$ and $b$.
}, and Ginsburg's (1996) version of Situation Semantics\<\footnote{
Ginsburg proposes a model of a dialogue participant $DP$ which consists of two parts: an unpublicized mental situation and a gameboard configuration $GB$ which consists of facts, question under discussion $QUD$, and the content of last move made.
$GB$ can be seen as the shared belief formed during a dialogue.
However, $GB$ has no circular structure, and no formalization of shared belief.
Rather, these devices are made to account for the (topical) structures of dialogues.
}
 are basically distributed belief semantics.
Kamp's (1990) version of DRT\<\footnote{The representation:
$
Shared({\bf x}''',{\bf y}'''\},a,i):\vline\hspace{-1mm}
\begin{array}[c]{l} \hline 
{\bf x}'''\; {\bf y}'''\\
\hline
{\bf x}'''\mbox{ is more massive than }{\bf y}'''\\
\hline
\end{array} \vline 
$
 is introduced in order to represent definite references between conversants, but no semantics for the representation is given.
}
is a shared belief semantics only in its treatment of definite reference.\<\footnote{
As for Dynamic Semantics, Groeneveld's (1994) approach to circular propositions can be applied to the dynamic semantics of dialogues as belief sharing by extending his original language as follows:
$$(\downarrow\bf{Bel(a,this\wedge p))\wedge Bel(b,this\wedge p)}.$$
However, this formula is not semantically equivalent to the desired formula:
$$(\downarrow\bf{Bel(a,this\wedge p)\wedge Bel(b,this\wedge p))},$$
since scope indicator $\downarrow$ cannot take scope dynamically.
\par
Gerbrandy and Groeneveld's (1997) Dynamic Epistemic Semantics (DES) can also be applied to the semantics of dialogues with some extension.
In DES, the formula $[\phi]_C\varphi$ means that an update of group $C$'s information with formula $\phi$ results in a situation where $\varphi$ is true.
We can extend DES formulas to express dialogues, for example, $[\phi?_A;yes_B]_{A,B}S_{A,B}Bel(B,\phi)$.
In the original DES, this is expressed as $[Bel(B,\phi)]_{A,B}S_{A,B}Bel(B,\phi)$.
That is, we only have to define a translation procedure from dialogues to formulas of the form $[,]_{A,B}$.
Then, we have two problems: (i) the validity of $[\phi]_CS_C\phi$; (ii) the undefinability of each move in a dialogue.
\cite{GG97} do not define the semantics of $S_C\varphi$ explicitly.
So, problem (i) can be solved if the semantics can be defined.
On the other hand, (ii) is crucial for applying DES to the semantics of dialogues.
DES (or its extension) can provide semantics to complete dialogues, but not to each move.
This is basically same as for van Eijck and Cepparello's (1994) approach.
}
On the other hand, the approach presented here belongs to the class of belief sharing semantics, and can account for the update corresponding to each move in a dialogue.
\section{Conclusion}\label{conc}
In this paper, we have developed a formal semantics of dialogues, {\it Hyper-Discourse Representation Theory}, which treats dialogues as belief sharing.
There are three aspects to this treatment: Dialogues are analyzed as (i) shared belief formations/revisions, (ii) compositional, and (iii) processes whose identity can be established from the formed shared beliefs.
Point (i) is handled by the proposal of Hyper-DRSs of which semantics depends on Hyperset Theory which can formalize shared beliefs with finite means, although any shared belief is an intrinsically infinite object.
Point (ii) is handled by the proposal of a Construction Algorithm, a Construction Rules of Hyper-DRSs and the design of Hyper-DRSs so as to be easy to update.
Point (iii) is handled by epistemic bisimulation of Hyper-DRSs which reflects observational equivalence of dialogues.
\section*{Acknowledgements}
I would like to thank Prof. Jun'ichi Tsujii, Roland Steiner, Kazushige Terui, Makoto Kanazawa, Nigel Collier and Emily Bender for their advice, comments and help.
I would also like to thank the anonymous reviewers for helpful and detailed comments on the preliminary version of the paper.


\bibliographystyle{nlpbbl}
\bibliography{v06n4_05}

\begin{biography}

\biotitle{}

\bioauthor{緒方　典裕(正会員)}
{
1988年東京学芸大学教育学部初等教育国語科卒業. 1997年筑波大学大学院文芸・言語研究科満期退学. 1997年-1999年, 日本学術振興会特別研究員PD. 言語学修士.
1999年, 大阪大学言語文化部講師. 自然言語の形式談話理論とその自然言語処理への応用が研究内容. 日本人工知能学会会員.
}

\bioreceived{Received}
\biorevised{Revised}
\bioaccepted{Accepted}

\end{biography}
             
\end{document}

