%%%%%
%%%%%  THIS FILE MUST BE CALLED structural-relations.tex
%%%%%

\documentstyle[basics,amssymbols,st]{article}

\newcommand{\App}{\ob{App}}
\newcommand{\Abs}{\ob{Abs}}
%\newcommand{\Si}{\Sigma}
\newtheorem{axth}{A}
\renewcommand{\ax}[2]{\begin{axth}\labelp{ax.#1} #2\end{axth}}
\newcommand{\Neg}{\ob{Neg}}
\newcommand{\Pos}{\ob{Pos}}
\newcommand{\NegOf}{\ob{NegOf}}
\newcommand{\Approp}{\ob{Approp}}
\newcommand{\Sbs}[3]{[#1\mapsto #2].#3}
\newcommand{\pnt}{\phi}

%
%% the definitions below need to go in one of the .sty files
%%%
%%%%

\newcommand{\EE}{{\cal E}}
%\newcommand{\pow}{{\cal P}}
\newcommand{\support}{{\it supp}}
\newcommand{\UU}{{\cal U}}
\newcommand{\Vafa}{V_{\it afa}}

\begin{document}



\section{A Theory of Structural Relations}
\label{section-structural-relations}

Information processed, inferred, conveyed, expressed, or otherwise
represented need not be of the simple kind considered in the previous
section; it may come in larger, more complex chunks.

Logical complexes present an obvious example: we need to be able to
model conjunctions, disjunctions, and perhaps negations of infons.
However, even with the first item on the list there is a potential
problem.  The identity condition for (well-founded) basic infons was
very clear: $\sigma$ and $\tau$ are identical if and only if they have
the same relation, and the same arguments filling the same roles.
It is much less clear what should be said about conjunctions.  A
strong condition, analogous to the one for basic infons, would be that
$\sigma_1\wedge\tau_1$ is identical to $\sigma_2\wedge\tau_2$ if and
only if $\sigma_1$ is identical to $\sigma_2$ and $\tau_1$ is
identical to $\tau_2$.   The problem arises if we combine this
condition with natural logically-motivated requirements on
conjunction, such as commutativity, associativity  and idempotence.
Then the condition becomes too strong.  For example, consider an
arbitrary conjunction $\sigma\wedge\tau$.  By idempotence,
$\sigma\wedge\tau=(\sigma\wedge\tau)\wedge(\sigma\wedge\tau)$, and so, by
the above condition, $\sigma=\sigma\wedge\tau=\tau$.

The heart of the problem is an inherent tension in the concept of
information.  On the one hand, information is {\em representation-independent}:
the same information may be represented
in many different ways.  On the other hand, information is {\em
fine-grained}: two pieces of information may be logically equivalent
without being identical.  Consequently, the identity conditions for
information represented by complex signs must lie somewhere
between those for the syntactic form of the sign and those for its
semantic content.  Striking the right balance is, in general, very
difficult.

Another problem is that there has been little agreement as to which
combinations of infons are needed.  Finite conjunction
and disjunction are commonly adopted;
infinite conjunctions and disjunction, quantified infons (with variable
binding), various negations and conditionals, have also been proposed; and
for applications in computer science other forms may be found useful---
for example, is not clear that the information stored as a
list is simply a conjunction of the items of information stored in each cell,
and even if it is some kind of conjunction, it is not clear that it is the same
conjunction as expressed by an unordered set of the same items.

In view of the above, it would seem sensible to pursue a fairly
open-minded policy about complex infons.  The approach adopted here
is intended to cover various proposals made in the literature, as well
as offering a framework in which other approaches may be tried.

\subsection{Extensional Structures}
\label{sec.extensional-structures}

Our idea is to generalize the notion of bisimulation to apply in a
wider context.  In the sequel, we will  have (relational) structures
of type
$$\relstr{A, S_1, \ldots, S_m; R_1, \ldots, R_n}$$
The relations in the first group, $S_1$, $\ldots$, $S_m$, are called
{\em structural relations} because they capture
the structure of elements of the domain.  A structural relation $S_i$
of arity $n+1$ is  to be thought of as relating a list of $n$ objects
to a single  structured object.  If $S_i(x_1,\ldots,x_n,y)$ then
$y$ is a structured object with components
$x_1,\ldots,x_n$, which may or may not be structured themselves.

More generally, we say that  $b$ is a {\em component} of
$a$  in $\goth{A}$ if there is a structural relation $S_i$ of
arity $n+1$ and elements $x_1,\ldots,x_n$ of $A$ such that
$S_i(x_1,\ldots,x_n,a)$ and $x_j=b$ for some $1\leq j\leq n$.
For technical reasons, we require that the number of components of
any is not a proper class---that is to say, the class of all components
of a given object can be placed in one-to-one correspondence with
some set. An object  $a$ is an  {\em atom} of $\goth{A}$ if
it has no components.

In an information structure, the only structured objects are the
infons. Relations, roles and ordinary objects are all atomic, but
infons have a component structure captured by the relations $\Rel$
and $\Arg$. These are the structural relations of information
structures.   Information structures have no other primitive
relations, but the  defined relation $\partof$ is an example of a
non-structural relation---albeit one whose extension is determined by
the structure of infons.   The important distinction between  $\Rel$
and $\Arg$, on the one hand, and
$\partof$, on the other, is that the identity of infons is determined
by the former, by virtue of adherence to Axiom~\axref{bisim}.

But now consider an arbitrary relational structure. What conditions
must  a relation  satisfy to qualify as a structural relation? Our
answer is based on the following definition.

\begin{defn}\labelp{bisimulation-defn}
Given a relational structure $\goth{A}$ of type
$$\relstr{A, S_1, \ldots, S_m; R_1, \ldots, R_n},$$
a binary relation $E$ on $A$ is said to be a
{\em bisimulation} on
$\goth{A}$ if for all $a,b\in A$, if $E(a,b)$
then the following three conditions hold:
\begin{enumerate}
\item if $a$ is atomic then $a = b$,
\item for $1\leq i\leq m$,  if $\nu_i = k$, then for all
$y_1,\ldots,y_k$ such that $S_i(y_1,\ldots,y_k,a)$, there are
$z_1,\ldots,z_k$ such that $S_i(z_1,\ldots,z_k,b)$, and $E(y_j,z_j)$ for
$1\leq j\leq k$, and
\item $E(b,a)$
\end{enumerate}
$a$ is {\em bisimilar} to $b$ in $\goth{A}$ iff
there is a bisimulation $E$ of $\goth{A}$ such that
$E(a,b)$. \label{defn.extensional}
The structure $\goth{A}$ is {\em extensional} if it has
no distinct, bisimilar objects, i.e. if  $a$ is bisimilar to $b$
in $\goth{A}$ then $a = b$.
\end{defn}


If two objects are bisimilar then they are structurally equivalent,
so there must be something else that distinguishes them. But if they
are structural objects, then there can be nothing else to distinguish
them.   In this way, the extensionality condition enforces
structural conditions of identity on the non-atomic objects of
the domain, with the structure of an object determined solely
by the relations structural relations. The non-structural relations, $R_1,
\ldots, R_n$, on the other hand, are
not constrained in any way. They are used to model additional facts
about the objects of the domain, which need not be dependent on their
structure alone.

Extensional structures will be used throughout the rest of this
chapter to model a variety of situation-theoretic objects.
Our strategy will be to define different kinds of extensional
structures to model different parts of the situation-theoretic
universe, but to do so in a modular fashion.  The modularity is
facilitated by the notion of a `sort'.

\begin{defn}
If $\goth{A}$ is an extensional structure, then for
each structural relation $S$ of $\goth{A}$, let
 $S^*$ be the class of those objects $a$
such that $S(\vec{x},a)$ in $\goth{A}$ for some
sequence $\vec{x}$ (possibly empty) of elements of $\univ{\goth{A}}$.
In other words, $S^*$ is the projection of $S$ along
its last co-ordinate.  We call these classes the
{\em (structural) sorts} of $\goth{A}$.
\end{defn}

Every generalized information structure is an extensional structure
with structural relations $\Rel$ and $\Arg$. This is given by
Axiom~\axref{bisim}. The standard structures and even the iterated
structures are also well-founded, by Axiom~\axref{foundation}. In a
standard information structure
$\Rel^*=\Arg^*$ is the class of infons, the only structured objects. In
generalized information structures, $\Rel^*$ and $\Arg^*$ may be
slightly different if there are infons with a relation but no arguments
or with arguments but no relation.  In any case, the class of infons is
$\Rel^*\cup\Arg^*$.  The relations, roles and ordinary objects are all
atoms.


Another, familiar example of an extensional structure is
the structure $\goth{V}=\tuple{V,\in^2;}$ where $V$ is the class of
all sets, and $\in$ is the binary relation of membership.
The class $\in^*$ consists of all non-empty sets.  Extensionality is
assured by the set-theoretic axiom of the same name, together with
the axiom of Foundation or Anti-foundation, depending on whether
$V$ is assumed to satisfy the axioms of well-founded or anti-founded
set theory.

\begin{defn}
An extensional structure $\goth{A}$ of of type
$\relstr{A,\Set^1,\in^2;}$ is called a {\em set structure} if
$\in^*\subseteq\Set^*$ and $\goth{A}$ satisfy the
axioms of ZFC$^-$ with quantifiers restricted to $\Set^*$.
\end{defn}

The ambiguity in our use of the word `set' and the predicate `$\in$'
is of the now familiar kind.  Internal sets are those elements of the
structure in $\Set^*$, which may or may not be (external) sets.   But
for any internal set $a$, we may define a corresponding external set
$a^*=\set{b}{\in(b,a)}$.


Our third example of an extensional structure presents functions as
structured objects whose components are their arguments and values.

\begin{defn}
An extensional
structure  $\goth{A}$ of type
$\relstr{A,\App^3,\Fun^1;}$ is a {\em function structure} if
$\App^*\subseteq\Fun^*$ and for all $\al,x,y$ and $i$ in $A$,
if $\App(i,x,\al)$ and $\App(i,y,\al)$,  then $x=y$.
\end{defn}

If $\al\in\App^*$ then $\al$ is an (internal) function of
$\goth{A}$.  We associate it with an external function $\al^*$ whose
domain consists of those elements $i$ of $A$ for which there
is an $x$ such that $\App(i,x,\al)$. For each such $i$, $\al^*(i)=x$,
which is uniquely specified, by the defining condition of function
structures.



What is the import of the extensionality requirement
on function structures?   It amounts to the
condition that different internal functions represent
different external functions.  For if $a^* = b^*$,
then $I_A \cup \{\tuple{a,b},\tuple{b,a}\}$ would be a bisimulation
relating $a$ and $b$.   If the structure is {\em flat}
(i.e., if no function is also  an argument),
then extensionality is equivalent to this condition.
In other structures, extensionality is  a stronger condition.


\subsection{Structural Types}
\label{section-afa}
\label{section-AFA}


In any extensional structure, one can identify a non-atomic  object
by listing its structural relationships with other objects. Suppose
$\goth{A}$ is an extensional structure and $x$ is an  object
not necessarily in $\univ{\goth{A}}$, which we call a {\em
parameter}. A {\em unary structural type} in $\goth{A}$ is a pair
$\tuple{x,T_x}$  where $T_x$ is a set of tuples of the form
$\tuple{S,b_1,\ldots.b_k}$  such that
$S$ is a structural relation of $\goth{A}$ of arity $k+1$ and
$b_1,\ldots,b_k$ are elements of $\univ{\goth{A}}\cup \{x\}$.

Now, if $T=\tuple{x,T_x}$ is a unary structural type and $a$ is an
object  of $\goth{A}$, let $a.T$ be the set of tuples of the form
$\tuple{S,b_1',\ldots.b_k'}$ such that $\tuple{S,b_1,\ldots.b_k}$ is
in $T_x$ and for $1\leq j\leq k$, $b_j'=a$ if $b_j=x$ and $b_j'=b_j$
if $b_j\neq x$.  An object  $a$ of $\goth{A}$ is {\em of type}
$T$ if for each structural relation $S$ of arity $k+1$,
and each sequence $b_1,\ldots b_k$ in $\univ{\goth{A}}$,
\begin{quote}
$S(b_1,\ldots b_k,a)$ in $\goth{A}$ \quad iff \quad
$\tuple{S,b_1,\ldots b_k}$ is in
$a.T$
\end{quote}
For example,  in an information structure the infon
$\si=\infon{r;i:\si,j:a}$ is of type
$$T \quadeq \tuple{x,\{ \tuple{\Rel,r}, \tuple{\Arg,i,x},
\tuple{\Arg,j,a}\}}$$
because $\si.T=\{ \tuple{\Rel,r}, \tuple{\Arg,i,\si},
\tuple{\Arg,j,a}\}$ and $\Rel(r,\si)$, $\Arg(i,\si,\si)$, and
$\Arg(j,a,\si)$; and these  are all the structural relationships
in which $\si$ participates.

Every object $a$ is of some type, for example, the type
$\tuple{a,T_a}$ where $T_a$ is the  set of tuples of the form
$\tuple{S,b_1,\ldots b_k}$ such that
$S(b_1,\ldots b_k,a)$ in $\goth{A}$.\footnote{$T_a$ cannot be
a proper class because we have assumed that every object has only a
set-sized class of components.} Also, by extensionality,
no two objects are of the same type. So the type of an object serves
as its unique identifier.  However, there are many more types than
there are objects of those types; many structural types  are
uninstantiated.  We may use this  idea to give some measure of how
rich our ontology is, and to express principles of existence.

\begin{defn}\label{defn.structural-type}
Suppose $\goth{A}$ is an extensional structure.
A {\em structural type} $T$ in $\goth{A}$ is an indexed family
$\{T_x\}_{x\in X}$  of sets $T_x$ of tuples of the form
$\tuple{S,b_1,\ldots.b_k}$  such that $S$ is a structural relation of
$\goth{A}$ of arity $k+1$ and $b_1,\ldots,b_k$ are elements of
$\univ{\goth{A}}\cup X$. The elements of the index class $X$ are
called {\em parameters}.   Given a mapping $s$ from $X$ to
$\univ{\goth{A}}$ let $s.T$ be the family of sets $s.T_x$
of tuples of the form
$\tuple{S,b_1',\ldots.b_k'}$ such that $\tuple{S,b_1,\ldots.b_k}$ is
in $T_x$ and for $1\leq j\leq k$, $b_j'=s(b_j)$ if $b_j$ is in $X$
and $b_j'=b_j$ if $b_j$ is not in $X$.  The mapping $s$ {\em
instantiates} $T$ if for each $x$ in $X$, $s(x)$ is of the unary type
$\tuple{s(x),s.T_x}$.\footnote{For typographical convenience,
we sometimes indicate applications by subscripts  (as in $T_x$)
and sometimes by using parentheses.}
\end{defn}

To see how this definition works, it is helpful to consider the
special case of set structures.  A set $a$ is of unary type
$T=\tuple{x,T_x}$ iff $T_a=\set{\tuple{\in,b}}{\mbox{$b$ in
$a^*$}}\cup\{\tuple{\Set}\}$.  Thus if we define
$T_a^*=\set{b}{\mbox{$\tuple{\in,b}$ in $T_a$}}$, then
$a$ is of type $T$ iff $a^*=T_a^*$.  Likewise, if $T$ is a
(polyadic) structural type, then $s$ instantiates $T$ iff
$s(x)^*=(s.T_x)^*$ for each parameter $x$ of $T$. We can therefore
think of a  structural type in a set structure as a system of
simultaneous equations, which is instantiated by a mapping
of parameters to sets that {\em solves} the equations.   For example,
consider the system of equations shown on the left below.

$$\begin{array}{lc|cl}
\begin{array}{lcl}
x & = & \{y,z\} \\
y & = & \emptyset \\
z & = & \{x,a\}
\end{array}
& \qquad  & \quad  & 
\begin{array}{lcl}
T_x &  = & \{ \tuple{\in,y}, \tuple{\in,z}  , \tuple{\Set}\} \\
T_y &  = & \{ \tuple{\Set}\} \\
T_z &  = & \{ \tuple{\in, x}, \tuple{\in, a} , \tuple{\Set}\} \\
\end{array}
\end{array}
$$
Here $a$ is some arbitrary object (perhaps not a set).
Now this system corresponds to the structural type shown
on the right.  Suppose that $s$ instantiates that type.
Then $s(x)$, $s(y)$, and $s(z)$ are sets, and 
$$\begin{array}{lcl}
s(x) & = & \{s(y), s(z)\} \\
s(y) & = & \emptyset \\
s(z) & = & \{s(x),a\}
\end{array}
$$
In other words, $s$ is a {\em solution} to the system of equations.

Now we can see why the Foundation Axiom precludes the existence
of instantiations of structural types: if $s$ exists,
then we get an infinite descending  sequence of arguments:
$$ s(x) \quad \ni \quad s(z) \quad \ni \quad \cdots 
\quad \ni \quad s(x) \quad \ni \quad s(z) \quad \ni \quad \cdots
$$



\begin{defn}
$\goth{A}$ is {\em well-founded} if there is no infinite sequence
$a_1,a_2,\ldots$ of elements of $A$ such that $a_{n+1}$ is a component
of $a_n$ for each positive integer $n$.

$\goth{A}$ is {\em structurally saturated}  if every structural
type in $\goth{A}$ is instantiated.
\end{defn}


Recall that we mentioned AFA in Section~\ref{section-circularity}.
We did not state AFA at the time, but we can do so now.

\begin{defn}
AFA is the statement that the universe
of sets $\goth{V} = \tuple{V,\in^2,\Set^1}$
is an  structurally saturated, extensional set structure.
\end{defn}


An equialent (and more standard)
 formulation of AFA is that all systems of equations involving sets
have  unique solutions.  Such systems are given by a 
set $X$ together with a map $e$  from $X$ to $X\cup V$.
A solution to a system is an instantiation of the corresponding
structural type.
As it happens, AFA implies that more general systems of equations
have solutions.  
Consider $X = \{x,y\}$ and
$$\begin{array}{lcl}
e(x) &   = & \{\tuple{x,y}\} \\
e(y) & = & \{x,y,\emptyset\} \\
\end{array}
$$ 
This system is unlike the ones we've seen so far because $e(x)$
contains the {\em ordered pair} $\tuple{x,y}$.  However,
in set theory, this pair is standardly taken to be
$\{\{x\},\{x,y\}\}$.  So when we want to solve a system involving
pairs, we add more variables to $X$ and more equations.
Here we would take $X' = \{x,y,z_0, z_1, z_2\}$ and
$$\begin{array}{lcl}
e(x) &   = & \{z_0\} \\
e(y) & = & \{x,y,\emptyset\} \\
e(z_0) & = & \{z_1,z_2\} \\
e(z_1) & = & \{x\}\\
e(z_2) &  = & \{x,y\}\\
\end{array}
$$ 
A solution to the expanded system gives us a solution
to the original system.  This would be a map $s$ defined
on $X$ with the property that $s(x) = \{\tuple{s(x),s(y)}\}$
and $s(y) = \{s(x),s(y),\emptyset\}$.



\begin{thm}
Every extensional structure $\goth{A}$
 is isomorphically embedded in a
structurally saturated extensional structure $\goth{B}$.
\label{thm-str-sat}
\label{thm.sat-extn} 
\end{thm}



\begin{proof}
Our proof here uses AFA.  With each structural relation
$S$ of $\goth{A}$, we associate some  urelement $z_s$.
We also may associate an urelement $z_a$ with every atom of $\goth{A}$.
We assume that the association is one-to-one, and also
that none of these $z$'s occurs in the support of $\goth{A}$.
Let $U$ be the collection of all  these  new  urelements.





For each structural type $T$ we associate a
system of equations $\EE(T)$ as follows:
The set $X$ of parameters of $X$ serves as the set
of  variables for $X$.  For each $x\in X$,
$e_t$ is  $T_x$, with each structural relation $S$
replaced by the  corresponding $z_s$.
Each $\EE(T)$ is a system of equations involving tuples, 
something close to what we have seen above.


By AFA, each $\EE(T)$ has a unique instantiation, say $s(T)$.
Let
$$B \quad = \quad
\{ s(T)_x : T \mbox{ a structural  type and $x$ is a parameter of $T$}\}.$$
We'll see how to interpret the relations
of $\goth{A}$ on this set to get
the desired structure $\goth{B}$.  But first, we
need a  subsidiary fact on structural types.

Recall  that each $a\in A$ satisfies a type $T_a$
in one variable  $x$.
Let $i : A \rightarrow B$ be given by $i(a) = s(T_a)_x$
for $a$ a non-atom of $\goth{A}$, and $i(a) =z_a$ if $a$ is an atom.
 Then  is
one-to-one: if $s(T_a)_x = s(T_b)_x$, then we could get
a bisimulation relation on $\goth{A}$ relating $a$ and $b$.
Since $\goth{A}$ is extensional, we would  have $a = b$.
And if $a$ is a non-atom, then $i(a)$ is  a set, so
it cannot equal $i(b) = z_b$ for $b$ a non-atom

Now we can see how  to make $B$ into a structure $\goth{B}$
of the same type as $\goth{A}$.  Let $S$ be a structural
relation.  We interpret it by
$$ S_{\goth{B}}(c_1,\ldots,  c_n,c)
\quad \mbox{iff} \quad \tuple{z_S, c_1, \ldots, c_n} \in c .$$
The definition of
the principal types $T_a$ implies that
$$ S_{\goth{A}}(b_1, \ldots,  b_k, a) \quad \mbox{iff} \quad
S_{\goth{A}}(i(b_1), \ldots,  i(b_k), i(a)).$$
The non-structural relations extend to the image
of $\goth{A}$ via the isomorphism;
we'll say that   on tuples outside
the image of $i$, each non-structural relation is false.

At this point we have $\goth{B}$.
This structure is extensional by AFA.
A   bisimulation of structures relating $c$ and $c'$
would give us a bisimulation of {\em sets} doing
the  same thing.  And according to AFA, bisimilar sets
are equal.

Finally, we sketch a proof that $\goth{B}$ is structurally
saturated.
Before we do this, we need to recall that
for each $c\in B$ there
is a structural type  $T_c$ over the original $\goth{A}$ and
a parameter $x$ of $T$ such that $s(T)_x = c$.
 Let $T'$ be a structural type in $\goth{B}$.
Now each $T_y$ may contain elements $c\in \univ{\goth{B}}$.
However, we may simply replace each such $c$ by a new urelement
(say $z_c$) and then  adjoin all of the
structural types $T_c$ to $T$.  Of course, we  must use
new  parameters to  do this.  In this way, $T'$ is
equivalent to a structural type in the original $\goth{A}$.
So by definition of $\goth{B}$, there is some $a\in\univ{\goth{B}}$
instantiating $T'$.
\end{proof}

\begin{cor}
Every extensional simple information structure 
 can be extended to an extensional structure in which
Axiom~\axref{afafull} holds. 
\end{cor}

\subsection{Partiality and order}
\label{section-partiality}


We have seen how infons may be ordered according by their arguments and
relations, enabling us to model the partiality of information. In fact,
the definition of $\partof$ is quite general.

\begin{defn}
Given an extensional structure $\goth{A} :
\relstr{A,S_1,\ldots,S_m;R_1,\ldots,R_n} $,
we define a relation $\partof$
on the non-atomic elements of $A$ as follows:
 $a\partof b$ if for $1\leq i\leq m$,  and each sequence
$\vec{x}$ of appropriate length, if $S_i(\vec{x},a)$ then
$S_i(\vec{x},b)$.
\end{defn}


For information structures, the definition of $\partof$ agrees with our
previous definition. For set structures,
\begin{quote}
$a\partof b$ iff $a^*\subseteq b^*$
\end{quote}
and for function structures, it is the usual order on partial functions:
\begin{quote}
$f\partof g$ iff each $i$ in the domain
of $f^*$ belongs to the domain of $g^*$ and $f^*(i)=g^*(i)$.
\end{quote}
In these examples, and in the general case, $\partof$ is a partial
order on structured (non-atomic) objects. It is clearly reflexive and
transitive, and anti-symmetry follows from extensionality.\footnote{If
$a\partof b$ and $b\partof a$ then the union of
$\{\tuple{a,b}, \tuple{b,a}\}$ and the identity relation is a
bisimulation of $\goth{A}$, and so $a=b$.}


Other ordering of structured objects are possible and have been
studied extensively.  The most important of these is the `hereditary'
order, which takes into account the order of components. Roughly, an
object $a$ is a hereditary part of $b$ if for every component $a'$ of
$a$ there is a component $b'$ of $b$ such that either $a'=b'$ or $a'$ is
a hereditary component of $b'$.  Stated thus, the definition is
circular.  In some cases we can  rectify this problem using an inductive
layering of the domain. Say that an object is of order
$0$ if it is atomic, and of order $n+1$ if it has a component of order $n$
but no
components of order greater that
$n$.  This enables us to give a recursive definition of the hereditary
order on objects of order $n$ in terms of the hereditary order of
objects of order less than $n$.

This strategy works for well-founded structures, in which every
object has an order. But in structures with a `circular' component
relation there are objects which do not have an order.  This is a
ubiquitous problem in the study of circular phenomena.  The solution is
as follows. First, we regard the `definition' of the order as an
operation on binary relations. Given one binary relation $R$, we let
$R^+$ be defined by
\begin{quote}
$R^+(a,b)$ if for every component $a'$ of
$a$ there is a component $b'$ of $b$ such that either $a'=b'$ or
$R(a',b')$.
\end{quote}
Now, the operation taking $R$ to $R^+$ is {\em monotone}: if
$R\subseteq S$ then $R^+\subseteq S^+$.  A basic result of the theory
of order is that every monotone operation has a {\em greatest fixed
point}. In other words, there is an $R$ such that $R^+=R$ and for any
$S$ such that $S^+=S$, $S\subseteq R$.\footnote{This
observation generalizes to any preorder (reflexive and transitive
relation). If $<$ is a preorder and $F$ is a monotone operation  on $<$
(if $x<y$ then
$F(x)<F(y)$) then there is an $x$ such that $F(x)=x$ and for all $y$
if $F(y)=y$ then $y<x$.} This observation enables to define the
hereditary order in the general case as follows.


\begin{defn}
The {\em hereditary order}, $\partof^h$,
on $\goth{A}:\relstr{A,S_1,\ldots,S_m;R_1,\ldots,R_n}$ is
the largest binary relation between non-atomic objects of
$\goth{A}$ such that if $a\partof^h b$ then for $1\leq i\leq m$, if
$S_i(x_1,\ldots,x_k,a)$ then  there are $y_1,\ldots,y_k$ such that
$S_i(y_1,\ldots,y_k,b)$ and
$x_j\partof^h y_j$ for each $1\leq j\leq k$.
\end{defn}

The hereditary order is also a partial order on non-atomic objects for
the same reason that $\partof$ is.  Other orders may be obtained by
defining different monotone operations.

It is important to realize that both $\partof$ and $\partof^h$ are
purely structural concepts. In the case of simple infons, if
$\si\partof\ta$ then it is possible to go further and interpret the
order in terms of epistemological advantage: knowing $\si$ is not as
valuable as knowing $\ta$. However, this gloss is not available in the
general case.  For example, in Section~\ref{section-complex-infons} we
shall show how to obtain a disjunction
$\si_1\vee\si_2$ whose components are  $\si_1$ and $\si_2$, and such
that $\si_1\vee\si_2\partof\si_1\vee\si_2\vee\si_3$.


The discussion of unification in information structures may  also be
generalized, although no uniform definition of compatibility is
available.  Instead, we may introduce the following abstract version.

\begin{defn}
A relational structure
$$\goth{A} : \relstr{A,S_1,\ldots,S_m;R_1,\ldots,R_n,C^2,P^2}$$
 is a {\em unification structure} with {\em order $P$} and {\em compatibility
relation $C$} if
\begin{enumerate}
\item $\goth{A}$ is extensional,
\item $C$ is symmetric and reflexive on non-atoms,
\item $P$ is a partial order of non-atoms, and
\item If $C(a,b)$ then $a$ and $b$ have a least upper bound in $P$.
\end{enumerate}
\end{defn}

For example, taking $C(\si,\ta)$ iff $\si$ and $\ta$ are compatible
simple infons, and $P(\si,\ta)$ iff $\si\partof\ta$, we see that
generalized information structures are unification structures; for
set structures, take $P$ to be $\partof$ and $C$ to be the
universal relation on $\Set^*$---the unification of any two sets is just
their union; and for function structures with $P$ taken to be the
$\partof$ order, let $C(f,g)$ iff there is no
$i$ in the domains of both $f^*$ and $g^*$ and such that $f^*(i)\neq
g^*(i)$. The hereditary orders may also be used to define unification
structures with weaker, hereditary compatibility relations.


\subsection{Complex Infons}
\label{section-complex-infons}
\label{sec.complex-infons}

We have seen that infons, sets and functions may all be modelled using
extensional structures.  In each of these cases, the identity conditions
are relatively straightforward. Now we shall show how structured
objects with more complicated identity conditions can also be modelled.

Suppose we wish to have a binary operation of conjunction with the
following properties:
\begin{enumerate}
\item[] (commutativity) $\si\wedge\ta=\ta\wedge\si$,
\item[] (associativity)
$\si\wedge(\ta_1\wedge\ta_2)=(\si\wedge\ta_1)\wedge\ta_2)$, and
\item[] (idempotence) $\si\wedge\si=\si$.
\end{enumerate}
We shall suppose that we already have a stock of infons $\Si$ in
some information structure $\goth{A}$ from which to form conjunctions.
Our task is to extend $\goth{A}$ with new elements and relations
designed to capture the structure of the conjunctions.

The solution is to define a new binary structural relation $\ConjunctOf$
which holds between conjuncts and conjunction.  Using this relation
we can define the operation of conjunction as follows:
\begin{quote}
given infons $\si$
and $\ta$, the conjunction $\si\wedge\ta$ is the  least $x$ in the
$\partof$ order such that $\ConjunctOf(\si,x)$ and
$\ConjunctOf(\ta,x)$.
\end{quote}
In other words, $\si\wedge\ta$ is the structurally smallest conjunction
containing $\si$ and $\ta$ as conjuncts. Clearly any such
conjunction is commutative. Additional properties of
$\wedge$ may be imposed by careful construction of $\ConjunctOf$.  By
way of example, we shall show that it is possible to extend an
information structure with a conjunction which is
associative and idempotent, and another which has neither of these
properties.

\begin{con}\label{con.idem-assoc-conjunction}
Let $\goth{A}$ be an extensional structure with a class $\Si$ of
non-atomic objects, which we shall call `infons'. We
shall define  an extensional structure $\goth{B}$ extending
$\goth{A}$ with new elements and a new binary structural
relation $\ConjunctOf$ such that the conjunction
$\wedge$ defined, as above, on objects in $\Si$ is both associative and
idempotent.   Let
$$\begin{array}{lcl}
B_0 & = & {0}\times(\univ{\goth{A}}-\Si)\\
B_1 & = & {1}\times\pow(\Si)
\end{array}$$
and for each $a\in\univ{\goth{A}}$ let
$$a^*\quadeq\defbycases{\tuple{0,a} & \mbox{if $a\not\in\Si$} \\
\tuple{1,\{a\}} & \mbox{if $a\in\Si$}}.$$
Now let $\goth{B}$ be the structure with universe $B_0\cup B_1$, and
with
\begin{quote}
$R(a^*_1,\ldots,a^*_n)$ in $\goth{B}$ iff $R(a_1,\ldots,a_n)$ in
$\goth{A}$
\end{quote}
for each primitive relation $R$ of $\goth{A}$ and
\begin{quote}
$\ConjunctOf(\tuple{1,x},\tuple{1,y})$ iff $x\subseteq y$.
\end{quote}
The new relation $\ConjunctOf$ is treated as a structural relation of
$\goth{B}$ so we must check that $\goth{B}$ is extensional.\footnote{If $a$ is
bisimilar to $b$ then $a=\tuple{i,a_0}$, $b=\tuple{j,b_0}$ for some $a_0$ and
$b_0$.  First observe that $i=j$. For if $i\neq j$, say $i=0$ and
$j=1$, then $b_0$ is a subset of $\Si$, and so
$\ConjunctOf(\tuple{1,\emptyset},b)$ whereas there is no $x$ such that
$\ConjunctOf(x,a)$, and this contradicts the assumption that $a$ is
bisimilar to $b$.  In the case that $i=j=0$, $a_0$ is bisimilar to
$b_0$ in $\goth{A}$, so $a_0=b_0$ by the extensionality of $\goth{A}$, and
so $a=b$.  And if  $i=j=1$ then for every $x\in a_0$, there is a $b_1\subseteq
b_0$ such that
$\tuple{1,\{x\}}$ is bisimilar to $\tuple{1,b_1}$. Then  for each $y\in
b_1$,  $\tuple{1,\{y\}}$ is bisimilar to $\tuple{1,\{x\}}$---it cannot be
bisimilar to $\tuple{1,\emptyset}$, the only other conjunct of
$\tuple{1,\{x\}}$.  But then either $x$ and $y$ are atoms of $\goth{A}$,
which is ruled out because $x,y\in\Si$, or $x$ is bisimilar to
$y$ in $\goth{A}$ and so $x=y$ by the extensionality of $\goth{A}$. Thus
$b_1=\{x\}$ and so $a_0\subseteq b_0$. By a symmetrical argument, it can be
shown that $b_0\subseteq a_0$, so $a_0=b_0$ and so $a=b$.}
The binary conjunction $\wedge$ is defined, as above, for all
`infons', which in this case refers to those objects in $B_1$. Now for any
$x,y\subseteq\Si$, it is easily checked that
$\tuple{1,x}\wedge\tuple{1,y}=\tuple{1,x\cup y}$.  Thus conjunction is both
idempotent and associative in $\goth{B}$.
\end{con}

\begin{con}\label{con.non-idem-assoc-conjunction}
For the second construction, let $\goth{A}$ and $\Si$ be as before.  Let
$\Si_1=\{1\}\times\pow(\{0\}\times\Si)$,
$\Si_{(n+1)}=\Si_n\cup\{1\}\times\pow\Si_n$, and
$\Si^*=\bigcup^{\omega}_{n=1}\Si_n$.
Now let $\goth{B}$ be the structure with universe
$\Si^*\cup\{0\}\times\univ{\goth{A}}$, and with
\begin{quote}
$R(\tuple{0,a_1},\ldots,\tuple{0,a_n})$ in $\goth{B}$ iff $R(a_1,\ldots,a_n)$
in $\goth{A}$
\end{quote}
for each primitive relation $R$ of $\goth{A}$ and
\begin{quote}
$\ConjunctOf(x,\tuple{1,y})$ iff $x\in y$
\end{quote}
Again we must check that $\goth{B}$ is extensional.\footnote{The proof  requires
the notion of the `rank' of an element of $\univ{\goth{B}}$.  An element
$b\in\univ{\goth{B}}$ is of rank $0$ if $b=\tuple{0,a}$ for some
$a\in\univ{\goth{A}}$ and is of rank
$n>0$ if $b\in\Si_n$ but $b\not\in\Si_m$ for each $m<n$.   We show that  if
$a$ is bisimilar to
$b$ then $a=b$, by induction on the maximum of the ranks of $a$ and $b$.
Suppose that $a$ is bisimilar to $b$. There are three cases: (i) both $x$
and $y$ have rank $0$; (ii) one of $x$ or $y$ has rank $0$ and the other
has rank greater than $0$; and (iii) both
$x$ and $y$ have ranks greater than $0$.  Case (i) is the base of the
induction.  In this case, $a=\tuple{0,x}$ and $b=\tuple{0,y}$ for some $x$
and $y$, so $x$ is bisimilar to $y$ in $\goth{A}$, so $x=y$ by the
extensionality of $\goth{A}$, and so $a=b$.  Case (ii) is impossible.
Suppose, for example, that $a=\tuple{0,x}$ and $b=\tuple{1,y}$. Then
either $y$ is empty, making $b$ an atom of $\goth{B}$ which is only bisimilar
to itself, or $y$ has an element $y'$ and so $\ConjunctOf(y',b)$, whereas
there is no $x'$  such that $\ConjunctOf(x',a)$, contradicting the
assumption that $a$ is bisimilar to $b$.  Case (iii) is the inductive case.
We may suppose that $a=\tuple{1,x}$ and $b=\tuple{1,y}$ for some
$x$ and $y$. Then for each $x'\in x$ there is a $y'\in y$ such that
$x'$ is bisimilar to $y'$.  But the ranks of $x'$ and $y'$ are strictly less
than those of $x$ and $y$ respectively, and so by the inductive hypothesis,
$x'=y'$.  Thus $x\subseteq y$, and by a similar argument $y\subseteq x$,
so $x=y$, and so $a=b$.}
The `infons' of $\goth{B}$ are those objects of non-zero rank together with
those objects of the form $\tuple{0,x}$ for which $x\in\Si$.  It is easy to
check that $a\wedge b=\tuple{1,\{a,b\}}$ and so conjunction is neither
idempotent nor associative.
\end{con}

Both constructions give a commutative conjunc\-tion.
In fact, commuta\-tivity
follows from the definition of $\wedge$ from $\ConjunctOf$. To get a
non-commutative conjunction, we would need  use  different structural
relations. For a non-associative, non-commutative conjunction we could use
two binary structural relations, say,
 $\ConjunctOf_1$ and $\ConjunctOf_2$,
with $\wedge$ defined such that $\ConjunctOf_1(\si,\si\wedge\ta)$ and
$\ConjunctOf_2(\ta,\si\wedge\ta)$. For an associative, non-commutative
conjunction, we could use a ternary structural relation $\ConjunctOf_*$,
with integer roles, and $\wedge$ defined so that
$$\ConjunctOf_*(i,\si_i,(\si_1\wedge\ldots\wedge\si_n)).$$

The goal in defining a structural notion of conjunction is to capture those
properties of conjunctive information which are immediately available to
anyone receiving the information, without further reflection on the
significance of the information itself.  For this reason, it may be that
conjunctive information represented in different forms may be best modelled by
different conjunctions. For example, information about the relative heights
of Indiana's Hoosiers may be conveyed in a list of sentences of the form
`$x$ is taller than $y$', or by a team photograph.  In the former case, the
information conveyed may be best represented by a non-commutative,
associative conjunction; in the latter case, a commutative, associative
conjunction would be preferable.

Similar issues affect the choice of structural relations for modelling other
complex infons, such as disjunctions and conditionals.  Negations may be
modelled as
complex infons, or as basic infons, as indicated in
Section~\ref{sec.identity}.   For disjunctions,
constructions almost identical to
Constructions~\ref{con.idem-assoc-conjunction} and
\ref{con.non-idem-assoc-conjunction} may be used.  We simply re-name
`$\ConjunctOf$' as `$\DisjunctOf$' and `$\wedge$' as `$\vee$' throughout.
This further underlines the point that the issues pertaining to the modelling
of complex infons are structural, not logical.  Definitions of several kinds
of structures  having complex infons are given in
Section~\ref{sec.infon-structures}, below.

The question of how to represent quantifiers
is even more vexed (Robin Cooper (1991)  and Richard Cooper (1991)).
 One approach is to use infinitary conjunctions and disjunctions.
In both structures constructed above we may define an infinitary conjunction
as follows:
\begin{quote}
given  a set $X$ of infons,
the conjunction $\bigwedge X$ is the  least $x$ in the
$\partof$ order such that $\ConjunctOf(\si,x)$ for each $\si\in X$.
\end{quote}
This operation has similar properties to the corresponding binary
conjunction.  In the structure defined in
Construction~\ref{con.idem-assoc-conjunction} it is both associative an
idempotent, but in the structure defined in
Construction~\ref{con.non-idem-assoc-conjunction} it is neither. Infinitary
conjunctions are always commutative.

Another approach is to model a quantified infon as a pair $\tuple{Q,\lambda
x.\si}$, in which $Q$ is a quantifier and $\lambda x.\si$ is a
`infon-abstract'.   We shall discuss the question of how to model abstracts
in Section~\ref{sec.abstraction}.

\subsection{Substitution}
\label{section-substitution}
\label{sec.substitution}

In any extensional structure there is a well-defined operation of
substitution.

\begin{defn}
Let $\goth{A}:\relstr{A, S_1, \ldots, S_m; R_1, \ldots, R_n}$.
A function $f$ is a {\em substitution} in $\goth{A}$ if its arguments
and values are all elements of $A$.  Given a substitution $f$, a binary
relation $E$ on $A$ is an {\em $f$-simulation} if  for all $a,b\in A$, if
$E(a,b)$ then $b=f(a)$ if $a$ is in the domain of $f$, and if $a$ is not in
the domain of $f$ then
\begin{enumerate}
\item if $a$ is atomic then $a = b$
\item for $1\leq i\leq m$,  if $S_i$ is of arity $k$ then for all
$x_1,\ldots,x_k$ such that $S_i(x_1,\ldots,x_k,a)$,
\\ there are
$y_1,\ldots,y_k$ such that $S_i(y_1,\ldots,y_k,b)$, and $E(x_j,y_j)$ for
$1\leq j\leq k$, and
\item for $1\leq i\leq m$,  if $S_i$ is of arity $k$ then for all
$y_1,\ldots,y_k$ such that $S_i(y_1,\ldots,y_k,b)$,
\\
 there are
$x_1,\ldots,x_k$ such that $S_i(x_1,\ldots,x_k,a)$, and $E(x_j,y_j)$ for
$1\leq j\leq k$.
\end{enumerate}
$a$ is {\em $f$-similar} to $b$ in $\goth{A}$ if there is an $f$-simulation
$E$ of $\goth{A}$ such that $E(a,b)$. For a given $f$ and $a$, there need
not be an element of $\goth{A}$ that is $f$-similar to $a$, but if there is
one then there is only one, by the extensionality of $\goth{A}$.  We write
$f.a$ for the unique element $f$-similar to $a$, should it exist. An
extensional structure is a {\em substitution structure} if $f.a$ exists for
every $f$ and $a$.
\end{defn}



For example, suppose that there are  solutions to the equations
$$\begin{array}{lcl}
v & = & \infon{r; a, b}\\
w & = & \infon{r; b, b}\\
x & = & \infon{r; y, a}\\
y & = & \infon{r; x, b}\\
z & = & \infon{r; z, b}
\end{array}$$
in an extensional information structure $\goth{A}$.  Let $[a\mapsto b]$ be the
function  with domain $\{a\}$ such that $[a\mapsto b](a)=b$, and let $E$ be
the relation with graph
$$\{\tuple{v,w},\tuple{x,z},\tuple{y,z},\tuple{a,b}\}\cup I_{\{b,r,z\}},$$
where
$I_{\{b,r,z\}}$ is the identity relation on $\{b,r,z\}$.  It is easy to check
that $E$ is an $[a\mapsto b]$-simulation on $\goth{A}$, and so
$[a\mapsto b].v=w$ and  $[a\mapsto b].x=[a\mapsto b].y=z$.

Set structures are substitution structures, by the set-theoretic axiom of
Replacement, together with Foundation or Anti-foundation, as the case may be;
but many of the structures in which we are interested are not. For example,
any simple information structure satisfying axioms
\axref{finite-roles} (finite roles) and \axref{bisim} (extensionality) is a
substitution structure if and only if it satisfies the generality principle
given in Axiom~\axref{generality}. No room is made for `legitimate' grounds
for the  non-existence of $f.a$, such as the sortal restrictions considered in
Section~\ref{sec.appropriateness}.  We would like to generalize the principle
of sortal generality, given by Axiom~\axref{sortal-generality},  but
it refers to specific features of the structure of simple infons
(their roles), and so cannot be generalized to arbitrary extensional
structures.   Instead, we rest content with the fact that all extensional
structures are at least {\em partial} substitution structures, and interpret
the non-existence of $f.a$ as the inappropriateness of the substitution $f$
for $a$.\footnote{An interesting,
weaker, substitutional property of
extensional structures is as follows: if $f.a$ and $g.a$ both exist and
$f$ and $g$ are compatible functions then $(f\sqcup g).a$ also exists.
This is implied by sortal generality if the domains of $f$ and $g$ do not
contain roles.}


We next want to prove a result that states that every
extensional structure may be embedded in a substitution structure.


\begin{prop}
Let
$\goth{A} : \relstr{A,S_1,\ldots,S_m;R_1,\ldots,R_n}$
be a structurally saturated extensional structure.
then $\goth{A}$ is a substitution structure.
\label{prop-str-sat-sub}
\end{prop}

\begin{proof}
Let $f$ be a substitution in $\goth{A}$.
Let $X = \{x_{a} : a \mbox{ a non-atom of $\goth{A}$}\}$.  We
consider a structural type $T = \{T(x)\}_{x\in X}$,
using $x$ as the set of parameters.

For a non-atom $a$, $T(x_a)$ is obtained from
the canonical type $T_a$
as follows:  For each $\tuple{S, b_1,\ldots, b_k}$
which holds in $\goth{A}$,
let  $y_i = f(b_i)$ if $b_i$ is in the domain of $f$
$y_i = x_{b_i}$ if $b_i$ is not in the domain of $f$.
We put the corresponding  tuple
 $\tuple{S, y_1,\ldots, y_k}$ into $T(x_a)$.
This defines the structural type $T$.

Since $\goth{A}$ is structurally saturated,
let  $s$ instantiate  $T$ in $\goth{A}$.
For each $a\in\goth{A}$, the construction
has arranged that  each $s(x_a)$ is
$f$-similar  to  $a$.
This proves that $f.a$ exists.
\end{proof}


As an immediate corollary of Proposition~\ref{prop-str-sat-sub}
and Theorem~\ref{thm-str-sat}, we see that
every extensional $\goth{A}$ may be embedded in
an extensional substitution structure.

Our notion of a substitution structure is inspired by
the work of Aczel (1990) and Aczel and Lunnon (1991).
It might be noted that their work was motivated by the
foundational needs of situation theory.  At the same time,
the methods seem applicable to other areas.




\subsection{Infon Structures}
\label{section-infon-structures}
\label{sec.infon-structures}

We are now in a position to improve our model of infons in a way that allows
for the smooth incorporation of complex infons and a uniform treatment of
abstraction (to be given in Section~\ref{sec.abstraction}).  An advantage of
the  models used in Section~\ref{sec.structure-of-information}---the `simple
information structures'---is their simplicity, with only two structural
relations. However, there are disadvantages. First, because `infon', as
applied to these structures, is a defined term that applies only to simple
infons, the move to structures containing  complex infons is tricky.
Second, the functions associating objects to roles in infons are not internal
objects.  This complicates the treatment of substitution and abstraction.

Now that we know how to represent the structure of functions (in function
structures) in the framework of the theory of structural relations, we can
solve this problem.  The basic idea is to represent the infon
$\si=\infon{r;i:a,j:b,k:c}$ by as a pair consisting of the relation $r$ and
an internal function $\al$ with domain $\{i,j,k\}$ and such that
$\al^*(i)=a$, $\al^*(j)=b$, and $\al^*(k)=c$.  The function $\al$ is called
the {\em assignment} of $\si$.  We adapt the functional notation for
assignments and write
\begin{quote}
$\al=[i:a,j:b,k:c]$ and $\si=\infon{r;\al}.$
\end{quote}
The structure of infons is now represented using three structural relations,
$\Rel^2$, $\Ass^2$ and $\Inf^1$, and one non-structural relation,
$\Approp^1$.   $\Inf(\si)$ iff $\si$ is an infon;
$\Rel(r,\si)$ and $\Ass(\al,\si)$  iff $\si=\infon{r;\al}$.
An assignment $\al=[i:a,j:b,k:c]$ is represented as
an internal function,
so that $\Fun(\al)$ and $\App(i,a,\al)$, and $\al$ is
appropriate iff $\Approp(\al)$.

\begin{defn}
A function structure of type
$\relstr{\goth{A},\Ass^2,\Rel^2,\Inf^1;\Approp^1}$ is an {\em infon
structure} if it satisfies the following conditions:
\begin{enumerate}
\item\label{item.sorts} (sorts) $\Ass^*\subseteq\Inf^*$,
$\Rel^*\subseteq\Inf^*$, and
$\Fun^*\cap\Inf^*=\emptyset$,
\item\label{item.basic-infons} (basic infons) if $\Rel(r,\si)$ then
$\exists\al$
$\Ass(\al,\si)$,
\item\label{item.appropriateness} (appropriateness) $\Approp(\al)$  iff
$\exists\si$ $\Ass(\al,\si)$, and
\item\label{item.substitution} (substitution) if
$\Ass(\al,\si)$ and if $f$ is substitution such that $f.\al$ exists and
$\Approp(f.\al)$, then $f.\si$ also exists.
\end{enumerate}
An infon $\si$ is {\em basic} if there is an $\al$ such that
$\Ass(\al,\si)$.  An infon structure is a {\em basic-infon structure} if every
infon is basic.
\end{defn}

Clause~\ref{item.appropriateness} (appropriateness) links
the appropriateness of an assignment to the existence of an infon with
that assignment. If, for example, $a$ is not
an appropriate filler for the  role $i$ then there is no $\al$ in $\Fun^*$
such that $\Approp(\al)$ and $\al^*(i)=a$. This is a generalization of the
treatment of appropriateness in information structures.
Clause~\ref{item.substitution} (substitution) ensures that the only
issue governing substitution of infons is the appropriateness of the
resulting assignment.  This is an abstract form of the various principles of
generality discussed in Section~\ref{sec.appropriateness}. To go further, we
must look at the unification structure of appropriate assignments.

\begin{defn}
A unification structure is an {\em infon unification structure} if it is an
infon structure and
\begin{enumerate}
\item $P(x,y)$ iff $x\partof y$,
\item\label{item.function-compatibility} (function compatibility) if
$\Fun(\al_1)$ and $\Fun(\al_2)$, then $C(\al_1,\al_2)$ iff  for every $i$, $a$
and $b$, if
$\App(i,a,\al_1)$ and $\App(i,b,\al_2)$ then
$a=b$,
\item\label{item.infon-compatibility} (infon compatibility) 
Suppose that
$\Ass(\al_1,\si_1)$,
$\Ass(\al_2,\si_2)$,
$\Rel(r_1,\si_1)$, and $\Rel(r_1,\si_1)$.
Then $C(\si_1,\si_2)$  iff $r_1=r_2$
and
$C(\al_1,\al_2)$, and
\item\label{item.appropriate-unif}(unification of appropriate assignments) if
$C(\al_1,\al_2)$,
$\Approp(\al_1)$  \\
and
$\Approp(\al_2)$,  then $\Approp(\al_1\sqcup\al_2)$.\footnote{In effect,
 both $\goth{A}$ and the structure in which
$\Fun^*$ is restricted to appropriate assignments are required to be
function unification structures.}
\end{enumerate}
\end{defn}

Infon unification structures give us our best theory of
appropriateness.  Part~\ref{item.appropriate-unif}
 ensures that the appropriateness of assignments
depends only on  `local' issues: if
$\al_1$ and $\al_2$ are compatible appropriate assignments, then so is
$\al_1\sqcup\al_2$; no additional grounds for inappropriateness can be
introduced. Moreover, by clause~\ref{item.substitution} (substitution) of the
definition of infon structures, substitutions which result in appropriate
assignments may always be used to obtain new infons. For example, if
\begin{itemize}
\item[] $\si=\infon{r;\al}$ and $\al=[i:a,j:b,k:c]$,
\item[] $f$ is the function with domain
$\{a,b\}$ such that $f(a)=x$ and $f(b)=y$, and
\item[] $g$ is the function with domain
$\{b,c\}$ such that $g(b)=y$ and $f(c)=z$,
\end{itemize}
and both $f.\al$ and $g.\al$ exist and are appropriate---that is,
$$\Approp([i:x,j:y,k:c]) \quad \mbox{and}\quad
\Approp([i:a,j:y,k:z]),$$
then  not only is
$[i:x,j:y,k:z]$ an assignment (by function unification), and appropriate
(by unification of appropriate assignments)  but
the infon $f.\si=\infon{r;i:x,j:y,k:z}$ exists (by substitution).  This is
still weaker than the principle of sortal generality, according to which
appropriateness is dependent only on restrictions applying to  individual
roles. In particular, in infon unification structures  there may be
restrictions on related roles, as countenanced in the example of
$\ob{next\mbox{-}to}$ at the send of Section~\ref{sec.appropriateness}.  If
$\ob{next\mbox{-}to}$ has roles $\ob{nt}_1$ and $\ob{nt}_2$, then we may
deem assignments  of the form $[\ob{nt}_1:x,\ob{nt}_2:x]$ inappropriate,
without jeopardizing  the unification principle.\footnote{This would
imply that either
$[\ob{nt}_1:x]$ or $[\ob{nt}_2:x]$ is also inappropriate, which may appear
counterintuitive until one realizes that this does not prevent
$[\ob{nt}_1:x,\ob{nt}_2:y]$ from being appropriate when $x\neq y$.}


The second feature of infon structures not present in information
structures, is the unary structural relation $\Inf$. We say that
$\si$ is a {\em basic infon} if $\Ass(\al,\si)$ for some assignment $\al$
---by clause~\ref{item.basic-infons} (basic infons) all infons having a
relation are required to have an assignment, possibly the empty assignment
$[\ ]$. In simple information structures, by definition of the term `infon', all
infons are basic, but in infon structures we may have non-basic infons. Of
course, by extensionality and clause~\ref{item.sorts} (sorts), if there are no
more structural relations in $\goth{A}$ then there is at most one non-basic
infon.  If there are more structural relations, such as $\ConjunctOf$, then
we can add the axiom that $\ConjunctOf^*\subseteq\Inf^*$ without any
conflict with the axioms for infon structures.

This is a good example of how the `holistic' nature of the extensionality
property, which quantifies over {\em all} structural relations, allows
a modular approach to the theory of structured objects. Another example is
the treatment of polarity, discussed earlier in Section~\ref{sec.identity}.
We need only add new structural relations to deal with polarity and the
extensionality condition takes care of the rest.

\begin{defn}
An infon structure of type $\relstr{\goth{A},\Pos^1,\Neg^1;}$
is {\em bi-polar} if it satisfies the following conditions:
\begin{enumerate}
\item $\si$ is a basic infon iff either $\Pos(\si)$ or $\Neg(\si)$, and
\item if $\Pos(\si)$ then not $\Neg(\si)$.
\end{enumerate}
Infons in $\Pos^*$ are {\em positive} and those in $\Neg^*$ are
{\em negative}.\footnote{For {\em bi-polar infon unification structures}
 we must modify clause
\ref{item.infon-compatibility} of the definition of infon unification
structures to take polarity into account:
\begin{enumerate}
\item[\ref{item.infon-compatibility}${}'$.] if $\Ass(\al_1,\si_1)$,
$\Ass(\al_2,\si_2)$,
$\Rel(r_1,\si_1)$, and $\Rel(r_1,\si_1)$, then $C(\si_1,\si_2)$  iff
$r_1=r_2$, $C(\al_1,\al_2)$, and $\Pos(\si_1)\leftrightarrow\Pos(\si_2)$.
\end{enumerate}}
\end{defn}


Finite conjunctions and disjunctions are introduced effortlessly, as follows:

\begin{defn}
An infon structure of type
$\relstr{\goth{A},\ConjunctOf^2,\DisjunctOf^2;}$
is {\em $\wedge\vee$-closed} if it satisfies the following conditions:
\begin{enumerate}
\item $\ConjunctOf^*\subseteq\Inf^*$ and $\DisjunctOf^*\subseteq\Inf^*$,
\item if $\Inf(\si)$ and $\Inf(\ta)$ then there is a $\partof$-minimal object
$\si\wedge\ta$ such that $\ConjunctOf(\si,\si\wedge\ta)$ and
$\ConjunctOf(\ta,\si\wedge\ta)$
\item if $\Inf(\si)$ and $\Inf(\ta)$ then there is a $\partof$-minimal object
$\si\vee\ta$ such that $\DisjunctOf(\si,\si\vee\ta)$ and
$\DisjunctOf(\ta,\si\vee\ta)$.
\end{enumerate}
\end{defn}

The principles of existence for infinite conjunctions and disjunctions
are similar. We would like to say that for each set $X$ of
infons there is a conjunction $\bigwedge X$ and a disjunction $\bigvee X$. In
stating these we must be careful because the properties of (external) sets are
determined by the metatheory, which---as we have seen---is not fixed.  It is
a good idea to bring recognize this indeterminacy explicitly by using internal
sets instead, leaing open the question of how many internal sets there
are.  Thus we define:

\begin{defn}
An infon structure of type
\begin{quote}
$\relstr{\goth{A},\Set^1,\in^2,\ConjunctOf^2,\DisjunctOf^2;}$
\end{quote}
is  {\em $\bigwedge\bigvee$-closed} if it is also a set structure,
and
\begin{enumerate}
\item $\ConjunctOf^*\subseteq\Inf^*$, $\DisjunctOf^*\subseteq\Inf^*$, and
$\NegOf^*\subseteq\Inf^*$
\item if $\Set(X)$ and $\Inf(\si)$ for each $\si$ such
that $\in(\si,X)$,  then there is a $\partof$-minimal object
$\bigwedge X$ such that $\ConjunctOf(\si,\bigwedge X)$ for each $\si$ such
that $\in(\si,X)$,
\item if $\Set(X)$ and $\Inf(\si)$ for each $\si$ such
that $\in(\si,X)$,  then there is a $\partof$-minimal object
$\bigvee X$ such that $\DisjunctOf(\si,\bigvee X)$ for each $\si$ such
that $\in(\si,X)$.\footnote{Every $\bigwedge\bigvee$-closed infon
 structure is also $\wedge\vee$-closed
because for infons $\si$ and $\ta$ there is an internal set
$X$ with $X^*=\{\si,\ta\}$ and so $\si\wedge\ta=\bigwedge X$; and similarly
for disjunction.}
\end{enumerate}
\end{defn}

Negations may be modelled using a structural relation $\NegOf^2$
with the following existence condition:  if $\Inf(\si)$ then
there is a unique object $\neg\si$ such that $\NegOf(\si,\neg\si)$.  Another
approach is to base our model on a bi-polar infon structure and treat
$\NegOf^2$ as a {\em non}-structural relation defined as follows:

\begin{defn}
A bi-polar infon structure of type $\relstr{\goth{A;\NegOf}}$ is a 
{\em  de Morgan infon
structure} if it is  $\bigwedge\bigvee$-closed and satisfies the following
conditions:
\begin{enumerate}
\item if $\NegOf(\si,\ta)$ then $\Inf(\si)$ and $\Inf(\ta)$,
\item if $\NegOf(\si,\ta)$ and $\NegOf(\si,\ta')$ then $\ta=\ta'$,
\item if $\NegOf(\si,\ta)$ then $\NegOf(\ta,\si)$,
\item if $\Rel(r,\si)$ and $\Arg(\al,\si)$ then
there is an infon $\neg\si\neq\si$ such that\\
$\NegOf(\si,\neg\si)$
$\Rel(r,\neg\si)$ and $\Arg(\al,\neg\si)$, and
\item if $\Set(X)$, $\Set(Y)$ and
\begin{enumerate}
\item for each $\si\in X^*$ there is a $\ta\in
Y^*$ such that $\NegOf(\si,\ta)$
\item for each $\ta\in Y^*$ there is a $\si\in
X^*$ such that $\NegOf(\si,\ta)$
\end{enumerate}
then $\NegOf(\bigwedge X,\bigvee Y)$.\footnote{No mention is made of
polarities here, but from the definition of
bi-polar infon structures we know that if $\si$ is a basic infon then it is
either positive or negative (but not both), and from clause 4,
$\si\neq\neg\si$; so if $\si$ is positive then  $\neg\si$ is negative, and
vice versa.}
\end{enumerate}
\end{defn}




A remaining question is how to distinguish between saturated and
unsaturated infons
in infon structures.  In basic-infon structures, the answer is clear from the
discussion in  Section~\ref{sec.partiality}:  saturated basic infons are
those that are
maximal in the $\partof$-ordering. For complex infons, it is not so easy.  In a
$\wedge\vee$-closed infon structure, if $\si$ and $\ta$ are distinct basic infon
then $\si\partof\si\wedge\tau$ and so $\si$ is not maximal, no matter how
many roles
are filled.  We decide the matter as follows.

\begin{defn}\label{def.saturated}
A basic infon $\si$ is {\em unsaturated} if there is a distinct basic infon
$\ta$
such that $\si\partof\ta$. A non-basic infon is {\em unsaturated} if it has a
component that is unsaturated.  An infon is {\em saturated} if it is not
unsaturated.\footnote{This is not a complete definition.  In particular, it does
not legislate on the saturation of a non-basic infon that is a component of
itself
but all of whose other components are saturated.  In all such cases we say
that the
infon is saturated.}
\end{defn}

By now, the reader will have an impression of some of the possibilities for
modelling basic and complex infons using the theory of structural relations.
Observers of the development of  Situation Theory have been somewhat
frustrated because of the  lack of consensus on which structures---or even on
which kinds of structures, obeying which axioms---are to be chosen for the
theory (see Barwise 1989).  We will see other reasons
for diversity in Section~\ref{sec-truth-circumstance}, but the basic reason
is clear from the above: logical and structural properties of infons are
separate but interdependent, and striking the right balance is a difficult
matter.



\subsection{Abstraction}
\label{sec.abstraction}

Abstraction is a natural operation in semantics. By abstracting Paul
from the information $\si$ that Raymond cooked the omelette for Paul,
we obtain the property of being someone for whom Raymond has cooked
the omelette.  By abstracting both Paul and the omelette from $\si$,
we obtain the relation which holds between $x$ and $y$ just in case
Raymond cooked $x$ for $y$.   This relation and the previous property
differ from the relations and properties we have considered so far in
that they are clearly not atomic. In this section we see how 
infon structures can be used to  model these complex relations.

It should be noted that our work in this section will be 
another outgrowth of  our theory of structural relations.
As such, it goes against the 
dominant trend of using structures such as the
lambda calculus or various type theories
 (see Chapter 9 in this handbook).
We feel that the integration of the two approaches would
be interesting.

There are two parts to abstraction over a structural object: the
object after abstraction containing holes where the abstracted
object used to be,  and something
indicating where the holes are so  that they may subsequently be
filled again---we call these the `abstract' and the `pointer',
respectively.\footnote{Analogues of pointer in the literature are
`indeterminates' and `parameters'.} The
relationship between abstract and pointer may be  captured by a
binary structural relation $\Abs$ with $\Abs(a,x)$ meaning that $x$ is
a pointer to the abstract $a$.


\begin{defn}
An  {\em abstraction structure} $\goth{A}$ is an extensional
structure with structural relation $\Abs^2$ such that if
$\Abs(a,x)$ and $\Abs(a',x)$ then $a=a'$.  The objects of sort
$\Abs^*$ are called {\em pointers}.  If $\Abs(a,x)$ then
$x$ is said {\em to point} to the {\em abstract} $a$.
\end{defn}

The objects of interest in abstraction structures are the
abstracts, but they do not form a structural sort; rather,
it is the pointers that are structurally determined.  The intention
is that each pointer $x$ of an abstract $a$ is a
hereditary component of $a$. We obtain the results of `applying'
an abstract $a$ to some argument $b$ by substituting $b$ for
a pointer $x$ in $a$. To see how this achieves the desired effect
we must consider how abstracts arise by abstraction from other
objects in the domain.

Suppose, for example, that we want to  abstract
$b$ from the infon $\si=\infon{r;i:b,j:c}$.  We would
expect to obtain an abstract $a$ with exactly one pointer $x$
such that the result of substituting $b$ for $x$ in $a$ in just
$\si$.  Furthermore, the result of substituting $b'$ for $x$ in $a$
should be the infon $\infon{r;i:b',j:c}$, if this infon exists.
This is captured in the following definition.

\begin{defn}
Suppose $\goth{A}$ is an abstraction structure. Given elements $a$
and $b$ in $\univ{\goth{A}}$, an abstract $\lambda b.a$ is
{\em the abstraction of $b$ from $a$} if there is an $x$
such that 
\begin{enumerate}
\item $\Sbs{b}{x}{a}=\lambda b.a$,
\item $\Abs(\lambda b.a,x)$, and 
\item the
only sort of $x$ is $\Abs^*$.
\end{enumerate}
\end{defn}

The definite article is justified in the above definition, because
if $\Abs(\Sbs{b}{x}{a},x)$ and $\Abs(\Sbs{b}{y}{a},y)$ then, by
extensionality, $x=y$.
For example, if $\si=\infon{r;i:b,j:c}$ and $\lambda
b.\si$ exists, then there is an $x$ such that
$\Abs(\infon{r;i:x,j:c},x)$.  But suppose there was a
$y$ such that $\Abs(\infon{r;i:y,j:c},y)$. Since this is these
are the only structural relations determining $x$ and $y$, they
are obviously bisimilar, and so equal.  A similar argument shows
that $$\lambda b.\infon{r;i:b,j:c}\quadeq \lambda b'.\infon{r;i:b',j:c},$$
assuming that $b$ and $b'$ are not hereditary components of $r$,
$i$, $j$, or $c$.  This is the expected principle of
$\alpha$-equivalence.

Notice also that under similar assumptions
the order of abstraction is insignificant. If, for example, $b$ and
$c$ are both atomic then
$$\lambda c.\lambda b.\infon{r;i:b,j:c}\quadeq
\lambda b.\lambda c.\infon{r;i:b,j:c}.$$
 In both cases, the abstract
obtained has two pointers, pointing to the positions
previously occupied by $b$ and $c$ respectively, but there nothing to
distinguish the pointers apart from that, and so
no trace of the order in which the abstraction was performed.
This motivates a slightly more general notion of abstraction.

\begin{defn}
Suppose $\goth{A}$ is an abstraction structure. Given an element $a$
of $\univ{\goth{A}}$ and a set $B$ of elements of $\univ{\goth{A}}$,
an abstract $\Lambda B.a$ is   {\em the simultaneous abstraction of
$B$ from $a$} if there is a function $\fun{\pi}{B}{\univ{\goth{A}}}$
such that
\begin{enumerate}
\item $\pi.a=\Lambda B.a$,
\item $\Abs(\pi.a,\pi(b))$ for each $b\in B$, and
\item for each $b\in B$, the only sort of $\pi(b)$ is $\Abs^*$.
\end{enumerate}
\end{defn}

Despite the previous observation about commuting lambdas, one should
be careful to distinguish simultaneous abstraction from successive
abstractions. When the elements of $B$ are structurally dependent,
the results obtained may differ (see  Aczel and Lunnon (1991),
Ruhrberg (1994)). However, it is clear that simultaneous abstraction is
a generalization of abstraction because $\lambda b.a=\Lambda\{b\}.a$.

We have already observed that abstraction obeys an identity principle
analogous to $\alpha$-equivalence in the $\lambda$-calculus, at
least in special cases.  To  state the general result
observe that if $\si=\infon{r;b,c}$ and $\si'=\infon{r;b',c}$
and $b$ and $b'$ are structurally independent then
$\Sbs{b}{b'}{\si}=\si$ and $\Sbs{b'}{b}{\si'}=\si$. These are the
conditions needed to show that the two abstracts are bisimilar and
so justify the claim that $\lambda b.\si=\lambda b'.\si'$.  We
state, without proof, the generalization of this result.

\begin{thm}
($\alpha$-identity) If $\Lambda B.a$ and $\Lambda B'.a'$ exist in an
abstraction structure and there is a one-to-one correspondence $f$
between $B$ and $B'$ such that $f.a=a'$ and $f^{-1}.a'=a$ then
$\Lambda B.a=\Lambda B'.a'$.
\end{thm}

We now show that extensional structures with abstraction really
exist.

\begin{defn}
An abstraction structure $\goth{A}$ is a {\em Lambda structure}
if for every element $a$ of $\univ{\goth{A}}$ and a set $B$ of
elements of $\univ{\goth{A}}$, the simultaneous abstraction $\Lambda
B.a$ exists.
\end{defn}


\begin{thm}
Every extensional structure can be extended to a Lambda structure.
\label{thm.Lambda-extension}
\end{thm}

\begin{proof}
Given an extensional structure $\goth{A}$,  extend it trivially to an
abstraction structure by adding the structural relation
$\Abs^2$ with an empty extension.  By Theorem~\ref{thm.sat-extn} this
can be extended to a structurally saturated structure
$\goth{B}_0$.  Throw away
all pointers in this structure that point to  more than one abstract
to obtain an abstraction structure $\goth{B}$. We show that $\goth{B}$
contains a Lambda structure extending $\goth{A}$.   Suppose $a$ is an
element of $\univ{\goth{B}}$ and $B$ is a set of elements of
$\univ{\goth{B}}$.  We exhibit a structural type whose satisfier
gives the needed element $\lambda B.a$.  For each $b\in B$, let
$T_b = \{\tuple{\Abs, a}\}$. Let $H$ be the set of hereditary
components of $a$ that are not in $B$, and for each $c\in H$,
 let $T_c$ be the canonical type of $c$ in $\goth{B}$.  Now the
structural type we want is  $T=\{T_x\}_{x\in B\cup H}$.  Since
$\goth{B}$ is contained in a structurally saturated structure, there
is a function $s$ mapping into $\goth{B}_0$
that instantiates $T$. But, clearly, the
range of $s$ does not contain any of the elements we threw away, so
$s$ maps into $\goth{B}$. Thus for each
$b$ in $B$, $s(b)$ is of type
$s.T_b=\{\tuple{\Abs, s.a}\}$ and so $\Abs(s.a,s(b))$. Moreover,
$s(b)$ is only of sort $\Abs^*$, and so $s.a$ is the required
abstract $\Lambda B.a$.
\end{proof}

A short digression on the ontology of abstracts is in order.
If $\si$ is an infon with argument $b$ then $\lambda b.\si$ is
also of sort $\Inf^*$.  But, intuitively,  it is a property not an
infon.  Moreover, it has a pointer as an argument, filling the role
left by $b$, and so interfering with whatever implicit
appropriateness conditions there may have been on this role.  It is
therefore useful to distinguish between genuine infons and  these new
entities, which we may call {\em infon abstracts}. Infon
abstracts are just properties (or relations if they
have more than one pointer) and so ontologically
acceptable. That is not quite the end of the matter.
Consider the infon $\ta=\infon{r,\si}$ and the abstract $\lambda
b.\ta$ with pointer $x$.  The abstract $\lambda b.\ta$ is an infon
abstract, not a genuine infon.  But it has an argument $x.\si$ which is
also of sort $\Inf^*$ but neither an infon abstract nor, intuitively,
a genuine infon.  The only reasonable position to adopt is that
$x.\si$ is a {\em part} of an abstract. Fortunately, it is easily
determined which abstract it is a part of, because the pointer $x$
points to it.  In this way, we may satisfy ourselves that no
unexpected ontological categories have been 
created.\footnote{There has been much discussion of
the ontological status of `parametric objects', which are closely
related to our abstracts and their parts. See, for
example,  Westerst{\aa}hl (1990).}

\subsection{Application}
\label{sec.application}

In the previous section we saw that an extensional structure may be
extended with abstracts of the form $\Lambda B.a$, obtained by
abstracting the elements of $B$ from the object $a$.   The purpose
of these abstracts is to model generalizations across a class of
structured objects. In particular, infon abstracts may be used to
model properties and relations.  To see how this works, we must first
give an account of application.

\begin{defn}
Suppose $\goth{A}$ is an abstraction structure.
If $a$ is an abstract then a function
 $\fun{f}{X}{\univ{\goth{A}}}$ is an {\em (external) assignment for}
$a$  if every $x$ in $X$ is a pointer of $a$. It is  {\em appropriate
for} $a$ if $f.a$ exists.   If $f$ is appropriate for $a$ then {\em
the application of $a$ to $f$}, written $a^*(f)$, is $f.a$.  In this
way, every abstract $a$ is associated with a (second-order) function
$a^*$ mapping appropriate assignments to elements of
$\univ{\goth{A}}$.
\end{defn}


\begin{thm}
($\beta$-identity)  if $\Lambda B.a$ exists and $f$ is an appropriate
assignment for $\Lambda B.a$ then $(\Lambda B.a)^*(f)=f.a$.
\end{thm}

This follows directly from the definitions of simultaneous
abstraction and application.

With the notion of application in place we can return to the
question of how to incorporate complex properties and relations into
infon structures.  The key point is that the appropriateness
conditions of infons having complex relations should be determined
by those of basic infons.

\begin{defn}
Let $\goth{A}$ be an infon structure
that is also an abstraction
structure.  $\goth{A}$ has {\em coherent appropriateness conditions} if
for each infon $\si=\infon{r;f}$ in $\univ{\goth{A}}$, if $r$ is an infon
abstract then $f^*$ is an appropriate assignment for $r$.
$\goth{A}$ is {\em relation-closed} if
for each infon $\si$ and each set $B$ of elements of $\goth{A}$,
the infon abstract $\Lambda B.\si$ exists and for each appropriate
assignment $f$ for $\Lambda B.\si$, the infon $\infon{\Lambda
B.\si;f}$ also exists.
\end{defn}

We state without proof the following result:

\begin{thm}
Every infon structure is extendible to a relation-closed infon
structure.
\label{thm.relation-closed-extension}
\end{thm}


By way of closing this section, we note that application has only
been modelled in an `external' way.  
We may ask what the properties of an `internal'
application operation should be.  For more on this,
see Aczel and Lunnon (1990), and Lunnon (to appear).

\end{document}

