ttr.tex

\renewcommand{\thechapter}{}
\chapter{TTR}{}{}
%\chapter{Appendix}
\label{app:ttr}
\renewcommand{\thesection}{\arabic{section}}



%\section*{TTR}
Unless otherwise stated this is the version of TTR presented in 
\cite{Cooper2012}.



 \section{Underlying set theory}
 \label{app:sets}
In previous statements of this system such as \cite{Cooper2012} we
tacitly assumed a standard underlying set theory such as ZF
(Zermelo-Fraenkel) with urelements (as formulated for example in \citealp{Suppes1960}).  This is what we take to be the
common or garden working set theory which is familiar from the core
literature on formal semantics deriving from Montague's original work
\citep{Montague1974}.  

In this version we
will assume that our set theory comes equipped with a set of
\textit{urelements} (entities which are not sets but which can be
members of sets).  We will assume that among the urelements is a countably infinite
set which is designated as the set of \textit{labels}. In addition we assume
that among the urelements there is a finite or countably infinite set,
disjoint from the set of labels, designated as the set of
\textit{flavours}.  Finally, we assume that there is a countably infinite set
of urelements, \fbox{0}, \fbox{1},\ldots, called indices, which is
disjoint from both the set of labels and the set of flavours.

A \textit{field} is either
\begin{quote}
  an ordered pair $\langle\ell,a\rangle$ where
  $\ell$ is a label and $a$ is not a label or a flavour
\end{quote}
or
\begin{quote}
  an ordered triple $\langle\ell,a,i\rangle$ where
  $\langle\ell,a\rangle$ is a field and $i$ is an index
\end{quote}


An \textit{(unflavoured) labelled set}
(Chapter~\ref{ch:percint}, p.~\pageref{sec:labelled-sets}) is a set
of fields% ordered pairs whose first member is a label and whose second
% element is either an urelement which is not a label or a set (possibly a labelled
% set)
such that no more than one field can contain any
particular label as its first member.  This means that a labelled set
whose members are all ordered pairs
is the traditional set theoretic construction of an extensional
function from a set of labels onto some set. A \textit{flavoured
labelled set} is an unflavoured labelled set, $X$, with the addition of
some flavour, $\mathfrak{f}$, that is, $X\cup\{\mathfrak{f}\}$. We use
flavours when we need to distinguish objects which correspond to the
same set of ordered pairs.

We refer to the first members of the fields in a
labelled set (flavoured or unflavoured) as \textit{labels} used in the labelled set and we will refer to
the second members of the fields as the \textit{labelled
  elements} of the labelled set.  If $X$ is a labelled set we use
$\mathrm{labels}(X)$ to represent the set $\{\ell\mid\exists 
x,i\ \langle\ell,x\rangle\in X\text{ or }\langle\ell,x,i\rangle\in X\}$, the left projection of $X$.  If
$\ell\in\mathrm{labels}(X)$ and $\langle\ell,v\rangle\in X$ or
$\langle\ell,v,i\rangle\in X$ for some $i$, then we
use $X.\ell$ to represent $v$.  We characterize the set of
\textit{paths} in a labelled set, $\mathrm{paths}(X)$ by the following
inductive definition:
\begin{quote}
If $X$ is a labelled set, then
\begin{enumerate} 
 
\item if $\ell\in\mathrm{labels}(X)$, then $\ell\in\mathrm{paths}(X)$ 
 
\item if $\ell\in\mathrm{labels}(X)$, $X.\ell$ is a labelled set and
  $\pi\in\mathrm{paths}(X.\ell)$, then $\ell.\pi\in\mathrm{paths}(X)$ 
 
\end{enumerate} 
\end{quote}

The set of \textit{total paths} in a labelled set, $X$,
$\mathrm{tpaths}(X)$ is the set of paths, $\pi$, such that
\mbox{$\pi\in\mathrm{paths}(X)$} and $X.\pi$ is not a labelled set.

$\pi_1$ is an \textit{initial subpath} (Chapter~\ref{ch:propnames}, p.~\pageref{ex:subpath}) of $\pi_2$,
    $\pi_1\leq\pi_2$, just in case either $\pi_1=\pi_2$ or there is
    some $\pi$ such that $\pi_2=\pi_1.\pi$.

$\pi_1$ is a \textit{proper initial subpath}
(Chapter~\ref{ch:propnames}, p.~\pageref{ex:subpath}) of $\pi_2$,
    $\pi_1<\pi_2$, just in case there is
    some $\pi$ such that $\pi_2=\pi_1.\pi$.

If $X$ is a labelled set, then \textit{$x$ is a component of $X$},
$x\varepsilon X$, iff there some $\pi\in\mathrm{paths}(X)$ such that $X.\pi=x$.

We characterize \textit{the subtraction of a path, $\pi$, from a
  labelled set $X$}, $X\ominus\pi$,  (Chapter~\ref{ch:quant},
  p.~\pageref{ex:subtraction-labelled-sets}) as follows: 

\begin{enumerate}

\item If $X$ is a labelled set, $\ell\in\mathrm{labels}(X)$ and
  $\langle\ell,\varphi\rangle\in X$, then $X\ominus\ell$  is
  \begin{quote}
    $X-\{\langle\ell,\varphi\rangle\}$
  \end{quote}

\item If $X$ is a labelled set, $\langle\ell,\varphi\rangle\in X$ and
  $\ell.\pi\in\mathrm{tpaths}(X)$, then
  \begin{quote}
    if $\ell.\pi$ is branching in $X$, then $X\ominus\ell.\pi$ is
    \begin{quote}
      $(X-\{\langle\ell,\varphi\rangle\})\cup\{\langle\ell,\varphi\ominus\pi\rangle\}$
    \end{quote}
    otherwise $X\ominus\ell.\pi$ is
    \begin{quote}
      $X-\{\langle\ell,\varphi\rangle\}$
    \end{quote}
  \end{quote}

\end{enumerate}




If $X$ is a labelled set and
$\pi_1,\ldots,\pi_n\in\mathrm{tpaths}(X)$, then we write
$X\ominus\pi_1,\ldots,\pi_n$ for $X\ominus\pi_1\ominus\ldots\ominus\pi_n$.

 
  
% When we introduced complex
% objects and types
% other than records and record types we were not explicit about exactly which
% structured set-theoretic object they represented.  The reason for this
% was that, except in the case of records and record types, it did not
% seem important exactly how you code structured objects in the set
% theory and a detailed exposition would seem to provide another level
% of complication over and above an already complicated story.  

% In this
% version we will take advantage of the freedom provided by an appendix
% and spell out a set theoretic coding for all of our structured
% objects.

If $\mathcal{L}$ is a set of labels, the $\mathcal{L}_+$ is defined
inductively by
\begin{enumerate} 
 
\item if $\ell\in\mathcal{L}$, then $\ell\in\mathcal{L}_+$ 
 
\item if $\ell\in\mathcal{L}$ and $\pi\in\mathcal{L}_+$, then $\ell.\pi\in\mathcal{L}_+$ 
 
\end{enumerate} 

If $\mathcal{L}$ is a set of labels and $X$ is a labelled set such
that $\mathrm{paths}(X)\subseteq\mathcal{L}_+$, then a
$\mathcal{L}$-relabelling of $X$ is a one-one function, $\eta$, such
that
\begin{enumerate} 
 
\item $\mathrm{dom}(\eta)\subseteq\mathrm{paths}(X)$ 
 
\item
  $\mathrm{rng}(\eta)\subseteq\mathcal{L}_+-(\mathrm{paths}(X)-\mathrm{dom}(\eta))$
  
\item if $\pi_1,\pi_2\in\mathrm{dom}(\eta)$ and $\pi_1<\pi_2$, then $\eta(\pi_1)<\eta(\pi_2)$
 
\end{enumerate} 

If $X$ is a labelled set based on $\mathcal{L}$ and $\eta$ is a
$\mathcal{L}$-relabelling of $X$, then $[X]_\eta$ is the labelled set
$X'$ exactly like $X$ except that
\begin{enumerate} 
 
\item if $\pi\in\mathrm{dom}(\eta)$, then $\eta(\pi)$ replaces $\pi$
  in $\mathrm{paths}(X')$, that is
  \begin{quote}
    $\mathrm{paths}(X')=(\mathrm{paths}(X)-\mathrm{dom}(\eta))\cup\mathrm{rng}(\eta)$
  \end{quote}
  
 
\item if $\pi\in\mathrm{dom}(\eta)$ and there is no
  $\pi'\in\mathrm{dom}(\eta)$ such that $\pi<\pi'$, then
  $X'.\eta(\pi)=X.\pi$
  
\item if $\pi\in\mathrm{tpaths}(X')$ and
  $\pi\not\in\mathrm{dom}(\eta)$, then $X'.\pi=X.\pi$
 
\end{enumerate} 

We represent a relabelling,
$\eta$, whose domain is $\{\pi_1,\ldots,\pi_n\}$ and which is defined
by $\eta(\pi_1)=\pi'_1,\ldots,\eta(\pi_n)=\pi'_n$ as:
\begin{quote}
$\pi_1\leadsto\pi'_1$\\
\vdots\\
$\pi_n\leadsto\pi'_n$
\end{quote}

% The remaining definitions relating to labelled sets are for the
% support of dependent record types.

% An \textit{indexed value, $v$, in a labelled set, $X$,} is a pair
% \begin{quote}
%   $\langle f,\langle\pi_1,\ldots,\pi_n\rangle\rangle$
% \end{quote}
% such that for some $\pi$ in $\mathrm{paths}(X)$
% \begin{enumerate}
  
% \item $X.\pi=v$
  
% \item $f$ is a function with $n$ arguments
  
% \item for $1\leq i\leq n$,
%   $\pi_i\in\mathrm{paths}(X)-\{\pi'|\pi'\leq\pi\}$
% \end{enumerate}

% A \textit{labelled set with path dependencies} is a labelled set, $X$,
% which has a component which is an indexed value in $X$.

% A \textit{parametric labelled set} is a function, $f$, whose range is
% a family of labelled sets.  If $f$ requires $n$ arguments then
% $\langle f, \langle i_1,\ldots,i_n\rangle\rangle$ is an
% \textit{indexed labelled set} indexed by $\langle
% i_1,\ldots,\i_n\rangle$.  If $X=\langle f, \langle
% i_1,\ldots,i_n\rangle\rangle$ is an indexed labelled set, then
% $\mathrm{labels}(X)$ is $\mathrm{labels}(f(a_1,\ldots,a_n))$ where
% $a_1,\ldots,a_n$ are appropriate arguments to $f$. \todo{Need to
%   restrict $f$ so there will be a unique set of labels}





\section{Basic types}
\label{sec:basic}

\paragraph{System of basic types} \mbox{}

A {\it system of basic types\/} (Chapter~\ref{ch:percint}, p.~\pageref{ex:def-basic-types}) is a pair:
\begin{quote}
{\bf TYPE$_B$} = $\langle${\bf Type}, $A$$\rangle$
\end{quote}
where:
\begin{enumerate} 
 
\item \textbf{Type} is a non-empty set 
 
\item $A$ is a function whose domain is \textbf{Type}

\item for any $T\in\textbf{Type}$, $A(T)$ is a set disjoint from
  \textbf{Type}

\item for any $T\in\textbf{Type}$, $a:_{\mathbf{TYPE_B}}T$ iff $a\in A(T)$
 
\end{enumerate}


% A \textit{modal system of basic types}\footnote{This definition was
%   not present in \cite{Cooper2012}.} (Chapter~\ref{ch:intensional},
% p.~\pageref{ex:def-modal-basic-types}) is a family of
% pairs:
% \begin{display}
% \textbf{TYPE$_{\mathit{MB}}$} = $\langle${\bf Type},
% $A\rangle_{A\in\mathcal{A}}$
% \end{display}
% where:
% \begin{enumerate} 
 
% \item $\mathcal{A}$ is a set of functions with domain \textbf{Type} 
 
% \item for each $A\in\mathcal{A}$, $\langle${\bf Type}, $A\rangle$ is a
%   system of basic types
 
% \end{enumerate} 

% This enables us to define some simple modal notions:

% If {\bf TYPE$_{\mathit{MB}}$} = $\langle${\bf Type},
% $A\rangle_{A\in\mathcal{A}}$
% is a modal system of basic types, we shall use the notation {\bf
%   TYPE$_{\mathit{MB}_A}$} (where $A\in\mathcal{A}$) to refer to that
% system of basic types in {\bf TYPE$_{\mathit{MB}}$} whose type assignment is
% $A$.    Then:  
% \begin{enumerate} 
 
% \item for any $T_1,T_2\in\textbf{Type}$, $T_1$ \textit{is
%     (necessarily) equivalent
%     to} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MB}}$},
%   $T_1\approx_{\mathbf{TYPE_{\mathit{MB}}}}T_2$,  iff for all
%   $A\in\mathcal{A}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T_1\}=\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T_2\}$
  
 
% \item for any $T_1,T_2\in\textbf{Type}$, $T_1$ \textit{is a
%     subtype of} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MB}}$},
%   $T_1\sqsubseteq_{\mathbf{TYPE_{\mathit{MB}}}}T_2$,  iff for all
%   $A\in\mathcal{A}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T_1\}\subseteq\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T_2\}$

% \item for any $T\in\textbf{Type}$, $T$ \textit{is necessary in} {\bf TYPE$_{\mathit{MB}}$}  iff for all
%   $A\in\mathcal{A}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T\}\not=\emptyset$

% \item for any $T\in\textbf{Type}$, $T$ \textit{is possible in} {\bf TYPE$_{\mathit{MB}}$}  iff for some
%   $A\in\mathcal{A}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MB}_A}}T\}\not=\emptyset$
 
% \end{enumerate}  

\section{Complex types}

\subsection{Predicates}
\label{app:predicates}
We start by introducing the notion of a predicate signature.

A \textit{predicate signature} (Chapter~\ref{ch:percint}, p.~\pageref{ex:pred-sig})
is a triple
\begin{quote}
$\langle$\textbf{Pred}, \textbf{ArgIndices}, \textit{Arity}$\rangle$
\end{quote}
where:
\begin{enumerate} 
 
\item \textbf{Pred} is a set (of predicates)

\item \textbf{ArgIndices} is a set (of indices for predicate
  arguments, normally types)
 
\item \textit{Arity} is a function with domain \textbf{Pred} and range
  included in the set of finite sequences of members of \textbf{ArgIndices}. 
 
\end{enumerate}

\medskip

A \textit{polymorphic predicate signature} (Chapter~\ref{ch:percint}, p.~\pageref{ex:poly-pred-sig})
is a triple 
\begin{quote}
$\langle$\textbf{Pred}, \textbf{ArgIndices}, \textit{Arity}$\rangle$
\end{quote}
where:
\begin{enumerate} 
 
\item \textbf{Pred} is a set (of predicates)

\item \textbf{ArgIndices} is a set (of indices for predicate
  arguments, normally types)
 
\item \textit{Arity} is a function with domain \textbf{Pred} and range
  included in the powerset of the set of finite sequences of members
  of \textbf{ArgIndices}. 
 
\end{enumerate}
 

\subsection{Systems of complex types}
\label{app:comptypes}

A {\it system of complex types\/} (Chapter~\ref{ch:percint},
p.~\pageref{ex:comp-types}) is a quadruple:
\begin{quote}
{\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$
\end{quote}
where:  
\begin{enumerate} 
 
\item $\langle$\textbf{BType}, $A$$\rangle$ is a system of basic types 
 
\item \textbf{BType}$\subseteq$\textbf{Type}

\item for any $T\in\textbf{Type}$, if $a:_{\langle\mathbf{BType},
    A\rangle}T$ then $a:_{\mathbf{TYPE_C}}T$

\item \label{cl:predtypes}$\langle${\bf Pred}, \textbf{ArgIndices},
  {\it Arity\/}$\rangle$ is a (polymorphic) predicate
  signature

\item\hspace*{-1ex}\footnote{This clause has been modified since
    \cite{Cooper2012} where it was a conditional rather than a biconditional.} %\sloppy  
  $P(a_1,\ldots a_n)\in\textbf{PType}$ iff $P\in\textbf{Pred}$, $T_1\in \mathbf{Type},\ldots,T_n\in
  \mathbf{Type}$, \textit{Arity}($P$)=$\langle
  T_1,\ldots,T_n\rangle$  ($\langle
  T_1,\ldots,T_n\rangle$$\in$\textit{Arity}($P$)) and $a_1:_{\mathbf{TYPE_C}}T_1,\ldots,a_n:_{\mathbf{TYPE_C}}T_n$

% If $P\in\textbf{Pred}$, $T_1\in \mathbf{Type},\ldots,T_n\in
%   \mathbf{Type}$, \textit{Arity}($P$)=$\langle
%   T_1,\ldots,T_n\rangle$  ($\langle
%   T_1,\ldots,T_n\rangle$$\in$\textit{Arity}($P$)) and $a_1:_{\mathbf{TYPE_C}}T_1,\ldots,a_n:_{\mathbf{TYPE_C}}T_n$ then
%   $P(a_1,\ldots a_n)\in\textbf{PType}$



\item \textbf{PType}$\subseteq$\textbf{Type}

\item for any $T\in\textbf{PType}$, $F(T)$ is a set disjoint from \textbf{Type}

\item for any $T\in\textbf{PType}$, $a:_{\mathbf{TYPE_C}}T$ iff $a\in F(T)$
 
\end{enumerate}

We call the pair $\langle A,F\rangle$ in a complex system of types the
\textit{model} because of its similarity to first order models in
providing values for the basic types and the ptypes constructed from
predicates and arguments.  It is this pair which connects the system
of types to the non-type theoretical world of objects and situations.

In \cite{Cooper2012} we did not define exactly what entity is
represented by $P(a_1,\ldots a_n)$.  Here we will specify it to be the
labelled set

$\{\langle\mathrm{pred},P\rangle,\langle\mathrm{arg}_1,a_1\rangle,\ldots,\langle\mathrm{arg}_n,a_n\rangle\}$

where `pred', `arg$_i$' are reserved labels (not used except as
required here).



%\section{Complex types in record types}

\section{Function types}
\label{app:funtypes}

A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
  function types} (Chapter~\ref{ch:percint}, p.~\pageref{ex:funtypes}) if
\begin{enumerate} 
 
\item for any $T_1,T_2 \in \textbf{Type}$, $(T_1\rightarrow T_2) \in \textbf{Type}$ 
 
\item for any $T_1,T_2 \in \textbf{Type}$, $f:_{\mathbf{TYPE_C}}(T_1\rightarrow T_2)$ iff
  $f$ is a function whose domain is $\{a\mid
  a:_{\mathbf{TYPE_C}}T_1\}$ and whose range is included in $\{a\mid a:_{\mathbf{TYPE_C}}T_2\}$ 
 
\end{enumerate}

In \cite{Cooper2012} we did not specify exactly what object is
represented by a function type $(T_1\rightarrow T_2)$.  Here we
specify it to be the labelled set

$\{\langle\mathrm{dmn},T_1\rangle,\langle\mathrm{rng},T_2\rangle\}$

where `dmn' (``domain'') and `rng' (``range'') are reserved labels.

We also introduce a limited kind of polymorphism is function types
which we did not have in \cite{Cooper2012}.

A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with function types
\textit{has
  partial function types} (Chapter~\ref{ch:infex},
p.~\pageref{ex:partialfuntypes}) if
\begin{enumerate} 
 
\item for any $T_1,T_2 \in \textbf{Type}$,
  $(T_1\rightharpoonup T_2) \in \textbf{Type}$ 
 
\item for any $T_1,T_2 \in \textbf{Type}$,
  $f:_{\mathbf{TYPE_C}}(T_1\rightharpoonup T_2)$ iff there is some type $T'$ such that
  $f:(T'\rightarrow T_2)$ and for any $a$, if $a:T'$ then $a:T_1$
   
 
\end{enumerate}

We
specify the type $(T_1\rightharpoonup T_2)$   to be the labelled set

$\{\langle\mathrm{partdmn},T_1\rangle,\langle\mathrm{rng},T_2\rangle\}$

where `partdmn' (``partial domain'') and `rng' (``range'') are
reserved labels (`rng' being the same reserved label that was used for
total function types).


% A\todo{Do we want both these definitions?} system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
% $\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
%   Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
%   polymorphic function types} if
% \begin{enumerate} 
 
% \item for any $T_1,T_2 \in \textbf{Type}$,
%   $\displaystyle{\bigvee_{T\sqsubseteq T_1}}(T\rightarrow T_2) \in \textbf{Type}$ 
 
% \item for any $T_1,T_2 \in \textbf{Type}$,
%   $f:_{\mathbf{TYPE_C}}\displaystyle{\bigvee_{T\sqsubseteq
%       T_1}}(T\rightarrow T_2)$ iff there is some type $T'$ such that
%   $f:(T'\rightarrow T_2)$ and $T'\sqsubseteq T_1$
   
 
% \end{enumerate}

% We
% specify the type $\displaystyle{\bigvee_{T\sqsubseteq T_1}}(T\rightarrow T_2)$   to be the labelled set

% $\{\langle\mathrm{polydmn},T_1\rangle,\langle\mathrm{rng},T_2\rangle\}$

% where `polydmn' (``polymorphic domain'') and `rng' (``range'') are
% reserved labels (`rng' being the same reserved label that was used for
% non-polymorphic function types).






We introduce a notation for functions which is borrowed from the
$\lambda$-calculus:

$\lambda v\!:\!T\ .\ \varphi$ (Chapter~\ref{ch:percint},
p.~\pageref{ex:fun-notation}) is that function $f$ such that for any
$a:T$, $f(a)$ (the result of applying $f$ to $a$) is represented by
$\varphi[v\leftarrow a]$ (the result of replacing any free occurrence
of $v$ in $\varphi$ with $a$).

%  as used by \cite{Montague1973}.  Let $O[v]$ be the
% notation for some object of our type theory which uses the variable
% $v$ and let $T$ be a type.  Then the function

% $\lambda v:T\ .\ O[v]$ 

% is to be the function

% $\{\langle v,O[v]\rangle\mid v:T\}$

% (Here we suppress the subscript $\mathbf{TYPE_C}$ on the `:'.)
For
example, the graph of the function

$\lambda v$:\textit{Ind} . run($v$)

is the set of ordered pairs

$\{\langle v,\mathrm{run}(v)\rangle\mid v:\mathit{Ind}\}$

Recall that `run($v$)' is itself a representation for the labelled
set

$\{\langle \mathrm{pred},\mathrm{run}\rangle, \langle
\mathrm{arg}_1,v\rangle\}$

Note that if $f$ is the function $\lambda v$:\textit{Ind} . run($v$)
and $a$:\textit{Ind} then $f(a)$ (the result of applying $f$ to $a$)
is `run($a$)'.  Our definition of function-argument application
guarantees what is called $\beta$-equivalence in the
$\lambda$-calculus.  When we discuss record types as arguments to
functions we will need to introduce one slight complication to our
notion of function application.  We will introduce that complication
when we discuss record types.

In order to maintain $\alpha$-equivalence (for example, if $v_1$ and
$v_2$ are distinct variables, $\lambda v_1\!:\!T\ .\ \varphi\dep{v_1}$
represents the same function as $\lambda v_2\!:\!T\ .\
\varphi\dep{v_2}$), we use a variant of de Bruijn indexing
\citep{deBruijn1972} in the labelled set we use to model functions.
We model functions as labelled sets with two fields with the
distinguished labels `lambda' and `body'.
Where de Bruijn uses natural numbers to index the variable positions
we use segments of paths in the labelled set which relate the
appropriate instance of the 'body'-label labelling the field which is
sister to the binding 'lambda'-field.  Thus
\begin{quote}
  $\lambda v$:\textit{Ind} . run($v$)
\end{quote}
is the labelled set
\begin{quote}
  \begin{tabbing}
    $\{$\=$\langle$lambda, \textit{Ind}$\rangle$,\\
    \>$\langle$body, $\{$\=$\langle$pred, run$\rangle$,\\
    \>\>                  $\langle$arg$_1$, body.arg$_1\rangle\}\rangle\}$
  \end{tabbing}
\end{quote}
and
\begin{quote}
  $\lambda v_1$:\textit{Ind} . $r_1(v_1,\lambda v_2$:\textit{Ind}
  . $r_2(v_2,v_1))$
\end{quote}
is the labelled set
\begin{quote}
  \begin{tabbing}
    $\{$\=$\langle$lambda, \textit{Ind}$\rangle$,\\
    \>   $\langle$body, $\{$\=$\langle$pred, $r_1\rangle$,\\
    \>\>                     $\langle$arg$_1$, body.arg$\rangle$,\\
    \>\>                     $\langle$arg$_2$, $\{$\=$\langle$lambda, \textit{Ind}$\rangle$,\\
    \>\>\>                                          $\langle$body, $\{$\=$\langle$pred, $r_2\rangle$,\\
    \>\>\>\>                                                            $\langle$arg$_1$, body.arg$_1\rangle$,\\
    \>\>\>\>                                                            $\langle$arg$_2$, body.arg$_2$.body.arg$_2\rangle\}\rangle\}\rangle\}\rangle\}$
  \end{tabbing}
\end{quote}





\section{Set types}
\label{app:settypes}

Set types were not included in \cite{Cooper2012}.

A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has set
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:settypes}) if
\begin{enumerate} 
 
\item for any $T \in \textbf{Type}$, $\mathrm{set}(T) \in \textbf{Type}$ 
 
\item for any $T \in \textbf{Type}$, 
$X:_{\mathbf{TYPE_C}}\mathrm{set}(T)$ iff  $X$ is a set and 
for all $a\in X$, $a:_{\mathbf{TYPE_C}}T$

\item for any $T \in \textbf{Type}$, if $X:\mathrm{set}(T)$, then
  $\mathfrak{T}(X)\in \textbf{Type}$ (Chapter~\ref{ch:quant},
  p.~\pageref{ex:mathfrakT})

  
\item $a:\mathfrak{T}(X)$ iff $a\in X$
   
 
\end{enumerate}

We let $\mathrm{set}(T)$ represent the labelled set
$\{\langle\mathrm{set},T\rangle\}$ where `set' is a reserved
label.

% If $T$ is a type and $X:\mathrm{set}(T)$, then $\mathfrak{T}(X)$ is a
% type.  $a:\mathfrak{T}(X)$ iff $a\in X$. (Chapter~\ref{ch:quant},
% p.~\pageref{ex:mathfrakT})\todo{Need to expand this to a system of
%   complex types with set types and membership types}

% We also introduce a special kind of set type known as a plurality
% type.  The idea here is that a plurality is a set that does not contain any two
% objects such that one is a proper part of the other.  The notion of
% proper part is characterized by:
% \begin{enumerate}
% \item If $r_1$ and $r_2$ are records then $r_1$ \textit{is a proper
%     part of} $r_2$, $r_1<r_2$, just in case $\varphi(r_1)\subset\varphi(r_2)$. 
 
% \item If $o_1$ and $o_2$ are objects of some type and at least one of
%   them is not of type \textit{Rec}, then $o_1$ is \textit{not} a
%   proper part of $o_2$, $o_1\not<o_2$ 
% \end{enumerate}

In order to define plurality types as subtypes of set types we
introduce a notion of one record being a proper part of another.

For any objects $r_1$ and $r_2$, $r_1$ \textit{is a proper
    part of} $r_2$, $r_1<r_2$, (Chapter~\ref{ch:commonnouns},
  p.~\pageref{ex:properpart}) just in case
  \begin{enumerate}
  \item $r_1$ and $r_2$ are records, 
  \item
    $\mathrm{paths}_{\text{rec}}(r_1)\subset\mathrm{paths}_{\text{rec}}(r_2)$
      and
    \item for all $\pi\in\mathrm{tpaths}(r_1)$, $r_1.\pi=r_2.\pi$
    \end{enumerate} 

A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with set types
\textit{has plurality types} (Chapter~\ref{ch:commonnouns},
p.~\pageref{ex:plurality-types}) if
\begin{enumerate} 
 
\item for any $T \in \textbf{Type}$, $\mathrm{plurality}(T) \in \textbf{Type}$ 
 
\item for any $T \in \textbf{Type}$, 
$A:_{\mathbf{TYPE_C}}\mathrm{plurality}(T)$ iff  
\begin{enumerate} 
 
\item $A :_{\mathbf{TYPE_C}} \mathrm{set}(T)$ 
 
\item if $a\in A$ then for any $b$ such that $a<b$, $b\not\in A$ 
 
\end{enumerate} 
  
   
 
\end{enumerate}

We let $\mathrm{plurality}(T)$ represent the labelled set
$\{\langle\text{plurality},T\rangle\}$ where `plurality' is a reserved
label. 

\section{Singleton types}
\label{app:singletontypes}

Singleton types were not included in the formal definition in \cite{Cooper2012}.

A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
  singleton types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:singleton-types}) if
% \begin{enumerate} 
 
% \item for any $T \in \textbf{Type}$ and $a:_{\mathbf{TYPE_C}}T$, $T_a \in \textbf{Type}$ 
 
% \item for any $T \in \textbf{Type}$ and $a:_{\mathbf{TYPE_C}}T$, 
% $b:_{\mathbf{TYPE_C}}T_a$ iff  $a=b$
   
 
% \end{enumerate}

% These clauses are those presented in \cite{Cooper2012}. A more general
% version of these clauses seems useful for the uses we wish to make of
% singleton types, for example, the restriction of properties discussed
% in Appendix~\ref{app:gramrulesuniv}.  The more general version allows
% singleton types to be created using an object of any type but will
% guarantee that the type is empty if the object is not of the type
% being restricted: 
\begin{enumerate} 
 
\item for any $T,T' \in \textbf{Type}$ and $a:_{\mathbf{TYPE_C}}T'$, $T_a \in \textbf{Type}$ 
 
\item for any $T,T' \in \textbf{Type}$ and $a:_{\mathbf{TYPE_C}}T'$, 
$b:_{\mathbf{TYPE_C}}T_a$ iff  $b:_{\mathbf{TYPE_C}}T$ and $a=b$
   
 
\end{enumerate}
% As we now allow singleton types that are empty (because the object
% used to restrict them is not of the required type) it may seem that
% the name ``singleton type'' is a misnomer.  The cases of empty types
% are those where we have failed to define a singleton type.


We let $T_a$ represent the labelled set
$\{\langle\mathrm{singleton},\langle T,a\rangle\rangle\}$ where `singleton' is a reserved
label.
 
\section{Join types}
\label{app:jointypes}


A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has join
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:jointypes}) if 

\begin{enumerate} 
 
\item for any $T_1,T_2 \in \mathbf{Type}$, $(T_1\vee T_2) \in \mathbf{Type}$ 
 
\item for any $T_1,T_2 \in \mathbf{Type}$, $a:_{\mathbf{TYPE_C}}(T_1\vee T_2)$ iff
  $a:_{\mathbf{TYPE_C}}T_1$ or $a:_{\mathbf{TYPE_C}}T_2$ 
 
\end{enumerate}

Here, but not in \cite{Cooper2012}, we specify that $(T_1\vee T_2)$
represents the labelled set
$\{\langle\mathrm{disj}_1,T_1\rangle,\langle\mathrm{disj_2},T_2\rangle\}$
where `disj$_1$' and `disj$_2$' are reserved labels (``disjunct'').

We add generalized join types which were not present in
\cite{Cooper2012}.  A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
  generalized join
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:genjointypes}) if 

\begin{enumerate} 
 
\item for any finite set of types, $\mathscr{T}$, such that $\mathscr{T}
  \subseteq\mathbf{Type}$, $\bigvee\mathscr{T} \in \mathbf{Type}$ 
 
\item for any finite $\mathscr{T} \subseteq\mathbf{Type}$, $a:_{\mathbf{TYPE_C}}\bigvee\mathscr{T}$ iff
  $a:_{\mathbf{TYPE_C}}T$ for some $T\in\mathscr{T}$
 
\end{enumerate}

We specify that $\bigvee\mathscr{T}$
represents the labelled set
$\{\langle\mathrm{disj},\mathscr{T}\rangle\}$
where `disj' is a reserved label (``disjunction'').

\section{Meet types}
\label{app:meettypes}

A system of complex types \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has meet
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:meettypes}) if
\begin{enumerate} 
 
\item for any $T_1,T_2 \in \mathbf{Type}$, $(T_1\wedge T_2) \in \mathbf{Type}$ 
 
\item for any $T_1,T_2 \in \mathbf{Type}$, $a:_{\mathbf{TYPE_C}}(T_1\wedge T_2)$ iff
  $a:_{\mathbf{TYPE_C}}T_1$ and $a:_{\mathbf{TYPE_C}}T_2$ 

\end{enumerate}

Here, but not in \cite{Cooper2012}, we specify that $(T_1\wedge T_2)$
represents the labelled set
$\{\langle\mathrm{conj}_1,T_1\rangle,\langle\mathrm{conj_2},T_2\rangle\}$
where `conj$_1$' and `conj$_2$' are reserved labels (``conjunct'').

We add generalized meet types which were not present in
\cite{Cooper2012}.  A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
  generalized meet
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:genmeettypes}) if 

\begin{enumerate} 
 
\item for any non-empty finite set of types, $\mathscr{T}$, such that $\mathscr{T}
  \subseteq\mathbf{Type}$, $\bigwedge\mathscr{T} \in \mathbf{Type}$ 
 
\item for any finite $\mathscr{T} \subseteq\mathbf{Type}$, $a:_{\mathbf{TYPE_C}}\bigwedge\mathscr{T}$ iff
  $a:_{\mathbf{TYPE_C}}T$ for all $T\in\mathscr{T}$
 
\end{enumerate}

We specify that $\bigwedge\mathbb{T}$
represents the labelled set
$\{\langle\mathrm{conj},\mathbb{T}\rangle\}$
where `conj' is a reserved label (``conjunction'').


\section{Models and modal systems of types}
\label{app:modal}



A modal system of complex types
provides a collection of models, $\mathcal{M}$, so that we can talk about properties of the whole collection of
type assignments provided by the various models $M\in\mathcal{M}$.

A \textit{modal system of complex types based on $\mathcal{M}$}
(Chapter~\ref{ch:percint}, p.~\pageref{ex:modalsys-complex}) is a
family of quadruples\footnote{This definition has been modified since
  \cite{Cooper2012} to make \textbf{PType} and \textbf{Type} be
  relativized to the model $M$.}:
\begin{quote}
{\bf TYPE$_{\mathit{MC}}$} = $\langle${\bf Type}$_M$, {\bf BType},
$\langle$\textbf{PType}$_M$, {\bf Pred}, \textbf{ArgIndices}, {\it Arity\/}$\rangle, M\rangle_{M\in\mathcal{M}}$
\end{quote}
where for each $M\in \mathcal{M}$, $\langle${\bf Type}$_M$, {\bf BType},
$\langle$\textbf{PType}$_M$, {\bf Pred}, \textbf{ArgIndices}, {\it Arity\/}$\rangle, M\rangle$ is
a system of complex types.

This enables us to define modal notions:

If {\bf TYPE$_{\mathit{MC}}$} = $\langle${\bf Type}$_M$, {\bf BType},
$\langle$\textbf{PType}$_M$, {\bf Pred}, \textbf{ArgIndices}, {\it Arity\/}$\rangle, M\rangle_{M\in\mathcal{M}}$
is a modal system of complex types based
on $\mathcal{M}$, we shall use the notation {\bf
  TYPE$_{\mathit{MC}_M}$} (where $M\in\mathcal{M}$) to refer to that
system of complex types in {\bf TYPE$_{\mathit{MC}}$} whose model is
$M$.  Let \textbf{Type}$_{\mathit{MC}_{\mathit{restr}}}$ be
  $\bigcap\limits_{M\in\mathcal{M}}\!\textbf{Type}_M$, the
  ``restrictive'' set of
  types which occur in all possibilities,  and \textbf{Type}$_{\mathit{MC}_{\mathit{incl}}}$ be
  $\bigcup\limits_{M\in\mathcal{M}}\!\textbf{Type}_M$, the
  ``inclusive'' set of
  types which occur in at least one possibility.  Then we can define
  modal notions either restrictively or inclusively (indicated by the
  subscripts $r$ and $i$ respectively):

\paragraph{restrictive modal notions}  
\begin{enumerate} 
 
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T_1$ \textit{is
    (necessarily) equivalent$_r$
    to} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
  $T_1\approx_{\mathbf{TYPE_{\mathit{MC}}}}T_2$,  iff for all
  $M\in\mathcal{M}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}=\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
  
 
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T_1$ \textit{is a subtype$_r$ of} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
  $T_1\sqsubseteq_{\mathbf{TYPE_{\mathit{MC}}}}T_2$,  iff for all
  $M\in\mathcal{M}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}\subseteq\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$

\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T$ \textit{is necessary$_r$ in} {\bf TYPE$_{\mathit{MC}}$}  iff for all
  $M\in\mathcal{M}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$

\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T$ \textit{is possible$_r$ in} {\bf TYPE$_{\mathit{MC}}$}  iff for some
  $M\in\mathcal{M}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
 
\end{enumerate}

\paragraph{inclusive modal notions}
\begin{enumerate} 
 
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T_1$ \textit{is
    (necessarily) equivalent$_i$
    to} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
  $T_1\approx_{\mathbf{TYPE_{\mathit{MC}}}}T_2$,  iff for all
  $M\in\mathcal{M}$, if $T_1$ and $T_2$ are members of
  \textbf{Type}$_M$, then $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}=\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
  
 
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T_1$ \textit{is a subtype$_i$ of} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
  $T_1\sqsubseteq_{\mathbf{TYPE_{\mathit{MC}}}}T_2$,  iff for all
  $M\in\mathcal{M}$, if $T_1$ and $T_2$ are members of
  \textbf{Type}$_M$, then $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}\subseteq\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$

\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T$ \textit{is necessary$_i$ in} {\bf TYPE$_{\mathit{MC}}$}  iff for all
  $M\in\mathcal{M}$, if $T\in$\textbf{Type}$_M$, then \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$

\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T$ \textit{is possible$_i$ in} {\bf TYPE$_{\mathit{MC}}$}  iff for some
  $M\in\mathcal{M}$, if $T\in$\textbf{Type}$_M$, then\\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
 
\end{enumerate}

It is easy to see that if any of the restrictive definitions holds for
given types in a particular system then the corresponding inclusive
definition will also hold for those types in that system.






\section{The type \textit{Type} and stratification}

\label{app:int}

% An intensional type system is one in which the types themselves become
% objects of a type. We introduce a distinguished type \textit{Type} to
% which all the members of the set \textbf{Type} belong.  Things are a
% little more complicated than this, though, since we want \textit{Type}
% itself to be a type and therefore it should belong to the set
% \textbf{Type}.  This would mean that \textit{Type} belongs to itself,
% i.e. \textit{Type}:\textit{Type}.  Allowing types to belong to
% themselves puts us in danger of creating a situation in which
% Russell's paradox arises.  If some members of \textbf{Type} belong to
% themselves then we should be able to talk of the set of types which do
% not belong to themselves,
% $\{T\in\mathbf{Type}\mid T\not\ : T\}$.  Suppose that some model
% assigns this set to $T'$.  Then the question arises whether $T'$
% belongs to itself and we can show that if $T':T'$ then $T'\not\ :T'$
% and if $T'\not\ :T'$ then $T':T'$.  

% In order to avoid this problem we
% will \textit{stratify} (or \textit{ramify}) our type system by introducing types of
% different \textit{orders}.   A type system of order 0 will be a
% system of complex types in the way we have defined it.  The
% set of types, \textbf{Type}$^1$ of a type
% system of order 1 based on this system will contain in addition to
% everything in the original type system a type, \textit{Type}$^1$, to
% which all the types of order 0, members of the set \textbf{Type}$^0$, belong.  In general for all the natural
% numbers $n$, \textit{Type}$^{n+1}$ will be a type to which all the
% types in \textbf{Type}$^n$ belong.  But there may be more additional
% types included in the higher sets of types.  Suppose, for example,
% that we want to introduce a predicate $P$ expressing a relationship
% between individuals and types.  (This will be our basic strategy for
% the treatment of attitude predicates such as \textit{believe} and
% \textit{know}.)  Then \textit{Arity}($P$) might be $\langle
% \mathit{Ind},\mathit{Type}^n\rangle$.  In systems of any order less
% than $n$, $P$ will not be able to be used to construct a type because
% clause~\ref{cl:predtypes} in our definition of systems of complex
% types requires that the types assigned to the arguments be types in
% the system.  However, in systems of order $n$ or greater the required
% type will be present and the predicate will form a type.

% This avoids the risk of running into Russell's paradox but it
% introduces another problem which it is best we deal with straight
% away.  We will illustrate the problem by creating a small example.
% Suppose that we have a system of complex types which includes the type
% \textit{Ind} (``individuals'') to which the objects $a$, $b$ and $c$
% belong.  Suppose further that we have three predicates
% \textit{run},\textit{know} and \textit{believe} and that
% \textit{Arity}(\textit{run})=$\langle\mathit{Ind}\rangle$ and
% \textit{Arity}(\textit{know})=\textit{Arity}(\textit{believe})=$\langle\mathit{Ind},\mathit{Type}^1\rangle$. 
% The set \textbf{Type}$^0$ will contain the types \textit{run}($a$),
% \textit{run}($b$) and \textit{run}($c$) but no types constructed with
% \textit{know} and \textit{believe}.  The set \textbf{Type}$^1$ will
% contain types
% such as \textit{believe}($a$, \textit{run}($a$)) and
% \textit{know}($c$, \textit{run}($b$)) in addition, since \textit{run}($a$),
% \textit{run}($b$) and \textit{run}($c$), being members of
% \textbf{Type}$^0$ will belong to the type \textit{Type}$^1$.  The set
% \textbf{Type}$^2$ will not get any additional types constructed with
% predicates since the arity of the predicates restricts the second
% argument to be of \textit{Type}$^1$.  But suppose we want to express
% that $a$ believes that $b$ knows that $c$ runs, that is we want to
% construct the type \textit{believe}($a$, \textit{know}($b$,
% \textit{run}($c$))).  Perhaps we could solve this by saying that the
% arity of \textit{know} and \textit{believe} is
% $\langle\mathit{Ind},\mathit{Type}^2\rangle$.  But now
% \textbf{Type}$^1$ will not contain any types constructed with these
% predicates and \textbf{Type}$^2$ will again only contain types such as
% \textit{know}($c$, \textit{run}($b$)).

% In order to solve this problem we need to introduce a limited amount
% of \textit{polymorphism} into our arities and assign these predicates
% the arity $\langle\mathit{Ind},\mathit{Type}^n\rangle_{n>0}$ (that is,
% the set of sequences $\langle\mathit{Ind},\mathit{Type}^n\rangle$
% where $n$ is a natural number greater than 0).  Predicates with this
% arity will be able to take arguments of any type \textit{Type}$^n$ where
% $n>0$.  We will say that the predicates \textit{know} and
% \textit{believe} have this arity.  Now it will be the case that
% \textit{run}($c$):\textit{Type}$^1$, \textit{know}($b$,
% \textit{run}($c$)):\textit{Type}$^2$, \textit{believe}($a$, \textit{know}($b$,
% \textit{run}($c$))):\textit{Type}$^3$ and so on.

% \bigskip

An {\it intensional system of complex types\/}
(Chapter~\ref{ch:percint}, p.~\pageref{ex:int-type-sys}) is a family of
quadruples indexed by the natural numbers:
\begin{quote}
{\bf TYPE$_\mathit{IC}$} = $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F^n\rangle$$\rangle_{n\in\mathit{Nat}}$
\end{quote}
where (using $\mathbf{TYPE}_{\mathit{IC}_n}$ to refer to the quadruple
indexed by $n$):
\begin{enumerate} 
 
\item for each $n$,$\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F^n\rangle$$\rangle$ is a 
system of complex types  
 
\item for each $n$, $\mathbf{Type}^n\subseteq\mathbf{Type}^{n+1}$ and
  $\mathbf{PType}^n\subseteq\mathbf{PType}^{n+1}$

\item for each $n$, if $T\in\mathbf{PType}^n$ then $F^n(T)\subseteq F^{n+1}(T)$%and $p\in F^n(T)$ then
  %$p\in F^{n+1}(T)$

\item for each $n>0$, $\mathit{Type}^n\in\mathbf{Type}^n$

\item for each $n>0$,
  $T:_{\mathbf{TYPE}_{\mathit{IC}_n}}\mathit{Type}^n$ iff $T\in\mathbf{Type}^{n-1}$
 
\end{enumerate}

Here, but not in \cite{Cooper2012}, we make explicit that
\textit{Type} is a distinguished urelement and that \textit{Type}$^n$
represents the labelled set
$\{\langle\mathrm{ord},n\rangle,\langle\mathrm{typ},\mathit{Type}\rangle\}$
where `ord' and `typ' are reserved labels (``order'', ``type'').

\label{pg:dep-fn-types}An intensional system of complex types \textbf{TYPE}$_\mathit{IC}$,
\begin{display}
{\bf TYPE$_\mathit{IC}$} = $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F^n\rangle$$\rangle_{n\in\mathit{Nat}}$
\end{display} 
\textit{has dependent function types} (Chapter~\ref{ch:infex},
p.~\pageref{ex:dep-fun-types}) if
\begin{enumerate} 
 
\item for any $n>0$, $T \in \mathbf{Type}^n$ and
  $\mathcal{T}:_{\mathbf{TYPE}_{\mathit{IC}_n}}(T\rightarrow\mathit{Type^n})$,
  $((a:T)\rightarrow \mathcal{T}(a)) \in \mathbf{Type}^n$ 
 
\item for each $n>0$,
$f:_{\mathbf{TYPE}_{\mathit{IC}_n}}((a:T)\rightarrow \mathcal{T}(a))$
iff $f$ is a function whose domain is $\{a\mid
a:_{\mathbf{TYPE}_{\mathit{IC}_n}}T\}$ and such that for any $a$ in the
domain of $f$, $f(a):_{\mathbf{TYPE}_{\mathit{IC}_n}}\mathcal{T}(a)$.
   
 
\end{enumerate} 
We might say that on this view dependent function types are
``semi-intensional'' in that they depend on there being a type of
types for their definition but they do not introduce types as
arguments to predicates and do not involve the definition of orders of
types in terms of the types of the next lower order.

Here, in contrast to \cite{Cooper2012}, we make explicit that
$((a:T)\rightarrow \mathcal{F}(a))$ represents the labelled set
$\{\langle\mathrm{dmn},T\rangle,\langle\mathrm{deprng},\mathcal{F}\rangle\}$
where `dmn' as before for function types is a reserved label
corresponding to ``domain'' and `deprng' is a reserved label
corresponding to ``dependent range''.

Let $M$ be a model, $\langle A,F\rangle$, where
$A$ is an assignment to basic types and $F$ an assignment to ptypes as
usual.  Let $\mathcal{M}$ be an infinite sequence of models, $M$, indexed by
the natural numbers, corresponding to the models for the type systems
of each order in an intensional type system.  We use $\mathcal{M}_n$
to represent the model for the $n$-th order in an intensional type
system.  We use $\mathfrak{M}$ to represent a set of such model
sequences, representing the model sequences for each of the
possibilities in the intensional modal type system.  Putting the definition of a modal type system and an intensional type
system together we obtain:\footnote{This explicit definition was not
  present in \cite{Cooper2012}.}

An {\it intensional modal system of complex types based on
  $\mathfrak{M}$\/} (Chapter~\ref{ch:intensional}, p.~\pageref{ex:intensional-modal-type-sys}) is a family,
indexed by the natural numbers, of families of quadruples indexed by
members of $\mathfrak{M}$:
\begin{display}
{\bf TYPE$_\mathit{IMC}$} = $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\mathscr{M}_n$$\rangle_{\mathscr{M}\in\mathfrak{M},n\in\mathit{Nat}}$
\end{display}
where:
\begin{enumerate} 
 
\item for each $n$, $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\mathscr{M}_n$$\rangle_{\mathscr{M}\in\mathfrak{M}}$ is a modal
  system of complex types based on $\{\mathscr{M}_n\mid \mathscr{M}\in\mathfrak{M}\}$ 
 
\item for each $\mathscr{M}\in\mathfrak{M}$, $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\mathscr{M}_n$$\rangle_{n\in\mathit{Nat}}$ is an
  intensional system of complex types
 
\end{enumerate} 
 


\section{Records and Record types}
\label{app:rectypes}



In this section we will define what it means for a system of complex
types to have record types.  The objects of record types, that is,
records, are themselves structured mathematical objects of a
particular kind and we will
start by characterizing them.

\subsection{Records}
\label{app:rec}

% A \textit{record according to a set of labels $\mathcal{L}$ and a type
% system $\mathbb{T}$} (Chapter~\ref{ch:percint}, p.~\pageref{ex:records})  is a
% finite labelled set (Appendix~\ref{app:sets})
% whose labels are included in $\mathcal{L}$ and whose labelled elements
% are witnesses of some type according to $\mathbb{T}$.

$r$ is a \textit{record according to a set of labels $\mathcal{L}$ and a type
system $\mathbb{T}$} (Chapter~\ref{ch:percint},
p.~\pageref{ex:records}) iff $r$ is a finite labelled set
(Appendix~\ref{app:sets}) whose labels are included in $\mathcal{L}$
and for any labelled element, $v$, in $r$, there is some type $T$ such
that $v:_{\mathbb{T}}T$.

% We call the ordered pairs which constitute a labelled set which is a record \textit{fields}.
% The labels of the labelled set we will refer to as \textit{labels} of
% the record and the labelled elements of the labelled set we refer to
% as \textit{values} in the record 

\ignore{A {\it record\/} is a finite set of ordered pairs (called {\it fields\/})
which is the graph of a function.}  If $r$ is a record and $\langle\ell,v\rangle$
is in $r$, we call $\langle\ell,v\rangle$ a \textit{field} of $r$,
$\ell$ a {\it label\/} in $r$ and $v$ a {\it value\/} in $r$ (the
\textit{value of $\ell$ in $r$}).
We use $r.\ell$ to denote $v$.  \ignore{$r.\ell$ is called a \textit{path}
in $r$.}  \ignore{This means that a record is a labelled set as introduced in Appendix~\ref{app:sets}.}

We use a tabular format to
represent records.  A record 
$\{\langle\ell_1,v_1\rangle,\ldots,\langle\ell_n,v_n\rangle\}$ is displayed as
\begin{display}
\record{\field{$\ell_1$}{$v_1$} \\
        &\vdots& \\
        \field{$\ell_n$}{$v_n$}}
\end{display}

An alternative notation is as a tree (or directed graph) whose root is
unlabelled:
\begin{quote}
\Tree [ [.$\ell_1$ $v_1$ ]  {\hspace*{4em}\ldots}   {\mbox{}}  [.$\ell_n$
$v_n$ ] ]   
\end{quote}

We will sometime says that the occurrences $\ell_1,\ldots,\ell_n$ are
\textit{sisters} in the record.\label{pg:sisters}

Records, as labelled sets, will have paths  as defined for labelled
sets.  However, we will want in addition a more restricted notion of
path for records which excludes those paths which include the
distinguished labels used in non-record structures which may be values
in a record (Chapter~\ref{ch:percint},p.~\pageref{pg:record-paths}).

If $r$ is a record, then
\begin{enumerate} 
 
\item if $\ell\in\mathrm{labels}(r)$, then $\ell\in\mathrm{paths}_{\text{rec}}(r)$ 
 
\item if $\ell\in\mathrm{labels}(r)$, $r.\ell$ is a record and
  $\pi\in\mathrm{paths}_{\text{rec}}(r.\ell)$, then $\ell.\pi\in\mathrm{paths}_{\text{rec}}(r)$
\end{enumerate}  

Similarly, $\mathrm{tpaths}_{\text{rec}}(r)$ is the set of paths,
$\pi$, such that $\pi\in\mathrm{paths}_{\text{rec}}(r)$ and $r.\pi$ is
not a record.

We say that $\eta$ is a $\mathcal{L}$-relabelling$_{\text{rec}}$ for a record,
$r$, just
in case it is a $\mathcal{L}$-relabelling for $r$ whose domain is a
subset of $\mathrm{paths}_{\text{rec}}(r)$.

We generally use `$\mathrm{paths}$' and `$\mathrm{tpaths}$' without the subscript for these
more restricted notions when there is no risk for confusion.
Similarly we talk of relabellings for records when what is meant are relabellings$_{\text{rec}}$.

% A value may itself be a record and paths may extend into embedded
% records.  A record which contains records as values is called a {\it
%   complex record\/} and otherwise a record is {\it simple\/}.  Values which are not records are called {\it
%   leaves\/}.  Consider a record $r$ \label{pg:record}
% \begin{display}
% \record{\field{$f$}{\record{\field{$f$}{\record{\field{$\mathit{ff}$}{$a$}\\
%                                                 \field{$\mathit{gg}$}{$b$}}}\\
%                             \field{$g$}{$c$}}}\\
%         \field{$g$}{\record{\field{$h$}{\record{\field{$g$}{$a$}\\
%                                                 \field{$h$}{$d$}}}}}}
% \end{display}
% Among the paths in $r$ are $r.f$, $r.g.h$ and $r.f.f.\mathit{ff}$ which denote,
% respectively, 
% \begin{display}
% \record{\field{$f$}{\record{\field{$\mathit{ff}$}{$a$}\\
%                                                 \field{$\mathit{gg}$}{$b$}}}\\
%                             \field{$g$}{$c$}}
% \end{display}
% \begin{display} 
% \record{\field{$g$}{$a$}\\
%                                                 \field{$h$}{$d$}}
% \end{display}
% and $a$.  We will make a distinction between \textit{absolute paths},
% such as those we have already mentioned, which consist of a record
% followed by a series of labels connected by dots and \textit{relative
%   paths} which are just a series of labels connected by dots,
% e.g. $g.h$.  Relative paths are useful when we wish to refer to
% similar paths in different records.  We will use \textit{path} to
% refer to either absolute or relative paths when it is clear from the
% context which is meant. 
The  \textit{extension} of a record, $r$, is
\begin{quote}
  $\displaystyle{\bigcup_{\pi\in\mathrm{tpaths}_{\text{rec}}(r)}\{r.\pi\}}$
\end{quote}
The \textit{multiset extension} of $r$ is similarly
\begin{quote}
  $\displaystyle{\biguplus_{\pi\in\mathrm{tpaths}_{\text{rec}}(r)}\{r.\pi\}}$
\end{quote}
(where $\uplus$ represents multiset union).

A record may be
regarded as a way of labelling and structuring its (multiset) extension.

An object, $a$, is a \textit{component} (Chapter~\ref{ch:gram}, p.~\pageref{pg:component}) of a record, $r$, in symbols,
$a\varepsilon r$, just in case there is some path, $\pi$, in $r$ such
that $r.\pi=a$.  % Thus the record, $r$, above has the following
% components: $r.f$, $r.f.f$, $r.f.f.\mathit{ff}$,
% $r.f.f.\mathit{gg}$, $r.f.g$, $r.g$, $r.g.h$, $r.g.h.g$ and
% $r.g.h.h$. An object, $a$, is \textit{present} (Chapter~\ref{ch:gram},
% p.~\pageref{pg:present}) in a record, $r$, in
% symbols, $a\underline{\varepsilon} r$, just in case either $a=r$ or
% $a\varepsilon r$.

% We can, of course, also think of complex records as trees, for
% example:
% \begin{quote}
% \Tree [ [.\textit{f} 
%           [.\textit{f}
%               [.\textit{ff} $a$ ]
%               [.\textit{gg} $b$ ]
%           ]
%         [.\textit{g} $c$ ]
%         ]
%         [.\textit{g}
%           [.\textit{h}
%               [.\textit{g} $a$ ]
%               [.\textit{h} $d$ ]
%           ]
%         ]        
%       ] 
% \end{quote}
% We can thus use tree terminology to describe relationships between
% occurrences of labels.  For example, we can say that the topmost
% occurrence of \textit{f} immediately dominates another occurrence of
% \textit{f} and an occurrence of \textit{g}.\label{pg:imm-dom}

% Two
% records are {\it (multiset) extensionally equivalent\/} if they have
% the same (multiset) extension.  Two important, though trivial, facts
%   about records are:
% \begin{quote}
% {\it Flattening.\/} \label{pg:flattening} For any record $r$, there is a multiset
% extensionally equivalent simple record.  We can define an operation of flattening on records which
% will always produce an equivalent simple record.  In the case of our
% example, the result of flattening is
% \begin{display}
% \record{\field{$f.f.\mathit{ff}$}{$a$} \\
%         \field{$f.f.\mathit{gg}$}{$b$} \\
%         \field{$f.g$}{$c$} \\
%         \field{$g.h.g$}{$a$} \\
%         \field{$g.h.h$}{$d$}}
% \end{display}
% assuming the flattening operation uses paths from the original record
% in a rather obvious way to create unique labels for the new record.

% {\it Relabelling.\/}  \label{pg:relabelling}For any record $r$, if $\pi_1.\ell.\pi_2$ is a
% path $\pi$ in $r$, and $\pi_1.\ell'.\pi{_2}'$ is {\it not\/} a path in
% $r$ (for any $\pi{_2}'$),
% then substituting $\ell'$ for the occurrence of $\ell$ in $\pi$ results in
% a record which is multiset equivalent to $r$.  We could, for example,
% substitute $k$ for the second occurrence of $g$ in the path $g.h.g$ in our example record.

% \record{\field{$f$}{\record{\field{$f$}{\record{\field{$\mathit{ff}$}{$a$}\\
%                                                 \field{$\mathit{gg}$}{$b$}}}\\
%                             \field{$g$}{$c$}}}\\
%         \field{$g$}{\record{\field{$h$}{\record{\field{$k$}{$a$}\\
%                                                 \field{$h$}{$d$}}}}}}

% \end{quote}

% We will first look in more detail at flattening.  Flattened records
% have \textit{complex labels} (or \textit{paths}) of the form
% $\ell_1.\ell_2.\ldots.\ell_n$.  If $L$ is a set of labels, the set of
% \textit{complex labels}, $L_\pi$, \textit{based on} $L$ is the minimal
% set such that:
% \begin{enumerate} 
 
% \item if $\ell\in L$, then $\ell\in L_\pi$ 
 
% \item if $\pi\in L_\pi$ and $\ell\in L$, then $\pi.\ell\in L_\pi$ 
 
% \end{enumerate}

% Recall that a record, $r$, is a set of fields, $f$, where each $f$, is
% an ordered pair, $\langle\ell,v\rangle$ where $\ell$ is a (complex)
% label and $v$ is the value of the field which may itself be a record
% or some other object.  If $r$ is a record, then $\varphi(r)$,
% \textit{the flattening of} $r$, is \label{pg:flattening}
% \begin{quote}
% $\displaystyle{\bigcup_{f\in r}}\mathrm{FlattenField}(f)$
% \end{quote}
% where $\mathrm{FlattenField}(\langle\ell,v\rangle)$ is
% \begin{quote}
% $\varphi(\{\langle\ell.\ell_1,v_1\rangle,
%            \langle\ell.\ell_2,v_2\rangle,
%            \ldots,
%            \langle\ell.\ell_n,v_n\rangle\})$
% \end{quote}
% if $v$ is the record
% $\{\langle\ell_1,v_1\rangle,
%    \langle\ell_2,v_2\rangle,
%    \ldots,
%    \langle\ell_n,v_n\rangle\}$
% and
% $\langle\ell,v\rangle$
% otherwise.

% We can show that if $r$ is a record then $\varphi(r)$ is a record.  It
% follows trivially from the requirement that records are graphs of
% functions from labels to values.  If $r$ is a record
% $\{\langle\ell_1,v_1\rangle,\ldots,\langle\ell_n,v_n\rangle\}$, then
% the \textit{set of labels of} $r$, $\mathrm{labels}(r)$, is
% $\{\ell_1,\ldots,\ell_n\}$.  For example, if $r$ is the record
% \begin{quote}
% \record{\field{x}{\record{\field{z}{$a$}\\
%                           \field{w}{$b$}}}\\
%         \field{y}{$c$}}
% \end{quote}
% then $\mathrm{labels}(r)$ is $\{\mathrm{x},\mathrm{y}\}$. That is, `labels' picks out
% the ``highest level'' of labels in a complex record.
% We use $\mathrm{tpaths}(r)$ to represent the \textit{set of total
%   paths} of $r$, $\mathrm{labels}(\varphi(r))$.



% If $L$ is a set of labels,
% then the set of \textit{complex labels} (or \textit{paths}), $L_+$,
% based on $L$ is the minimal set such that
% \begin{enumerate} 
 
% \item if $\ell\in L$, then $\ell\in L_+$ 
 
% \item if $\pi\in L_+$ and $\ell\in L$, then $\pi.\ell\in L_+$ 
 
% \end{enumerate}

% If $r$ is a record such that $\mathrm{labels}(r)\subseteq L_+$, then
% the \textit{inverse flattening} (or \textit{expansion}) \textit{of}
% $r$, $\varphi^-(r)$, is the minimal set such that
% \begin{enumerate} 
 
% \item if $\langle\ell,v\rangle\in r$ and $\ell\in L$, then $\langle\ell,v\rangle\in\varphi^-(r)$ 
 
% \item if $\ell\in L$, $\pi\in L_+$ and $\langle\ell.\pi,v\rangle\in
%   r$, then 
% $\langle\ell,\varphi^-(\{\langle\pi',v'\rangle\mid\langle\ell.\pi',v'\rangle\in r\})\rangle\in\varphi^-(r)$
 
% \end{enumerate}

% \paragraph{Claim:} If $r$ is a record, then $\varphi^-(\varphi(r))=r$.

% The \textit{set of total paths of} $r$, $\mathrm{tpaths}(r)$, is
% $\mathrm{labels}(\varphi(r))$.

% If $r$ is a record, then the \textit{set
%   of paths of} $r$, $\mathrm{paths}(r)$, is the minimal set such that
% \begin{enumerate} 
 
% \item If $\pi\in\mathrm{tpaths}(r)$, then $\pi\in\mathrm{paths}(r)$ 
 
% \item If $\ell$ is a label (in $L$), $\pi$ is a non-empty path based
%   on $L$ and
%   $\pi.\ell\in\mathrm{paths}(r)$, then $\pi\in\mathrm{paths}(r)$ 
 
% \end{enumerate} 

% If $\Pi$ is a set of paths (in $L_+$), then the \textit{set of longest
%   paths in} $\Pi$, $\mathrm{longest}(\Pi)$ is such that
% $\pi\in\mathrm{longest}(\Pi)$ iff $\pi\in\Pi$ and there is no $\pi'$
% such that $\pi.\pi'\in\Pi$.

% \paragraph{Claim:}
% $\mathrm{longest}(\mathrm{paths}(r))=\mathrm{tpaths}(r)$

% If $R$ is a set of records, then 
% the \textit{set of common paths of} $R$,
% $\mathrm{cpaths}(R)$,\label{pg:cpaths} is
% \begin{quote}
% $\displaystyle{\bigcap_{r\in R}}\mathrm{paths}(r)$,
% \end{quote}
% the \textit{set of longest common
%   paths of} $R$, $\mathrm{lcpaths}(R)$, is
% \begin{quote}
% $\mathrm{longest}(\displaystyle{\bigcap_{r\in R}}\mathrm{paths}(r))$
% \end{quote} 
% and the \textit{set of common total paths of} $R$,
% $\mathrm{ctpaths}(R)$,\label{pg:ctpaths} is
% \begin{quote}
% $\displaystyle{\bigcap_{r\in R}}\mathrm{tpaths}(r)$
% \end{quote}

% \paragraph{Claim:} $\mathrm{lcpaths}(R)=\mathrm{ctpaths}(R)$



% Consider the records
% \begin{quote}
% $r_1$ = \record{\field{x}{\record{\field{x}{$a$}\\
%                                   \field{y}{$b$}}}\\
%                 \field{y}{\record{\field{x}{$c$}\\
%                                   \field{y}{$d$}}}}

% $r_2$ = \record{\field{x}{\record{\field{z}{$e$}\\
%                                   \field{w}{$f$}}}\\
%                 \field{y}{\record{\field{x}{$g$}\\
%                                   \field{y}{$h$}}}}
% \end{quote}
% The following hold true:
% \begin{quote}
% $\mathrm{paths}(r_1) = \{\mathrm{x},\mathrm{x.x},\mathrm{x.y},\mathrm{y},\mathrm{y.x},\mathrm{y.y}\}$\\
% $\mathrm{paths}(r_2) = \{\mathrm{x},\mathrm{x.z},\mathrm{x.w},\mathrm{y},\mathrm{y.x},\mathrm{y.y}\}$\\
% $\mathrm{lcpaths}(\{r_1,r_2\}) = \{\mathrm{x},\mathrm{y.x},\mathrm{y.y}\}$
% \end{quote} 
% The notion of longest common paths for a set of records will be
% important when we discuss paths in record types below.  [Is this still true?] 
  

% If $r$ is the record 
% \begin{quote}
% $\left\{\begin{array}{l}
%           \langle\ell_1.\pi_{1,1},v_{1,1}\rangle,
%           \langle\ell_1.\pi_{1,2},v_{1,2}\rangle,
%           \ldots,
%           \langle\ell_1.\pi_{1,m_1},v_{1,m_1}\rangle,\\
%           \langle\ell_2.\pi_{2,1},v_{2,1}\rangle,
%           \langle\ell_2.\pi_{2,2},v_{2,2}\rangle,
%           \ldots,
%           \langle\ell_2.\pi_{2,m_2},v_{2,m_2}\rangle,\\
%           \vdots\\
%           \langle\ell_n.\pi_{n,1},v_{n,1}\rangle,
%           \langle\ell_n.\pi_{n,1},v_{n,1}\rangle,
%           \ldots,
%           \langle\ell_n.\pi_{n,m_n},v_{n,m_n}\rangle
%           \end{array}
% \right\}$
% \end{quote}
% then $\varphi^-(r)$, the \textit{inverse
%   flattening} (or \textit{expansion}) \textit{of} $r$, is
% \begin{quote}
% $\left\{\begin{array}{l}
%           \langle\ell_1,\varphi^-(\{\langle\pi_{1,1},v_{1,1}\rangle,
%                                     \langle\pi_{1,2},v_{1,2}\rangle,
%                                     \ldots,
%                                     \langle\pi_{1,m_1},v_{1,m_1}\rangle\})
%                  \rangle,\\
%           \langle\ell_2,\varphi^-(\{\langle\pi_{2,1},v_{2,1}\rangle,
%                                     \langle\pi_{2,2},v_{2,2}\rangle,
%                                     \ldots,
%                                     \langle\pi_{2,m_2},v_{2,m_2}\rangle\})
%                  \rangle,\\
%           \vdots \\
%           \langle\ell_n,\varphi^-(\{\langle\pi_{n,1},v_{n,1}\rangle,
%                                     \langle\pi_{n,2},v_{n,2}\rangle,
%                                     \ldots,
%                                     \langle\pi_{n,m_n},v_{n,m_n}\rangle\})
%                  \rangle
%         \end{array}\right\}$
%     \end{quote}



% We now turn our attention to relabelling.\label{pg:relabelling}   
% An $L$\textit{-relabelling} is a one-one function whose domain and range
% are included in $L_+$.

% If $r$ is a record
% $\{\langle\ell_1,v_1\rangle,\ldots,\langle\ell_n,v_n\rangle\}$ and
% $\eta$ is a relabelling, the \textit{application of $\eta$ to $r$},
% $\eta*r$ is
% $\{\langle\ell'_1,v_1\rangle,\ldots,\langle\ell'_n,v_n\rangle\}$ where
% for each $i$ such that $1\leq i\leq n$, $\ell'_i$ is $\eta(\ell_i)$ if
% $\ell_i$ is in the domain of $\eta$ and $\ell_i$ otherwise.  Suppose
% $\eta$ is the relabelling $\mathrm{x}\leadsto\mathrm{xx},
% \mathrm{z}\leadsto\mathrm{zz}$ and $r$ is as above.  Then $\eta*r$ is
% \begin{quote}
% \record{\field{xx}{\record{\field{z}{$a$}\\
%                           \field{w}{$b$}}}\\
%         \field{y}{$c$}}
% \end{quote}
% That is, the label `x' is changed, but nothing else.

% We say that a relabelling, $\eta$, is \textit{limited} to a record,
% $r$, just in case $\mathrm{dom}(\eta)\subseteq\mathrm{labels}(r)$.\label{pg:limited}

% We are, however, mainly interested in replacing total paths in a
% record which is why we have defined relabellings on the set of paths,
% $L_+$ rather than the set of labels, $L$.  The \textit{result of
%   relabelling a record, $r$, with a relabelling, $\eta$}, in symbols,
% $[r]_\eta$, is $\varphi^-(\eta*\varphi(r))$.  We say that $\eta$ is a
% \textit{proper relabelling}\label{pg:proper-relabelling} for $r$ just in case $[r]_\eta$ is a
% record.

% Suppose $r$ is the record
% \begin{quote}
% \record{\field{x}{\record{\field{x}{$a$}\\
%                           \field{y}{$b$}}}\\
%         \field{y}{\record{\field{x}{$c$}}}}
% \end{quote}
% and $\eta$ is the relabelling
% \begin{quote}
% x.x $\leadsto$ y.z\\
% x.y $\leadsto$ x\\
% \end{quote}
% $\varphi(r)$ is the flattened record
% \begin{quote}
% \record{\field{x.x}{$a$}\\
%         \field{x.y}{$b$}\\
%         \field{y.x}{$c$}}
% \end{quote}
% $\eta*\varphi(r)$ is
% \begin{quote}
% \record{\field{y.z}{$a$}\\
%         \field{x}{$b$}\\
%         \field{y.x}{$c$}}
% \end{quote}
% Then $[r]_\eta$ is the expansion of this record, that is, the record
% \begin{quote}
% \record{\field{x}{$b$}\\
%         \field{y}{\record{\field{x}{$c$}\\
%                           \field{z}{$a$}}}}
% \end{quote}
% and $\eta$ is a proper relabelling for $r$.  

% Now let us consider a case where the relabelling is not proper.
% Suppose we start with the same record, $r$, as above but take a new
% relabelling, $\eta'$:
% \begin{quote}
% x.x $\leadsto$ x
% \end{quote}
% Now $\eta'*\varphi(r)$ is the record
% \begin{quote}
% \record{\field{x}{$a$}\\
%         \field{x.y}{$b$}\\
%         \field{y.x}{$c$}}
% \end{quote}
% However, the expansion $\varphi^-(\eta'*\varphi(r))$ is the set of
% ordered pairs:
% \begin{quote}
% $\{\langle\mathrm{x},a\rangle,
%    \langle\mathrm{x},\{\langle\mathrm{y},b\rangle\}\rangle,
%    \langle\mathrm{y},\{\langle\mathrm{x},c\rangle\}\rangle\}$
% \end{quote}
% which is not a record since it is not the graph of a function:  it has
% two ordered pairs whose first member is `x'.  We can read the problem
% already from the flattened record since it has a label, `x', which is a
% proper initial segment of another of its labels, `x.y'.  Therefore
% $\eta'$ is not a proper relabelling for $r$.  Note that we cannot read
% the improperness off $\eta'$ alone.  $\eta'$ is a proper relabelling
% for the record $r'$:
% \begin{quote}
% \record{\field{x}{\record{\field{x}{$a$}}}\\
%         \field{y}{\record{\field{x}{$c$}}}}
% \end{quote}
% $[r']_{\eta'}$ is the record:
% \begin{quote}
% \record{\field{x}{$a$}\\
%         \field{y}{\record{\field{x}{$c$}}}}
% \end{quote}



% We use $\eta^-$ to represent the inverse of the labelling $\eta$.
% That is, for any $\pi$, $\pi'$, $\pi\leadsto\pi'$ is in $\eta$ just in
% case $\pi'\leadsto\pi$ is in $\eta^-$. 
% \paragraph{Claim:} If
% $\eta$ is a proper relabelling for $r$ limited to $\varphi(r)$, then $\eta^-$ is a proper
% relabelling for $[r]_\eta$ and $[[r]_\eta]_{\eta^-}=r$.  

% The
% requirement that $\eta$ is limited to $\varphi(r)$ is important here
% since it prevents cases where $\eta^-$ would change labelling not
% changed by $\eta$.  Consider an example where $\eta$ is 
% \begin{quote}
% x $\leadsto$ z\\
% x.x $\leadsto$ y
% \end{quote}
% and $r$ is
% \begin{quote}
% \record{\field{x}{\record{\field{x}{$a$}}}\\
%         \field{z}{$b$}}
% \end{quote}
% Note that in this case $\eta$ is \textit{not} limited to $\varphi(r)$ whose
% labels are `x.x' and `z' but do not include `x'.  $\eta$ is
% proper for $r$ and $[r]_\eta$ is
% \begin{quote}
% \record{\field{y}{$a$}\\
%         \field{z}{$b$}}
% \end{quote}
% Now consider $\eta^-$ which is
% \begin{quote}
% z $\leadsto$ x\\
% y $\leadsto$ x.x
% \end{quote}
% The relabelling of $[r]_\eta$ by $\eta^-$ will be the set of ordered
% pairs
% \begin{quote}
% $\{\langle\mathrm{x},b\rangle,\langle\mathrm{x},\{\langle\mathrm{x},a\rangle\}\rangle\}$
% \end{quote}
% which is not a record (since `x' occurs twice as a label).  Hence in
% this case $\eta^-$ is not a proper relabelling for $[r]_\eta$ and
% $[[r]_\eta]_{\eta^-}$ is not identical with $r$.  The reason for this
% is that $\eta^-$ relabels a field that was not relabelled by $\eta$.
% Hence it is doing more than simply ``undoing'' the relabelling
% performed by $\eta$.  This state of affairs will be prevented by
% requiring that $\eta$ is limited to $r$, for example by removing `x
% $\leadsto$ z' from $\eta$.  Only paths changed by $\eta$ will be
% changed back by $\eta^-$ and our claim will hold true.

\paragraph{Using records as assignments}\mbox{}

From Chapter~\ref{ch:quant}, p.~\pageref{ex:vary-assgnmnt}:

If $r$ is a record, $\pi$ is $\ell_0.\ell_1.\ldots.\ell_n$ where
    $\ell_0,\ell_1,\ldots,\ell_n$ are labels and $v$ is an object of some
    type, then
    \begin{quote}
      if $\pi\not\in\mathrm{paths}(r)$, then $r[\pi=v]$ is the
      smallest record, $r'$, such that
      \begin{enumerate} 
        
      \item $\pi\in\mathrm{paths}(r')$ 
        
      \item $r'.\pi=v$
        
      \item for any $\pi'\in\mathrm{paths}(r)$,
        $\pi'\in\mathrm{paths}(r')$ and $r'.\pi'=r.\pi'$
        
      \end{enumerate} 

      if $\pi\in\mathrm{paths}(r)$, then $r[\pi=v]$ is the
      smallest record, $r'$, such that
      \begin{enumerate} 
        
      \item  $\pi\in\mathrm{paths}(r')$ and $r'.\pi=v$
        
      \item  for any $\pi'\in(\mathrm{paths}(r)-\{\pi''\mid
        \pi''\leq\pi\})$, $\pi'\in\mathrm{paths}(r')$ and $r'.\pi'=r.\pi'$
        
      \end{enumerate}
    \end{quote}

    If $r_1$ is a record and $r_2$ is a record such that
    $\mathrm{tpaths}(r_2)=\{\pi_1,\ldots,\pi_n\}$, then $r_1[r_2]$ is
    \begin{quote}
$r_1[\pi_1=r_2.\pi_1]\ldots[\pi_n=r_2.\pi_n]$
\end{quote}

\subsection{Record types}
\label{app:rectypes}

% A (proper) record \textit{type} is a labelled set 
% where the objects labelled are types or, in some cases, certain
% kinds of mathematical objects which can be used to construct types.

% A record $r$ is \textit{well-typed} with respect to a system of types
% \textbf{TYPE} with set of types \textbf{Type} and a set of labels $L$
% iff for each field $\langle\ell,a\rangle\in r$, $\ell\in L$ and
% either $a:_\mathbf{TYPE}T$ for some $T\in\mathbf{Type}$ or $a$ is
% itself a record which is well-typed with respect to \textbf{TYPE}
% and $L$.

We will model record types as flavoured labelled sets (see
Appendix~\ref{app:sets}) using a distinguished flavour `RT', the
``record type flavour''.  This is to distinguish record types from
records, which may in certain cases correspond to the same set of
ordered pairs.

A system of complex types \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
  (non-dependent) record
  types based on $\langle \mathcal{L}, \mathbf{RType}\rangle$},
 where $\mathcal{L}$ is a countably infinite set (of labels)
and \textbf{RType} $\subseteq$ \textbf{Type} 
(Chapter~\ref{ch:percint}, p.~\pageref{ex:ndrectypes}) if
\begin{enumerate} 
 
\item $\mathit{Rec}\in\mathbf{RType}$

\item $r:_{\mathbf{TYPE}_C}\mathit{Rec}$ iff $r$ is a record according
  to $\mathcal{L}$ and \textbf{TYPE$_C$}.

\item $\mathit{ERec}\in\mathbf{RType}$

\item $r:_{\mathbf{TYPE}_C}\mathit{ERec}$ iff $r=\emptyset$

\item if $\ell\in\mathcal{L}$ and $T\in\mathbf{Type}$, then
  $\{\text{RT},\langle\ell,T\rangle\}\in\mathbf{RType}$.

\item $r:_{\mathbf{TYPE}_C}\{\text{RT},\langle\ell,T\rangle\}$ iff
  $r:_{\mathbf{TYPE}_C}\mathit{Rec}$, $\langle\ell,a\rangle\in r$ and
  $a:_{\mathbf{TYPE}_C}T$.

\item if $R\in\mathbf{RType}-\{\mathit{Rec},\mathit{ERec}\}$, $\ell\in\mathcal{L}$, $\ell$ does not occur as a
  label in $R$ (i.e. there is no field $\langle\ell',T'\rangle$ in $R$
  such that $\ell'=\ell$) and $T\in\mathbf{Type}$, then
  $R\cup\{\langle\ell,T\rangle\}\in\mathbf{RType}$.\label{cl:ndrectype-emb}

\item $r:_{\mathbf{TYPE}_C}R\cup\{\langle\ell,T\rangle\}$ iff
  $r:_{\mathbf{TYPE}_C}R$, $\langle\ell,a\rangle\in r$ and $a:_{\mathbf{TYPE}_C}T$.
 
\end{enumerate}

% We say that $T$ is a \textit{proper} record type if it is a non-empty
% set of fields.\footnote{This terminology was not introduced in
% \cite{Cooper2012}.}\label{pg:proprectype}

 If  $T$ is a record type, then  (Chapter~\ref{ch:percint}, p.~\pageref{ex:paths-rectype})
\begin{quote} 
 

  $\pi\in\mathrm{paths}_{\text{rectype}}(T)$ iff for any $r:T$, $\pi\in\mathrm{paths}_{\text{rec}}(r)$ 
\end{quote}
and
\begin{quote}
 $\pi\in\mathrm{tpaths}_{\text{rectype}}(T)$ iff for any $r:T$, $\pi\in\mathrm{tpaths}_{\text{rec}}(r)$  
 
\end{quote} 

% The notion of paths for record types is the set of paths viewing the
% record type as a labelled set but without those paths which include
% distinguished labels used in the labelled sets for non-record
% structures except in the case of those used in meet types:
% `$\mathrm{conj}$', `$\mathrm{conj}_1$' and `$\mathrm{conj}_2$'.  We
% include modified versions of such paths where such labels have been
% removed.  

          
          
  


% This gives us non-dependent record types in a system of complex types.
% We can extend this to intensional systems of complex types (with
% stratification).  

% We can introduce a limited
% dependency into a system of complex types with record types by
% requiring that the values associated with certain fields are the
% results of applying an operation to the values of other fields. We
% first define an operation signature based on a system of complex
% types.

% An \textit{operation signature} based on  \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
% $\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
%   Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ is a set
% $\mathcal{O}$ of
% quadruples $\langle O, \langle T_1,\ldots,T_n\rangle, T, o\rangle$
% such that
% for any $\omega$ and $\omega'$ in $\mathcal{O}$, if
%   $\omega_1=\omega'_1$ (that is, the first elements of the tuples
%   are identical) then $\omega=\omega'$ (that is, $\mathcal{O}$
%   defines a function on the first elements of the tuples).  
%  Each quadruple is such that
% \begin{enumerate} 
 
% \item $O$ is a symbol (``operator symbol'') 
 
% \item for some $n$, $\langle T_1,\ldots,T_n\rangle$ is a sequence of
%   types in \textbf{Type} (``the arity of the operator'')

% \item $T$ is a type in \textbf{Type} (``the type of the range of the operator'')

% \item $o$ is an operator with domain $\{a\mid a:_{\mathbf{TYPE}_C}
%   T_1\}\times\ldots\times\{a\mid a:_{\mathbf{TYPE}_C} T_n\}$ and range
%   included in $\{a\mid a:_{\mathbf{TYPE}_C} T\}$
 
% \end{enumerate} 

% \sloppy{
% A system of complex types \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
% $\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
%   Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with record
%   types based on $\langle L, \mathbf{RType}\rangle$ \textit{has
%   operator dependent record types based on $\mathcal{O}$}, where
% $\mathcal{O}$ is an operation signature based on \textbf{TYPE}$_C$ if}
% \begin{enumerate} 
 
% \item  if $R$ is a member of {\bf RType}, $\ell\in L$ not occurring as a label in $R$, 
%   $R.\pi_1,\ldots,R.\pi_n$ are paths in $R$  and for some
%   $\omega\in\mathcal{O}$, $\omega_1$ is the operation symbol $O$ and
%   $\omega_2$ is an $n$-place sequence
%    $\langle
%   T_1,\ldots,T_n\rangle$ (that is $O$ is an $n$-place operation symbol
%   with arity $\langle
%   T_1,\ldots,T_n\rangle$) such that if $r:R$ then
%     $r.\pi_1:_{\mathbf{TYPE}_C}T_1,\ldots, r.\pi_n:_{\mathbf{TYPE}_C}T_n$ and $T$ is the range type $\omega_3$, then $R \cup \{\langle\ell, T_{O(\pi_1,\ldots,\pi_n)}\rangle\}$ is a
%     member of {\bf RType}.
    
    

 
% \item Using $o$ to represent the operator $\omega_4$, $r :_{\mathbf{TYPE}_C} R \cup \{\langle\ell, T_{O(\pi_1,\ldots,\pi_n)}\rangle\}$ iff $r :_{\mathbf{TYPE}_C}
%     R$, $\langle\ell,a\rangle$ is a field in $r$ and $a :_{\mathbf{TYPE}_C} T_{o(r.\pi_1,\ldots,r.\pi_n)}$. 
 
% \end{enumerate} 
  
    



An {\it intensional system of complex types\/} {\bf TYPE$_\mathit{IC}$} = $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle
A,F^n\rangle$$\rangle_{n\in\mathit{Nat}}$  \textit{has (non-dependent) record types
  based on} $\langle\mathcal{L}, \mathbf{RType}^n\rangle_{n\in\mathit{Nat}}$ (Chapter~\ref{ch:percint},
p.~\pageref{ex:int-ndrectype-sys}) if
for each $n$,  $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle
A,F^n\rangle$$\rangle$ has record types based on $\langle\mathcal{L},\mathbf{RType}^n\rangle$ and
\begin{enumerate} 
 
\item for each $n$, \textbf{RType}$^n$ $\subseteq$ \textbf{RType}$^{n+1}$ 
 
\item for each $n>0$, \textit{RecType}$^n$ $\in$ \textbf{Type}$^n$

\item for each $n>0$,
  $T:_{\mathbf{TYPE}_{\mathit{IC}_n}}\mathit{RecType}^n$ iff $T\in\mathbf{RType}^{n-1}$
 
\end{enumerate} 

Here, but not in \cite{Cooper2012}, we make explicit that
\textit{RecType} is treated in a similar manner to 
\textit{Type}, that is, it is a distinguished urelement and \textit{RecType}$^n$
represents the labelled set
$\{\langle\mathrm{ord},n\rangle,\langle\mathrm{typ},\mathit{RecType}\rangle\}$
where `ord' and `typ' are reserved labels (``order'', ``type'').


Intensional type systems 
may in addition contain \textit{dependent} record types.  

An {\it intensional system of complex types\/} {\bf TYPE$_\mathit{IC}$} = $\langle${\bf Type}$^n$, {\bf BType},
$\langle$\textbf{PType}$^n$, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle
A,F^n\rangle$$\rangle_{n\in\mathit{Nat}}$ \textit{has dependent record types
  based on} $\langle\mathcal{L}, \mathbf{RType}^n\rangle_{n\in\mathit{Nat}}$,
(Chapter~\ref{ch:percint}, p.~\pageref{ex:int-drectype-sys})
if it has record types based on $\langle\mathcal{L},
\mathbf{RType}^n\rangle_{n\in\mathit{Nat}}$ and for each $n>0$
\begin{enumerate} 
 
\item if $R\in\textbf{RType}^n$, $\ell\in\mathcal{L}-\mathrm{labels}(R)$, $T_1,\ldots,T_m\in\mathbf{Type}^n$, $\pi_1,\ldots,\pi_m\in\mathrm{paths}(R)$ and
    % ${\cal F}$ is a function of type $((a_1:T_1)\rightarrow\ldots\rightarrow((a_m:T_m)\rightarrow\mathit{Type}^n)\ldots)$, then $R \cup \{\langle\ell, \langle{\cal F}, \langle\pi_1,\ldots,\pi_m\rangle\rangle\rangle\}\in\mathbf{RType}^n$.
${\cal F}$ is a function of type $(T_1\rightarrow\ldots\rightarrow(T_m\rightarrow\mathit{Type}^n)\ldots)$, then $R \cup \{\langle\ell, \langle{\cal F}, \langle\pi_1,\ldots,\pi_m\rangle\rangle\rangle\}\in\mathbf{RType}^n$.

   


 
\item $r :_{\mathbf{TYPE}_{\mathit{IC}_n}}R\cup\{\langle\ell, \langle{\cal F}, \langle\pi_1,\ldots,\pi_m\rangle\rangle\rangle\}$ iff $r :_{\mathbf{TYPE}_{\mathit{IC}_n}} R$, $\langle\ell, a\rangle$ is a field
in $r$,  $r.\pi_1:_{\mathbf{TYPE}_{\mathit{IC}_n}}T_1,\ldots,r.\pi_m:_{\mathbf{TYPE}_{\mathit{IC}_n}}T_m$ and  $a :_{\mathbf{TYPE}_{\mathit{IC}_n}} {\cal F}(r.\pi_1)\ldots(r.\pi_m)$.  
 
\end{enumerate} 




We represent a record type $\{\text{RT},\langle\ell_1,T_1\rangle,\ldots,\langle\ell_n,T_n\rangle\}$
graphically as
\begin{quote}
\record{\tfield{$\ell_1$}{$T_1$} \\
        \ldots \\
        \tfield{$\ell_n$}{$T_n$}}
\end{quote}


In the case of a manifest field, that is, one containing a singleton
type, as in $\langle\ell,T_a\rangle$, we display this
\begin{display}
\record{\mfield{$\ell$}{$a$}{$T$}}
\end{display}
In the case of a multiple singleton type (a singleton type formed from
a singleton type) as in $\langle\ell,T_{a,b,\ldots}\rangle$, we display
\begin{display}
\record{\mfield{$\ell$}{$a,b,\ldots$}{$T$}}
\end{display}


In the case of dependent record types
we sometimes use a convenient notation representing e.g. 
\begin{display}
\mbox{$\langle\lambda u \lambda v\ 
\textrm{love}(u,v), \langle\pi_1,\pi_2\rangle\rangle$}
\end{display}
 as 
\begin{display}
love($\pi_1,\pi_2$)
\end{display}

% @@\todo{Move what follows into Ch. 1?  Move a redefinition of unique
%   identifier notation here and use for $\beta$-conversion?}

% [This is just wrong.  The paths in type only start from the level at
% which the dependent field is placed.  But what is the consequence for relabelling?]

% Our systems now allow both function types and dependent record types
% and allow dependent record types to be arguments to functions.  We
% have to be careful when considering what the result of applying a
% function to a dependent record type should be.  Consider the following
% simple example:
% \begin{display}
% $\lambda
% v_0:$\textit{RecType} . \smallrecord{\smalltfield{c$_0$}{$v_0$}}
% \end{display}
% What should be the result of applying this function to the record type
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v_1:$\textit{Ind} . dog($v_1$),
%           $\langle$x$\rangle\rangle$}}
% \end{display}
% Given normal assumptions about function application the result would
% be
% \begin{display}
% \record{\tfield{c$_0$}{\record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v_1:$\textit{Ind} . dog($v_1$),
%           $\langle$x$\rangle\rangle$}}}} (incorrect!)
% \end{display}
% but this would be incorrect.  In fact it is not a well-formed record
% type since x is not a path in it.  Instead the result should be 
% \begin{display}
% \record{\tfield{c$_0$}{\record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v_1:$\textit{Ind} . dog($v_1$),
%           $\langle$c$_0$.x$\rangle\rangle$}}}}
% \end{display}
% where the path from the top of the record type is specified.  However,
% in the abbreviatory notation we write just `x' when the label is used
% as an argument and interpret this as the path from the top of the
% record type to the field labelled `x' in the local record type.  Thus
% we will write
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{dog(x)}}
% \end{display}
% (where the `x' in `dog(x)' signifies the path consisting of just the
% single label `x') and
% \begin{display}
% \record{\tfield{c$_0$}{\record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{dog(x)}}}}
% \end{display}
% (where the `x' in `dog(x)' signifies the path from the top of the
% record type down to `x' in the local
% record type, that is, `c$_0$.x').\footnote{This convention of
%   representing the path from the top of the record type to the
%   ``local'' field by the final label on the path is new since \cite{Cooper2012}.}

% Note
% that this adjustment of paths is only required when a record type is being
% substituted into a position that lies on a path within a resulting
% record type.  It will not, for example, apply in a case where a record
% type is to be substituted for an argument to a predicate such as when
% applying the function
% \begin{display}
% $\lambda v_0:$\textit{RecType} . \smallrecord{\tfield{c$_0$}{appear($v_0$)}}
% \end{display}
% to
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v:$\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$} \\
%         \tfield{c$_2$}{$\langle\lambda v:$\textit{Ind} . approach($v$),
%           $\langle$x$\rangle\rangle$}}
% \end{display}
% where the position of $v_0$ is in an ``intensional context'', that is,
% as the argument to a predicate and there is no path to this position
% in the record type resulting from applying the function.  Here the
% result of the application is
% \begin{display}
% \record{\tfield{c$_0$}{appear(
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v:$\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$} \\
%         \tfield{c$_2$}{$\langle\lambda v:$\textit{Ind} . approach($v$),
%           $\langle$x$\rangle\rangle$}}
% )}}
% \end{display}
% with no adjustment necessary to the paths representing the
% dependencies.\footnote{This record corresponds to the interpretation
%   of \textit{it appears that a dog is approaching}.}  (Note that `c$_0$.x' is not a path in this record
% type.) 

% Suppose that we wish to represent a type which requires that there is
% some dog such that it appears to be approaching (that is a \textit{de
%   re} reading).  In the abbreviatory notation we might be tempted to
% write
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{dog(x)} \\
%         \tfield{c$_0$}{appear(\record{\tfield{c$_2$}{approach(x)}})}}
%       (incorrect!)
% \end{display}
% corresponding to
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v$:\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$} \\
%         \tfield{c$_0$}{appear(\record{\tfield{c$_2$}{$\langle\lambda
%               v$:\textit{Ind} . approach($v$),
%               $\langle$x$\rangle\rangle$}})}} (incorrect!)
% \end{display}
% This is, however, incorrect since it refers to a path `x' in the type
% which is the argument to `appear' which does not exist.  Instead we
% need to refer to the path `x' in the record type containing the field
% labelled `c$_0$':
% \begin{display}
%  \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{$\langle\lambda v$:\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$} \\
%         \tfield{c$_0$}{$\langle\lambda v$:\textit{Ind} . appear(\record{\tfield{c$_2$}{approach($v$)}}),
%               $\langle$x$\rangle\rangle$}}
% \end{display}
% In the abbreviatory notation we will use `$\Uparrow$' to indicate that
% the path referred to is in the ``next higher'' record
% type\footnote{This notation is new since \cite{Cooper2012}.}:
% \begin{display}
% \record{\tfield{x}{\textit{Ind}} \\
%         \tfield{c$_1$}{dog(x)} \\
%         \tfield{c$_0$}{appear(\record{\tfield{c$_2$}{approach($\Uparrow$x)}})}}
% \end{display}

% These matters arise as a result of our choice of using paths to
% represent dependencies in record types (rather than, for example,
% introducing additional unique identifiers to keep track of the
% positions within a record type as has been suggested by Thierry Coquand).  It seems like a matter of implementation rather than a matter
% of substance and it is straightforward to define a path-aware notion
% of substitution which can be used in the definition of what it means
% to apply a TTR function to an argument.  If $f$ is a function
% represented by $\lambda v:T\ .\ \varphi$ and $\alpha$ is the representation
% of an object of type $T$, then the result of applying $f$ to $\alpha$,
% $f(\alpha)$, is represented by Subst($\alpha$,$v$,$\varphi$,$\emptyset$),
% that is, the result of substituting $\alpha$ for $v$ in $\varphi$ with
% respect to the empty path where for arbitrary
% $\alpha,v,\varphi,\pi$,
% Subst($\alpha$,$v$,$\varphi$,$\pi$) is defined as 
% \begin{enumerate} 
 
% \item extend-paths($\alpha$,$\pi$), if $\varphi$ is $v$ 
 
% \item $\varphi$, if $\varphi$ is of the form $\lambda v:T\ .\ \zeta$, for some
%   $T$ and $\zeta$ (i.e. don't do any substitution if $v$ is bound
%   within $\varphi$)

% \item $\lambda u:T$ . Subst($\alpha$,$v$,$\zeta$,$\pi$), if $\varphi$ is
%   of the form $\lambda u:T . \zeta$ and $u$ is not $v$.

% \item
%   \record{\tfield{$\ell_1$}{Subst($\alpha$,$v$,$T_1$,$\pi.\ell_1$)} \\
%           \ldots \\
%           \tfield{$\ell_n$}{Subst($\alpha$,$v$,$T_n$,$\pi.\ell_n$)}},
%         if $\varphi$ is \record{\tfield{$\ell_1$}{$T_1$} \\
%                              \ldots \\ 
%                              \tfield{$\ell_n$}{$T_n$}}

% \item $P$(Subst($\alpha$,$v$,$\beta_1$,$\pi$),\ldots,Subst($\alpha$,$v$,$\beta_n$,$\pi$)),
%   if $\alpha$ is $P(\beta_1,\ldots,\beta_n)$ for some predicate $P$

% % \item $O$(Subst($\alpha$,$v$,$\beta_1$,$\pi$),\ldots,Subst($\alpha$,$v$,$\beta_n$,$\pi$)),
% %   if $\alpha$ is $O(\beta_1,\ldots,\beta_n)$ for some operator symbol $O$

% \item $\varphi$ otherwise
 
% \end{enumerate} 
 
% extend-paths($\alpha$,$\pi$) is
% \begin{enumerate} 
 
% \item $\langle f, \langle \pi.\pi_1,\ldots,\pi.\pi_n\rangle\rangle$,
%   if $\alpha$ is $\langle f, \langle \pi_1,\ldots,\pi_n\rangle\rangle$ 
 
% \item \record{\tfield{$\ell_1$}{extend-paths($T_1,\pi$)} \\
%               \ldots \\
%               \tfield{$\ell_n$}{extend-paths($T_n,\pi$)}} if $\alpha$
%             is \record{\tfield{$\ell_1$}{$T_1$} \\
%                        \ldots \\
%                        \tfield{$\ell_n$}{$T_n$}}

% \item
%   $P$(extend-paths($\beta_1,\pi$),\ldots,extend-paths($\beta_n,\pi$)),
%   if $\alpha$ is $P(\beta_1,\ldots,\beta_n)$ for some predicate $P$

% % \item $O$(extend-paths($\beta_1,\pi$),\ldots,extend-paths($\beta_n,\pi$)),
% %   if $\alpha$ is $O(\beta_1,\ldots,\beta_n)$ for some operator symbol $O$

% \item $\alpha$, otherwise
 
% \end{enumerate} 



\subsection{Merges of record types}
\label{app:merge}


This definition of the merge operation on types is first introduced
and discussed in Chapter~\ref{ch:infex}, p.~\pageref{pg:merge}.
We define a function $\mu$ which maps meets of record types to an
equivalent record type, record types to equivalent types where meets
in their values have been simplified by $\mu$ and any other types to
themselves.  $\mu$ is also defined on labelled sets which are not
types in order to account for merging inside a record type of
structures which depend on fields in the type outside the structure:
\begin{enumerate}
  \item if for some $T_1,T_2$, $T=(T_1\wedge T_2)$ and $T_1\sqsubseteq T_2$
  then $\mu(T)=T_1$ 
 
\item if for some $T_1,T_2$, $T=(T_1\wedge T_2)$ and $T_2\sqsubseteq T_1$
  then $\mu(T)=T_2$
  
\item otherwise:
\begin{enumerate} 
 
\item if for some labelled sets $T_1$, $T_2$, $T=(T_1\wedge T_2)$ then
  $\mu(T)=\mu'(\mu(T_1)\wedge\mu(T_2))$. 
 
\item if $T$ is a labelled set then $\mu(T)$ is $T'$ such that for any
  $\ell$,$v$, $\langle\ell,\mu(v)\rangle\in T'$ iff
  $\langle\ell,v\rangle\in T$.

\item otherwise $\mu(T)=T$.
 
\end{enumerate}
\end{enumerate}

$\mu'(T_1\wedge T_2)$ is defined by:
\begin{enumerate} 
 
\item if $T_1$ and $T_2$ are labelled sets, then $\mu'(T_1\wedge
  T_2)=T_3$ such that
\begin{enumerate} 
 
\item for any $\ell,v_1,v_2$, if $\langle\ell,v_1\rangle\in T_1$ and
  $\langle\ell,v_2\rangle\in T_2$, then 

\begin{enumerate} 
 
\item if $v_1$ and $v_2$ are
\begin{quote}
  $\langle\lambda u_1\!\!:\!\!T'_1\ldots\lambda
  u_i\!\!:\!\!T'_i\ .\ \phi,\langle\pi_1\ldots\pi_i\rangle\rangle$
  \end{quote}
  and
  \begin{quote}
    $\langle\lambda u'_1\!\!:\!\!T''_1\ldots\lambda
  u'_k\!\!:\!\!T''_k\ .\ \psi,\langle\pi'_1\ldots\pi'_k\rangle\rangle$
\end{quote}
respectively, then
\begin{quote}
$\langle\lambda u_1\!\!:\!\!T'_1\ldots\lambda
  u_i\!\!:\!\!T'_i,\lambda u'_1\!\!:\!\!T''_1\ldots\lambda
  u'_k\!\!:\!\!T''_k\ .\ \mu(\phi\wedge\psi), \langle\pi_1\ldots\pi_i,\pi'_1\ldots\pi'_k\rangle\rangle\in T_3$
\end{quote}

\item if $v_1$ is
  \begin{quote}
$\langle\lambda u_1\!\!:\!\!T'_1\ldots\lambda
u_i\!\!:\!\!T'_i\ .\ \phi,\langle\pi_1\ldots\pi_i\rangle\rangle$
\end{quote}
and $v_2$ is a
  type (i.e. not of the form $\langle f,\Pi\rangle$ for some function
  $f$ and sequence of paths $\Pi$), then
  \begin{quote}
    $\langle\lambda u_1\!\!:\!\!T'_1\ldots\lambda
  u_i\!\!:\!\!T'_i\ .\ \mu(\phi\wedge
  v_2),\langle\pi_1\ldots\pi_i\rangle\rangle\in T_3$
\end{quote}

\item if $v_2$ is
  \begin{quote}
    $\langle\lambda u'_1\!\!:\!\!T''_1\ldots\lambda
  u'_k\!\!:\!\!T''_k\ .\
  \psi),\langle\pi'_1\ldots\pi'_k\rangle\rangle$
\end{quote}
and $v_1$
is a type, then
\begin{quote}
  $\langle\lambda u'_1\!\!:\!\!T''_1\ldots\lambda
  u'_k\!\!:\!\!T''_k\ .\ \mu(v_1\wedge\psi)),\langle\pi'_1\ldots\pi'_k\rangle\rangle\in
  T_3$
  \end{quote}

\item otherwise $\langle\ell,\mu(v_1\wedge
  v_2)\rangle\in T_3$ 
 
\end{enumerate} 
  


 
\item for any $\ell,v_1$, if $\langle\ell,v_1\rangle\in T_1$ and there
  is no $v_2$ such that $\langle\ell,v_2\rangle\in T_2$, then
  $\langle\ell,v_1\rangle\in T_3$

\item for any $\ell,v_2$, if $\langle\ell,v_2\rangle\in T_2$ and there
  is no $v_1$ such that $\langle\ell,v_1\rangle\in T_1$, then
  $\langle\ell,v_2\rangle\in T_3$
 
\end{enumerate} 

% \item if $T_1$ and $T_2$ are record types and $T_2\sqsubseteq T_1$, then
%   $\mu'(T_1\wedge T_2)=T_2$

% \item if $T_1$ and $T_2$ are record types and $T_1\sqsubseteq T_2$, then
%   $\mu'(T_1\wedge T_2)=T_1$

\item if $T_1$ is $\mathrm{list}(T_1')$ ($\mathrm{set}(T_1')$, $\mathrm{plurality}(T_1')$) and
  $T_2$ is $\mathrm{list}(T_2')$ ($\mathrm{set}(T_2')$, $\mathrm{plurality}( T_2')$), then
  $\mu'(T_1\wedge T_2)=\mathrm{list}(\mu(T_1'\wedge T_2'))$ ($\mathrm{set}(\mu(T_1'\wedge
  T_2'))$, $\mathrm{plurality}(\mu(T_1'\wedge T_2'))$)
   
 
\item \label{item:mergeotherwise} otherwise $\mu'(T_1\wedge T_2)=T_1\wedge T_2$ 
 
\end{enumerate} 

$(T_1$ \d{$\wedge$} $T_2)$ is used to represent $\mu(T_1\wedge T_2)$.
We call  $(T_1$ \d{$\wedge$} $T_2)$ the \textit{merge} of $T_1$ and $T_2$.   

% The following two clauses could be added at
% the beginning of the definition of $\mu$ (after providing a
% characterization of the subtype relation, $\sqsubseteq$).
% \begin{enumerate} 
 
 
 
% \end{enumerate} 

% The current first clause would then hold in case neither of the
% conditions of these two clauses are met.  The definition without these
% additional clauses only accounts for simplification of meets which
% have to do with merges of record types whereas the definition with the
% additional clauses would in addition have the effect, for example, that
% $\mu(T\wedge T_a)=T_a$ and $\mu(T_1\wedge(T_1\vee T_2))= T_1$
% (provided that we have an appropriate definition of $\sqsubseteq$)
% whereas the current definition without the additional clauses means
% that $\mu$ 
% leaves these types unchanged.

We define also a notion of \textit{asymmetric merge}
(Chapter~\ref{ch:infex}, p.~\pageref{pg:asymmerge}) of $T_1$ and
$T_2$ which is defined by a function, $\mu_{\mathrm{asym}}$, exactly
like $\mu$ except that the first two clauses of the definition of
$\mu$ are missing and $\mu'$ is replaced by another function
$\mu_{\mathrm{asym}}'$.  Thus the definition of $\mu_{\mathrm{asym}}$
is:
\begin{enumerate} 
 
\item if for some $T_1$, $T_2$, $T=(T_1\wedge T_2)$ then
  $\mu_{\mathrm{asym}}(T)=\mu_{\mathrm{asym}}'(\mu_{\mathrm{asym}}(T_1)\wedge\mu_{\mathrm{asym}}(T_2))$. 
 
\item if $T$ is a record type then $\mu_{\mathrm{asym}}(T)$ is $T'$ such that for any
  $\ell$,$v$, $\langle\ell,\mu_{\mathrm{asym}}(v)\rangle\in T'$ iff
  $\langle\ell,v\rangle\in T$.

\item otherwise $\mu_{\mathrm{asym}}(T)=T$.
 
\end{enumerate}

The definition of $\mu_{\mathrm{asym}}'$ is exactly like $\mu'$,
replacing $\mu$ and $\mu'$ with $\mu_{\mathrm{asym}}$ and $\mu_{\mathrm{asym}}'$ respectively, except that
the
clause~\ref{item:mergeotherwise} of the definition of $\mu'$ is replaced by 
\begin{enumerate} 
 
\item[\ref{item:mergeotherwise}$'$.] otherwise $\mu_{\mathrm{asym}}'(T_1\wedge T_2)=T_2$ 
 
\end{enumerate} 
  
We use $T_1$ \fbox{\d{$\wedge$}} $T_2$  to represent the asymmetric
merge of $T_1$ and $T_2$.  

Asymmetric merge may result in an ill-formed record type if we take
the asymmetric merge of a record type, $T_1$, and a non-record type,
$T_2$, since $T_1$ may be embedded in a larger type with fields
dependent on paths into $T_1$ which will not be present in the result
where $T_2$ has been substituted for $T_1$ thus removing the relevant
paths.  % These definitions do not in general avoid
% the formation of ill-formed record types since they allow record types
% to be replaced with non-record types within a record type thus
% potentially removing paths that might be included in dependent type
% fields elsewhere in the resulting type.  However, if merging is
% restricted to either two record types or two non-record types this
% problem should not occur since all paths from both types will be
% preserved.  In the case of asymmetric merges we can allow the
% replacement of non-record types by record types without risk.  Note
% that our definition of dependent record types in \ref{app:rectypes}
% allows for dependencies to fields that have conflicting types.  Such
% record types will be well-formed though will not have any witnesses.

\paragraph{Merging functions which return types}

$\lambda r\!:\!T_1\ .\ T_2\dep{r}$ \d{\d{$\wedge$}} $\lambda r\!:\!T_3\ .\ T_4\dep{r}$
denotes the function $\lambda r\!:\!T_1$\d{$\wedge$}$T_3\ .\
T_2\dep{r}$\d{$\wedge$}$T_4\dep{r}$.

\subsection{Constructing fixed point types for functions which return
  record types} (Chapter~\ref{ch:commonnouns}, p.~\pageref{pg:fixedpointtype-discussion}ff.)
\label{pg:fixedpointtype}

% If, for
% some type $T_1$, $f:(T_1\rightarrow\textit{Type})$ then $\mathcal{F}(f)$ is a \textit{fixed
% point type} for $f$, that is $a:\mathcal{F}(f)$ implies $a:f(a)$.
% $\mathcal{F}$ is defined by
% \begin{quote}
% $\mathcal{F}(\lambda r\!:\!T_1\ .\ T_2(r)) = T_1$\d{$\wedge$}$T'$

% where $T'$ is like $T_2(r)$ except that any path $r.\pi$ is
% replaced by $\pi$.
% \end{quote}

If $T$ is a
  record type and $r$ is a record of any type, we will use
  $T_{r.\pi\leadsto\pi}$ to designate the type like $T$ except that
  for any $\pi\in\mathrm{paths}(T)$ any occurrence of $r.\pi$ is
  replaced by $\pi$.

A dependent type, $\mathcal{T}$, is \textit{path-dependent on $r$},
$\mathcal{T}\dep{r}_{\text{path}}$, just in case $\mathcal{T}$ depends
on paths in $r$ but not on the whole object $r$. 

  If $\mathcal{T}$ is a dependent record type of the form $\lambda
r\!:\!T_1\ .\ T_2\dep{r}_{\text{path}}$ where $T_1$ is a record type and for any
$r$,
$\mathrm{paths}(T_1)\cap\mathrm{paths}(\mathcal{T}(r))=\emptyset$,
then
\begin{quote}
  $\mathcal{F}(\mathcal{T})$ is that type $T$ such that for any
  $r^*:T_1$, $\lambda r\!:\!T_1\ .\
  (T_1\text{\d{$\wedge$}}T_2)_{r.\pi\leadsto\pi}(r^*)=T$
\end{quote}

If $\mathcal{T}$ is a dependent record type of the form $\lambda
r\!:\!T_1\ .\ T_2\dep{r}$ where $T_1$ is a record type,
then
\begin{quote}
  $\mathcal{F}_{\text{quasi}}(\mathcal{T})$ is that type $T$ such that for any
  $r^*:T_1$, $\lambda r\!:\!T_1\ .\
  (\text{\smallrecord{\smalltfield{$\mathfrak{c}^*$}{$T_1$}}\d{$\wedge$}\smallrecord{
      \smalltfield{$\mathfrak{r}^*$}{$T_2$}}})_{r.\pi\leadsto\mathfrak{c}^*.\pi}(r^*)=T$
\end{quote}

% If $\mathcal{T}$ is a dependent record type of the form $\lambda
% r\!:\!T_1\ .\ T_2\dep{r}$ where $T_1$ is a record type,
% then
% \begin{quote}
%   $\mathcal{F}_{\text{quasi}}(\mathcal{T})$ is that type $T$ such that for any
%   $r^*:T_1$, $\lambda r\!:\!T_1\ .\
%   (\text{\smallrecord{\smalltfield{$\mathfrak{c}^*$}{$T_1$}}\d{$\wedge$}}T_2)_{r.\pi\leadsto\mathfrak{c}^*.\pi}(r^*)=T$
% \end{quote}

If $\mathcal{T}$ is a dependent record type of the form $\lambda
r\!:\!T_1\ .\ T_2\dep{r}$ where $T_1$ is a record type and for any $r$
in its domain $\mathcal{T}(r)$ is a record type, then
\begin{quote}
  $\mathcal{F}_{\text{quasi}^*}(\mathcal{T}) =
  \mathcal{F}_{\text{quasi}}(\mathcal(T))$
\end{quote}
else if $\mathcal{T}$ is a dependent record type of the form $\lambda
r\!:\!T_1\ .\ \mathcal{T}'\dep{r}$  where  $T_1$ is a record type and
for any $r$ in its domain $\mathcal{T}(r)$ is a dependent record type,
then
\begin{quote}
  $\mathcal{F}_{\text{quasi}^*}(\mathcal{T})$ is that type $T$ such
  that for any $r^*:T_1$, $T = \lambda r\!:\!T_1\ .\
  (\text{\smallrecord{
      \smalltfield{$\mathfrak{c}^*$}{$T_1$}}\d{$\wedge$}\smallrecord{
      \smalltfield{$\mathfrak{r}^*$}{$\mathcal{F}_{\text{quasi}^*}(\mathcal{T}')$}}})_{r.\pi\leadsto\mathfrak{c}^*.\pi}$
\end{quote}
% Strictly speaking this definition is not quite correct since $T'$ may
% not be a type because there may be a path occurring as an argument to
% a predicate which is not introduced in $T'$.  A more correct, though
% less perspicuous, definition would be
% \begin{quote}
% $\mathcal{F}(\lambda r\!:\!T_1\ .\ T_2(r)) =
% [(\lambda r\!:\!T_1\ .\ T_1$\d{$\wedge$}$T_2(r))(r^*)]^{-r^*}$

% where $r^*$ is a record of type $T_1$ such that there is no path occurring as an
% argument to a predicate in $T_1$ or $T_2(r)$ of the form $r^*.\pi$ for
% any $\pi$ and $[T]^{-r}$ is the result of replacing any path of the
% form $r.\pi$, for any $\pi$, occurring as an argument to a predicate
% in $T$, with $\pi$.
% \end{quote}

% This definition, however, fails to capture that $\mathcal{F}$ must be
% defined as a partial function which is undefined on functions meeting
% a certain condition.  This is taken account of in the following final
% definition:
% \begin{quote}
% $\mathcal{F}$ is a partial function on functions such that if, for
% some type $T_1$, $f:(T_1\rightarrow \textit{Type})$, $f=\lambda
% r\!:\!T_1\ .\ T_2(r)$, $g$ is the function
% \begin{quote}
% $\lambda r\!:\!T_1\ .\ T_1$\d{$\wedge$}$T_2(r)$
% \end{quote}
% and for any $r_1,r_2:T_1$
% \begin{quote}
% $[g(r_1)]^{-r_1} = [g(r_2)]^{-r_2}$
% \end{quote}
% then if $r^*:T_1$,
% \begin{quote}
% $\mathcal{F}(f) = [g(r*)]^{-r^*}$
% \end{quote}

% For any function $f$ not covered by the above, $\mathcal{F}(f)$ is undefined.
% \end{quote}
% Let us take some concrete examples based on the discussion in
% Chapter~\ref{ch:commonnouns}, Section~\ref{sec:dgqs}.  Suppose that
% $f$ is the function
% \begin{quote}
% $\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
%   . \record{\tfield{e}{dog($r$.x)}}
% \end{quote}
% Then $g$ will be
% \begin{quote}
% $\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
%   . \smallrecord{\smalltfield{x}{\textit{Ind}}} \d{$\wedge$} \smallrecord{\smalltfield{e}{dog($r$.x)}}
% \end{quote}
% That is,
% \begin{quote}
% $\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}}
% . \record{\tfield{x}{\textit{Ind}}\\
%           \tfield{e}{dog($r$.x)}}
% \end{quote}
% If we now compute $[g(r^*)]^{-r^*}$ for some
% $r^*$:\smallrecord{\smalltfield{x}{\textit{Ind}}}, that is we apply
% $g$ to $r^*$ and then remove $r^*$ from all path-names that begin with
% it we will obtain
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}\\
%           \tfield{e}{dog(x)}}
% \end{quote}
% We would have obtained the same result no matter which record we chose
% to be $r^*$, since $r$ only occurs in $g$ at the head of path names.
% Now consider $f$ to be a variant of what we propose to be the content
% of \textit{temperature} in Chapter~\ref{ch:commonnouns} (in fact,
% similar to a
% variant that we have proposed in previous work):
% \begin{quote}
% $\lambda r$:\textit{Rec} . \record{\tfield{e}{temperature($r$)}}
% \end{quote}
% Now $g$ will be
% \begin{quote}
% $\lambda r$:\textit{Rec} . \textit{Rec} \d{$\wedge$} \smallrecord{\smalltfield{e}{temperature($r$)}}
% \end{quote}
% That is,
% \begin{quote}
% $\lambda r$:\textit{Rec} . \record{\tfield{e}{temperature($r$)}}
% \end{quote}
% which happens to be identical with $f$.  If we apply this to a record
% $r^*$ we will obtain
% \begin{quote}
% \record{\tfield{e}{temperature($r^*$)}}
% \end{quote}
% The result of removing all occurrences of $r^*$ at the head of a path
% will be identical since $r^*$ occurs here not as the head of a path
% but as an argument to a predicate. Consequently if we choose a
% different record for $r^*$ the result will be a different type.  Thus
% $\mathcal{F}$ is not defined on this function.  This is intuitively
% correct since defining fixed points for this function would involve a
% kind of non-well foundedness which we have not allowed in TTR.

% The moral of this tale is that if you wish to define a dependent type
% (that is, a function returning a type), $\lambda r\!:\!T_1\ .\ T_2(r)$,
% for which you will be able to compute a fixed point type, make sure
% that $T_2$ only depends on $r$ in that $r$ may be the head of path
% names in $T_2(r)$.  Normally, you will also want to ensure that $T_1$
% and $T_2$ do not share any labels in order to avoid unwanted clashes
% when $T_1$ and $T_2$ are merged.
 
% \paragraph{Constructing backgrounding types corresponding to functions which return
%   types}
% \label{pg:backgroundingtype}
% We introduced backgrounding types for dependent types (functions which
% return types).  These are like the fixed point types generated by
% $\mathcal{F}$ except that an additional label `bg' (``background'') is
% placed before the domain type of the function in the resulting type.
% If $f$ is a function returning a type (a dependent type) then we will
% represent the corresponding backgrounding type as $\mathcal{B}(f)$.
% Here is an example:
% \begin{quote}
% $\mathcal{B}$($\lambda r$:\smallrecord{\smalltfield{x}{\textit{Ind}}\\
%                                        \smalltfield{e}{female(x)}} . 
% \smallrecord{\smalltfield{e}{leave($r$.x)}}) = 
% \record{\tfield{bg}{\record{\tfield{x}{\textit{Ind}}\\
%                             \tfield{e}{female(x)}}}\\
%         \tfield{e}{leave(bg.x)}}
% \end{quote}

% More generally, if $f:(T_1\rightarrow\textit{Type})$ then $\mathcal{B}(f)$ is the
% \textit{backgrounding type} for $f$.
% $\mathcal{B}$ is defined by
% \begin{quote}
% $\mathcal{B}(\lambda r\!:\!T_1\ .\ T_2(r))$ = \smallrecord{\smalltfield{bg}{$T_1$}}\d{$\wedge$}$T'$

% where $T'$ is like $T_2(r)$ except that any path $r.\pi$ is
% replaced by bg.$\pi$.
% \end{quote}

% In an exactly parallel way to the definition of the function
% $\mathcal{F}$ which creates fixed point types, this definition is strictly speaking not quite correct since $T'$ may
% not be a type because there may be a path occurring as an argument to
% a predicate which is not introduced in $T'$.  A more correct, though
% less perspicuous, definition parallel to that for $\mathcal{F}$, would be
% \begin{quote}
% $\mathcal{B}(\lambda r\!:\!T_1\ .\ T_2(r))$ =
% [($\lambda r$:$T_1$ . \smallrecord{\smalltfield{bg}{$T_1$}}\d{$\wedge$}$T_2(r)$)($r^*$)]$^{r^*/\mathrm{bg}}$

% where $r^*$ is a record of type \smallrecord{\smalltfield{bg}{$T_1$}} such that there is no path occurring as an
% argument to a predicate in $T_1$ or $T_2(r)$ of the form $r^*.\pi$ for
% any $\pi$ and $[T]^{r^*/\mathrm{bg}}$ is the result of replacing any path of the
% form $r^*.\pi$, for any $\pi$, occurring as an argument to a predicate
% in $T$, with bg.$\pi$.
% \end{quote}

% \section{Relabelling of record types}
% \label{app:relabelling-rectypes}

% \subsection{Some considerations}
% \label{app:relabelling-rectypes-considerations}

% We extend the notion relabelling of records
% discussed in Appendix~\ref{app:rectypes} to record types.\footnote{This was
% not made explicit in \cite{Cooper2012}.}  For non-dependent record
% types both flattening and relabelling can be regarded as exactly parallel to that of
% records since non-dependent record types are sets of ordered pairs of
% labels and types.  They are just like records except that the second
% members of the pairs are types.  However, in the case of dependent
% record types, flattening and relabelling introduces some complications
% which need to be taken account of.  We shall start with an informal
% discussion of the complications.  

% \paragraph{Labels in dependent fields} First of all we need to
% note that labels not only occur as the first members of the ordered
% pairs that constitute the record type but also in the paths which
% occur in dependent fields.  This introduces complications if we
% attempt to define an operation of flattening for record types.
% Also in relabelling we need to make sure that the relabelling applies
% to the paths in the dependent fields as well as the labels of the
% record type.  

% Consider the record type which in abbreviatory notation
% we write as:
% \begin{quote}
% \record{\tfield{x}{\record{\tfield{x}{\textit{Ind}}\\
%                            \tfield{e}{dog(x)}}}}
% \end{quote}
% It would be incorrect to represent the flattening of this type as:
% \begin{quote}
% \record{\tfield{x.x}{\textit{Ind}}\\
%         \tfield{x.e}{dog(x)}}
% \end{quote}
% The `x' in `dog(x)' does not represent a path in the flattened record
% type. Rather the flattened type should be, in abbreviatory notation:
% \begin{quote}
% \record{\tfield{x.x}{\textit{Ind}}\\
%         \tfield{x.e}{dog(x.x)}}
% \end{quote}
% This is a notational complication.  Recall that 'dog(x)' in the first
% type uses 'x' to represent the path 'x.x', that is, the path to the
% 'x' in the immediate record containing 'dog(x)'.

% Let us consider how this would work in the official notation with full
% paths represented in dependent fields.  In order to define flattening
% and unflattening we would need to convert:
% % We need also to guarantee that the unflattening of this type returns
% % the original unflattened type.  We will, of course, work to achieve
% % this, not with the abbreviatory notation but with the official
% % notation, or rather with the set theoretic objects which the official
% % notation represents.  That is, we need to convert: 
% \begin{quote}
% \record{\tfield{x}{\record{\tfield{x}{\textit{Ind}}\\
%                            \tfield{e}{$\langle\lambda v$:\textit{Ind}
%                              .  dog($v$), $\langle$x.x$\rangle\rangle$}}}}
% \end{quote}
% to:
% \begin{quote}
% \record{\tfield{x.x}{\textit{Ind}}\\
%         \tfield{x.e}{$\langle\lambda v$:\textit{Ind}
%                              .  dog($v$), $\langle$x.x$\rangle\rangle$}}
% \end{quote}
% and back again.

% % But now consider a slightly different (equivalent) type:
% % \begin{quote}
% % \record{\tfield{x}{$\langle\lambda v$:\textit{Ind}
% %     . \record{\tfield{x}{\textit{Ind}}\\
% %               \tfield{e}{dog($v$)}}, $\langle$x.x$\rangle\rangle$}}
% % \end{quote}
% % [No!  This is not a type according to the definition since x.x is not
% % a path in the type before you add the dependent field!]


% % or, in abbreviatory notation:
% % \begin{quote}
% % \record{\tfield{x.x}{\textit{Ind}}\\
% %         \tfield{x.e}{dog(x.x)}}
% % \end{quote}
% \paragraph{Relabelling can require adjustment of dependent fields}
% A relabelling such as:
% \begin{quote}
% x.x $\leadsto$ y
% \end{quote}
% applied to the flattened type leads to a different problem involved in
% expansion.  
% The relabelled flattened record would be:
% \begin{quote}
% \record{\tfield{y}{\textit{Ind}}\\
%         \tfield{x.e}{$\langle\lambda v$:\textit{Ind}
%                              .  dog($v$), $\langle$y$\rangle\rangle$}}
% \end{quote}
% % or, in abbreviatory notation:
% % \begin{quote}
% % \record{\tfield{y}{\textit{Ind}}\\
% %         \tfield{x.e}{dog(y)}}
% % \end{quote}
% Expanding the relabelled flattened type in the way we did for records will result in:
% \begin{quote}
% \record{\tfield{y}{\textit{Ind}}\\
%         \tfield{x}{\record{\tfield{e}{$\langle\lambda v$:\textit{Ind}
%                              .  dog($v$), $\langle$y$\rangle\rangle$}}}}
% \end{quote}
% This is incorrect because the label `y' is not present in 
% \begin{quote}
% \record{\tfield{e}{$\langle\lambda v$:\textit{Ind}
%                              .  dog($v$), $\langle$y$\rangle\rangle$}}
% \end{quote}
% and this is not a type as require in Clause~\ref{cl:ndrectype-emb} of
% the definition of non-dependent record types on
% p.~\pageref{cl:ndrectype-emb}.  Rather the correct result should be:
% \begin{quote}
% \record{\tfield{y}{\textit{Ind}}\\
%         \tfield{x}{$\langle\lambda v$:\textit{Ind}
%                              . \record{\tfield{e}{dog($v$)}},
%                              $\langle$y$\rangle\rangle$}}
% \end{quote}
% In abbreviatory notation this is:
% \begin{quote}
% \record{\tfield{y}{\textit{Ind}}\\
%         \tfield{x}{\record{\tfield{e}{dog($\Uparrow$y)}}}}
% \end{quote}

% This, then, is a problem for defining relabelling of record types in
% terms of a notion of flattening and unflattening as we did for
% records.  This problem is not insurmountable given the techniques that
% we will develop below.  However, there is another problem which seems
% to strongly suggest that we should not use flattening in the same way
% that we did for records.


% % This is well-formed when we consider that the `y' in the dependent
% % field is a total path beginning at the top of the record.  [Is this
% % true?  What happens with ``appears to be approaching''?  Should we
% % push the label inside the function?]

% \paragraph{Dependencies involving paths which are not total}  
% In the examples above the dependencies involve objects at the end of
% paths.  It is also possible to have dependencies on records
% corresponding to the value of a partial path.  Consider the following
% example:
% \begin{quote}
% \record{\tfield{s}{\record{\tfield{x}{\textit{Ind}}\\
%                            \tfield{c}{dog(x)}\\
%                            \tfield{e}{run(x)}}}\\
%         \tfield{e}{see(sam,s)}}
% \end{quote}
% which might be a way of representing the type which is the content of
% \textit{Sam saw a dog run}.  The official notation for this type (with
% unabbreviated paths) is:
% \begin{quote}
% \record{\tfield{s}{\record{\tfield{x}{\textit{Ind}}\\
%                            \tfield{c}{$\langle\lambda v$:\textit{Ind}
%                              . dog($v$), $\langle$s.x$\rangle\rangle$}\\
%                            \tfield{e}{$\langle\lambda v$:\textit{Ind}
%                              . run($v$),
%                              $\langle$s.x$\rangle\rangle$}}}\\
%         \tfield{e}{$\langle\lambda v$:\textit{Rec} . see(sam,$v$), $\langle$s$\rangle\rangle$}}
% \end{quote}
% \label{pg:sam-saw-a-dog-run}
% We might think that the flattening of this type is:
% \begin{quote}
% \record{\tfield{s.x}{\textit{Ind}}\\
%         \tfield{s.c}{$\langle\lambda v$:\textit{Ind}
%                              . dog($v$), $\langle$s.x$\rangle\rangle$}\\
%         \tfield{s.e}{$\langle\lambda v$:\textit{Ind}
%                              . run($v$),
%                              $\langle$s.x$\rangle\rangle$}\\
%         \tfield{e}{$\langle\lambda v$:\textit{Rec} . see(sam,$v$), $\langle$s$\rangle\rangle$}}
% \end{quote} 
% But this is, of course, not correct since the path `s' in the
% `e'-field is not a path in the flattened type.  
% % This shows that we
% % cannot naively adapt the technique for flattening we used with records
% % to dependent record types.  Instead we will make
% % the flattened type depend on a record of the type required for the
% % argument to `see' in the original unflattened type (and also on any
% % objects on which that type depends):
% % \begin{quote}
% % $\lambda r$:\smallrecord{\smalltfield{s}{\smallrecord{\smalltfield{x}{\textit{Ind}}\\
% %                          \smalltfield{c}{dog(x)}\\
% %                          \smalltfield{e}{run(x)}}}} . 
% % \record{\tfield{e}{see(sam, $r$.s)}}
% % \end{quote}
% % Call this $\mathcal{T}$.  This is, of course, not a type to which the 
% % flattening of a record
% % belonging to the unflattened type can belong. 
% Our strategy will be not
% to define relabelling in terms of flattening as we did for records,
% but to define relabelling of types in terms of direct replacement of
% paths in unflattened types.  In order to do this we will, however,
% find it convenient to use a ``flattened'' representation of the
% unflattened type which explicitly lists its paths. 
% Instead we say if $r$
% is of the non-flattened type, then there is some $r'$ such that
% $\varphi(r):\mathcal{T}(r')$ and there is some flattening, $T_{\varphi}$, of the
% domain type of $\mathcal{T}$ such that $\varphi(r):T_{\varphi}$.
% We are now free to apply flattening or relabelling to the domain or
% range of this function without creating the problem that the second
% argument of `see' will not be defined.  Note that there may be several
% dependencies in the flattened type depending on how many partial paths
% occur in the dependent fields of the unflattened type and what the
% dependencies of the types pointed at by those partial paths are.  Thus the
% dependent type which is the flattening may take several arguments.

% \subsection{Basic definitions of flattening and
%   relabelling of record types}
% \label{app:flattening-def}

% We start with a definition of what it means for a relabelling to be
% limited to a type.  This is given in terms of the notion of a
% relabelling being limited to a record (p.~\pageref{pg:limited}).
% \begin{quote}
% A relabelling, $\eta$, is \textit{limited to} a record type, $T$, just
% in case for any record, $r$, $r:T$ implies $\eta$ is limited to
% $\varphi(r)$.
% \end{quote}
% We can then define the notion of relabelling of record types as
% follows:
% \begin{quote}
% If $T_1$ and $T_2$ are record types and $\eta$ is a relabelling
% limited to $T_1$, then $T_2$ \textit{is an $\eta$-relabelling of}
% $T_1$ just in case for any record, $r$, such that $\eta$ is a proper
% relabelling (see p.~\pageref{pg:proper-relabelling}) of $r$, $r:T_1$
% implies $[r]_\eta:T_2$.
% \end{quote}
% Note that this definition does not require a definition of the
% flattening of types but relies of the notion of flattening of records
% which is necessary to define relabelling of records.  Thus if all we
% are interested in is the relabelling of types as in the notions of
% matching discussed in Chapter~\ref{ch:intensional}, then we do not
% have to address the problem of dependence involving partial paths
% discussed in Appendix~\ref{app:flattening-considerations}.

% However, for the sake of completeness we give definitions of
% flattening and unflattening of record types.  There are two cases to
% consider: that where the flattening is a record type and that where
% the flattening is a dependent type which returns a record type when
% applied to an appropriate argument.  We first give the definitions for
% the case where the flattening is a record type.
% \begin{quote}
% If $T_1$ and $T_2$ are record types, 

% $T_2$ \textit{is a flattening of}
% $T_1$ just in case for any record, $r$, $r:T_1$ implies
% $\varphi(r):T_2$

% $T_2$ \textit{is an unflattening of} $T_1$ just in case for any
% record, $r$, $r:T_1$ implies $\varphi^-(r):T_2$.

% \end{quote}
% For the cases where the flattening is a dependent type we have the
% following definitions:
% \begin{quote}
% If $T_1$, $T_2$ and ${T_2}_\varphi$ are record types such that ${T_2}_\varphi$ is a
% flattening of $T_2$ and
% $\mathcal{T}:(T_2\rightarrow\textit{RecType})$, 

% $\mathcal{T}$
% \textit{is a flattening of} $T_1$ just in case for any record, $r$,
% $r:T_1$ implies that for some record, $r'$, such that  $r':T_2$,
% $\varphi(r):(\mathcal{T}(r')\wedge {T_2}_\varphi)$

% $T_1$ \textit{is an unflattening of} $\mathcal{T}$ just in case for
% any record, $r$, $r:({T_2}_\varphi\wedge\mathcal{T}(\varphi^-(r))$
% implies $\varphi^-(r):T_1$
% \end{quote}

% Note that if $T_1$ ($\mathcal{T}$) is a flattening of $T_2$ if and
% only if $T_2$ is an unflattening of $T_1$ ($\mathcal{T}$).



% \subsection{Relabellings of record types}

% % The definitions in Section~\ref{app:flattening-def} enable us to tell
% % whether one type is a flattening or relabelling of another but they do
% % not give us an algorithm for constructing a flattening or relabelling
% % of a particular type.
% Here we will consider how, for a given record
% type, $T$, an $\eta$-relabelling of $T$, $[T]_\eta$ can be defined.

% We start by defining the notion of paths for record types.  This can
% be defined in terms of the paths which are common to all witnesses for
% the types.  If $T$ is a record type, then the \textit{set of paths of}
% $T$, $\mathrm{paths}(T)$, is
% \begin{quote}
% $\mathrm{cpaths}(\down{T})$
% \end{quote}
% where $\mathrm{cpaths}$ is as defined on p.~\pageref{pg:cpaths} and the
% \textit{set of total paths of} $T$, $\mathrm{tpaths}(T)$, is
% \begin{quote}
% $\mathrm{ctpaths}(\down{T})$
% \end{quote}
% where $\mathrm{ctpaths}$ is as defined on p.~\pageref{pg:ctpaths}.

% It may look from these definitions as if you have to compute all the
% witnesses for a record type before you can compute its paths, but in
% fact this is not true.  For any type, we can compute what paths are
% witness of that type must have. For example, any witness of the type
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}\\
%         \tfield{c}{$\langle\lambda v$:\textit{Ind}
%           . \smallrecord{\smalltfield{e}{dog($v$)}},
%           $\langle$x$\rangle\rangle$}}
% \end{quote}
% must be a record of the form
% \begin{quote}
% \record{\field{x}{$a$}\\
%         \field{c}{\record{\field{e}{$s$}\\
%                           \ldots}}\\
%         \ldots}

% where:

% $a$ : \textit{Ind}\\
% $s$ : dog($a$)
% \end{quote}
% Hence, any record of this type must have `x' and `c.e' among its total
% paths and these will be the only total paths that are common to all
% witnesses for the type.  

% In a similar way, we can say that tree relations holding in all
% witnesses of a type hold for the types (see
% p.~\pageref{pg:imm-dom}). Thus, for example, we can say that `c'
% immediately dominates `e' in the type in virtue of the fact that the
% relation holds in all witnesses of the type, despite the fact the `e'
% is embedded in a function below `c' in the type.

% It will be convenient to define the computation of 
% relabellings of types in terms of a notation which gives unique
% identifiers to the occurrences of labels and which eshews representing
% the functions in dependent fields explicitly, rather representing the
% dependencies by using the unique identifiers.  To increase
% readability, we will only represent the unique identifiers on those
% labels which are referenced in some dependent field.  As an example,
% consider the following types, presented in official notation.
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}\\
%         \tfield{c}{$\langle\lambda v$:\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$}\\
%         \tfield{e}{$\langle\lambda v$:\textit{Ind} . 
%                              appear(\smallrecord{\smalltfield{e}{approach($v$)}}),
%                              $\langle$x$\rangle\rangle$}}

% \bigskip

% \record{\tfield{x}{\textit{Ind}}\\
%         \tfield{c}{$\langle\lambda v$:\textit{Ind}
%           . \smallrecord{\smalltfield{e}{dog($v$)}},
%           $\langle$x$\rangle\rangle$}}
% \end{quote}
% In the unique identfier notation these will be:
% \begin{quote}
% \record{\tfield{x\{0\}}{\textit{Ind}}\\
%         \tfield{c}{dog(\{0\}:\textit{Ind})}\\
%         \tfield{e}{appear(\smallrecord{\smalltfield{e}{approach(\{0\}:\textit{Ind})}})}}

% \bigskip

% \record{\tfield{x\{0\}}{\textit{Ind}}\\
%         \tfield{c}{\smallrecord{\smalltfield{e}{dog(\{0\}:\textit{Ind})}}}}

% \end{quote}
% The unique identifier notation can be obtained from the official
% notation by 
% \begin{enumerate} 
 
% \item adding a unique identifier $\{i\}$ (where $i$ is a natural
%   number) to each occurrence of a label in the type, other than in the paths
%   following a function in dependent fields.  In practice we only add
%   identifiers to those labels which are addressed in some dependent
%   field. 

% \item replacing any path in a dependent field with the unique identifier
%   associated with the final label occurrence on the path which it references.
 
% \item replacing any pair in a dependent field of the form 
% \begin{quote}
% $\langle\lambda v_1:T_1\ldots\lambda v_n:T_n\
% .\ \varphi[v_1,\ldots,v_n], \langle \{i_1\},...,\{i_n\}\rangle\rangle$
% \end{quote}
% with
% \begin{quote}
% $\varphi[\{i_1\}:T_1,\ldots,\{i_n\}:T_n]$
% \end{quote}
 
% \end{enumerate} 
% The final step involves a variant of $\beta$-conversion.  It is
% important to represent the type restriction associated with the unique
% identifier by the domain type of the function since the domain type of
% the function may be distinct from the type associated with the
% identifier in the field labelled by the identifier.

% It is important to note that we are manipulating the representations
% of types here, not the types themselves.  The unique identifier
% notation does not introduce additional types.

% We also need to show how to convert back from unique identifier
% notation for a type, $T^*$, to official notation.   We can do this by
% carrying out the following in order:
% \begin{enumerate} 
 
% \item  replace all the dependencies on unique identifiers with
% appropriate pairs of functions and sequences of paths
 
% \item  remove the unique identifiers
 
% \end{enumerate} 
  
% We replace all the dependencies on
% unique identifiers by carrying out the
% following for each occurrence of a label, $\ell$, in $T^*$ associated with
% an identifier, $\{i\}$, which is referenced elsewhere in $T^*$:
% \begin{enumerate} 
 
% \item for each sister, $\ell'$, of $\ell\{i\}$, if $\ell'$ immediately
%   dominates
%   a subtree, $\tau$, containing $\{i\}\!:\!T$ for some type, $T$, then:
% \begin{quote}
% if $\tau$ is not an ordered pair consisting of a function and a
% sequence of paths:
% \begin{quote}
% replace $\tau$ with $\langle\lambda v_i\!:\!T\ .\ \tau[\{i\}\!:\!T\leadsto v_i],\langle\ell\rangle\rangle$
% \end{quote}
% otherwise, if $\tau$ is $\langle f, \langle\pi_1,\ldots,\pi_n\rangle\rangle$:
% \begin{quote}
% replace $\tau$ with $\lambda v_i\!:\!T\ . \ f[\{i\}\!:\!T\leadsto v_i],
% \langle\ell,\pi_1,\ldots,\pi_n\rangle\rangle$
% \end{quote}
% \end{quote}
 
% \item Let $\ell_0.\ldots.\ell_n.\ell\{i\}$ be the path ending in
%   $\ell\{i\}$ in $T^*$.  For each $\ell_k$ in order in
%   $\langle\ell_n,\ldots,\ell_0\rangle$, where $\pi^*$ is the path starting
%   with $\ell_k$ and ending with $\ell\{i\}$, and for each sister,
%   $\ell'$, of $\ell_k$, if $\ell'$ immediately dominates a subtree,
%   $\tau$, containing $\{i\}\!:\!T$ for some type, $T$, then:
%  \begin{quote}
% if $\tau$ is not an ordered pair consisting of a function and a
% sequence of paths:
% \begin{quote}
% replace $\tau$ with $\langle\lambda v_i\!:\!T\ .\ \tau[\{i\}\!:\!T\leadsto v_i],\langle\pi^*\rangle\rangle$
% \end{quote}
% otherwise, if $\tau$ is $\langle f, \langle\pi_1,\ldots,\pi_n\rangle\rangle$:
% \begin{quote}
% replace $\tau$ with $\langle\lambda v_i\!:\!T\ . \ f[\{i\}\!:\!T\leadsto v_i],
% \langle\pi^*,\pi_1,\ldots,\pi_n\rangle\rangle$
% \end{quote}
% \end{quote}
 
% \end{enumerate} 
   
% Consider as an example the type which in abbreviatory notation is
% written (with abbreviatory representation of the path `id$_0$.x' in
% the `id$_0$.e'-field) as:
% \begin{quote}

% \record{\tfield{id$_0$}{\record{\tfield{x}{\textit{Ind}}\\
%                                 \tfield{e}{dog(x)}}}\\
%         \tfield{id$_1$}{\record{\tfield{e}{run($\Uparrow$id$_0$.x)}}}}

% \end{quote}
% This is a type which relates to our discussion of long term memory in
% Chapters~\ref{ch:propnames}--\ref{ch:intensional}.  In official
% notation this type is represented as:
% \begin{quote}

% \record{\tfield{id$_0$}{\record{\tfield{x}{\textit{Ind}}\\
%                                 \tfield{e}{$\langle\lambda
%                                   v$:\textit{Ind} . dog($v$),
%                                   $\langle$x$\rangle\rangle$}}}\\
%         \tfield{id$_1$}{$\langle\lambda v$:\textit{Ind}
%           . \record{\tfield{e}{run($v$)}},
%           $\langle$id$_0$.x$\rangle\rangle$}}

% \end{quote}
% In the unique identifier notation this would be
% \begin{quote}

% \record{\tfield{id$_0$}{\record{\tfield{x\{0\}}{\textit{Ind}}\\
%                                 \tfield{e}{dog(\{0\}:\textit{Ind})}}}\\
%         \tfield{id$_1$}{\record{\tfield{e}{run(\{0\}:\textit{Ind})}}}}

% \end{quote}
% This in turn can be represented in tree-notation to make the
% sisterhood relations clear.
% \begin{quote}

% \Tree [ [.id$_0$
%           [.x\{0\} \textit{Ind} ]
%           [.e dog(\{0\}:\textit{Ind}) ] ]
%         [.id$_1$
%           [.e run(\{0\}:\textit{Ind}) ] ] ]

% \end{quote}
% To convert this back to official notation, we first look at the sister
% of `x\{0\}', that is, `e', and replace the subtree it immediately
% dominates with the corresponding dependent field.
% \begin{quote}

% \Tree [ [.id$_0$
%           [.x\{0\} \textit{Ind} ]
%           [.e {$\langle\lambda v_0$:\textit{Ind} . dog($v_0$), $\langle$x$\rangle\rangle$} ] ]
%         [.id$_1$
%           [.e run(\{0\}:\textit{Ind}) ] ] ]

% \end{quote} 
% Next we go up one node from `x\{0\}' to `id$_0$' and look at its
% sister, `id$_1$'.  We then form an appropriate dependent field from
% its immediate subtree.
% \begin{quote}

% \Tree [ [.id$_0$
%           [.x\{0\} \textit{Ind} ]
%           [.e {$\langle\lambda v_0$:\textit{Ind} . dog($v_0$), $\langle$x$\rangle\rangle$} ] ]
%         [.id$_1$
%           {$\langle\lambda v_0$:\textit{Ind} .  \smallrecord{\smalltfield{e}{run($v_0$)}},
%             $\langle$id$_0$.x$\rangle\rangle$} ] ]

% \end{quote}
% Finally, we remove the unique identifier `\{0\}'.
% \begin{quote}

% \Tree [ [.id$_0$
%           [.x \textit{Ind} ]
%           [.e {$\langle\lambda v_0$:\textit{Ind} . dog($v_0$), $\langle$x$\rangle\rangle$} ] ]
%         [.id$_1$
%           {$\langle\lambda v_0$:\textit{Ind} .  \smallrecord{\smalltfield{e}{run($v_0$)}},
%             $\langle$id$_0$.x$\rangle\rangle$} ] ]

% \end{quote}
% This is now the tree variant of the official notation for the type.

% The flattened variant of the unique identifier notation,
% \begin{quote}
% \record{\tfield{id$_0$}{\record{\tfield{x\{0\}}{\textit{Ind}}\\
%                                 \tfield{e}{dog(\{0\}:\textit{Ind})}}}\\
%         \tfield{id$_1$}{\record{\tfield{e}{run(\{0\}:\textit{Ind})}}}}
% \end{quote}
% is:
% \begin{quote}
% \record{\tfield{id$_0$.x\{0\}}{\textit{Ind}}\\
%         \tfield{id$_0$.e}{dog(\{0\}:\textit{Ind})}\\
%         \tfield{id$_1$.e}{run(\{0\}:\textit{Ind})}}
% \end{quote}
% where we have made the paths in the original type explicit.  Note,
% that this again is not introducing a new type.  It is merely a variant
% notation for the original unflattened type.  If we think of the
% notation itself as a record, that is, a set of ordered pairs, we can
% obtain the flattened representation of the type by applying the same
% procedure as we used for records.  Thus the unflattened representation
% corresponds to the set
% \begin{quote}
% \begin{tabbing}
% \{\=$\langle$id$_0$, \{\=$\langle$x\{0\}, \textit{Ind}$\rangle$,\\
% \>\>                    $\langle$e, dog(\{0\}:\textit{Ind})$\rangle$\}\\
% \>$\langle$id$_1$, \{$\langle$e, run(\{0\}:\textit{Ind})$\rangle$\}\}
% \end{tabbing}
% \end{quote}
% We can now apply the flattening algorithm defined on
% p.~\pageref{pg:flattening} to this set, yielding the set:
% \begin{quote}
% \begin{tabbing}
% \{\=$\langle$id$_0$.x\{0\}, \textit{Ind}$\rangle$\\
% \>  $\langle$id$_0$.e, dog(\{0\}:\textit{Ind})$\rangle$\\
% \>  $\langle$id$_1$.e, run(\{0\}:\textit{Ind})\}
% \end{tabbing}
% \end{quote}
% Thus we are not flattening the
% type, but we \emph{are} flattening the \emph{representation} of the type
% which can itself
% be conceived of as a record.

% Now consider the relabelling:
% \begin{quote}
% id$_0$.x$\leadsto$x\\
% id$_0$.e$\leadsto$e$_1$\\
% id$_1$.e$\leadsto$e$_2$
% \end{quote}
% This relabelling can be decorated with the unique identifiers
% corresponding to the flattened representation of the type.  On the
% left hand side of the relabelling we copy whatever unique identifiers
% occur associated with the label in the type.  We then place a copy of
% the unique identifier occurring on the left hand side also on the
% right hand side.  Thus the decorated version of this relabelling
% corresponding to this type will be:
% \begin{quote}
% id$_0$.x\{0\}$\leadsto$x\{0\}\\
% id$_0$.e$\leadsto$e$_1$\\
% id$_1$.e$\leadsto$e$_2$
% \end{quote}
% Now, again considering the flattened representation of the type as a
% record, we can apply the relabelling to the representation in the
% manner characterized on pp.~\pageref{pg:relabelling}ff.
% Thus for the above type
% this relabelling will yield:
% \begin{quote}
% \record{\tfield{x\{0\}}{\textit{Ind}}\\
%         \tfield{e$_1$}{dog(\{0\}:\textit{Ind})}\\
%         \tfield{e$_2$}{run(\{0\}:\textit{Ind})}}
% \end{quote}
% which in official notation is
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}\\
%         \tfield{e$_1$}{$\langle\lambda v$:\textit{Ind} . dog($v$),
%           $\langle$x$\rangle\rangle$}\\
%         \tfield{e$_2$}{$\langle\lambda v$:\textit{Ind} . run($v$),
%           $\langle$x$\rangle\rangle$}}
% \end{quote}
% In this example the unique identifier occurred at the end of a path,
% but this is not always the case.  Consider the example discussed on
% p.~\pageref{pg:sam-saw-a-dog-run}.  In unique identifier notation this
% is
% \begin{quote}
% \record{\tfield{s\{1\}}{\record{\tfield{x\{0\}}{\textit{Ind}}\\
%                                 \tfield{c}{dog(\{0\}:\textit{Ind})}\\
%                                 \tfield{e}{run(\{0\}:\textit{Ind})}}}\\
%         \tfield{e}{see(sam,\{1\}:\textit{Rec})}}

% \end{quote}
% The flattened variant of the unique identifier notation for this type
% is below, where the unique identifier `\{1\}' occurs on three copies
% of the label `s':
% \begin{quote}
% \record{\tfield{s\{1\}.x\{0\}}{\textit{Ind}}\\
%         \tfield{s\{1\}.c}{dog(\{0\}:\textit{Ind})}\\
%         \tfield{s\{1\}.e}{run(\{0\}:\textit{Ind})}\\
%         \tfield{e}{see(sam,\{1\}:\textit{Rec})}}
% \end{quote}
% We require that any relabelling for a type must preserve partial paths
% terminated with a label associated with a unique identifier in the sense that
% while the partial path itself may be changed, it must be changed to the same
% partial path in each path where the unique identifier occurs.  Thus the
% following would be an admissible relabelling for this type:
% \begin{quote}
% s.x $\leadsto$ id$_0$.id$_1$.x \\
% s.c $\leadsto$ id$_0$.id$_1$.e \\
% s.e $\leadsto$ id$_0$.e \\
% e $\leadsto$ id$_2$.e
% \end{quote}
% We can decorate this relabelling with unique identifiers corresponding
% to the type:
% \begin{quote}
% s\{1\}.x\{0\} $\leadsto$ id$_0$\{1\}.id$_1$.x\{0\} \\
% s\{1\}.c $\leadsto$ id$_0$\{1\}.id$_1$.e \\
% s\{1\}.e $\leadsto$ id$_0$\{1\}.e \\
% e $\leadsto$ id$_2$.e
% \end{quote}
% How do we know where to place the identifier `\{1\}' on the right-hand
% side of the annotated relabelling?  It goes after the longest partial
% path which the three paths corresponding to left-hand side paths
% containing \{1\} have in common.  So, for example, if the relabelling
% had been:
% \begin{quote}
% s.x $\leadsto$ id$_0$.id$_1$.x \\
% s.c $\leadsto$ id$_0$.id$_1$.e$_1$ \\
% s.e $\leadsto$ id$_0$.id$_1$.e$_2$ \\
% e $\leadsto$ id$_2$.e
% \end{quote}
% the decorated version would be:
% \begin{quote}
% s\{1\}.x\{0\} $\leadsto$ id$_0$.id$_1$\{1\}.x\{0\} \\
% s\{1\}.c $\leadsto$ id$_0$.id$_1$\{1\}.e$_1$ \\
% s\{1\}.e $\leadsto$ id$_0$.id$_1$\{1\}.e$_2$ \\
% e $\leadsto$ id$_2$.e
% \end{quote}

% According to the first relabelling the relabelled type would be:
% \begin{quote}
% \record{\tfield{id$_0$\{1\}.id$_1$.x\{0\}}{\textit{Ind}}\\
%         \tfield{id$_0$\{1\}.id$_1$.e}{dog(\{0\}:\textit{Ind})}\\
%         \tfield{id$_0$\{1\}.e}{run(\{0\}:\textit{Ind})}\\
%         \tfield{id$_2$.e}{see(sam,\{1\}:\textit{Rec})}}
% \end{quote}
% In standard notation with unabbreviated paths this type is represented
% as
% \begin{quote}
% \record{\tfield{id$_0$}{\record{\tfield{id$_1$}{\record{\tfield{x}{\textit{Ind}}\\
%                                                         \tfield{e}{$\langle\lambda
%                                                           v$:\textit{Ind}
%                                                           . dog($v$),
%                                                           $\langle$id$_0$.id$_1$.x$\rangle\rangle$}}}\\
%                                 \tfield{e}{$\langle\lambda
%                                   v$:\textit{Ind} . run($v$),
%                                   $\langle$id$_0$.id$_1$.x$\rangle\rangle$}}}\\
%         \tfield{id$_2$}{$\langle\lambda
%               v$:\textit{Rec} . \smallrecord{\smalltfield{e}{see(sam,$v$)}},
%               $\langle$id$_0\rangle\rangle$}}
% \end{quote}
% Using abbreviated paths, this is
% \begin{quote}
% \record{\tfield{id$_0$}{\record{\tfield{id$_1$}{\record{\tfield{x}{\textit{Ind}}\\
%                                                         \tfield{e}{$\langle\lambda
%                                                           v$:\textit{Ind}
%                                                           . dog($v$),
%                                                           $\langle$x$\rangle\rangle$}}}\\
%                                 \tfield{e}{$\langle\lambda
%                                   v$:\textit{Ind} . run($v$),
%                                   $\langle$id$_1$.x$\rangle\rangle$}}}\\
%         \tfield{id$_2$}{$\langle\lambda
%               v$:\textit{Rec} . \smallrecord{\smalltfield{e}{see(sam,$v$)}},
%               $\langle$id$_0\rangle\rangle$}}
% \end{quote}
% Suppose we had tried to use the following relabelling instead.
% \begin{quote}
% s.x $\leadsto$ id$_0$.id$_1$.x \\
% s.c $\leadsto$ id$_0$.id$_1$.e \\
% s.e $\leadsto$ id$_1$.e \\
% e $\leadsto$ id$_2$.e
% \end{quote}
% This relabelling cannot be decorated according to the unique identifiers
% of the type because the three occurrences of `s' do not have a
% corresponding partial path on the right-hand side.  This relabelling
% is thus inadmissible for this type.  We thus define admissibility of a
% relabelling for a type as follows:
% \begin{quote}
% A relabelling, $\eta$, is \textit{admissible} for a record type, $T$,
% just in case $\eta$ can be decorated according to the flattened unique
% identifier representation of $T$.

% \end{quote}

% We can now define the notion of relabelling for types using the
% notions of flattening and relabelling we used for records:
% \begin{quote}
% If $T$ is a record type with unique identifier representation, $r$, and $\eta$ is an admissible relabelling for $T$,
% then the \textit{result of relabelling $T$ with $\eta$}, $[T]_\eta$,
% is that $T'$ whose unique identifier representation is $[r]_\eta$.
% \end{quote}




% If $T$ is a type, then $\varphi(T)$, \textit{the flattening of} $T$ is
% \begin{enumerate} 
 
% \item $\displaystyle{\bigcup_{f\in T}}\mathrm{FlattenField}(f)$,  if $T$ is a proper record type (see p.~\pageref{pg:proprectype}) 
 
% \item $T$, otherwise 
 
% \end{enumerate} 
% where $\mathrm{FlattenField}$ is defined as follows:

% $\mathrm{FlattenField}(\langle\ell, T\rangle)$ is
% \begin{enumerate} 
 
% \item $\varphi(\left\{\begin{array}{l}\langle\ell.\ell_1, T_1\rangle,\\
%                                  \langle\ell.\ell_2, T_2\rangle,\\
%                                  \vdots \\
%                                  \langle\ell.\ell_n, T_n\rangle
%                  \end{array}\right\})$, if $T$ is $\left\{\begin{array}{l}\langle\ell_1, T_1\rangle,\\
%                                  \langle\ell_2, T_2\rangle,\\
%                                  \vdots \\
%                                  \langle\ell_n, T_n\rangle
%                  \end{array}\right\}$
 
% \item $\langle\ell, T\rangle$, otherwise 
 
% \end{enumerate} 
    
% Correspondingly, we can define a way of computing the inverse of
% flattening.  

% If $T$ is a type, $\varphi^-(T)$, \textit{the inverse flattening
%   (expansion) of} $T$ is
% \begin{enumerate} 
 
% \item $\left\{\begin{array}{l}\langle\ell_1,
%                                     \varphi^-(\left\{\begin{array}{l}\langle\pi_{1,1},T_{1,1}\rangle\\
%                                                                      \langle\pi_{1,2},T_{1,2}\rangle\\ 
%                                                                      \vdots\\
%                                                                      \langle\pi_{1,m_1},T_{1,m_1}\rangle
%                                                      \end{array}
%                                               \right\}\rangle,\\
%                                \langle\ell_2,
%                                     \varphi^-(\left\{\begin{array}{l}\langle\pi_{2,1},T_{2,1}\rangle\\
%                                                                      \langle\pi_{2,2},T_{2,2}\rangle\\ 
%                                                                      \vdots\\
%                                                                      \langle\pi_{2,m_2},T_{1,m_2}\rangle
%                                                      \end{array}
%                                               \right\}\rangle,\\
%                                \vdots\\
%                                \langle\ell_n,
%                                     \varphi^-(\left\{\begin{array}{l}\langle\pi_{n,1},T_{n,1}\rangle\\
%                                                                      \langle\pi_{n,2},T_{n,2}\rangle\\ 
%                                                                      \vdots\\
%                                                                      \langle\pi_{n,m_n},T_{n,m_n}\rangle
%                                                      \end{array}
%                                               \right\}\rangle\end{array}\right\}$,
%                                             if $T$ is 
% $\left\{\begin{array}{l}\langle\ell_1.\pi_{1,1},T_{1,1}\rangle\\
%                         \langle\ell_1.\pi_{1,2},T_{1,2}\rangle\\
%                         \vdots\\
%                         \langle\ell_1.\pi_{1,m_1},T_{1,m_1}\rangle\\
%                         \langle\ell_2.\pi_{2,1},T_{2,1}\rangle\\
%                         \langle\ell_2.\pi_{2,2},T_{2,2}\rangle\\
%                         \vdots\\
%                         \langle\ell_2.\pi_{2,m_2},T_{2,m_2}\rangle\\
%                         \vdots\\
%                         \langle\ell_n.\pi_{n,1},T_{n,1}\rangle\\
%                         \langle\ell_n.\pi_{n,2},T_{n,2}\rangle\\
%                         \vdots\\
%                         \langle\ell_n.\pi_{n,m_n},T_{1,m_n}\rangle\\
%          \end{array}\right\}$
  
% \item $T$, otherwise 
 
% \end{enumerate}

% The set of \textit{complex labels} (or \textit{paths}), $L_\pi$,  \textit{based
%   on a set of labels}, $L$, is a set such that
% \begin{enumerate} 
 
% \item if $\ell\in L$, then $\ell\in L_\pi$ 
 
% \item if $\pi\in L_\pi$ and $\ell\in L$, then $\pi.\ell\in L_\pi$

% \item nothing else is a member of $L_\pi$
 
% \end{enumerate} 
   


% If $T$ is a type in a system of types based on labels $L$, then a
% \textit{relabelling} for $T$ is a one-one function,
% $\eta$, whose domain is the set of labels of the flattened type
% $\varphi(T)$ and whose range is included in $L_\pi$ and such that for
% no $\pi_1$, $\pi_2$ and $\pi$, $\eta(\pi_2)=\eta(\pi_1).\pi$, that is,
% no new complex label can be assigned by the relabelling which is a
% proper initial part of another complex label assigned by the relabelling.  The result of
% \textit{relabelling} $T$ with $\eta$, a relabelling for $T$, is $\varphi^-([\varphi(T)]_\eta)$
% where for any flattened type $T$, $[T]_\eta$ is the result of replacing every
% occurrence of all the labels $\ell$ in $T$ (including those that occur as arguments to predicates,
% i.e. in dependent fields) with $\eta(\ell)$.

% \textbf{Alternative definition which should be used throughout [????]:}  The result of
% \textit{relabelling} $T$ with $\eta$, a relabelling for $T$, is
% denoted by  $[T]_\eta$ and is defined by $\varphi^-(\{\varphi(T)\}_\eta)$
% where for any flattened type $T$, $\{T\}_\eta$ is the result of replacing every
% occurrence of all the labels $\ell$ in $T$ (including those that occur as arguments to predicates,
% i.e. in dependent fields) with $\eta(\ell)$.

% The fact that a relabelling $\eta$ is one-one means that the inverse
% of $\eta$, $\eta^-$, is also a function which we can use to recover
% the original labelling.  This gives us the opportunity to relabel,
% carry out some operation on the relabelled type and then restore the
% original labelling.  This is, for example, exploited in the discussion
% of accommodation in Chapter~\ref{ch:propnames} on p.~\pageref{pg:inverserelabelling}.

% If fields $f_1$ and $f_2$ have the same label, that is
% $f_1=\langle\ell, T_1\rangle$ and $f_2=\langle\ell, T_2\rangle$ for
% some $\ell$, $T_1$ and $T_2$, then the result of \textit{merging} the two
% \textit{fields} is $\langle\ell,T_1$\d{$\wedge$}$T_2\rangle$.


\subsection{Unique identifier notation for record types}
\label{app:unique-id}

The unique identifier notation for a type, $T$, can be obtained from the official
notation for $T$ by carrying out in order the following manipulations
(Chapter~\ref{ch:infex}, p.~\pageref{ex:official-to-unique-id}):
\begin{enumerate} 
 
\item Add a unique identifier \fbox{$i$} (where $i$ is a natural
  number) to the last label occurrence in any path, $\pi$, which is referenced
  in a dependent field, $\langle f,\langle\ldots,\pi,\ldots\rangle\rangle$, somewhere in $T$. 

\item Replace $\pi$ in any dependent field, $\langle f,\langle\ldots,\pi,\ldots\rangle\rangle$, with the unique identifier
  associated with the final label occurrence in $\pi$.
 
\item Replace any pair in a dependent field of the form 
\begin{quote}
$\langle\lambda v_1:T_1\ldots\lambda v_n:T_n\
.\ \varphi\dep{v_1,\ldots,v_n}, \langle \text{\fbox{$i_1$}},\ldots,\text{\fbox{$i_n$}}\rangle\rangle$
\end{quote}
with
\begin{quote}
$\varphi\dep{\text{\fbox{$i_1$}}:T_1,\ldots,\text{\fbox{$i_n$}}:T_n}$
\end{quote}
 
\end{enumerate}

We also show how to convert back from unique identifier
notation for a type, $T$, to official notation.   We can do this by
carrying out the following manipulations (Chapter~\ref{ch:infex},
p.~\pageref{ex:unique-id-to-official}):
\begin{enumerate} 
 
\item For each occurrence of \fbox{$i$} in a dependent field labelled
  $\ell_d$ (the label for the dependent field) for some
  natural number, $i$, locate the smallest record structure, $\Delta$, in $T$
  which contains a path, $\pi_d$, to $\ell_d$ and a path $\pi_a$ to a
  label $\ell_{\text{\fbox{i}}}$ (the label for the addressed field)
 
\item Let $\ell$ be the first label on $\pi_d$. If $\Delta.\ell$ is an
  ordered pair $\langle \lambda v_j\!:\!T_j\ .\ \varphi\dep{\text{\fbox{$i$}}\!:\!T_i},
  \langle\pi_1,\ldots,\pi_n\rangle\rangle$, then replace $\Delta.\ell$
  with $\langle \lambda v_i\!:\!T_i\ .\ \lambda v_j\!:\!T_j\ .\
  \varphi[\text{\fbox{$i$}}\!:\!T_i\leadsto v_i],
  \langle\pi_1,\ldots,\pi_n,\pi_a\rangle\rangle$.  Otherwise, if
  $\Delta.\ell$ is $\varphi\dep{\text{\fbox{$i$}}\!:\!T_i}$, replace
  $\Delta.\ell$ with $\langle \lambda v_i\!:\!T_i\ .\
  \varphi[\text{\fbox{$i$}}\!:\!T_i\leadsto v_i],
  \langle\pi_a\rangle\rangle$

\item For any number $i$, remove the subscript \fbox{$i$} on any label
  on which it occurs.
 
\end{enumerate}

This notational conversion can be characterized also in terms of
labelled sets:

If $T$ is a dependent record type then a unique identifier correlate
for $T$ is obtained by the following operations applied to $T$ in
order.
\begin{enumerate} 
 
\item For each $\pi$ and $\ell$ occurring in a dependent value,
  $v=\langle f,\langle\ldots,\pi.\ell,\ldots\rangle\rangle$ such that
  for som $\pi'$ and $\ell'$, $T.\pi'.\ell'=v$ and
  $T.\pi'.\pi.\ell=v'$, change the field $\langle\ell,v'\rangle$ to
  $\langle\ell,v',\text{\fbox{$i$}}\rangle$, where \fbox{$i$} is a
  fresh identifier, and replace $\pi.\ell$ in $v$ with \fbox{$i$}.  
 
\item Replace any pair in a dependent field of the form
  \begin{quote}
    $\langle\lambda v_1\!:\!T_1\ .\ \ldots\ .\ \lambda v_n\!:\!T_n\ .\
    \varphi\dep{v_1,\ldots,v_n},
    \langle\text{\fbox{$i_1$}},\ldots,\text{\fbox{$i_n$}}\rangle\rangle$
  \end{quote}
  with
  \begin{quote}
    $\varphi\dep{\langle\text{\fbox{$i_1$}},T_1\rangle,\ldots,\langle\text{\fbox{$i_n$}},T_n\rangle}$
  \end{quote}
  
 
\end{enumerate}

The following procedure can be used for finding a dependent record
type for a unique identifier correlate.
\begin{enumerate} 
 
\item If $X$ is a labelled set, then for each occurrence, $\xi$ of
  $\langle\text{\fbox{$i$}},T\rangle$, for some $i$ and $T$, in $X$,
  find the smallest labelled set, $\Delta$, such that
  $\Delta\underline{\varepsilon}X$ and contains $\xi$ and
  $\langle\ell,v,\text{\fbox{$i$}}\rangle$ for some $\ell$ and $v$.

  Let $\pi_a$ be the path in $\Delta$ such that
  $\Delta.\pi_a=\langle\ell,v,\text{\fbox{$i$}}\rangle$.

  Let $\ell_d.\pi_d$ be the longest path in $\Delta$ (not containing a
  reserved label) such that $\xi$ occurs in $\Delta.\ell_d.\pi_d$.

  If $\Delta.\ell_d$ is an ordered pair
  \begin{quote}
    $\langle\lambda v_j\!:\!T_j\ .\
    \varphi\dep{\langle\boxed{i},T\rangle},\langle\pi_1,\ldots,\pi_n\rangle\rangle$
  \end{quote}
  then replace $\Delta.\ell_d$ with
  \begin{quote}
    $\langle\lambda v_i\!:\!T\ .\ \lambda v_j\!:\!T_j\ .\
    \varphi\dep{v_i},\langle\pi_1,\ldots,\pi_n,\pi_a\rangle\rangle$
  \end{quote}
  Otherwise if $\Delta.\ell_d$ is
  $\varphi\dep{\langle\boxed{i},T\rangle}$, replace it with
  \begin{quote}
    $\langle\lambda v_i\!:\!T\ .\
    \varphi\dep{v_i},\langle\pi_a\rangle\rangle$
  \end{quote}
  
  
 
\item  For any $\ell$, $v$ and $\boxed{i}$, replace any occurrence of
  $\langle\ell,v,\boxed{i}\rangle$ in $X$ with $\langle\ell,v\rangle$.
 
\end{enumerate}   

\subsection{Dependency in record types and record type generalization}
\label{app:dep-rectype}
\label{app:gen-rectypes}

If $T$ : \textit{RecType}, $\ell\in\text{labels}(T)$ and
$\langle\ell,T'\rangle\in T$ where $T'$: \textit{Type} (that is,
$[\ell,T']$ is a non-dependent field in $T$), then \textit{the
  generalization of $T$ to its $\ell$-field} (Chapter~\ref{ch:quant}, p.~\pageref{ex:gen-to-ell}, $T^\ell$, is
\begin{quote}
\record{\tfield{$\ell$}{$T'$}}
\end{quote}
(This simple definition is made more general in the definition of
generalization to a path given below.)

If $T$ is a record type, $\pi_1\in\mathrm{paths}(T)$ and
$\pi_2\in\mathrm{tpaths}(T)$, then $\pi_2$ \textit{depends on} $\pi_1$
(Chapter~\ref{ch:quant}, p.~\pageref{ex:path-dep})
iff, in unique identifier notation, $\pi_1$ is indexed with \fbox{$i$}
and the representation of $T.\pi_2$ contains \fbox{$i$}, for some
natural number $i$.

If $T$ is a record type and $\pi\in\mathrm{paths}(T)$ then \textit{the
  dependency family of $\pi$ in $T$} (Chapter~\ref{ch:quant}, p.~\pageref{ex:path-dep-fam}),
$\mathrm{paths}_\pi(T)$, is that subset, $\Pi$, of $\mathrm{paths}(T)$
such that
\begin{enumerate} 
 
\item $\pi\in\Pi$ 
 
\item for any $\pi'\in\Pi$ and $\pi''\in\mathrm{tpaths}(T)$, if
  $\pi''$ depends on $\pi'$, then $\pi''\in\Pi$

\item for and $\pi'\in\Pi$ and $\pi''\in\mathrm{paths}(T)$, if $\pi'$
  depends on $\pi''$, then $\pi''\in\Pi$
 
\end{enumerate}

If $T$ is a record type and $\pi\in\mathrm{paths}(T)$, then $T$
\textit{generalized to} $\pi$ (Chapter~\ref{ch:quant}, p.~\pageref{ex:rectype-gen}), $T^\pi$, is the smallest labelled set $T'$ such
that $\mathrm{paths}_\pi(T)\subseteq\mathrm{paths}(T')$ and for all
$\pi'\in\mathrm{tpaths}(T')$, $T'.\pi=T.\pi$.

If $T$ is a record type and $\{\pi_1,\ldots,\pi_n\}\subset\mathrm{paths}(T)$, then $T$
\textit{generalized to} $\pi_1,\ldots,\pi_n$, $T^{\pi_1,\ldots,\pi_n}$
(Chapter~\ref{ch:quant}, p.~\pageref{ex:rectype-gen-gen}), is the smallest labelled set $T'$ such
that for all $\pi_i\in\{\pi_1,\ldots,\pi_n\}$, $\mathrm{paths}_{\pi_i}(T)\subseteq\mathrm{paths}(T')$ and for all
$\pi'\in\mathrm{tpaths}(T')$, $T'.\pi=T.\pi$.



\subsection{Using records to restrict % and specify
  record types}
\label{app:specrec}

(These definitions were not included in \citealp{Cooper2012}.)

% If $T$ is a type and $r$ is a record, then the \textit{restriction of
%   $T$ by $r$} (Chapter~\ref{ch:gram}, p.~\pageref{pg:typerestriction}),
% $T\!\restriction\!r$, is a
% type. $a:T\!\restriction\!r$ iff $a\underline{\varepsilon} r$ (see
% Appendix~\ref{app:rectypes}) and $a:T$.

 %  A type system $\mathbb{T}$ \textit{has restricted types according to a
%   set of labels} $\mathcal{L}$ (Chapter~\ref{ch:gram},
% p.~\pageref{pg:typerestriction}) if it is the case that
% \begin{enumerate} 
 
% \item   if  $T$ is a type according to $\mathbb{T}$ and
%   $r$ is a record according to $\mathcal{L}$ and $\mathbb{T}$, then the
%   restriction of $T$ by $r$, $T\!\restriction\!r$, is a
% type according to $\mathbb{T}$.
 
% \item $a:_{\mathbb{T}}T\!\restriction\!r$ iff $a\underline{\varepsilon} r$  and $a:_{\mathbb{T}}T$. 
 
% \end{enumerate}

A type system $\mathbb{T}$ \textit{has restricted types according to a
  set of labels} $\mathcal{L}$ (Chapter~\ref{ch:gram},
p.~\pageref{pg:typerestriction}) if it is the case that
\begin{enumerate} 
 
\item   if  $T$ is a type, but not a record type, according to $\mathbb{T}$ and
  $r$ is a record according to $\mathcal{L}$ and $\mathbb{T}$, then the
  restriction of $T$ by $r$, $\rho(T, r)$, is a
  type according to $\mathbb{T}$.
  
 
\item $a:_{\mathbb{T}}\rho(T,r)$ iff $a\underline{\varepsilon} r$  and
  $a:_{\mathbb{T}}T$.

\end{enumerate}


% If $T$ is a record type other than \textit{Rec} and \textit{ERec} then
% \textit{the recursive restriction of $T$ by $r$},
% $T\!\restriction\restriction\!r$, is the result of replacing each
% field in $T$ of the form $[\ell:T']$, where $T'$ is a type, with the
% field $[\ell:T'\!\restriction\restriction\!r]$ and each field of the
% form $\langle\ell,\langle f,\Pi\rangle\rangle$ (where $f$ is a
% function and $\Pi$ a sequence of paths) with $\langle\ell,\langle
% f',\Pi\rangle\rangle$ where $f'$ is like $f$ except that for any
% arguments $a_1,\ldots,a_n$ appropriate to $f$,
% $f'(a_1)\ldots(a_n)=f(a_1)\ldots(a_n)\!\restriction\restriction r$.

% Otherwise if $T$ is a type, then
% $T\!\restriction\restriction\!r=T\!\restriction\!r$.

% If $\mathcal{T}$ is a dependent type (for example, a property)
% $\lambda r_1\!:\!T_1\ldots\lambda r_n\!:\!T_n\ .\
% T\dep{r_1,\ldots,r_n}$, then $\mathcal{T}\!\restriction\!s$ is $\lambda r_1\!:\!T_1\ldots\lambda r_n\!:\!T_n\ .\
% T\dep{r_1,\ldots,r_n}\!\restriction\restriction\!s$.

We then generalize restriction to record types and other objects using
$o\!\restriction\!r$ to represent the object $o$ restricted to $r$.


\begin{enumerate} 
 
\item If $T$ is a type but not a record type then
  \begin{quote}
    $T\!\restriction\!r=\rho(T,r)$
  \end{quote}
  
 
\item If $X$ is a labelled set whose labels are not distinguished (as
  for example in ptypes, that is $\mathrm{labels}(X)$ is a set of
  labels which can be used in record types)
  \begin{quote}
    $\{\langle\ell_1,o_1\rangle,\ldots,\langle\ell_n,o_n\rangle\}$
  \end{quote}
  then
  \begin{quote}
    $X\!\restriction\!r=\{\langle\ell_1,o_1\!\restriction\!r\rangle,\ldots,\langle\ell_n,o_n\!\restriction\!r\rangle\}$
  \end{quote}

  
\item if $o$ is
  \begin{quote}
    $\langle\mathcal{T},\Pi\rangle$
  \end{quote}
  where $\mathcal{T}$ is
  a dependent type and $\Pi$ is a sequence of paths, then
  \begin{quote}
    $o\!\restriction\!r=\langle\mathcal{T}\!\restriction\!r,\Pi\rangle$
  \end{quote}
  
\item if $\mathcal{T}$ is a dependent type
  \begin{quote}
    $\lambda v_1\!:\!T_1\ .\ \ldots\ .\ \lambda v_n\!:\!T_n\ .\
    T\dep{v_1,\ldots,v_n}$
  \end{quote}
  then
  \begin{quote}
    $\mathcal{T}\!\restriction\!r=\lambda v_1\!:\!T_1\ .\ \ldots\ .\
    \lambda v_n\ .\ T\dep{v_1,\ldots,v_n}\!\restriction\!r$
  \end{quote}
  
\item otherwise $o\!\restriction\!r=o$
 
\end{enumerate} 

  
  
We use a similar notation for restricted fields in record types as we
do for manifest fields.  That is, we represent
\begin{quote}
  \record{\tfield{$\ell$}{$T\!\restriction\!r$}}
\end{quote}
as
\begin{quote}
  \record{\rfield{$\ell$}{$r$}{$T$}}
\end{quote}
in the case where $T$ is not a record type or a pair of a
dependent type and a sequence of paths.



% \todo{The remaining versions of restriction are perhaps not necessary}If $T$ is a record type and $r$ is a record, then $T\!\mid\!\restriction\! r$, the
% \textit{restriction} of $T$ by
% $r$ is the result
% of replacing each field, $\langle \ell, T'\rangle$, in $T$ such that
% $\ell$ is a label in $r$, with 
% \begin{enumerate}
% \item  $\langle\ell,T'\!\restriction\!r.\ell\rangle$\footnote{That is,
%     in an adaptation of our
% graphical notation for manifest fields, \smallrecord{\smalltfield{$\ell$}{$T'$}} is
% replaced by \smallrecord{\smallrfield{$\ell$}{$r.\ell$}{$T'$}}}, if
% $T'$ is a type
% \item $\langle\ell,\langle f',\Pi\rangle\rangle$, if $T'=\langle
%   f,\Pi\rangle$ where $f$ is a function and $\Pi$ is a sequence of
%   paths of length $n$ and for any
%   $a_1,\ldots,a_n$, $f'(a_1)\ldots(a_n)$ is defined iff
%   $f(a_1)\ldots(a_n)$ is defined and $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)\!\restriction\!r.\ell$
% \end{enumerate}

% A variant of this notion of restriction is default restriction
% which will only require restriction of fields which are not already
% restricted. If $T$ is a record type and $r$ is a record, then
% $T\drestr r$, the
% \textit{default restriction} of $T$ by
% $r$ is the result
% of replacing each field, $\langle \ell, T'\rangle$, in $T$ such that
% $\ell$ is a label in $r$, with 
% \begin{enumerate}
% \item  $\langle\ell,T'\!\restriction\!r.\ell\rangle$, if
% $T'$ is a type but not a restricted type. If $T'$ is a
% singleton type then $\langle \ell, T'\rangle$ is replaced by itself.
% \item $\langle\ell,\langle f',\Pi\rangle\rangle$, if $T'=\langle
%   f,\Pi\rangle$ where $f$ is a function and $\Pi$ is a sequence of
%   paths of length $n$ and for any
%   $a_1,\ldots,a_n$, $f'(a_1)\ldots(a_n)$ is defined iff
%   $f(a_1)\ldots(a_n)$ is defined and $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)\!\restriction\!r.\ell$ if $f(a_1)\ldots(a_n)$ is not a
%   restricted type. Otherwise, $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)$.
% \end{enumerate}  


% If $T$ is a record type and $r$ is a record, then $T\parallel r$, the
% \textit{specification} (or \textit{anchoring}) of $T$ by
% $r$\footnote{$r$ could also be referred to as a \textit{partial
%     specifier} or \textit{partial assignment} for $T$} is the result
% of replacing each field, $\langle \ell, T'\rangle$, in $T$ such that
% $\ell$ is a label in $r$, with 
% \begin{enumerate}
% \item  $\langle\ell,T'_{r.\ell}\rangle$\footnote{That is, in our
% standard graphical notation, \smallrecord{\smalltfield{$\ell$}{$T'$}} is
% replaced by \smallrecord{\smallmfield{$\ell$}{$r.\ell$}{$T'$}}}, if
% $T'$ is a type
% \item $\langle\ell,\langle f',\Pi\rangle\rangle$, if $T'=\langle
%   f,\Pi\rangle$ where $f$ is a function and $\Pi$ is a sequence of
%   paths of length $n$ and for any
%   $a_1,\ldots,a_n$, $f'(a_1)\ldots(a_n)$ is defined iff
%   $f(a_1)\ldots(a_n)$ is defined and $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)_{r.\ell}$
% \end{enumerate}

% A variant of this notion of specification is default specification
% which will only require specification of fields which are not already
% specified. If $T$ is a record type and $r$ is a record, then
% $T\dspec r$, the
% \textit{default specification} (or \textit{default anchoring}) of $T$ by
% $r$ is the result
% of replacing each field, $\langle \ell, T'\rangle$, in $T$ such that
% $\ell$ is a label in $r$, with 
% \begin{enumerate}
% \item  $\langle\ell,T'_{r.\ell}\rangle$, if
% $T'$ is a type but not a singleton type.\footnote{That is, $\langle
%   \ell, T'\rangle$ is not already a manifest field.} If $T'$ is a
% singleton type then $\langle \ell, T'\rangle$ is replaced by itself.
% \item $\langle\ell,\langle f',\Pi\rangle\rangle$, if $T'=\langle
%   f,\Pi\rangle$ where $f$ is a function and $\Pi$ is a sequence of
%   paths of length $n$ and for any
%   $a_1,\ldots,a_n$, $f'(a_1)\ldots(a_n)$ is defined iff
%   $f(a_1)\ldots(a_n)$ is defined and $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)_{r.\ell}$ if $f(a_1)\ldots(a_n)$ is not a
%   singleton type. Otherwise, $f'(a_1)\ldots(a_n) =
%   f(a_1)\ldots(a_n)$.
% \end{enumerate}


% Types can also be specified by records which have different labels to
% the type by using a relabelling.  Thus $T\parallel_\eta r$ is the
% result of replacing each field in $T$, $\langle\ell,T'\rangle$,  such
% that $\eta(\ell)$ is a label in $r$ and $r.\eta(\ell):T'$, with a
% manifest field$\langle\ell,T'_{r.\eta(\ell)}\rangle$.  More exactly we
% will define $T\parallel_\eta r$ in terms of flattening, relabelling
% and specification by a record:
% \begin{quote}
% $T\parallel_\eta r$ =
% $\varphi^-([[\varphi(T)]_\eta\parallel\varphi(r)]_{\eta^-})$
% \end{quote}
% Here are two examples:  suppose that % $a:T_1$, $b:T_2$ and 
% $\eta$ is a
% function with domain $\{\ell_1,\ell_2\}$ such that
% $\eta(\ell_1)=\ell_3$ and $\eta(\ell_2)=\ell_4$.  Then:
% \begin{quote}
% \record{\tfield{$\ell_1$}{$T_1$}\\
%         \tfield{$\ell_2$}{$T_2$}} $\parallel_\eta$ 
% \record{\field{$\ell_3$}{$a$}\\
%         \field{$\ell_4$}{$b$}}
% =
% \record{\mfield{$\ell_1$}{$a$}{$T_1$}\\
%         \mfield{$\ell_2$}{$b$}{$T_2$}}
% \end{quote}
% Suppose now that % $a$ and $b$ are as above and that 
% $\eta$ is a
% function with domain $\{\ell_5.\ell_1, \ell_5.\ell_2, \ell_6\}$ (where
% $\ell_5.\ell_1$ and $\ell_5.\ell_2$ are complex labels) such that
% $\eta(\ell_5.\ell_1)=\ell_7.\ell_3$,
% $\eta(\ell_5.\ell_2)=\ell_8.\ell_4$ and $\eta(\ell_6)=\ell_6$.  Then:
% \begin{quote}
% \record{\tfield{$\ell_5$}{\record{\tfield{$\ell_1$}{$T_1$}\\
%                                   \tfield{$\ell_2$}{$T_2$}}}\\
%         \tfield{$\ell_6$}{$T_3$}} $\parallel_\eta$
% \record{\field{$\ell_7$}{\record{\field{$\ell_3$}{$a$}}}\\
%         \field{$\ell_8$}{\record{\field{$\ell_4$}{$b$}\\
%                                  \field{$\ell_9$}{$c$}}}} =
% \begin{quote}
% \record{\tfield{$\ell_5$}{\record{\mfield{$\ell_1$}{$a$}{$T_1$}\\
%                                   \mfield{$\ell_2$}{$b$}{$T_2$}}}\\
%         \tfield{$\ell_6$}{$T_3$}}
% \end{quote}
% \end{quote}  

%\section{Generalizing record types}
%\label{app:gen-rectypes}

% One way to make a record type more general is to pick out one of its
% non-dependent fields.  Consider 
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}\\
%         \tfield{e}{dog(x)}}
% \end{quote}
% We can pick out the `x'-field which is not dependent, unlike the
% `e'-field. The result is
% \begin{quote}
% \record{\tfield{x}{\textit{Ind}}}
% \end{quote}
% In general for a record type,  $T$, we will represent the generalization
% of $T$ to its non-dependent $\ell$-field as $T^\ell$.  The general
% definition of this is:


\subsection{Path alignment within record types}
\label{app:path-align-rectype}
(Chapter~\ref{ch:underspec}, p.~\pageref{pg:path-alignment-types}) Suppose that $T$ is a record type and that $\pi_1$ and $\pi_2$ are
paths in $T$.  Then we use $T_{\pi_1=\pi_2}$ to represent the type
exactly like $T$ except that $T_{\pi_1=\pi_2}.\pi_1=
(T.\pi_1)_{\pi_2}$, that is, whatever type, $T'$, is at the end of the path
$\pi_1$, is replaced by the singleton type $T'_{\pi_2}$, or if
$T.\pi_1$ is
\begin{quote}
$\langle\lambda v_1\!:\!T_1\ldots \lambda v_n\!:\!T_n\
.\ T'\dep{v_1,\ldots,v_n}, \Pi\rangle$
\end{quote}
then it is replaced by
\begin{quote}
$\langle\lambda v_1\!:\!T_1\ldots \lambda v_n\!:\!T_n\ 
.\ (T'\dep{v_1,\ldots,v_n})_{\pi_2}, \Pi\rangle$
\end{quote}
We use $T_{\pi_{11}=\pi_{21},\ldots,\pi_{1n}=\pi_{2n}}$ to
represent $(\ldots(T_{\pi_{11}=\pi_{21}})\ldots)_{\pi_{1n}=\pi_{2n}}$.

(Chapter~\ref{ch:underspec}, p.~\pageref{ex:path-alignment-fcts}.)  If $\varphi=\ulcorner\lambda r\!:\!T\ .\ \psi\urcorner$ and
  $\pi_1,\pi_2\in\mathrm{paths}(T)$, then
  \begin{quote}
    $\varphi_{\pi_1=\pi_2}=\ulcorner\lambda r\!:\!T_{\pi_1=\pi_2}\ .\
    \psi\urcorner$
  \end{quote}
  

\section{List types}
\label{app:listtypes}

List types were not included in \cite{Cooper2012}.

A system of complex types with record types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has list
  types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:listtypes}) if
\begin{enumerate} 
 
\item for any $T \in \textbf{Type}$, $\mathrm{list}(T) \in \textbf{Type}$ 
 
\item for any $T \in \textbf{Type}$, 
\begin{enumerate} 
 
\item $[\ ]:_{\mathbf{TYPE_C}}\mathrm{list}(T)$ 

\item $a\!\mid\! L:_{\mathbf{TYPE_C}}\mathrm{list}(T)$ iff
  $a:_{\mathbf{TYPE_C}}T$ and $L:_{\mathbf{TYPE_C}}\mathrm{list}(T)$ 
 
\end{enumerate}

\end{enumerate}

In \cite{Cooper2012}
we did not specify an encoding of lists in terms of sets.  Here we
will use records with the reserved labels
`fst' and `rst' for the first member of the list and the remainder
(``rest'') of
the list respectively.  We let the empty list, [], be the empty set,
$\emptyset$.\footnote{If it is important to distinguish the empty list
  from the empty set we could use an additional reserved label,
  e.g. `lst',  and
  have the empty list be the labelled set $\{\langle
  \mathrm{lst},\emptyset\rangle\}$.}  If $L$ is a list then $a\!\mid\! L$
is to be the record
\begin{quote}
\record{\field{fst}{$a$}\\
          \field{rst}{$L$}}
\end{quote}

% labelled set $\{\langle\mathrm{fst},a\rangle,\langle\mathrm{rst},L\rangle\}$.


% We use $a\!\mid\! L$ to represent the record
% \begin{quote}
% \record{\field{fst}{$a$}\\
%         \field{rst}{$L$}}
% \end{quote}
% where `fst' (``first'') and `rst' (``rest'') are reserved labels used
% only in lists.


% We use $[\ ]$ to represent the empty list which is identical with the
% empty set, $\emptyset$.  

% A system of complex types {\bf TYPE$_C$} = $\langle${\bf Type}, {\bf BType},
% $\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
%   Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
%   non-empty list types} (Chapter~\ref{ch:infex},
% p.~\pageref{ex:nelisttypes}) if
% \begin{enumerate} 
 
% \item for any $T \in \textbf{Type}$, $\mathrm{nelist}(T) \in \textbf{Type}$ 
 
% \item for any $T \in \textbf{Type}$, 
% \begin{enumerate} 

% \item $[a]:_{\mathbf{TYPE_C}} \mathrm{nelist}(T)$ iff $a:T$
 
% \item $a\mid L:_{\mathbf{TYPE_C}} \mathrm{nelist}(T)$ iff
%   $a:_{\mathbf{TYPE_C}}T$ and $L:_{\mathbf{TYPE_C}} \mathrm{nelist}(T)$ 
 

 
% \end{enumerate}

% \end{enumerate}
We sometimes use $\mathrm{nelist}(T)$ as an abbreviation for the type
of non-empty lists:
\begin{quote}
  \record{
    \tfield{fst}{$T$}\\
    \tfield{rst}{$\mathrm{list}(T)$}
  }
\end{quote}

If
$L$ is a list we often use $\mathrm{fst}(L)$ and $\mathrm{rst}(L)$ to
represent $L$.fst and $L$.rst respectively.
% If $a\mid L :_{\mathbf{TYPE_C}} \mathrm{nelist}(T)$ for some system of
% complex types {\bf TYPE$_C$} and type $T$, then we use fst($a\mid L$)
% to refer to $a$ and rst($a\mid L$) to refer to $L$.

In contrast to \cite{Cooper2012} we here make it explcit that $\mathrm{list}(T)$
represents $\{\langle\mathrm{lst},T\rangle\}$ % and
% $\mathrm{nelist}(T)$ represents $\{\langle\mathrm{nelst},T\rangle\}$
where `lst' % and `nelst' are
is a reserved label. 


\section{Strings and regular types}
\label{sec:regular}
\label{app:strings}

% A \textit{string algebra over a set of objects} $O$ is a pair $\langle S,
% ^{\frown}\rangle$ where:
% \begin{enumerate} 
 
% \item $S$ is the closure of $O\cup\{\varepsilon\}$ ($\varepsilon$ is the empty string) under the binary operation `$^{\frown}$' (``concatenation'') 
 
% \item for any $s$ in $S$, $\varepsilon^{\frown}s = s^{\frown}\varepsilon = s$

% \item for any $s_1,s_2,s_3$ in $S$,
%   $(s_1^{\frown}s_2)^{\frown}s_3=s_1^{\frown}(s_2^{\frown}s_3)$.  For
%   this reason we normally write $s_1^{\frown}s_2^{\frown}s_3$ or more
%   simply $s_1s_2s_3$.
 
% \end{enumerate}

% The objects in $S$ are called strings.  Strings have length.  $\varepsilon$ has
% length 0.  If $s$ is a string in $S$
% with length $n$ and $a$ is an object in $O$ then $s^{\frown}a$ has
% length $n+1$.  We use $s[n]$ to represent the $n$th element of string
% $s$.

% In TTR strings are records\footnote{This is new since \cite{Cooper2012}.} with fields labelled by a distinguished
% ordered countably infinite set of labels (corresponding to the natural
% numbers):  t$_0$,t$_1$,\ldots.  The empty string is the empty record,
% that is the empty set.  This has length 0.  (Recall that records are sets of ordered
% pairs.)  A string with one element $a$ (of some type) is the
% record \smallrecord{\field{t$_0$}{$a$}}. If $s$ is a string whose
% highest label in the order is t$_n$ ($n\geq 0$) and $a$ is an object of
% some type then $s^{\frown}a$ is $s\cup\{\langle t_{n+1},a\rangle\}$.  If
% $s$ is a string whose highest label in the order is t$_n$ then the
% length of $s$ is $n+1$.  $s[n]$ is defined to be $s$.t$_n$.
% Concatenation (`$^{\frown}$') can be extended to include concatenation
% of strings of arbitrary length.  If $s$ is a string and $s_n$ is a
% string of length $n$, then $s^{\frown}s_n$ is
% $s^{\frown}s_n[0]^{\frown}\ldots^{\frown}s_n[n-1]$. 



A system of complex types  \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with record types
based on $\langle\mathcal{L}, \mathbf{RType}\rangle$ \textit{has
  strings} (Chapter~\ref{ch:infex}, p.~\pageref{ex:string-sys})
if
\begin{enumerate} 
 
\item for each natural number $i$, t$_i\in\mathcal{L}$
 
\item \textit{String} $\in$ \textbf{BType}

\item $\emptyset:_{\mathbf{TYPE}_C}$ \textit{String}

\item if $T \in$ \textbf{Type} and $a:_{\mathbf{TYPE}_C}T$ then
  $\{\langle\text{t}_0,a\rangle\} : \textit{String}$

\item if $s$ :$_{\mathbf{TYPE}_C}$ \textit{String}, t$_n\in\mathrm{labels}(s)$ such that
  there is no $i>n$ where t$_i\in\mathrm{labels}(s)$, $T \in$ \textbf{Type}
  and $a:_{\mathbf{TYPE}_C}T$ then $s\cup\{\langle \mathrm{t}_{n+1},a\rangle\}$ :$_{\mathbf{TYPE}_C}$
  \textit{String}

\item Nothing is of type \textit{String} except as required above.
 
\end{enumerate}

If $s$ is a string according to some type system with strings we write
$\mathrm{length}(s)$ for $|s|$ (that is the cardinality of the set of
ordered pairs constituting the record modelling the string).  If $s_1$
and $s_2$ are
strings, then the concatenation $s_1s_2$ is $s_1\cup s_2'$ where $s_2'$
is the result of replacing each label $t_i$ in $\mathrm{labels}(s_2)$ with $t_{i+\mathrm{length}(s_1)}$.

If $s$ is a string according to some type system and $\text{t}_n\in\mathrm{labels}(s)$, we use $s[n]$ to
represent $s.\text{t}_n$.  We use $\varepsilon$ to represent the empty
string (which is identical with the empty set).

A system of complex types  \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with strings has
\textit{length determining string types} (Chapter~\ref{ch:infex}, p.~\pageref{ex:ldstringtypes}) if
\begin{enumerate} 
 
\item for any $T\in\textbf{Type}$ and $n$ a natural number, the string
  types $T^{=n}$,
  $T^{\leq n}$, $T^{\geq n}\in\textbf{Type}$ 
 
\item $s:_{\mathbf{TYPE}_C}T^{=n}\ (T^{\leq n}, T^{\geq n})$ iff
  $s:_{\mathbf{TYPE}_C}\textit{String}$, for all $i$, $0\leq
  i<\mathrm{length}(s)$, $s[i]:_{\mathbf{TYPE_C}}T$ and $\mathrm{length}(s) =
  (\leq,\geq)\ n$ 
 
\end{enumerate}

When there is not source of confusion we write $T^n$ for $T^{=n}$. We
also write $T^*$ for $T^{\geq0}$ (Kleene star) and $T^+$ for
$T^{\geq1}$ (Kleene plus).

As with other complex types we model $T^{\xi n}$ (where $\xi$ is
`$=$', `$\leq$' or `$\geq$') as a labelled set:
\begin{quote}
$\{\langle\mathrm{str}_0,\{\langle\mathrm{comp},\xi\rangle,\langle\mathrm{num},n\rangle,\langle\mathrm{type},T\rangle\}\rangle\}$
\end{quote} 

A system of complex types  \textbf{TYPE}$_C$ = $\langle${\bf Type}, {\bf BType},
$\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
  Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ with strings and
length determining string types has \textit{concatenation types}
(Chapter~\ref{ch:infex}, p.~\pageref{ex:concatenation-types}) if
\begin{enumerate} 
 
\item if $T_1$, $T_2\in\textbf{Type}$ then the string type $T_1^\frown T_2\in\textbf{Type}$ 
 
\item $s:_{\mathbf{TYPE}_C}T_1^\frown T_2$ iff there are $s_1$ and
  $s_2$ such that
\begin{enumerate} 
 
\item $s_1s_2=s$ 
 
\item $s_1:_{\mathbf{TYPE}_C}T_1$ if $T_1$ is a string type, otherwise
  $s_1:_{\mathbf{TYPE}_C}{T_1}^{=1}$

\item $s_2:_{\mathbf{TYPE}_C}T_2$ if $T_2$ is a string type, otherwise
  $s_2:_{\mathbf{TYPE}_C}{T_2}^{=1}$  
 
\end{enumerate} 
   
 
\end{enumerate} 

The labelled set represented by ${T_1}^\frown T_2$ can be characterized as
follows:
\begin{quote}
Let $T_1'$ be ${T_1}^{=1}$ if $T_1$ is not a string type and $T_1$
otherwise and similarly let $T_2'$ be ${T_2}^{=1}$ if $T_2$ is not a
string type and $T_2$ otherwise.  Then $T_1^\frown T_2$ represents the
labelled set \mbox{$T_1'\cup T_2''$} where $T_2''$ is the result of replacing
any label `str$_i$' in $\mathrm{labels}(T_2')$ with `str$_{i+n+1}$',
where `str$_n$' is in $\mathrm{labels}(T_1')$ and there is no $j$ such
that `str$_j$' is in $\mathrm{labels}(T_1')$ and $j>n$.
\end{quote}  
This definition has as a consequence that `$^\frown$' is associative:
$(T_1^\frown T_2)^\frown T_3=T_1^\frown(T_2^\frown T_3)$.  


\subsection{Concatenation of values on a defined path in a string of
  records}

This definition is introduced in Chapter~\ref{ch:gram}, p.~\pageref{pg:concat-i}.

If $s$ is a string of length $n$ of records such that for each $i$,
$0\leq i<n$, $s[i].\pi$ is a defined path, 
$\displaystyle\mathop{\mathrm{concat}}_{0\leq i<n}(s[i].\pi)$ denotes
$s[0].\pi\ldots s[n-1].\pi$.  We use
concat$_i$($s[i].\pi$) to represent $\displaystyle\mathop{\mathrm{concat}}_{0\leq i<\mathrm{length}(s)}(s[i].\pi)$. 
  
 
% We can define types whose elements are strings.  Such types correspond
% to regular expressions and we will call them \textit{regular types}.
% Here we will define just two kinds of such types:  concatenation types
% and Kleene-+ types.

% A system of complex types with string types \textbf{TYPE}$_S$ = $\langle${\bf Type}, {\bf BType},
% $\langle$\textbf{PType}, {\bf Pred}, \textbf{ArgIndices}, {\it
%   Arity\/}$\rangle$, $\langle A,F\rangle$$\rangle$ \textit{has
%   concatenation types} if 
% \begin{enumerate} 
 
% \item 
% \begin{enumerate}
% \item for any $T_1$, $T_2$ $\in$ {\bf Type},  $({T_1}^\frown\!T_2)$
%   $\in$ {\bf Type}

% \item for any $T_1$, $T_2$, $T_3$ $\in$ \textbf{Type},
%   $({T_1}^{\frown}T_2)^{\frown}T_3 =
%   {T_1}^{\frown}({T_2}^{\frown}T_3)$\footnote{This has been added to
%     the definition in \cite{Cooper2012} to make associativity explicit.}
% \end{enumerate}
 
% \item $a :_{\mathbf{TYPE}_S} {T_1}^\frown\!T_2$ iff $a=x^\frown\!y$, $x:_{\mathbf{TYPE}_S}T_1$ and $y:_{\mathbf{TYPE}_S}T_2$ 
 
% \end{enumerate} 
% \textbf{TYPE}$_S$ \textit{has Kleene-+ types} if
% \begin{enumerate} 
 
% \item 
% for any $T$ $\in$ {\bf Type},  $T^+$ $\in$ {\bf Type} 
 
% \item $a:_{\mathbf{TYPE}_S}T^+$ iff $a=x_1^\frown\!\ldots^\frown\!x_n$, $n>0$ and for $i$, $1\leq
% i\leq n$, $x_i:_{\mathbf{TYPE}_S}T$ 
 
% \end{enumerate} 

% \textbf{TYPE}$_S$ \textit{has Kleene-* types} if
% \begin{enumerate} 
 
% \item 
% for any $T$ $\in$ {\bf Type},  $T^*$ $\in$ {\bf Type} 
 
% \item $a:_{\mathbf{TYPE}_S}T^*$ iff
%   $a=x_1^\frown\!\ldots^\frown\!x_n$, $n\geq 0$ and for $i$, $1\leq
% i\leq n$, $x_i:_{\mathbf{TYPE}_S}T$ 
 
% \end{enumerate} 

% Note that this definition distinguishes and object $a$ and the unit
% string consisting of $a$, that is, \smallrecord{\field{$t_0$}{$a$}}.
% We will use $\overset{\frown}{a}$ to represent this.

   
% Strings are used standardly in formal language theory where strings of
% symbols or strings of words are normally considered.  Following
% important insights by Tim Fernando
% \cite{Fernando2004,Fernando2006,Fernando2008,Fernando2009} we shall be
% concerned rather with strings of events.   We use informal notations
% like ` ``sam'' ' and ` ``ran'' '  to represent phonological types of
% speech events (utterances of \textit{Sam} and \textit{ran}).  Thus `
% ``sam''$^{\frown}$``ran'' ' is the type of speech events which are
% concatenations of an utterance of \textit{Sam} and an utterance of \textit{ran}.

\subsection{Predicates which relate strings}
\label{app:stringrels}

We introduce a number of distinguished predicates which are used to
relate strings.  The following predicates all have arity
[\textit{String},\textit{String}]: init, final, final\_align
\begin{description}
\item[init] ``$s_1$ is an initial substring of $s_2$''

If $s_1$ is a string of length $n$ and $s_2$ is a string of any
length, then $s$ : init($s_1$,$s_2$) iff the length of $s_2$ is
greater than or equal to $n$ and for each $i$, $0\leq i<n$,
$s_1[i]=s_2[i]$ and $s=s_2$.

\item[final] ``$s_1$ is an final substring of $s_2$''

If $s_1$ is a string of length $n$ and $s_2$ is a string of 
length $m$, then $s$ : final($s_1$,$s_2$) iff $m$ is
greater than or equal to $n$ and for each $i$, $0\leq i<n$,
$s_1[i]=s_2[(m-n)+i]$ and $s=s_2$.

\item[final\_align] ``$s_1$ is aligned with a final substring of
  $s_2$''

If $s_1$:\textit{Rec}$^+$ is a string of length $n$ and $s_2$:\textit{Rec}$^+$ is a string of 
length $m$, then $s$ : final\_align($s_1$,$s_2$) iff 
\begin{enumerate} 
 
\item $m$ is
greater than or equal to $n$ 
 
\item  $s$ is a string of length $m$

\item for each
$i$, $0\leq i<n$, 

\begin{enumerate} 
 
\item  $s[(m-n)+i]$ :
\smallrecord{\smalltfield{e$_1$}{\textit{Rec}} \\
             \smalltfield{e$_2$}{\textit{Rec}}} 
\item  $s[(m-n)+i]$.e$_1$ =
$s_1[i]$

\item $s[(m-n)+i]$.e$_2$ = $s_2[(m-n)+i]$
 
\end{enumerate} 

\item  otherwise for each
$i$, $0\leq i<m$, $s[i]=s_2[i]$ 
 
\end{enumerate} 


\end{description}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "ttl"
%%% End: