\documentstyle[a4wide,examples,11pt,macros,tree-dvips]{article}
% tree-dvips needs tree-dvips.pro

% amstex was in the style file.  Is it needed?

% AVM macros
%
\newcommand{\avmplus}[1]{{\setlength{\arraycolsep}{0.8mm}       
                       \renewcommand{\arraystretch}{1.1} % 1.2
                       \left[                   
                       \begin{array}{l}
                       \\[-1.5mm] #1 \\[-1.5mm] \\ %2
                       \end{array}              
                       \right]
                    }}
%
\newcommand{\att}[1]{{\mbox{\small {\bf #1}}}}
\newcommand{\attval}[2]{{\mbox{\small #1}\ :\ {{#2}}}}
\newcommand{\attvalterm}[2]{{\mbox{\small #1}\ :\ {\myvalue{#2}}}}
\newcommand{\attvaltyp}[2]{{\mbox{\small #1}\ :\ {\myvaluebold{#2}}}}
\newcommand{\myvalue}[1]{{\mbox{\normalsize {\it #1}}}}
\newcommand{\myvaluebold}[1]{{\mbox{\small {\bf #1}}}}
\newcommand{\ind}[1]{{\setlength{\fboxsep}{0.5mm} \: \fbox{{\tiny #1}} \:}}
%
\def\implies{\rightarrow}
\hyphenation{dis-ambig-uate dis-ambig-uated dis-ambig-uation}

\newcommand {\lsembrac}         {\mbox{[ \kern -0.5 em [}}
\newcommand {\rsembrac}         {\mbox{] \kern -0.5 em ]}}
\newcommand {\sem} [1]          {{\lsembrac #1 \rsembrac}}
\newcommand {\etal} {{\it et al.}}
%\newcommand{\hidden}[1]{}
\newcommand{\hidden}[1]{#1}
% \csmodels is the consequence relation in a formula; \csmodel is the
% consequence relation in running text.
\newcommand {\csmodels}         {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5
em $\approx$}\hspace*{0.5em}}
\newcommand {\csmodel}  {\mbox{$\mid$ \kern -0.5 em $\approx$}}

\newcommand {\notcsmodels} {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em
$\approx$ \kern -1 em $/$}\hspace*{0.5em}}

\newcommand {\csproves}         {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em $\sim$}\hspace*{0.5em}}
\newcommand {\csprove}  {\mbox{$\mid$ \kern -0.5 em $\sim$}}

\newcommand {\notcsproves} {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em $\sim$ \kern -1 em $/$}\hspace*{0.5em}}

\newcommand{\pdumodel}{\csmodel_{pdu}}
\newcommand{\pduprove}{\csprove_{pdu}}

\newcommand{\tag}[1]{\mbox{\^{ #1 }}}

\newcommand{\happyface} {\mbox{\Large
$\bigcirc$\small\raisebox{-0.02in}{\hspace*{-0.17in}$\smile$}
\raisebox{0.06in}{\hspace*{-0.17in}.\hspace*{0.03in}.}}\normalsize
\hspace{0.05in}}
% Used as in, e.g., \sem{\phi}^{\rm DPL}_{M,w,t}
%
% Unification
% -----------
\newcommand{\subsumes}{\op{\sqsubseteq}}
\newcommand{\subsumeseq}{\op{\sqsubseteq}}
\newcommand{\generalize}{\sqcup}
\newcommand{\unify}{\sqcap}
\newcommand{\sunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}_{s}}
\newcommand{\cunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}_{c}}
\newcommand{\dunify}{\stackrel{{\scriptscriptstyle <}}
                              {\sqcap}}
\newcommand{\ddunify}{\stackrel{{\scriptscriptstyle <>}}
                              {\sqcap}}
\newcommand{\unifyset}[1]{\bigsqcap #1}
\newcommand{\join}{\sqcap}
\newcommand{\meet}{\sqcup}
\newcommand{\setlist}[1]{\{ #1 \}}
\newcommand{\setstack}[1]{ \left\{ 
                           \begin{array}{l} #1 \end{array} 
                           \right\} }
\newcommand{\setcomp}[2]{\setlist{#1 \, \mid \, #2 }}
%

\newcommand{\modal}[1]{\langle #1 \rangle}



\newtheorem{defn}{Definition}
\newtheorem{translation}{Translation}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}


\begin{document}

\title{Order Independent and Persistent\\[1mm] 
Typed Default Unification}
\author{{\bf Alex Lascarides}\\
{\small Department of Linguistics,}\\
{\small Stanford University, {\em and}}\\
{\small Human Communication Research Centre,}\\
{\small University of Edinburgh,}\\
{\small 2 Buccleuch Place,}\\
{\small Edinburgh, EH8 9LW,}\\
{\small Scotland, UK}\\
{\small {\tt alex@cogsci.ed.ac.uk}}
\and
{\bf Ted Briscoe}\\ 
{\small Rank Xerox European Research Centre, {\em and}}\\
{\small Computer Laboratory,} \\
{\small University of Cambridge,}\\
{\small New Museums Site,}\\
{\small Pembroke Street,}\\
{\small Cambridge, CB2 3QG,}\\
{\small England, UK}\\
{\small {\tt ejb@cl.cam.ac.uk}}
\and
{\bf Nicholas Asher}\\
{\small IRIT, Universit\'{e} Paul Sabatier,}\\
{\small Toulouse, {\em and}}\\
{\small Department of Philosophy,}\\
{\small University of Texas at Austin,}\\
{\small Austin, Texas 78759,}\\
{\small USA}\\
{\small {\tt asher@bertie.la.utexas.edu}}
\and
{\bf Ann Copestake}\\
{\small Computer Laboratory,}\\
{\small University of Cambridge, {\em and}}\\
{\small CSLI,}\\
{\small Stanford University,}\\
{\small Stanford, CA 94305,}\\
{\small USA}\\
{\small {\tt aac@csli.stanford.edu}}}
\maketitle

\begin{abstract}
We define an order independent version of default unification on typed
feature structures.  The operation is one where default information in
a feature structure typed with a more specific type, will override
default information in a feature structure typed with a more general
type, where specificity is defined by the subtyping relation in the
type hierarchy.  The operation is also able to handle feature
structures where reentrancies are default.  We provide a formal
semantics, prove order independence and demonstrate the utility of
this version of default unification in several linguistic
applications.  First, we show how it can be used to define multiple
orthogonal default inheritance in the lexicon in a fully declarative
fashion. Secondly, we show how default lexical specifications
(introduced via default lexical inheritance) can be made to usefully
`persist beyond the lexicon' and interact with syntagmatic rules.
Finally, we outline how persistent default unification might underpin
default feature propagation principles and a more restrictive and
constraint-based approach to lexical rules.
\end{abstract}

\section{Introduction}

The utility of default feature specifications has been argued for in
the domain of feature propagation and specification in syntactic
theory (e.g. Gazdar, 1987; Shieber, 1986b), the analysis of gapping
constructions (Kaplan, 1987), and most frequently in inheritance-based
accounts of lexical organisation (Boguraev and Pustejovsky, 1990;
Briscoe \etal, 1990; Vossen and Copestake, 1993; Daelemans 1987; Evans
and Gazdar 1989a,b; Flickinger \etal, 1985; Flickinger, 1987;
Flickinger and Nerbonne, 1992; Krieger and Nerbonne, 1993; Shieber,
1986a and others). In this context, a frequent motivation for allowing
default inheritance in the lexicon is to capture phenomena of
blocking, or the overriding of regularities by subregularities (e.g.
Calder, 1989; Copestake and Briscoe, 1992; Briscoe \etal, 1993).
Approaches to formalising and implementing inheritance-based lexicons
include utilising object-oriented programming techniques (Daelemans,
1987; Flickinger \etal, 1985), knowledge representation languages
(Pustejovsky and Boguraev, 1993; Flickinger, 1987), path-based
inheritance (Evans and Gazdar, 1989a,b), overwriting templates
(Karttunen, 1986; Shieber, 1986a) and various definitions of default
unification (Copestake, 1993; Russell \etal, 1991, 1993). None of
these approaches achieves the perspicuity and declarativity of
subsumption-based approaches to non-default inheritance (e.g.
Carpenter, 1992), since in all these accounts inheritance must be carried
out in a predetermined order.

In order to provide an account of defaults which is more closely
integrated with the usual monotonic operations on feature structures
({\sc fs}s), it is natural to assume a notion of default unification.
Most definitions have followed Kaplan (1987) in assuming that this is
an asymmetric binary operation, with one default {\sc fs} being
regarded as adding consistent information to a non-default {\sc fs}.
The result is taken to be either a single {\sc fs} or a disjunction of
{\sc fs}s.  Carpenter (1993) reviews extant definitions of default
unification and concludes that none provide a good underpinning for a
perspicuous account of default lexical inheritance, because an
inheritance hierarchy must be separately defined for which inheritance
order must be stipulated, since default unification is not
associative under any of these definitions. Apart from this,
individual specifications of defaults which pertain to a class cannot
be evaluated incrementally with an asymmetric operation because the
information contributed by earlier defaults becomes non-default.
Furthermore, non-associativity makes default unification unsuitable
for use in situations where the application of defaults cannot be
circumscribed.  Order independence is not an essential property for
operations on static hierarchies, although it is highly desirable, but
it is necessary for applications where the order in which information
can be accumulated is not predefined.

In this paper, we address these problems by defining a symmetric,
order independent version of default unification on typed feature
structures.  Order independence is one way of allowing a series of
default unifications to be evaluated incrementally, and so the order
in which information can be accumulated need not be predefined. The
operation will extend previous work on default unification (e.g. Bouma
1990, 1992; Copestake, 1993; Carpenter, 1993; Russell \etal, 1991,
1993) in that, following Young and Rounds (1993) we mark default
information explicitly in feature structures rather than treating
default unification as an asymmetric operation on a defeasible {\sc
fs} and indefeasible {\sc fs}.  We call these {\sc fs}s, where default
information is explicitly marked as such, {\em default} {\sc fs}s (or
{\sc dfs}s).  In {\sc dfs}s, the defeasible information, if it
survives unification, persists as defeasible information, via the
explicit marking.  So we term this approach `persistent' default
unification.

Young and Rounds (1993) define a version of persistent default
unification, and provide a semantics via Default Logic (Reiter 1980).
The operation is order independent, but it has two limitations which
restrict its range of linguistic application.  First, the operation
does not permit more specific default information to override less
specific default information.  Secondly, the operation is not defined
over {\sc fs}s that incorporate default reentrancies.  As Young and
Rounds choose to formalise default unification within Default Logic,
the most straightforward way of extending their definition to one
which prioritises defaults, would be to re-encode their definition in
the extensions of default logic that are designed for prioritisation.
But all these extensions deploy one of the following two strategies.
Either the {\em order} of the application of default rules to the
premises is constrained extralogically (e.g. Konolige, 1988), or
prioritisation is introduced by translating the premises into the
logic in a context-sensitive way.  For example, 
if we have a class {\bf b} which is more specific than a class {\bf a},
and {\bf a} defeasibly implies $\phi$ while {\bf b} 
defeasibly implies the
incompatible information $\psi$, and we wish to unify two {\sc fs}s of
classes {\bf a} and {\bf b}, then, and {\it only} then, we add the
formula $b\rightarrow \neg \phi$ into the translation of the premises.
In this manner the order in which defaults concerning {\bf a} or the
defaults concerning {\bf b} are considered will not affect the result
(e.g. Brewka, 1991). 

Thus, extending Young and Rounds' operation to prioritise defaults via
extending Default Logic, will require specifications on the order in
which the default information in the two feature structures being
unified is considered, or it will considerably complicate the
translation of the {\sc fs}s into the logic.
Conditional logics for nonmonotonic reasoning have proved useful
exactly because the prioritisation of defaults is defined by the
axioms of the logic, and thus the priorities follow from the semantics
of the defaults themselves (e.g., Boutilier 1992, Delgrande 1988,
Asher and Morreau 1991, Morreau 1992).  So conditional logics don't
have to specify an order in which default rules are applied,
nor do they have to invoke a context-sensitive translation.
We will therefore use a conditional logic rather than an extension of
default logic to prioritise defaults.

In addition, we also extend persistent default unification to {\em
typed} default feature structures ({\sc tdfs}s) and to {\sc tdfs}s
containing specifications of defeasible reentrancy. We provide a
translation of {\sc tdfs}s into a conditional logic, define the
default
unification operation via the logical consequence relation of this
logic, and prove order
independence via this logical consequence relation.  We
also discuss the computational
complexity of default unification in the framework we develop.  We
motivate allowing default specification to `persist beyond the
lexicon' in order to elegantly encode defeasible lexical semantic
information and to support seamless interaction with principles of
discourse interpretation. However, we begin with constraint-based
approaches to lexical organisation, motivating the utility of
order-independent and persistent typed default unification as the
operation underpinning (default) inheritance in the lexicon.

\section{Inheritance-based Lexicons and Default Unification}

Recent unification/constraint-based accounts of the lexicon have
largely moved away from a conception of the lexicon as an unstructured
list of lexical entries towards a hierarchical or network,
inheritance-based view in which lexical entries are defined via
cross-classification of their similarities (see e.g. Pollard and Sag,
1987). Under this view the lexicon is still seen by the syntagmatic
component as a list of lexical entries (represented as {\sc fs}s), but
generalisations concerning their structure are captured by the
inheritance network.  For example, we may wish to define lexical
signs, intransitive verbs and monadic predicates, as in
Figure~\ref{one}.
\hidden{
\begin{figure}
\begin{tabular}{lll}
{\bf sign}  & $\implies$ & 
{\tiny
$\avmplus{\attvaltyp{PHON}{orth}}$
}\\[1mm]
{\bf intrans-verb}  & $\implies$ & {\bf sign} $\wedge$
{\tiny
$\avmplus{\attval{SYN}{\avmplus{
             \attvaltyp{CAT}{verb}  \\
             \attval{SUBJ}{\avmplus{
                \attval{SYN}{\avmplus{
                         \attvaltyp{CAT}{np}}}}}}}}$
}\\[1mm]
{\bf monadic}  & $\implies$ & {\bf sign} $\wedge$
{\tiny
$\avmplus{\attval{SYN}{\avmplus{            
             \attval{SUBJ}{\avmplus{
                \attval{SEM}{\ind{1}}}}}} \\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\ind{1}}}}}$
}\\[1mm]
{\bf monadic-intrans-verb}  & $\implies$ & {\bf monadic} $\wedge$ {\bf intrans-verb}
\end{tabular}
\caption{{\sc fs} Constraints}
\label{one}
\end{figure}
} 
We can specify that classes are in a partial order, illustrated as a
Hasse diagram in Figure~\ref{three}, so that there is a homomorphism
between the partial order and the constraints on the classes.  Under
these conditions, the constraint specifications shown as {\sc avm}s in
Figure~\ref{one} can be treated as being monotonically inherited and
the constraint on a class can be calculated by unifying the
constraints on its parents with its own constraint specification.  The
constraint on {\bf monadic-intrans-verb} is thus the {\sc avm} shown
in Figure~\ref{two}.
\begin{figure}
\begin{center}
\setlength{\unitlength}{0.05in}
\begin{picture}(30,20)
{\put(20,20){\makebox(0,0){\bf sign}}
\put(18,18){\line(-1, -1){6}}
\put(22,18){\line(1, -1){6}}
\put(10,10){\makebox(0,0){\bf intrans-verb}}
%\put(8,8){\line(-1, -1){6}}
\put(12,8){\line(1, -1){6}}
\put(20,0){\makebox(0,0){\bf monadic-intrans-verb}}
\put(30,10){\makebox(0,0){\bf monadic}}
\put(28,8){\line(-1, -1){6}}}
\end{picture}
\end{center}
\caption{Schematic partial inheritance network}
\label{three}
% there has to be a better way of doing this...
\end{figure}
\hidden{
\begin{figure}
\begin{center}
{\tiny
$\avmplus{\att{monadic-intrans-verb} \\
         \attvaltyp{PHON}{orth}\\
         \attval{SYN}{\avmplus{
                  \attvaltyp{CAT}{verb}\\
                  \attval{SUBJ}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{1}}}}}}\\

         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\ind{1}}}}}$
}\\[1mm]
\caption{Constraint on {\bf monadic-intrans-verb} represented as an {\sc avm}}
\label{two}
\end{center}
\end{figure}
}

The description of {\it sleep} can simply state that it is a {\bf
monadic-intrans-verb} with idiosyncratic values for phonology and
semantics.  Thus unifying the constraint for {\bf
monadic-intrans-verb} with the lexical description will allow us to
construct the {\sc fs} for {\it sleep}.  As unification is an
associative operation, partial orders / Hasse diagrams can be
interpreted algebraically or logically and no `extralogical' ordering
or procedurality is being smuggled into the theory (e.g. Carpenter,
1992; de Paiva, 1993; Smolka and A\"{\i}t-Kaci, 1988; Zajac, 1993).
Classes can be seen as simply being part of the lexical description
language, however, in what follows we assume a typed feature structure
framework where the classes are types (or sorts in the terminology of
Pollard and Sag (1987)) which label {\sc fs} nodes.  Therefore, types
are an integral part of the feature structure language.  Nevertheless,
most of our discussion of inheritance is applicable to both typed and
untyped frameworks.

Further abbreviation and generalisation can be obtained if the
inheritance network is interpreted in a default fashion.
Figure~\ref{simple-eg} gives a simple example of an inheritance
hierarchy based on default inheritance. This data does not provide a
convincing motivation for introducing the considerable extra machinery
required to formalise default inheritance as opposed to a monotonic
subsumption hierarchy --- this can be found in the works cited above
and in \S4 and \S6. However, it does suffice to illustrate the
weaknesses of current definitions of default unification regarded as
the operation underlying default inheritance.
\begin{figure}
\setlength{\unitlength}{0.5in}
\begin{center}
\begin{picture}(6.5,3.4)(-0.25, 0.5)
\thicklines
\put(4,4.2){\makebox(0,0){{\boldmath $\top$}}}
\put(4,4){\line(-1, -1){1}}
\put(4,4){\line(1, -1){1}}
\put(4,4){\line(-3, -1){3}}
\put(4,4){\line(3, -1){3}}
\put(4,4){\line(0, -1){1}} %
\put(1, 2.6){\makebox(0,0){{\tiny $\avmplus{\att{verb}\\
\attval{PST}{\ind{1}\myvaluebold{+ed}}\\ \attval{PSP}{\ind{1}}}$}}}
\put(3.1, 2.6){\makebox(0,0){{\tiny $\att{+en}$}}}
\put(5, 2.6){\makebox(0,0){{\tiny $\att{+t}$}}}
\put(4, 2.6){\makebox(0,0){{\tiny $\att{+ed}$}}}
%\put(5, 2.6){\makebox(0,0){{\tiny $\att{t-or-ed}$}}}
\put(7, 2.6){\makebox(0,0){{\tiny $\att{stg-vow}$}}}
\put(1, 2.1){\line(-1, -1){0.5}}
\put(1, 2.1){\line(1, -1){0.5}}
%\put(5, 2.3){\line(-1, -1){0.5}}
%\put(5, 2.3){\line(1, -1){0.5}}
\put(7, 2.3){\line(-1, -1){0.5}}
\put(7, 2.3){\line(1, -1){0.5}}
\put(0, 1.3){\makebox(0,0){{\tiny $\avmplus{\att{pst-t-vb}\\ \attvaltyp{PST}{+t}}$}}}
\put(2.1, 1.3){\makebox(0,0){{\tiny $\avmplus{\att{stg-vb}\\ \attvaltyp{PST}{stg-vow}}$}}}
%\put(4.5, 1.6){\makebox(0,0){{\tiny $\att{+ed}$}}}
%\put(5.5, 1.6){\makebox(0,0){{\tiny $\att{+t}$}}}
\put(6.5, 1.6){\makebox(0,0){{\tiny $\att{+u}$}}}
\put(7.5, 1.6){\makebox(0,0){{\tiny $\att{+o}$}}}
%\put(0, 1){\line(0, -1){0.5}}
\put(2, 1){\line(0, -1){0.5}}
%\put(0, 0){\makebox(0,0){{\tiny $\avmplus{\att{dual-pst-vb}\\ \attvaltyp{PST}{t-or-ed}}$}}}
\put(2.2, 0){\makebox(0,0){{\tiny $\avmplus{\att{psp-diff-vb}\\ \attvaltyp{PSP}{+en}}$}}}
\end{picture}
\end{center}
\vspace*{2mm}
\caption{Partial Default Inheritance Hierarchy}
\label{simple-eg}
\end{figure}
The intended interpretation of Figure~\ref{simple-eg} is that elements
in bold represent types, with most general types at the top; thus {\bf
psp-t-vb} is a subtype of {\bf verb}. The {\sc fs}s in {\sc avm}
notation associated with types represent {\em default constraint
specifications} associated with such types.  Furthermore, there is a
subsumption ordering on values as indicated on the right with {\bf +u}
being an atomic leaf type which is more specific than {\bf stg-vow}.
{\sc pst} encodes the past tense suffixes of English verbs. {\sc psp}
encodes their past and passive participle suffixes.  The full
specification of {\bf verb} will include much more information
appropriate to regular verbs and each subtype will inherit this
information, unless it is explicitly overridden by a specification on
that subtype. Thus {\bf psp-t-vb}s are specified to be identical to
{\bf verb}s, and thus fully regular except in their specification of
the past tense suffix. Since, by default, {\sc pst} is reentrant with
{\sc psp} on {\bf verb}, all the classes are meant to inherit this
reentrancy constraint, except {\bf psp-diff-vb}s where it is
overridden. Thus {\it walk, walked} can simply be specified as {\bf
verb}, {\it keep, kept} as {\bf pst-t-vb}, {\it strike, struck} as
{\bf stg-vb}, and {\it break, broke, broken} as {\bf
psp-diff-vb}.\footnote{We intend that the lexical hierarchy should
interact with lexical rules which relate past tense and participle
forms of verbs to base forms by changing the specification of {\sc
vform} values and phonologically adjoining the value of {\sc psp} or
{\sc pst} to the stem. Pollard and Sag (1987) describe this approach
to lexical rules and Bird and Klein (1994) describe how
morphophonological operations can be characterised in a
constraint-based formalism.}

The assumption behind the use of default unification in inheritance
hierarchies is that it is used instead of monotonic unification to
construct the constraint on a class from its default constraint
specification and the constraints on its parents.  Thus the {\sc fs}
associated with {\bf pst-t-verb} would be default unified with that of
{\bf verb}.  However, as it stands, this example is incoherent.  The
{\sc fs} associated with {\bf verb} specifies a defeasible value and a
defeasible reentrancy between two attributes. An operation of default
unification defined to combine this information with the conflicting
value specification on {\bf pst-t-vb} is problematic because it is not
clear which aspects of the defeasible information on the supertype
constraint should survive -- the reentrancy or the value or neither.
The situation is represented in Figure~\ref{unif1} where $\dunify$
denotes default unification of an indefeasible {\sc fs} with a
defeasible {\sc fs}, $\mbox{{\em indefeasible} {\sc fs}} \dunify
\mbox{{\em defeasible} {\sc fs}}$ (or
equivalently here of a subtype {\sc fs} with a parent type {\sc fs}).
(We use $\top$ as equivalent to unspecified.)  The results shown are
those using the definitions proposed by Carpenter (1993): the first
(credulous) result is the set of maximally informative default
extensions of the indefeasible {\sc fs}, the second (skeptical) result
is the generalisation of this set.\footnote{The results given by some
alternative definitions are discussed in Copestake (1993).
Carpenter's definitions treat path equality (reentrancy) information
as having equal status with path value information, but there are
alternative options where one or other is treated as having priority.}
In Figure~\ref{simple-eg} it is now possible to see that different
choices are required at different points: in all cases except {\bf
psp-diff-vb} we want the original defeasible reentrancy between {\sc
pst} and {\sc psp} to survive; with {\bf psp-diff-vb} we want the
reentrancy to be rejected in favour of the distinct values.  Clearly,
if we are to adopt a single consistent definition of default
unification we must alter the hierarchy of Figure~\ref{simple-eg} by
explicitly specifying that the reentrancy is retained in {\bf
pst-t-vb} and {\bf stg-vb}.  One important design consideration in the
definition of a useful default unification operation is the
computational complexity of the resultant system. For this reason, in
the case of such indeterminacies, we would prefer to adopt Carpenter's
(1993) skeptical approach and define the result as the skeptical
extension of the indefeasible or more specific information with (more
general) default information; thus, avoiding indeterminacy in the
outcome.
\begin{figure}
\begin{tabular}{llcc}
{\tiny
$\avmplus{\attvaltyp{PST}{+t}\\
                 \attvaltyp{PSP}{{\boldmath $\top$}}}$
}
\normalsize 
$ \dunify $
{\tiny
$\avmplus{\attval{PST}{\ind{1}\ \myvaluebold{+ed}}\\
                 \attval{PSP}{\ind{1}}}$}
& 
$=$
&
{\tiny
$\left\{
\avmplus{\attvaltyp{PST}{+t}\\
                 \attvaltyp{PSP}{+ed}} , 
\avmplus{\attval{PST}{\ind{1}\ \myvaluebold{+t}}\\
                 \attval{PSP}{\ind{1}}} \right\}$} 
& (credulous)\\[0.1in]
& $=$ & 
{\tiny
$\avmplus{\attvaltyp{PST}{+t}\\
                 \attvaltyp{PSP}{{\boldmath $\top$}}}$} & (skeptical)
\end{tabular}
\caption{Indeterminacy of Default Unification}
\label{unif1}
\end{figure}

But there is a general problem with the asymmetric definitions of
default unification considered by Bouma (1990, 1992), Carpenter
(1993), Copestake (1993) and Russell \etal\, (1991, 1993), because
defeasible and indefeasible information in {\sc fs}s is not kept
distinct.  Instead, in each application of the operation one argument
{\sc fs} is treated as entirely defeasible and the other as entirely
indefeasible, and the result is a `normal' {\sc fs} or set of {\sc
fs}s as in Figure~\ref{unif1}. It is straightforward to see that none
of these definitions is commutative --- if we switch the order of the
arguments in Figure~\ref{unif1} the result will be different because
we also switch the defeasibility of the information in each {\sc fs}.
What is less obvious is that the results are also not associative:
Figure~\ref{non-assoc-unif} shows one example which illustrates this
for Carpenter's credulous and skeptical operations.  Thus, if we use a
definition of this type to implement default inheritance in a lexical
hierarchy, we either have to define the result as the values obtained
by considering all possible orders (or their generalisation), which is
clearly unattractive both for computational tractability and
perspicuity, or we have to make an additional procedural stipulation
of inheritance order.  For example, we would, in general, obtain
different results if we proceeded `top-down', composing successively
more specific default constraints, than if we proceed `bottom-up'
adding successively more general default specifications (see
Carpenter, 1993 for further discussion).  
\begin{figure}
\begin{center}
\begin{tabular}{lll}
{\tiny 
$\left(
\avmplus{\attvaltyp{F}{c}\\
                 \attvaltyp{G}{c}}

\mbox{\normalsize $\dunify$} 

\avmplus{\attvaltyp{F}{a}\\
                 \attvaltyp{G}{b}}
\right)

\mbox{\normalsize $\dunify$} 

\avmplus{\attval{F}{\ind{1}}\\
                 \attval{G}{\ind{1}}}$
}
& 
$=$
&
{\tiny
$\avmplus{\attval{F}{\ind{1} \myvaluebold{c}}\\
                 \attval{G}{\ind{1}}}$}\\[0.1in]
% next line
{\tiny
$\avmplus{\attvaltyp{F}{c}\\
                 \attvaltyp{G}{c}}$}

$\dunify$

{\tiny
$\left(
\avmplus{\attvaltyp{F}{a}\\
                 \attvaltyp{G}{b}}

\mbox{\normalsize $\dunify$}

\avmplus{\attval{F}{\ind{1}}\\
                 \attval{G}{\ind{1}}}
\right)$
}
& 
$=$
&
{\tiny
$\avmplus{\attvaltyp{F}{c}\\
                 \attvaltyp{G}{c}}$}
\end{tabular}
\end{center}
\caption{Non-associativity of Asymmetric Default Unification}
\label{non-assoc-unif}
\end{figure}

Young and Rounds (1993) provide a definition of default unification of
{\sc fs}s in which defeasible information is explicitly marked. This
enables them to provide a definition which is both commutative and
associative. However as we've mentioned, their approach is limited by
two factors; firstly, their definition doesn't deal with reentrancy,
so their operation would not support the overriding of reentrancy in
Figure~\ref{simple-eg} on {\bf psp-diff-vb}; secondly, they do not
prioritise defaults.  Thus, their definition is limited to cases of
indefeasible values overriding conflicting defeasible ones. This would
be adequate to capture the overriding of {\sc psp} on {\bf stg-vb} in
Figure~\ref{simple-eg}, but not to allow this value to be overridden
by that on {\bf psp-diff-vb}, for example.  We have argued in favour
of extending their work by formalising default unification in a
conditional logic, rather than an extension of Default Logic.  This
will enable us to introduce prioritisation of defaults into the
operation, without constraining the order in which default information
is accumulated into the result of unifying two {\sc fs}s.

\section{Persistent Default Unification}
\label{PDUdefn}

In this section we present a definition of persistent default
unification of typed feature structures ({\sc tfs}s) which is order
independent, allows for default reentrancy and has a built-in notion
of specificity.  We begin by defining typed default feature structures
({\sc tdfs}s), which are more complex than normal {\sc fs}s in order
to incorporate both default and non-default information, and then
informally describe persistent default unification ($\ddunify$) and
illustrate its behaviour with examples.  To formalise $\ddunify$ we
provide a translation function between {\sc tdfs}s and formulae of a
conditional logic in \S\ref{logic-operation}, and axiomatise the
conditional logic so that the operation $\ddunify$ has the desired
properties.

\subsection{Typed default feature structures}

We assume a theory of {\sc tfs}s which is similar to that of Carpenter
(1992), Copestake \etal\ (1993) and Zajac (1993) in which types label
nodes in {\sc fs}s (shown in bold in {\sc avm} diagrams but omitted
where irrelevant).  The definition of the type hierarchy $\langle
\mbox{{\sf Type}}, \sqsubseteq \rangle$ is equivalent to that in Carpenter (1992).
However, we use a convention where more specific types are described
as being lower in the hierarchy, thus $\top$ is the most general type,
and $\bot$ indicates inconsistency.  The hierarchy is a lattice, so
any set of types will have a unique greatest lower bound or meet.
Monotonic unification ($\unify$) of a set of {\sc tfs}s is defined to
result in an {\sc fs} which has a type equal to the meet of the types
of the unified structures and is usually said to fail if this is
$\bot$.  However, in what follows, we will allow {\sc fs}s to contain
nodes which are typed $\bot$.  We assume all {\sc tfs}s are acyclic
and we treat all values as intensional; that is, there can be more than
one instance of any type in a {\sc tfs} (see Carpenter 1992 for
details).  Treating values this way is more general than treating them
as extensional: persistent default unification can handle both kinds of
structures.  
On the other hand, we leave open how the operation would
have to be extended to handle cyclic structures.

To define order independent persistent default unification of {\sc
tfs}s we introduce a notation for {\sc tdfs}s which, informally,
contains a `double' {\sc tfs} in which the left-hand {\sc fs}
specifies what is indefeasible and the right-hand {\sc fs} what is
defeasible. For instance, the constraint associated with {\bf verb}
could be represented as (\ref{tdfs}), which makes explicit the fact
that it is the reentrancy specification and value on {\sc pst} which
are default, rather than the presence of the attributes {\sc pst} and
{\sc psp}.
\begin{examples}
\item   \label{tdfs}
{\tiny
$
\avmplus{\att{verb$^1$}\\
        \attvaltyp{PST}{\boldmath $\top$}\\
        \attvaltyp{PSP}{\boldmath $\top$}}
\left/ \begin{array}{c}
\avmplus{\att{verb$^1$}\\
        \attval{PST}{\ind{1}\myvaluebold{+ed}}\\ 
        \attval{PSP}{\ind{1}}}
               \end{array} 
\right.
$}
$
\left/ 
\{\langle \mbox{PST},\{\langle \mbox{+ed,verb}\rangle\}\rangle,
\langle \mbox{PSP},\{\langle \mbox{+ed,verb}\rangle\}\rangle\}
\right. 
$
\end{examples}
The third element in the structure is a {\it tail}.  Tails record the
information we need from the history of default unifications a {\sc
tdfs} has undergone, in order to guarantee order independence of the
operation.  For each path, the tail contains {\em value-specificity}
pairs, which record a default {\em value} that appeared on that path
in a {\sc tdfs} that was used to build the {\sc tdfs} being
considered, together with the type of the root node of
that {\sc tdfs}.  The
position of this root type in the type hierarchy (which we assume to
be a finite bounded complete partial order, as defined in Carpenter
(1992; 11--13)) records the {\em specificity} of the default
information.  In general, during a series of default unifications,
tails will record the values on paths of original {\sc tdfs}s,
together with the specificity of those {\sc tdfs}s.  For example, if a
{\sc tdfs} has a tail of the form:
\[
\{\langle \pi,\{\langle a,t_1\rangle,\langle
b,t_2\rangle\}\rangle, \langle \pi',\{\langle c,t_3\rangle,\langle
d,t_4\rangle\}\rangle\}
\]
then this means that to produce this {\sc tdfs} we unified: a {\sc
tdfs} that had a root type $t_1$ and defeasible path $\pi:a$; a {\sc
tdfs} that had a root type $t_2$ and defeasible path $\pi:b$; a {\sc
tdfs} that had a root type $t_3$ and defeasible path $\pi':c$; and a
{\sc tdfs} that had a root type $t_4$ and defeasible path $\pi':d$.
The relative order of $t_1$, $t_2$, $t_3$ and $t_4$ in the type
hierarchy determines the relative specificity of the paths $\pi:a$,
$\pi:b$, $\pi':c$ and $\pi':d$ respectively.  As will become clear
below, keeping track of this information is the cost we pay for being
able to define default unification as an order independent operation.
We will refer to the initial specifications of defaults as the initial
knowledge base ({\sc kb}): for any {\sc fs} in the initial {\sc kb}
the tail will just contain the path value information present which is
defeasible; i.e., it appears in the defeasible {\sc fs}, but is
strictly more specific than the indefeasible {\sc fs}.  We may refer
to such information as {\em strictly default}.  
Note
that we recorded the values on both the equivalent paths
PST and PSP in the tail of
(\ref{tdfs}).  
Path equivalences themselves
are not recorded in tails, however.
A fourth element in a
{\sc tdfs} is a tag shown as a superscript on the root types of the
{\sc fs}s.  This is used to identify {\sc tdfs}s, to aid the translation
to conditional logic.  We will normally omit indices in this
section, since they do not affect the results of the
default unification operation.

We can make some convenient abbreviations, so that the `double' {\sc
avm} notation can be factored across individual paths into a single {\sc avm}
representation where we have \linebreak[4]$\mbox{{\em IndefeasibleValue}} / 
\mbox{{\em DefeasibleValue}}$
which in turn can be abbreviated to $\mbox{{\em IndefeasibleValue}}$
where $\mbox{{\em IndefeasibleValue}}$ is the same as {\em
DefeasibleValue}, and $/\mbox{{\em DefeasibleValue}}$ where
$\top/\mbox{{\em DefeasibleValue}}$, without ambiguity. We can also
omit the tail, when it can be determined from the default {\sc fs}.
Thus (\ref{tdfs}) can be represented as (\ref{tdfs2}).
\begin{examples}
\item   \label{tdfs2}
{\tiny
$
\avmplus{\att{verb}\\
        \attval{PST}{/\ind{1}\myvaluebold{+ed}}\\
        \attval{PSP}{/\ind{1}}}
$}
\end{examples}

Using this notation, our new version of the default inheritance hierarchy
introduced in the previous section is shown in Figure~\ref{final-eg}.
\begin{figure}
\setlength{\unitlength}{0.5in}
\begin{center}
\begin{picture}(6.5,3.4)(-0.25, 0.5)
\thicklines
\put(4,4.2){\makebox(0,0){\boldmath $\top$}}
\put(4,4){\line(-1, -1){1}}
\put(4,4){\line(1, -1){1}}
\put(4,4){\line(-3, -1){3}}
\put(4,4){\line(3, -1){3}}
\put(4,4){\line(0, -1){1}} %
\put(1, 2.6){\makebox(0,0){{\tiny $\avmplus{\att{verb}\\
\attval{PST}{/\ind{1}\myvaluebold{+ed}}\\ \attval{PSP}{/\ind{1}}}$}}}
\put(3.1, 2.6){\makebox(0,0){{\tiny $\att{+en}$}}}
\put(5, 2.6){\makebox(0,0){{\tiny $\att{+t}$}}}
\put(4, 2.6){\makebox(0,0){{\tiny $\att{+ed}$}}}
%\put(5, 2.6){\makebox(0,0){{\tiny $\att{t-or-ed}$}}}
\put(7, 2.6){\makebox(0,0){{\tiny $\att{stg-vow}$}}}
\put(1, 2.1){\line(-1, -1){0.5}}
\put(1, 2.1){\line(1, -1){0.5}}
%\put(5, 2.3){\line(-1, -1){0.5}}
%\put(5, 2.3){\line(1, -1){0.5}}
\put(7, 2.3){\line(-1, -1){0.5}}
\put(7, 2.3){\line(1, -1){0.5}}
\put(0, 1.3){\makebox(0,0){{\tiny $\avmplus{\att{pst-t-vb}\\ \attvaltyp{PST}{$/$+t}}$}}}
\put(2.1, 1.3){\makebox(0,0){{\tiny $\avmplus{\att{stg-vb}\\ \attvaltyp{PST}{stg-vow}}$}}}
%\put(4.5, 1.6){\makebox(0,0){{\tiny $\att{+ed}$}}}
%\put(5.5, 1.6){\makebox(0,0){{\tiny $\att{+t}$}}}
\put(6.5, 1.6){\makebox(0,0){{\tiny $\att{+u}$}}}
\put(7.5, 1.6){\makebox(0,0){{\tiny $\att{+o}$}}}
%\put(0, 1){\line(0, -1){0.5}}
\put(2, 1){\line(0, -1){0.5}}
%\put(0, 0){\makebox(0,0){{\tiny $\avmplus{\att{dual-pst-vb}\\ \attvaltyp{PST}{t-or-ed}}$}}}
\put(2.2, 0){\makebox(0,0){{\tiny $\avmplus{\att{psp-diff-vb}\\ \attvaltyp{PSP}{+en}}$}}}
\end{picture}
\end{center}
\vspace*{2mm}
\caption{Partial Default Inheritance Hierarchy (new version)}
\label{final-eg}
\end{figure}

In the formal definition of {\sc tdfs} below, we ensure that in a
well-formed {\sc tdfs} the indefeasible specification subsumes the
defeasible specification; that is, defaults {\em add} information to
what is known indefeasibly.  However, it does not specify any
relationship between the {\sc fs}s and the tail.  This relationship in
the {\sc tdfs}s for the initial {\sc kb} is conventionally defined as
above, and the way tails are merged during unification will be defined
by the unification operation itself, rather than via the definition of
{\sc tdfs}s.  This means there are some {\sc tdfs}s that are
well-formed, but which would never be in an initial {\sc kb}, nor
constructed via unification from those {\sc tdfs}s in the initial {\sc
kb}.

Firstly, we reiterate Carpenter's (1992) definition of a type
hierarchy, on which the definition of {\sc tdfs}s rests.

\begin{defn}{\bf Type Hierarchy}\\
A type hierarchy is a finite bounded complete partial order $\langle
\mbox{{\sf Type}},\sqsubseteq\rangle$.
\end{defn}

This guarantees that any set of types will have a unique most general
unifier, which will be $\bot$ in the case of inconsistent types.  We
now define tails, and then {\sc tdfs}s.

\begin{defn}{\bf Tails}\\
A tail is a set of pairs, where
\begin{itemize}
\item   The first member of the pair is a sequence of features (i.e. a path);
\item   the second member of the pair is a set of pairs of types.
\end{itemize}
\end{defn}

\begin{defn}{\bf Typed Default Feature Structure}\\
A typed default feature structure 
defined on a set of features {\sf Feat}, a set
of types {\sf Type} in a type hierarchy $\langle\mbox{{\sf
    Type}},\sqsubseteq\rangle$ and a set of indices $N$
is a tuple $\langle  {\cal T}, i,  Q, {\cal R},
\delta,\theta\rangle$, where:
\begin{itemize}
\item   ${\cal T}$ is a tail.
\item   $i\in N$ is the tag of the {\sc tdfs}.
\item   $Q$ is a finite set of nodes,
\item   ${\cal R} \in Q\times Q$ \\
(${\cal R}$ are the root nodes of
  the indefeasible and defeasible {\sc tfs}s).
\item   $\theta: Q\longrightarrow \mbox{{\sf Type}}$ is a partial
typing function.
\item   $\delta: Q\times \mbox{{\sf Feat}} \longrightarrow Q$ is a
partial feature value function, 
\end{itemize}
such that if $\langle n_1,n_2\rangle = {\cal R}$ then 
\begin{enumerate}
\item   $n_1$ and $n_2$ aren't $\delta$-descendants.
\item   All members of $Q$ are $\delta$-descendants of $n_1$ or $n_2$
(but not both).
\item   There is no node $n$ such that
  $\delta\ldots(\delta(n,F_1),F_2)\ldots F_k)=n$
\item   $\theta(n_2) = \theta(n_1)$ 
\item   If $n\in Q$ is a $\delta$-descendant of $n_1$, 
and $\theta(n_2) \neq \bot$, then there is an
isomorphic $m\in Q$ that is a $\delta$-descendant of $n_2$.  That is:
\begin{enumerate}
\item   If $\delta(\ldots(\delta(n_1,F_1),F_2)\ldots F_k) = n$, then 
$\delta(\ldots(\delta(n_2,F_1),F_2)\ldots F_k) = m$; and
\item   $\theta(m)\sqsubseteq \theta(n)$
\end{enumerate}
(1, 2 and 3 ensure that we have two {\sc dag}s rooted at $n_1$ and $n_2$,
and 4 and 5 ensure that defeasible information is at least as specific
as indefeasible information).
\end{enumerate}
\end{defn}

In the above definition, there is an {\sc fs} containing the
indefeasible information rooted at $n_1$, and another containing the
defeasible information rooted at $n_2$.  Constraints 1, 2 and 3 on
$\delta$ ensure that we have two rooted {\sc dags}.  Constraints 4 and
5 ensure that the defeasible information entails the indefeasible
information (as long as the root of the defeasible part isn't $\bot$,
in which case nothing consistent can be said about what normally holds
of the {\sc tdfs}).  Note in particular that constraint 5a ensures any
indefeasible reentrancy is also present in the defeasible {\sc dag}.
There are no constraints on the relation between a tail and the {\sc
dag}s in the {\em definition} of {\sc tdfs}s, but we will specify
below how tails are constructed, as part of the logic of default
unification.

\subsubsection{A detailed example}

(\ref{egtdfs}) is a {\sc tdfs}, which is indexed 1 (as shown by the
superscript on the root type).
\begin{examples}
\item   \label{egtdfs}
{\tiny
$
\begin{array}{c}
\avmplus{\att{t$^1$}\\
        \attval{F}{\avmplus{\attvaltyp{G}{a}}}\\
        \attvaltyp{H}{b}}
\end{array}
\left/
\begin{array}{c}
\avmplus{\att{t$^1$}\\
        \attval{F}{\avmplus{\attval{G}{\ind{2} \myvaluebold{a}}\\
                        \attval{H}{\ind{2}}}}\\
        \attvaltyp{H}{c}}
\end{array}
\right.
$}
$
\left/
\begin{array}{l}
\{\langle F \cdot H,\{\langle a,t\rangle\}\rangle,
\langle H,\{\langle c,t\rangle\}\rangle\}
\end{array}
\right.
$
\end{examples}

Or using the abbreviated AVM notation, we obtain (\ref{eg2tdfs}):
\begin{examples}
\item   \label{eg2tdfs}
{\tiny
$
\begin{array}{c}
\avmplus{\att{t$^1$}\\
        \attval{F}{\avmplus{\attval{G}{\myvaluebold{a}/\ind{2}}\\
                        \attval{/H}{\ind{2}}}}\\
        \attvaltyp{H}{b$/$c}}
\end{array}
$
}
\end{examples}

A tuple that describes this {\sc tdfs} is $\langle {\cal T}, 1, Q,
(n_1,n_5), \delta, \theta\rangle$, where:
\begin{enumerate}
\item ${\cal T} = \{\langle F\cdot H, \{\langle a,t\rangle\}\rangle,
\langle H,\{\langle c,t\rangle\}\rangle\}$
\item $Q= \{n_1,n_2,n_3,n_4,n_5,n_6,n_7,n_8\}$
\item $\delta(n_1,F)=n_2$, $\delta(n_2,G)=n_3$, $\delta(n_1,H)=n_4$,
$\delta(n_5,F)=n_6$, $\delta(n_6,G)=n_7$, $\delta(n_6,H)=n_7$,
$\delta(n_5,H)=n_8$
\item $\theta(n_1)=t$, $\theta(n_3) = a$,
$\theta(n_4) = b$, $\theta(n_5) = t$, 
$\theta(n_7)=a$, $\theta(n_8)=c$
\end{enumerate}

The two rooted {\sc dags} can be drawn pictorially as follows:
\begin{center}
\setlength{\unitlength}{0.92pt}
\begin{picture}(202,147)
\thinlines    \put(138,2){$n_7$}
              \put(189,74){$n_8$}
              \put(121,14){\begin{picture}(230,213)
                  \put(5,0){\begin{picture}(16,54)
\thinlines            \put(13,53){\line(-2,-5){11}}
                      \put(2,25){\vector(1,-2){12}}
                      \end{picture}}
\thinlines        \put(0,21){\hspace*{-0.05in}G}
                  \end{picture}}
              \put(142,16){\begin{picture}(227,210)
\thinlines        \put(20,20){H}
                  \put(0,0){\begin{picture}(17,53)
\thinlines            \put(15,25){\vector(-1,-2){12}}
                      \put(1,52){\line(1,-2){13}}
                      \end{picture}}
                  \end{picture}}
\thinlines    \put(138,73){$n_6$}
              \put(141,86){\begin{picture}(26,46)
\thinlines        \put(1,22){F}
                  \put(24,45){\vector(-1,-2){22}}
                  \end{picture}}
              \put(171,88){\begin{picture}(25,46)
\thinlines        \put(18,21){H}
                  \put(1,45){\vector(1,-2){22}}
                  \end{picture}}
\thinlines    \put(162,137){$n_5$}
              \put(54,75){$n_4$}
              \put(38,87){\begin{picture}(25,46)
\thinlines        \put(18,21){H}
                  \put(1,45){\vector(1,-2){22}}
                  \end{picture}}
              \put(0,35){\begin{picture}(11,39)
\thinlines        \put(0,17){G}
                  \put(9,39){\vector(0,-1){39}}
                  \end{picture}}
\thinlines    \put(3,23){$n_3$}
              \put(6,85){\begin{picture}(26,46)
\thinlines        \put(1,22){F}
                  \put(24,45){\vector(-1,-2){22}}
                  \end{picture}}
\thinlines    \put(3,77){$n_2$}
              \put(31,134){$n_1$}
\end{picture}

\end{center}
Note that for the {\sc tdfs} to be well defined, $c$ must be a subtype
of $b$.

This {\sc tdfs} could have been part of the initial {\sc kb}, since
the value-type pairs in the tails match exactly the strictly
defeasible information in the defeasible {\sc fs}.  If the tail were
totally unrelated to the information in the {\sc fs}s---for example,
it specified values on paths that don't appear in the {\sc fs}s---then
it is a well-defined {\sc tdfs}, but it would never be generated from
the initial {\sc kb} via the unification operation $\ddunify$ defined
below. We abbreviate the part of the tail for a path $\pi$, for a
{\sc tdfs} tagged 1, to $\pi^1$.  For example $F\cdot H^1=\{\langle
a,t\rangle\}$ in this example.

\subsection{An informal definition of $\ddunify$}
\label{informal}

We have assumed requirements for default unification which correspond
to those in Copestake (1993), adapted because we are assuming
persistent defaults with the addition of order independence and
specificity.  We want our definition of $\ddunify$ to meet the
following criteria:
\begin{enumerate}
\item Default information must always be consistent with non-default
information. 
\item Default unification behaves like monotonic unification in the cases
where there are no conflicts in the default
information.\footnote{As we will see in \S\ref{proofs}, the definition
of conflict is more complex because of tails.}
\item Default unification never fails when the non-default information is
consistent. 
\item Default unification returns a single result, deterministically.
\item Default values can be given a specificity ordering, such that
defaults associated with a more specific class take priority over
those associated with a more general class.
\item Default unification can be described using a binary, order
independent operation.
\end{enumerate}

The first five criteria can be understood to apply globally to a set
of {\sc tdfs}s which are to be unified.  In contrast, the last
criterion is necessary because we assume that we cannot, in general,
expect to have all this information available at once.  In principle,
this would be possible for a static inheritance hierarchy, although in
practice it would seriously constrain possible implementations and
would make the operation much less perspicuous than monotonic
unification.  Furthermore, defaults have utility in applications where
there is no definite point at which it is possible to decide that no
further relevant information will apply.

But the assumption of a binary operation is problematic since by the
very definition of nonmonotonicity, one cannot in general divide the
premises into groups, work out the inferences from those groups, and
expect the inferences to survive the whole. The only way to gain order
independence, therefore, is to ensure that each time the binary
operation is performed, it is influenced by the necessary pieces of
information that are `outside' the immediate context, of the {\sc fs}s
it is unifying.  Tails cover this necessary information by recording
sufficient information for us to define $\ddunify$ so that it has all
the desired properties.

We now informally describe the operation which we define logically
in section~\ref{logic-operation}.  We also prove
that this operation meets the above criteria in that section.

Let $F_1 = I_1/D_1/T^1$ be a {\sc tdfs}, and so $I_1$ is the indefeasible {\sc
  tfs}, $D_1$ the defeasible {\sc tfs} and $T^1$ the tail.  Similarly
for $F_2$.  Then $F_{12} =_{def} I_{12}/D_{12}/T^{12} =_{def}
F_1\ddunify F_2$ is calculated as follows:\footnote{Note that we
sometimes abbreviate the index $1\wedge 2$ to 12, when there's no confusion.}
\begin{enumerate}
\item   The Indefeasible Part:\\
$I_{12} = I_1 \unify I_2$.\\
That is, the indefeasible {\sc tfs} is the unification of the
indefeasible parts of the arguments.
\item   Default Reentrancies and Paths:\\
They all survive in $D_{12}$.  \\
We use $\approx$ to indicate reentrancy, and $\pi\approx_{D_1}\pi'$
means $\pi\approx\pi'$ is true in $D_1$.  So if $\pi\approx_{D_1}\pi'$
or $\pi\approx_{D_2}\pi'$, then $\pi\approx_{D_{12}}\pi'$.  If adding
all the reentrancies in $D_1$ and $D_2$ gives a cycle, then as in
normal unification, $D_{12}$ is $\bot$ and we're done.  
If not, then
note that paths also survive, 
because for any path $\pi$, $\pi\approx\pi$; the defeasible values are
then calculated according to step 4 below.
\item   Tails:\\
We calculate $T^{12}$ as follows:\\ For each path $\pi$
which has a value in $T^1$ or $T^2$, $\pi^{12}$ is the union of
$\pi'^1$ and $\pi'^2$, for all $\pi'$ that are reentrant with
$\pi$ in $D_{12}$.
\[
\pi^{12} = \{\pi'^1: \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}
\cup \{\pi'^2: \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}
\]
Note we already know which paths are reentrant
because we've done step 2.  Also note that
$\pi^{12}\subseteq\pi^1\cup\pi^2$, because $\pi\approx\pi$.
\item   Default Values:\\
These are calculated via the tail $T^{12}$, and each path $\pi$ is
considered separately.\\
For any path $\pi$ which has a value in $D_1$ or $D_2$,
the default value on $\pi$ in $D_{12}$ is the unification of the
following:
\begin{description}
\item[Indef] $\mbox{\em Indef}_{\pi}^{12}$ is the unification
of the indefeasible values in $I_{12}$ on all the
paths that are reentrant with $\pi$ in $D_{12}$

$\mbox{\em Indef}_{\pi}^{12} = \sqcap\{\phi_{\pi'}:
\modal{\pi'}=_{I_{12}} \phi_{\pi'} 
\wedge \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}$

Where $\modal{\pi'}=_{I_{12}}\phi_{\pi'}$ means that $I_{12}$ has a
$\pi'$
path, and the
value on this path is $\phi_{\pi'}$.
\item[Spec]  $\mbox{{\em Spec}}_{\pi}^{12}$ 
is the set of values in $\pi^{12}$ that are associated
with the maximally 
specific types, and are also compatible with $\mbox{\em Indef}_{\pi}^{12}$

$\mbox{{\em Spec}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall \langle\phi',t_{\phi'}\rangle\in
\pi^{12}, t_{\phi'}\not\sqsubset t_{\phi}
\mbox{ and } \phi\unify
\mbox{{\em Indef}}_{\pi}^{12}\neq \bot\}$
\item[Comp]   $\mbox{{\em Comp}}_{\pi}^{12}$ is the
set of values in $\pi^{12}$ that are individually
compatible with $\mbox{\em Indef}_{\pi}^{12}$ and each value of 
$\mbox{{\em Spec}}_{\pi}^{12}$

$\mbox{{\em Comp}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall v\in \mbox{{\em Spec}}_{\pi}^{12}, v\unify
\phi\neq \bot
\mbox{ and } \phi\unify \mbox{{\em Indef}}_{\pi}^{12}
\neq \bot\}$
\end{description}
\end{enumerate}
Some explanation of the steps 2, 3 and 4 are in order.  First, step 2
ensures all reentrancies and paths survive, regardless of the indefeasible and
defeasible values involved. 

It is possible to extend the logic so that
defeasible reentrancies can be overridden, but this comes at a cost in
computational complexity, as discussed in \S\ref{complexity}.
The
operation that extends $\ddunify$ in this way is defined in Lascarides
and Copestake (1995).  Second, step 3 merges tails so that the $\pi$
and $\pi'$ parts of the new tail are equal if $\pi'$ is reentrant with $\pi$.
We must construct new tails this way, so that the defeasible values as
defined in step 4 produce a well defined {\sc tdfs}.  If we did not add
$\pi'$ parts where $\pi'$ is reentrant with $\pi$ to the $\pi$-part of
the new tail, then step 4 would not guarantee that the defeasible
values on defeasibly reentrant paths were equal.

Finally, we explicate {\it Indef}, 
{\it Spec} and {\it Comp} in step 4.  First, {\it Indef}
ensures that the defeasible value on a path is at least as specific as
the indefeasible value on that path.  It's also at least as specific
as the values on the paths with which it's defeasibly reentrant.  This
is essential for the results of $\ddunify$ to be a well-defined {\sc
tdfs}.  Without this, the defeasible values are not guaranteed to be
both at least as specific as the indefeasible ones, and equal on
defeasibly reentrant paths.  Second, 
{\it Spec} and {\it Comp} use only the values
from the tails, and not the values in $D_1$ and $D_2$.  This feature
yields order independence; this is proved in
\S\ref{logic-operation}.  {\it Spec} ensures values associated with
most specific types survive, but only if they were compatible with the
indefeasible information.  If we did not ensure compatibility,
then indefeasible information would not override defeasible
information; rather we would get the value $\bot$ when they conflict.
The set {\it Comp} ensures that compatible
information on more general types also survives.  This is necessary for
both order independence, and ensuring that $\ddunify$ reduces to
$\unify$ when no conflicts arise.  Again, this is proved in
\S\ref{logic-operation}.  It also means that values that
originated from more general {\sc tdfs}s than those used to construct
{\it Spec}, which are incompatible with the values in 
{\it Spec}, do not survive.
This ensures that $\ddunify$ incorporates specificity.  The more
specific defaults will survive in {\it Spec}, and block the more general
conflicting defaults from being in {\it Comp}.

These steps can be carried out in the order specified, and each step
produces a deterministic result.  Nothing in step 2, for example, is
dependent on the results of step 4.  Furthermore, note that one can do
step 4 path by path in any order: the value calculated at one
node does not affect the value of another node.  The one exception is
when the reentrancies in $D_1$ and $D_2$ produce a cylce.  In this
case, the logic in section~\ref{logic-operation} 
yields the result that $D_{12}=\bot$.

It is possible to illustrate the persistent default
unification of any two {\sc tdfs}s using this informal definition.

{\bf Defeat of Defeasible Modus Ponens}

Where $t_2 \sqsubset t_1$ and $a\unify b = \bot$
\begin{center}
{\tiny
$\avmplus{\att{t$_1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a}}}}
$}
$
\left/
\{\}
\right.
\ddunify
$
{\tiny
$
\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}
$
}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$
$=$\\
{\tiny
$\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$
\end{center}

To show that the above holds, we work through each step of the
definition of $\ddunify$ in turn.  We concentrate on the
value on the $F\cdot G$ path; the root type of the two {\sc tdfs}s in the
result is calculated in a similar fashion.
\begin{enumerate}
\item   The indefeasible $F\cdot G$ value is $a\unify\top = a$.
\item   All defeasible paths and reentrancies survive (there are no
defeasible reentrancies).
\item   $F \cdot G^{12} = F\cdot G^1 \cup F \cdot G^2 
= \{\langle b, t_2\rangle\}$
\item   The defeasible $F\cdot G$ value is the unification of:
\begin{description}
\item[Indef]     $a$
\item[Spec]     $\{\}$ (because $b$ is incompatible with $a$).
\item[Comp]     $\{\}$.
\end{description}
which is $a$.
\end{enumerate}

{\bf Specificity}

The following example demonstrates the prioritisation of defaults.

Where $t_2\sqsubseteq t_1$ and $a\unify b =\bot$

\begin{center} 
{\tiny
$
\avmplus{\att{t$_1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$a}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle a,t_1\rangle\}\rangle\}
\end{array}
\right.
\ddunify
$
{\tiny
$\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$\\
$ = $
{\tiny
$\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{\attvaltyp{G}{$/$b}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle a,t_1\rangle,\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$
\end{center}
Again, we concentrate on just the $F\cdot G$ path.
\begin{enumerate}
\item   The indefeasible value on $F\cdot G$ is $\top \unify \top = \top$
\item   The defeasible reentrancies and paths survive.
\item   The $F\cdot G^{12}$ tail is $F\cdot G^{1}\cup F\cdot G^{2} = \{\langle
  a,t_1\rangle,\langle b,t_2\rangle\}$
\item   The defeasible value on the $F\cdot G$ tail is\\
the unification of:
\begin{description}
\item[Indef]     $\top$
\item[Spec]     $\{b\}$ (because $b$ is associated with a more specific
  type (namely $t_2$) than $a$ is (namely $t_1$), and $b$ is
  compatible with $\top$).
\item[Comp]     $\{b\}$ ($a$ is not compatible with $b$ and so $a$ is not
  in this set).
\end{description}
which is $b$.
\end{enumerate}

{\bf The Nixon Diamond}

We now show what happens where there is no prioritisation between
conflicting defaults.

Where $a\unify b =\bot$

\begin{center}
{\tiny
$
\avmplus{\att{t$_1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$a}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle a,t_1\rangle\}\rangle\}
\end{array}
\right.
\ddunify
$
{\tiny
$
\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}
$
}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$\\
$ = $
{\tiny
$
\avmplus{\att{t$_2$}\\
        \attval{F}{\avmplus{\attvaltyp{G}{$/${\boldmath $\bot$}}}}}
$}
$
\left/
\begin{array}{l}
\{\langle F\cdot G,\{\langle a,t_1\rangle,\langle b,t_2\rangle\}\rangle\}
\end{array}
\right.
$
\end{center}

Again, we concentrate just on the results on the $F\cdot G$ path.
\begin{enumerate}
\item   The indefeasible value on $F\cdot G$ is $\top \unify \top = \top$
\item   The defeasible paths and reentrancies all survive.
\item   The $F\cdot G^{12}$ tail is $F\cdot G^{1}\cup F\cdot G^{2} = \{\langle
  a,t_1\rangle,\langle b,t_2\rangle\}$
\item   The defeasible value on the $F\cdot G$ tail is\\
the unification of:
\begin{description}
\item[Indef]     $\top$
\item[Spec]     $\{a, b\}$ \\(since both are as specific as possible)
\item[Comp]     $\{\}$ \\($a$ is incompatible with $b$ and $b$ with $a$)
\end{description}
which is $\bot$.
\end{enumerate}

The value on the default node is $\bot$, indicating that nothing
coherent can be said about the default information.  This value could
be overridden by a subsequent default unification, however, by a default
$F\cdot G$ value that was associated with a more specific type than both
$t_1$ and $t_2$.

{\bf Reentrancy}

Since reentrancy always survives, we also get $\bot$ to be the default
value when the indefeasible values on defeasibly reentrant paths are
incompatible.

Where $a\unify b = \bot$
\begin{center}
{\tiny
$\avmplus{\att{t}\\
        \attvaltyp{F}{a}\\
        \attvaltyp{G}{b}}
$}
$
\ddunify
$
{\tiny
$
\avmplus{\att{t}\\
        \attval{F}{/\ind{1}}\\
        \attval{G}{/\ind{1}}}
$}
$=$
{\tiny
$
\avmplus{\att{t}\\
        \attval{F}{\myvaluebold{a}/\ind{1}\mbox{\small\boldmath$\bot$}}\\
        \attval{G}{\myvaluebold{b}/\ind{1}}}
$}
\end{center}

We calculate the values on just the $F$ path here; the one for $G$ is
similar.  
\begin{enumerate}
\item   The indefeasible value on $F$ is $a$.
\item   All default reentrancies survive; so $F\approx G$ survives.
\item   The $F^{12}$ tail is
$F^{1}\cup F^{2}\cup G^{1} \cup G^{2} = \emptyset$
\item   The default value on the $F$ path is\\
the unification of:
\begin{description}
\item[Indef]     The indefeasible value on $F$ {\em and} $G$\\
$a \unify b= \bot$\\
(must do this for {\sc tfs}s to be well defined).
\item[Spec]     $\{\}$
\item[Comp]     $\{\}$
\end{description}
which is $\bot$.
\end{enumerate}

This examples clarifies the motivation for defining {\it Indef} in the way we
do.  If we did not unify the indefeasible values on the paths that are
defeasibly reentrant with $F$, then we would not obtain a well-defined
{\sc tdfs} via the operation: either the defeasible values on
the $F$ and $G$ paths would be different in spite of the defeasible
reentrancy, or the defeasible value on $F$ would not be at least as
specific as the indefeasible value.  Since defeasible reentrancies
always survive, and indefeasible values can only get more specific
with subsequent unifications, the value $\bot$ in this case could not
be overridden in subsequent unifications, in contrast to the
Nixon Diamond case above.

As a further example, we consider the inheritance hierarchy shown 
in Figure~\ref{final-eg}.  We do not need to make any stipulation of
top-down versus bottom-up inheritance order to be able to calculate the
inherited constraint specification using this definition of default
unification.  The constraint on {\bf pst-t-vb}, for example, is
determined by default unification with the constraints on its
supertypes.  
\begin{center}
$\mbox{{\bf pst-t-vb}}\sqsubset \mbox{{\bf verb}}$

1) 
{\tiny
$
\avmplus{\att{verb}\\
        \attval{PST}{/\ind{1}\myvaluebold{+ed}}\\
        \attval{PSP}{/\ind{1}}}
$}
\hspace*{0.5in}
2)
{\tiny
$
\avmplus{\att{pst-t-vb}\\
        \attvaltyp{PST}{$/$+t}\\
        \attvaltyp{PSP}{\boldmath $\top$}}
$
}\\
$1 \ddunify 2 = 2\ddunify 1 =$
{\tiny
$\avmplus{\att{pst-t-vb}\\
        \attval{PST}{/\ind{1}\myvaluebold{+t}}\\
        \attval{PSP}{/\ind{1}}}
$}
$
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +t}, \mbox{\bf pst-t-verb}\rangle, 
\langle \mbox{\bf +ed}, \mbox{\bf verb}\rangle \}\rangle, \\
\langle \mbox{PSP},\{\langle \mbox{\bf +t},\mbox{\bf pst-t-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle\}
\end{array}
\right.
$
\end{center}
Inheritance hierarchies
are discussed in more detail in \S\ref{incorp}.

So far we've shown how the definition works.  We now informally demonstrate
why tails are required for order independence.  We do
this via two more examples.

\subsubsection{Keeping track of specificity}

Consider another version of the hierarchy given in Figure~\ref{final-eg}, 
such that we
have the constraint specifications shown in (\ref{blahblah}).
\begin{examples}
\item   \label{blahblah}
$\mbox{{\bf psp-diff-vb}}\sqsubset \mbox{{\bf stg-vb}}\sqsubset \mbox{{\bf verb}}$

1) 
{\tiny
$
\avmplus{\att{verb}\\
        \attvaltyp{PST}{$/$+ed}\\
        \attvaltyp{PSP}{$/$+ed}}
$}
2)
{\tiny
$
\avmplus{\att{stg-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{$/$+o}}
$}
3)
{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{\boldmath $\top$}\\
        \attvaltyp{PSP}{+en}}
$}
\end{examples}
Here, {\bf verb} is specified to necessarily have two attributes {\sc psp}
and {\sc pst} both with default values {\bf +ed}, {\bf stg-vb} 
has {\bf +o} for both attributes, and {\bf psp-diff-vb} has {\bf +en} for
{\sc psp}.  
We will assume that the latter specification is indefeasible,
although making it defeasible would not affect the order dependence of
the result discussed below.
We can also assume that the user has made no stipulation about
{\sc pst} for {\bf psp-diff-vb} 
but that the constraint specification is well-typed, 
so that its value for {\sc pst} is $\top$, although the
results would be the same if we simply assumed {\sc pst} was absent.

Suppose that, instead of having tails, we defined specificity to be driven
by the root type of the current feature structure.  This is a reasonable
idea, since types persist in the {\sc fs} (in contrast with template names in
{\sc patr-ii} and similar systems).
Unfortunately it would result in order dependence, as shown in 
Figure~\ref{od}. 
\begin{figure}
\[
\begin{array}{l l}
1 \ddunify 2 = &
\mbox{\tiny
$
\avmplus{\att{stg-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{$/$+o}}
$}
\\
(1 \ddunify 2) \ddunify 3 = &
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{+en}}
$}
\\
1 \ddunify 3 = & 
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+ed}\\
        \attvaltyp{PSP}{+en}}
$}
\\
(1 \ddunify 3)\ddunify 2 = &
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+ed}\\
        \attvaltyp{PSP}{+en}}
$}
\end{array}
\]
\caption{Order Dependence if Specificity is Driven by the Root Type}
\label{od}
\end{figure}
This occurs because a constraint
which invokes a general value on a path is promoted in specificity:
namely, the information that {\sc pst} $=$ {\bf +ed} 
is promoted in specificity when unifying 1 and 3.  It starts as a
default on a {\sc fs} of type {\bf verb}, and becomes a default
on a {\sc fs} of type {\bf psp-diff-verb}, with nothing to
distinguish it from the value of {\sc psp} which was actually stipulated.
Intuitively, one needs to record for each
path in each {\sc tdfs}, the specificity of the {\sc tdfs} from which
that path's value {\em originated}.  And it must be the
{\em original} specificity that determines which defaults survive
during unification.   
Our use of
tails to record the original specificity achieves this, as shown in
Figure~\ref{right}.
\begin{figure}
\[
\begin{array}{l l}
1 \ddunify 2 = &
\mbox{\tiny
$
\avmplus{\att{stg-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{$/$+o}}
$}
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +o}, \mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle, \\
\langle \mbox{PSP},\{\langle \mbox{\bf +o},\mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle\}
\end{array}
\right.
\\
(1 \ddunify 2) \ddunify 3 = &
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{+en}}
$}
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +o}, \mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle, \\
\langle \mbox{PSP},\{\langle \mbox{\bf +o},\mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle\}
\end{array}
\right.
\\
1 \ddunify 3 = & 
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+ed}\\
        \attvaltyp{PSP}{+en}}
$}
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle, 
\langle \mbox{PSP},\{\langle \mbox{\bf +ed}\mbox{\bf ,verb}\rangle \}\rangle\}
\end{array}
\right.
\\
(1 \ddunify 3)\ddunify 2 = &
\mbox{\tiny
$
\avmplus{\att{psp-diff-vb}\\
        \attvaltyp{PST}{$/$+o}\\
        \attvaltyp{PSP}{+en}}
$}
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +o}, \mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle, \\
\langle \mbox{PSP},\{\langle \mbox{\bf +o},\mbox{\bf stg-vb}\rangle, 
\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle \}\rangle\}
\end{array}
\right.
\end{array}
\]
\caption{Order Independence Through Tails}
\label{right}
\end{figure}

\subsubsection{Keeping track of specificity and values}

For many examples, including that just shown, we do not need such complex tails.
In \S\ref{index}, we
describe a sublanguage for which the information that must
be retained to give order independence is just the original specificity for a
given path.  We could do this by associating an index with each path, 
represented below as an integer superscript, and
having a specificity order on indices, which mirrored the specificity order
on the original root types.
But tails are doing more than this,
since they are also recording the original values, and the next example
illustrates why this is necessary for the full language. 

\begin{center}
$t_3 \sqsubset t_1\sqsubset t_2$ \hfill
$3 \sqsubset 1 \sqsubset 2$ \hfill
$a\sqsubset b$ \hfill
$d \unify b = c$ \hfill
$d \unify a = \bot$\\
(1)
{\tiny
$
\avmplus{\att{t$_1^1$}\\
         \attvaltyp{F}{$/$a$^1$}}$
}
\hfill
(2)
{\tiny
$\avmplus{\att{t$_2^2$}\\
         \attvaltyp{F}{$/$b$^2$}}$
}
\hfill
(3)
{\tiny
$\avmplus{\att{t$_3^3$}\\
        \attvaltyp{F}{$/$d$^3$}}$}
\end{center}

We want $\ddunify$ to reduce
to typed unification when there's no conflict between the {\sc fs}s to
be unified.  So $1\ddunify 2$ must be as follows:
\[
1 \ddunify 2 = \mbox{\tiny $\avmplus{\att{t$_1^1$}\\
                        \attvaltyp{F}{$/$a$^1$}}$}
\]

And $(1\ddunify 2)\ddunify 3$ is determined by the fact that indices
must determine which default survives when there is conflict:
\[
(1\ddunify 2)\ddunify 3 = \mbox{\tiny $\avmplus{\att{t$_3^3$}\\
                                \attvaltyp{F}{$/$d$^{3}$}}$}
\]
Similarly, $2\ddunify 3$ must be as below, if $\ddunify$ reduces to
monotonic typed unification when there's no conflict:
\[
2 \ddunify 3 = \mbox{\tiny $\avmplus{\att{t$_3^3$}\\
                        \attvaltyp{F}{$/$c$^{3}$}}$}
\]
And so $(2\ddunify 3)\ddunify 1$ is again determined by the
specificity of the indices, since there is conflict:
\[
(2 \ddunify 3)\ddunify 1 = \mbox{\tiny $\avmplus{\att{t$_3^3$}\\
                                        \attvaltyp{F}{$/$c$^{3}$}}$}
\]
This is different from $(1\ddunify 2)\ddunify 3$.

The problem is that sometimes the specificity of
the default path determines the result in unification:
specifically, when two defaults conflict, and one originated from a
more specific {\sc tdfs} than the other.  On the other hand, because
we want default unification to reduce to monotonic typed unification when
there is no conflict, the values on the paths can also sometimes
determine the results of persistent default unification: specifically,
when there's no conflict.  The above example shows that these two
factors don't work independently, and therefore unless the dependence
between them is recorded in some way, order dependence will result.

This example demonstrates that the indices don't record enough
information from the unification history.  We must also keep track of
values that have been `overridden', because they must sometimes
influence the result of subsequent unifications.  This is achieved by
tails, as shown briefly below, and in more detail in
\S\ref{examples}.  According to the above definition of $\ddunify$,
the results are as follows:
\[
1 \ddunify 2 =  \mbox{\tiny $\avmplus{\att{t$_1$}\\
                        \attvaltyp{F}{$/$a}}$}
\left/ \{\langle F,\{\langle a,t_1\rangle,\langle b,t_2\rangle\} \rangle\}\right.
\]

\[
(1\ddunify 2)\ddunify 3 =  \mbox{\tiny $\avmplus{\att{t$_3$}\\
                                \attvaltyp{F}{$/$c}}$}
\left/ \{\langle F, \{\langle a,t_1\rangle,\langle
b,t_2\rangle,\langle d,t_3\rangle\} \rangle\}\right.
\]

\[
2 \ddunify 3 =  \mbox{\tiny $\avmplus{\att{t$_3$}\\
                        \attvaltyp{F}{$/$c}}$}
\left/ \{\langle F,\{\langle b,t_2\rangle,\langle
d,t_3\rangle\}\rangle \} \right.
\]
\[
(2 \ddunify 3)\ddunify 1 =  \mbox{\tiny $\avmplus{\att{t$_3$}\\
                                        \attvaltyp{F}{$/$c}}$}
\left/ \{\langle F, \{\langle b,t_2\rangle,\langle d,t_3\rangle, 
\langle a,t_1\rangle\} \rangle\}\right.
\]

In this informal presentation of persistent default unification, we
have not proved properties such as order independence. This is done in
\S\ref{logic-operation}. There are two limitations to the operation
as we have defined it. Firstly, specificity is determined by an
inheritance hierarchy which allows only {\em strict} inheritance links
between the types rather than defeasible ones.  We leave open how we
could extend the prioritisation of defaults to cases where the
priorities themselves were default statements.  Secondly,
although any node in the {\sc fs} may be typed, 
the operation does not take account of any indefeasible type 
constraints which may apply and thus the result may not be well-formed.  
We discuss this issue in detail in \S\ref{wellf}, and
Lascarides and Copestake (1995) extend the operation defined here, to
overcome this limitation.
% Alex - We do?  
% Ann---yes, well sort of.  If well-formedness is handled by typed
% unification, then since YADU is defined in terms of typed
% unification, any treatment of well-formedness from typed unification
% will work for YADU as well.  

\section{Exploiting Persistent Default Unification}

In this section, we briefly cover a number of topics concerning the
implementation of persistent associative default unification and its
integration in a representation language.  We first describe an
algorithm for computing $\ddunify$ 
and show that it is of polynomial complexity, then discuss
inheritance hierarchies and how {\sc tdfs}s can be converted into {\sc
tfs}s.  At this point, we can compare persistent default unification
to asymmetric default unification and show the latter corresponds to a
special case of persistent default unification combined with the
conversion of persistent default to non-default {\sc fs}s.  Finally,
we make some remarks on well-formedness with respect to a type system.

\subsection{Implementation and complexity}
\label{complexity}

The algorithm for computing the results of persistent default
unification ($\ddunify$) can be described in terms of the informal
definition given in \S\ref{informal}.  It involves the following
steps:
\begin{enumerate}
\item Construct an indefeasible {\sc fs} by monotonic unification.
\item Construct a {\sc fs} for the defeasible reentrancy by monotonic
unification of the reentrancy information in the defeasible parts of
the input {\sc fs}s.
\item Merge the tails.
\item Calculate the defeasible {\sc fs} values.
\end{enumerate}
By examining the informal definition of $\ddunify$ (and the conditions
on the logical axioms in \S\ref{logic-operation}) it is obvious that
these steps can be carried out in this order because no step depends
on the results of any later one.  The first two steps have the same
order of complexity as monotonic unification which is near linear in
the number of nodes in the input {\sc fs}s (e.g.  Carpenter,
1992).\footnote{Assuming types on nodes, requires an extra step in the
algorithm over the untyped case to find the greatest common subtype,
but since we are assuming that this is unique, this just adds a lookup
overhead which will depend on the number of types.  For the moment we
ignore the extra complexity which arises for well-typed unification,
see \S\ref{wellf}, below.}

The third step, the calculation of tails for each path $\pi$, involves
constructing the union of the value/specificity pairs for each tail 
for each path $\pi'$ which is equivalent to $\pi$ due to reentrancy.  
\[
\pi^{12} = \{\pi'^1: \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}
\cup \{\pi'^2: \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}
\]
At first sight it appears that the resulting tail could contain more
value/specificity pairs than were in the originals.  However,
information about reentrant paths can be amalgamated, because tails
for reentrant paths will be equivalent and reentrancy accumulates
monotonically in the default {\sc fs}.  In fact, we can modify the
notation, so that the first member of each element in a tail is a set
of reentrant paths rather than a single path, for example, instead of
(\ref{tail1}) we can write (\ref{tail2}) if $F$, $G$ and $H$ are reentrant:
\begin{examples}
\item   \label{tail1}
$\begin{array}{l}
\{\langle F,\{\langle a,t\rangle\, \langle c,t\rangle\}\rangle,
\langle G,\{\langle a,t\rangle, \langle c,t\rangle\}\rangle
\langle H, \{\langle a,t\rangle, \langle c,t\rangle\}\rangle\}
\end{array}$
\item \label{tail2}
$\begin{array}{l}
\{\langle \{F, G, H\} ,\{\langle a,t\rangle\, \langle c,t\rangle\}\rangle
\end{array}$
\end{examples}
In this case, the maximum number of tail elements (i.e.~path
set/value set pairs) is equal to the number of nodes in the default
result {\sc fs}.  Merging tails involves using set union to construct
each such element, where the maximal number of value/specificity pairs
in each value set will be the number of {\sc tdfs}s in the original
{\sc kb} which are being unified.  In practice, tails will normally be
much smaller than this implies, because we only keep track of default
values which are more specific than the non-default values in the
original {\sc kb}.  Furthermore, although for simplicity we described
tails so that they can contain values which are
inconsistent with the non-default values in the {\sc tdfs},  such
values never have an impact on the unification by the definitions of
{\em Spec} and {\em Comp}.  So in practice, they could be removed from
the tail.

The final step is the calculation of the default {\sc fs} values.
For convenience,
we repeat the earlier definition of the three values to be unified:
\begin{description}
\item[Indef] The indefeasible value:\\
$\mbox{\em Indef}_{\pi}^{12}$ is the unification
of the indefeasible values in $I_{12}$ on all the
paths that are reentrant with $\pi$ in $D_{12}$

$\mbox{\em Indef}_{\pi}^{12} = \sqcap\{\phi_{\pi'}:
\modal{\pi'}=_{I_{12}} \phi_{\pi'} 
\wedge \modal{\pi}\approx_{D_{12}}\modal{\pi'}\}$
\item[Spec] The most specific default values:\\
$\mbox{{\em Spec}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall \langle\phi',t_{\phi'}\rangle\in
\pi^{12}, t_{\phi'}\not\sqsubset t_{\phi}
\mbox{ and } \phi\unify
\mbox{{\em Indef}}_{\pi}^{12}\neq \bot\}$
\item[Comp] The compatible default values:\\
$\mbox{{\em Comp}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall v\in \mbox{{\em Spec}}_{\pi}^{12}, v\unify
\phi\neq \bot
\mbox{ and } \phi\unify \mbox{{\em Indef}}_{\pi}^{12}
\neq \bot\}$
\end{description}
Note that the defeasible value of a path can be determined without
reference to the defeasible values on other nodes or to previous
defeasible values on any node: the result is just dependent on the
indefeasible structure, the reentrancy and the tail. 
Thus the
result can be calculated individually for each node and subsequent
calculations of defeasible values on different paths will not alter
the result. 
The worst case complexity is where there is maximal
reentrancy, since this gives the longest 
tails.\footnote{If we allow reentrancy to be overridden by default
values, as in Lascarides and Copestake (1995), interactions can occur
between nodes, and the algorithm to 
compute this version of default unification has 
exponential complexity in the worst case.  See also
\S\ref{wellf}, below, for discussion of imposing
well-formedness conditions, in which nodes could interact.}

We will derive the complexity for a node in a default {\sc fs} with
$p$ paths leading to it, after $k$ {\sc fs}s from the original {\sc kb}
have been considered, which gives a maximum tail length of $t = kp$:
\begin{enumerate}
\item {\it Spec}
is the set of the maximally specific values in the tails, excluding those
which are incompatible with the non-default {\sc fs}.
Constructing this set involves 
$O(t^2)$ comparisons for specificity
and $t$ type unification checks with the non-default values in (a).
\item 
{\it Comp} 
is the set of all values in the tails which unify with every member of
{\it Spec} and with the non-default value.  
This involves $O(t^{2})$ type checks.
\item The final step is to unify together all the members of (b) and (c)
with the non-default values.  This is $O(t)$ in the number of 
type unifications.
\end{enumerate}
Thus, if we have $n$ nodes in the resulting {\sc fs}, the overall
complexity of the calculation of the default
values is $O(nt^{2})$.  So, although 
the complexity of $\ddunify$ is worse than that of monotonic
typed unification, none of the steps for each node in the result
involves complexity worse than $O(t^{2})$ in the length of the tails,
and these will normally be short.

It is worth noting that it is not actually necessary to calculate
default {\sc fs} values at each step if we know we are applying a
sequence of $\ddunify$ operations: the intermediate results are
irrelevant, since the values on the
default {\sc fs} can be calculated by looking at the indefeasible {\sc fs},
the default reentrancy and paths and the tails.  (This is formally proved by
Lemma~1 in \S\ref{proofs}.)
So, for each step apart from
the last one within a sequence of $\ddunify$ operations, the only
essential overhead compared with monotonic typed unification is
calculation of the default reentrancy and merging the tails.

\subsection{Inheritance hierarchies}
\label{incorp}

In inheritance hierarchies such as that shown in
Figure~\ref{final-eg}, $\ddunify$ can be used to implement inheritance
in a straightforward way.  A type $t$ will have a constraint $C(t)$
which is calculated by persistent default unifying its constraint
specification with those of its supertypes.  Because of order
independence, this is equivalent to defining the constraint to be the
persistent default unification of the constraint specification with
the constraints of the immediate supertypes.  For example,
\begin{examples}
\item
$\begin{array}{ll}
C(\mbox{\bf pst-t-vb}) & =  C(\mbox{\bf verb}) \ddunify 
\mbox{\tiny 
$\avmplus{\att{pst-t-vb}\\
                  \attvaltyp{PST}{$/$+t}}$} \\
& = \mbox{\tiny $\avmplus{\att{pst-t-vb}\\
                  \attval{PST}{/\ind{1}\myvaluebold{+t}}\\
                  \attval{PSP}{/\ind{1}}}$} 
\left/
\begin{array}{l}
\{\langle \mbox{PST},\{\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle, 
\langle \mbox{\bf +t},\mbox{\bf pst-t-verb}\rangle\}\rangle,\\
\langle \mbox{PSP},\{\langle \mbox{\bf +ed},\mbox{\bf verb}\rangle,
\langle \mbox{\bf +t},\mbox{\bf pst-t-verb}\rangle\}\rangle\}
\end{array}
\right.
\end{array}$
\end{examples}

For type hierarchies, we follow the convention that the type of a
constraint specification {\sc fs} is the type being defined and
therefore the correct specificity order is built into the operation
automatically.  But if we were defining inheritance of classes in an
untyped framework, all that would be necessary would be to define
tails so that instead of types defining the specificity of values we
used a tag which reflected the partial order of classes in the
inheritance hierarchy.  Nothing in our definition of $\ddunify$ apart
from this initial instantiation depends on specificity being
determined by a type hierarchy.  Multiple inheritance in either case
needs no special stipulations, although clearly if a type or class has
two or more immediate parents these will not be ordered with respect
to one another and therefore any conflicts in the default parts of
their constraints will lead to nodes with value $\bot$.

Most previous work on default unification has assumed that defaults do
not persist outside the lexicon, and that 
syntactic and semantic specification can be couched
entirely in terms of monotonic constraints as is done in current HPSG,
for example.
Within our current framework this would mean we have to `convert'
persistent defaults which have survived a series of default
unifications into indefeasible specifications. 
For example, the
morphological specifications in Figure~\ref{final-eg} must not remain
default at the point when the resulting {\sc fs}s are utilised in
parsing, otherwise a {\it +ing} phonological form may unify with an
{\sc fs} default specifying a {\it +ed} suffix. In many cases of
lexical inheritance, default inheritance is for convenience of
description, and the ultimate objects of the description are intended
to be monotonic {\sc tfs}s.  For {\bf pst-t-verb}, for example, we
want to be able to derive the {\sc tfs}:
\begin{center}
{\tiny $\avmplus{\att{pst-t-vb}\\
                  \attval{PST}{\ind{1}\myvaluebold{+t}}\\
                  \attval{PSP}{\ind{1}}}$}
\end{center} 
We therefore need to define an operation which combines the
defeasible information with the indefeasible structure,
which we can apply when we know that all
necessary default unification operations have been carried out, for
example at the interface between the lexicon and the
syntagmatic component. This
operation, however, is not an integral part of the definition of
persistent default unification, since it is only relevant to its use
where defaults are used to describe objects which are treated as
ordinary {\sc tfs}s with respect to some other level of processing.
In fact, in \S\ref{applications}, we will assume that some 
classes of defaults
persist beyond the lexicon, 
while others are encapsulated within it.  (Even for the latter class,
persistence within the lexicon is important, because it allows
defaults to be accumulated incrementally, without the sensitivity to
textual order in descriptions found in most previous uses of 
lexical defaults.)
For expository convenience
we will describe the operation as converting the entire {\sc tdfs}
into a standard {\sc tfs}, but this easily generalises to the case
where only part of the default {\sc fs} is made indefeasible.

It
should be clear from \S2 that any operation which makes default
information non-default cannot be applied within a series of default
unifications without the result being order dependent, so it only
makes sense to apply the conversion after all applications of
$\ddunify$ within a given `module', such as the lexicon.  We refer to
the conversion operation as DefFill, because it fills in the
non-default structure from the default information and is thus roughly
analogous to the Fill operation which is applied to make a {\sc tfs}
well-formed with respect to a type hierarchy (cf Carpenter, 1992). We
first give a definition of DefFill, and then explain why it takes this
form.

We define $\mbox{{\em DefFill}}(F)$, the result of converting a {\sc
tdfs} $F$ into a {\sc tfs}, as the result of unifying the non-default
part of the {\sc tdfs} with a {\sc fs} derived from the default part,
by ignoring all nodes which are typed $\bot$, all nodes which have
features and atomic types and all $\delta$-descendants of these nodes.
With respect to reentrancy, we only incorporate it into the
non-default if there is no inconsistent node either before or after
the reentrant node being considered.
\begin{defn}
Let $F=_{def} I/D/T$.  Then
$\mbox{{\em DefFill}}(F)$ is the most general {\sc tfs} which satisfies the following:
\begin{enumerate}
\item $\mbox{{\em DefFill}}(F) \sqsubseteq I$ 
i.e. it is subsumed by the indefeasible 
part of $F$
%
\item  If $m_1$  the root node of $\mbox{{\em DefFill}}(F)$ and
$n_2$ is the root node of $D$ then for all {\rm consistent} paths $\pi$
$\theta(\delta(\pi, m_1)) = \theta(\delta(\pi, n_2))$
%
\item For all consistent paths $\pi$ and $\pi'$ such that
$\delta(\pi, n_2) = \delta(\pi', n_2)$ then, if all paths $\pi \cdot \pi''$ are
consistent,
$\delta(\pi, m_1) = \delta(\pi', m_1)$
\end{enumerate}
Where we define a path $\pi$ to be {\rm consistent} if there 
are no (possibly empty) paths $\pi'$ and 
$\pi''$ such that $\pi' \cdot \pi'' = \pi$ and 
either 
\begin{itemize}
\item $\theta(\delta(\pi',n_2)) = \bot$ 
\item $\theta(\delta(\pi',n_2)) = a$ where $a$ is defined to be an atomic type
and $\delta(f, \delta(\pi',n_2))$ is defined for any feature $f$
\end{itemize}
\end{defn}

Because of the condition that all values on the nodes in the default
{\sc fs} must be consistent with those in the non-default {\sc fs},
the {\sc tdfs} to {\sc tfs} conversion operation essentially involves
adding in the default values to the indefeasible part of the {\sc
tdfs} ignoring nodes typed with $\bot$ and all their
$\delta$-descendants (because $\bot$ implies everything, and therefore
we cannot assume anything about nodes which follow $\bot$). However,
the definition above reflects two complications, the first concerning
reentrancy, and the second a (very weak) notion of well-formedness.

The problem with reentrancy is that it is retained in the default {\sc
fs} even if there is a clash of indefeasible values, and therefore we
cannot guarantee that reentrancy is compatible with the non-default
structure if there is any node typed $\bot$ which is a
$\delta$-descendant of the reentrant node.  For example, consider
Figure~\ref{reentprob}.
\begin{figure}
\begin{center}
$a\unify b = \bot$\\
$\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{a}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{b}}}}
$}
\end{array}
\ddunify
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{/\ind{1}}\\
        \attval{G}{/\ind{1}}}$}
\end{array}
=
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{a}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{b}}}}$}
\end{array}
\left/
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\ind{1} \avmplus{\attvaltyp{H}{\boldmath $\bot$}}}\\
        \attval{G}{\ind{1}}}$}
\end{array}
\right.
$
\end{center}
\caption{Reentrancy Causing Value Conflict}
\label{reentprob}
\end{figure}
We need to discard the reentrancy from the default {\sc fs} when
constructing the {\sc tfs}, and for this particular case we can
therefore add nothing to the non-default structure.  Unfortunately, we
cannot distinguish between cases such as this where the reentrancy is
incompatible because of the indefeasible values and those where
reentrancy is compatible with the indefeasible structure, but there
has been a clash of default values which is unrelated to the
reentrancy.  An example of this is shown in Figure~\ref{reentprob2}.
\begin{figure}
\begin{center}
$a\unify b = \bot$\\
$
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{c$/$a}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{d}\\
                            \attvaltyp{I}{e}}}}$}
\end{array}
%\left/
%\{\langle F\cdot H,\{\langle, a,t\rangle\}\rangle\}
%\right.
\ddunify
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{\boldmath $\top$}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{\boldmath $\top$}}}}$}
\end{array}
\left/
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\ind{1} \avmplus{\attvaltyp{H}{b}}}\\
        \attval{G}{\ind{1}}}$}
\end{array}
\right.
%\left/
%\{\langle F\cdot H,\{\langle, b,t\rangle\}\rangle\}
%\right.\\
=$\\ \hfill
$\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{c}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{d}\\
                            \attvaltyp{I}{e}}}}$}
\end{array}
\left/
\begin{array}{c}
\mbox{\tiny
$\avmplus{\att{t}\\
        \attval{F}{\ind{1} \avmplus{\attvaltyp{H}{\boldmath $\bot$}\\
                                    \attvaltyp{I}{e}}}\\
        \attval{G}{\ind{1}}}$}
\end{array}
\right.
\left/
\begin{array}{l}
\{\langle F\cdot H,\{\langle b,t\rangle,\langle a,t\rangle\}\rangle,\\
\langle G\cdot H,\{\langle b,t\rangle,\langle a,t\rangle\}\rangle\}
\end{array}
\right.
$
\end{center}
\caption{Values Conflicting Independently of Reentrancy}
\label{reentprob2}
\end{figure}
The distinction between $\bot$ caused by conflict in indefeasible
values and conflict in defeasible values (in this case on the same
path), cannot be deduced simply by looking at the tail since a
conflict between the indefeasible values $c$ and $d$ might also have
been present.

We have adopted the approach of ignoring default reentrancy on a node
which is typed $\bot$ or has $\bot$ as a successor, even though this
implies that information which could have been incorporated from the
default is neglected in some cases.  The only other option would be
for the \mbox{{\em DefFill}} operation to itself carry out a check for
compatibility with the non-default.  We currently think this is less
attractive, both theoretically, because this is making \mbox{{\em
DefFill}} do work which should properly be part of the logic of
persistent default unification, and practically, because it would need
to check all possible combinations of default reentrancy with the
non-default {\sc fs}, an operation which is potentially of exponential
complexity.  The result of converting the {\sc tdfs} in
Figure~\ref{reentprob2} to a {\sc tfs} is shown in
Figure~\ref{reentprob3} (this will be obtained irrespective of the
compatibility of $c$ and $d$).
\begin{figure}
\begin{center}
{\tiny
$
\begin{array}{c}
\avmplus{\att{t}\\
        \attval{F}{\avmplus{\attvaltyp{H}{c}\\
                            \attval{I}{\ind{1}\ \myvaluebold{e}}}}\\
        \attval{G}{\avmplus{\attvaltyp{H}{d}\\
                            \attval{I}{\ind{1}}}}} 
\end{array}
$
}
\end{center}
\caption{Loss of Reentrancy when Nodes are typed $\bot$}
\label{reentprob3}
\end{figure}
The reentrancy between paths F$\cdot$ I and G$\cdot$I is retained
because the corresponding node in the default {\sc fs} had no
$\delta$-descendants marked with $\bot$, but the reentrancy between F
and G and between F$\cdot$H and G$\cdot$H is lost because
F$\cdot$H/G$\cdot$H was marked $\bot$.

The well-formedness problem is that $\ddunify$ will not in general
yield a {\sc tdfs} with a default component
which is well-formed, even ignoring $\bot$
nodes.  The result of $\ddunify$ does not necessarily conform to even
the weakest notion of well-formedness: that there are some atomic
types for which no features are appropriate.  (We will discuss
stronger notions of well-formedness with respect to a type system in
\S\ref{wellf}.)  Thus, as things stand, our system is too weak to be
able to define an analogue of untyped {\sc fs} systems, where nodes
which have (atomic) values cannot also have features.  For example, if
$t \sqsubset t'$, then
\[ \mbox{\tiny $\avmplus{\att{t}\\
                  \attvaltyp{F}{$/$a}}$} 
\ddunify
\mbox{\tiny $\avmplus{\att{t$'$}\\
                  \attval{F}{/\avmplus{\attvaltyp{G}{\boldmath $\top$}}}}$}
=
\mbox{\tiny $\avmplus{\att{t}\\
                  \attval{F}{/\avmplus{\att{a}\\
                              \attvaltyp{G}{\boldmath $\top$}}}}$}
\]
even though for some types $a$ 
we want to be able to exclude as not well formed {\sc fs}s such as:
\[ 
\mbox{\tiny $\avmplus{\att{t}\\
                  \attval{F}{\avmplus{\att{a}\\
                              \attvaltyp{G}{\boldmath $\top$}}}}$}
\]

One possibility, of course, would be to attempt to define $\ddunify$
so that structures like this were excluded.  But it is not clear that
this is possible without order dependence.  For example, suppose we
instead defined $\ddunify$ so that the result of the example above was
the following:
\[ \mbox{\tiny $\avmplus{\att{t}\\
                  \attvaltyp{F}{$/$a}}$}
\]
It is then not clear what to do about cases where there is reentrancy, such as:
\[ \mbox{\tiny $\avmplus{\att{t}\\
                  \attvaltyp{F}{$/$a}}$}
\ddunify
\mbox{\tiny $\avmplus{\att{t$'$}\\
                  \attval{F}{/\avmplus{\attval{G}{\ind{1} \ \ \mbox{\small\boldmath $\top$}}}}\\
                  \attval{H}{/\ind{1}}}$}
\]
The reentrancy cannot simply be lost, because then further default
unification with a {\sc fs} with a more specific type than {\bf t}
which `reinstated' the path F$\cdot$G would result in order
dependence.  Furthermore, although it may intuitively look reasonable
to drop the feature G if the atomic type is preferred, what we have
here is not a conflict between values but a conflict between a value
and a path.  It seems preferable to regard the imposition of
well-formedness conditions as part of the operation of incorporation
of default information into the non-default {\sc fs}.  It is, after
all, clear that the default part of 
a {\sc tdfs} is potentially always ill-formed
as a {\sc fs} since it admits nodes typed $\bot$, so it seems
unreasonable to impose any stricter well-formedness conditions.

With respect to the very weak notion of well-formedness described so
far, the resulting {\sc tfs} will be well-formed.  The notion of
typing normally implies stricter well-formedness conditions and we
consider some of these in \S\ref{wellf} below.  But first we briefly
examine how our definition of persistent default unification relates
to previous definitions of default unification as priority union.

\subsection{Persistent default unification and priority union}
\label{comparison}

The asymmetric or priority union class of definitions of default
unification can now be seen as very special cases of $\ddunify$
combined with the default incorporation function defined above.  Apart
from Copestake (1993) and Grover {\em et al} (1994), all definitions
of priority union of which we are aware have involved untyped feature
structures.  This is equivalent in the current formulation to having a
type lattice which is completely flat apart from $\top$ and $\bot$,
and consists of a series of atomic types corresponding to values and a
single non-atomic type, $t$.  The priority union, $\dunify$ of two
{\sc fs} $X \dunify Y$ corresponds to $\mbox{{\em DefFill}}(X'
\ddunify Y')$ where $X'=X'/X'/T_X$ and $Y'=
\top/Y'/T_Y$ 
(i.e.~$X'$ contains only indefeasible information and $Y'$ only
defeasible information) and $X'$ and $Y'$ both have type $t$ (so there
is no specificity order).  Of the definitions surveyed in Copestake
(1993), the closest to the behaviour of $\ddunify$ in this special
case is Carpenter's skeptical version of default unification.  One
case where Carpenter's definition does give different results is shown
in Figures~\ref{carpdef} and~\ref{carpcont}.
\begin{figure}
\begin{center}
$\begin{array}{l}
\mbox{\tiny$
\avmplus{\attval{F}{\avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attvaltyp{I}{\boldmath $\top$}}
$}
\dunify 
\mbox{\tiny$
\avmplus{\attval{F}{\ind{1} \avmplus{\attval{G}{\ind{2}}\\
                             \attval{H}{\ind{2}}}}\\
         \attval{I}{\ind{1}}}
$}
=
\mbox{\tiny$
\avmplus{\attval{F}{ \avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attval{I}{ \avmplus{\attvaltyp{G}{\boldmath $\top$}\\
                             \attvaltyp{H}{\boldmath $\top$}}}}
$}
\end{array}$
\end{center}
\caption{Default unification by Carpenter's definition.}
\label{carpdef}
\begin{center}
$
\begin{array}{l}
\mbox{\tiny $\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attvaltyp{I}{\boldmath $\top$}}
$}
\ddunify 
\mbox{\tiny $\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{\boldmath $\top$}\\
                             \attvaltyp{H}{\boldmath $\top$}}}\\
         \attvaltyp{I}{\boldmath $\top$}}
$}
\left/
\mbox{\tiny $\avmplus{\att{t}\\
         \attval{F}{\ind{1} \avmplus{\attval{G}{\ind{2}}\\
                             \attval{H}{\ind{2}}}}\\
         \attval{I}{\ind{1}}}
$}
\right.
=\\
\hfill
\mbox{\tiny$
\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attvaltyp{I}{\boldmath $\top$}}
$}
\left/
\mbox{\tiny$
\avmplus{\att{t}\\
         \attval{F}{\ind{1} \avmplus{\attval{G}{\ind{2} \bot}\\
                             \attval{H}{\ind{2}}}}\\
         \attval{I}{\ind{1}}}
$}
\right.\\[0.2in]
\mbox{{\em DefFill}}(\mbox{\tiny$\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attvaltyp{I}{\boldmath $\top$}}$}
\left/
\mbox{\tiny$
\avmplus{\att{t}\\
         \attval{F}{\ind{1} \avmplus{\attval{G}{\ind{2} \bot}\\
                             \attval{H}{\ind{2}}}}\\
         \attval{I}{\ind{1}}}$}
\right.)
=
\mbox{\tiny$
\avmplus{\att{t}\\
         \attval{F}{\avmplus{\attvaltyp{G}{a}\\
                             \attvaltyp{H}{b}}}\\
         \attvaltyp{I}{\boldmath $\top$}}$}
\end{array}$
\end{center}
\caption{Persistent Default Unification followed by \mbox{{\em DefFill}}}
\label{carpcont}
\end{figure}

The disparity in results is a consequence of the treatment of
reentrancy in $\ddunify$ and in $\mbox{{\em DefFill}}$, since
skeptical default unification retains the maximal information
possible, whereas our definition sometimes results in potentially
viable information being lost.  The advantage of our current version,
even considered purely as an implementation of priority union, is that
it is computationally tractable, whereas computing the results using
Carpenter's definition potentially 
involves checking all possible combinations of default information for
consistency.


\subsection{Well-formedness} 
\label{wellf}

A variety of different notions of constraints in typed feature
structure systems have been proposed, for example by Carpenter (1992),
Zajac (1993), Copestake \etal (1993) and Gerdemann and King (1994).
The ramifications of fully integrating default unification with any
one of these systems are considerable.  Rather than discussing a
particular proposal in detail here, we introduce some of the general
issues which have to be considered and outline an approach, which
while somewhat restrictive, is adequate for the examples described in
this paper.

We first consider well-formedness of {\sc tdfs}s as a whole.  Type
hierarchies with constraints differ fundamentally from untyped
inheritance systems such as templates in that type constraints on {\sc
fs}s are generally assumed to apply uniformly, however the typed {\sc
fs} arises, whereas templates only apply during a preliminary
processing phase associated with the evaluation of {\sc fs}
descriptions.  If we consider a description of a template as
inheriting from two template {\sc fs}s the result will be subsumed by
their unification, just as a subtype of two types will have a
constraint which is subsumed by the unification of the constraints on
its parents.  But while templates are restricted to the descriptive
metalanguage, types are a part of the object language.  Thus, if we
define two templates, Intrans-verb and Monadic as shown in
Figure~\ref{temptypes} and define Monadic-stative-intrans-verb to
inherit from both of them, this does not affect the result of
unification of two {\sc fs}s which happen to be equal to the template
descriptions.  In contrast, consider the type system also shown in
Figure~\ref{temptypes} which implies that any time two {\sc fs}s of
types {\bf intrans-verb} and {\bf monadic} are unified, the result
must be of type {\bf monadic-stative-intrans-verb} and therefore, to
be well-formed, must be subsumed by its constraint, which can be more
specific than the unification of its parent constraints.  So typed
unification defined simply as a version of untyped unification
augmented with the calculation of greatest common subtypes for each
pair of input nodes does not return a result which respects all type
constraints. In general, an extra step may be needed for each node, of
unifying in the constraint on that node's type.  Well-typed
unification, $\unify_t$ can be defined in these terms (see Carpenter,
1992:92).
\begin{figure}
\begin{verbatim}
Intrans-verb
< SYN CAT > = verb
< SYN SUBJ SYN CAT > = np

Monadic
< SEM PRED > = pred
< SYN SUBJ SEM > = < SEM PRED ARG1 >

Monadic-stative-intrans-verb 
Monadic Intrans-verb
< SEM PRED > = stative
\end{verbatim}
\begin{tabular}{lll}
{\bf intrans-verb}  & $\implies$ & 
{\tiny
$\avmplus{\attval{SYN}{\avmplus{
             \attvaltyp{CAT}{verb}  \\
             \attval{SUBJ}{\avmplus{
                \attval{SYN}{\avmplus{
                         \attvaltyp{CAT}{np}}}}}}}}$
}\\[1mm]
{\bf monadic}  & $\implies$ & 
{\tiny
$\avmplus{\attval{SYN}{\avmplus{            
             \attval{SUBJ}{\avmplus{
                \attval{SEM}{\ind{1}}}}}} \\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\ind{1}}}}}$
}\\[1mm]
{\bf monadic-stative-intrans-verb}  & $\implies$ & {\bf monadic} $\wedge$
{\bf intrans-verb} $\wedge$
{\tiny
$\avmplus{\attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{stative}}}}$}
\end{tabular}
\caption{Templates and types}
\label{temptypes}
\end{figure}

The approaches to typing {\sc fs}s mentioned above assume that every
node in a {\sc fs} is typed, and that monotonic constraints can be
stipulated with respect to any of these types.  In this paper, we have
limited the notion of a default constraint so that the root node of
the constraint {\sc fs} is typed but we do not allow embedded nodes in
constraints to carry types which independently have their own default
constraints.  Since constraint {\sc fs}s can be of arbitrary size,
this does not prevent any subpart of a {\sc fs} being default, but it
does avoid the complex interactions between different sources of
defaults which would otherwise be possible.  We also assume that the
root type of the default part of the {\sc tdfs} is equal to the root
type of the non-default.  Under these conditions, calculation of
inheritance as described in \S4.2 will give a {\sc tdfs} which is
well-formed in that it is subsumed by the indefeasible part of the
constraint on its type, and incorporates all possible information from
the defeasible part, but this is only true because we know the type of
the result beforehand and are already unifying in its
constraint.\footnote{In the monotonic case, well-formedness is usually
described in terms of subsumption: a constraint on a type will subsume
any well-formed {\sc fs} which has a root node of that type.
Obviously we cannot define well-formedness of {\sc tdfs}s by
subsumption, since constraints may have default components.  However,
the definition in the monotonic case could be rephrased as a condition
that a well-formed {\sc fs} is unchanged when it is unified with the
relevant constraint, and an equivalent definition applies here: any
well-formed {\sc tdfs} will be unchanged by the result of persistent
default unification with the constraint on its root node type.} To
ensure persistent default unification always returns a result which is
well-formed by this definition, an extra default unification operation
may be required, just as it is in the monotonic typed unification
case.  We thus define a well-formed default unification operation
$\ddunify_t$:
\begin{defn}
$FS_1\ddunify_t FS_2 = (FS_1\ddunify FS_2)\ddunify 
\mbox{\rm C}(\theta(n_1))$ where $n_1$ is the root node of the
indefeasible part of
$FS_1\ddunify FS_2$
and $\mbox{\rm C}(t)$ gives the {\sc tdfs} representing the constraint on $t$.
\end{defn} 
Clearly, since this is just another $\ddunify$ it is irrelevant at
what stage it is carried out within in a series of default
unifications.  This is not completely analogous to the $\unify_t$
operation described above, because there is no need to consider nodes
internal to the root node and recursively apply their constraints.

We return now to the question of typing with respect to a series of
monotonic constraints on nodes other than the root.  The concept of an
atomic type given in \S\ref{incorp} is an example of an
appropriateness condition which restricts the range of features
possible as transitions from a node of a given type.  This is a very
weak example of an appropriateness condition: an atomic type has no
appropriate features, but all features are possible for all non-atomic
types.  In general, however, we want to be able to state stricter
conditions than this, which will apply in addition to the subsumption
condition mentioned above, and which will affect all typed nodes, not
just root nodes.  The most straightforward case is where we can
stipulate the appropriate features for a type, and for each feature
independent of type we can stipulate an appropriate value.  This can
be implemented as part of the incorporation operation in a manner
analogous to the atomic type stipulation discussed in \S\ref{incorp}.
If we find a node which has a feature which is not appropriate for its
type (or any of its subtypes) we ignore that node when constructing
the {\sc tfs}.

This notion of typing is adequate for the examples discussed in this
paper.  However it is a weaker version of the appropriateness
conditions discussed by Carpenter (1992), because we do not allow
values to be stipulated by types.  Difficulties arise once we allow
types to affect values on successor nodes, because we lose
independence between node values.  Consider the following
appropriateness conditions:
\begin{center}
{\bf t3} $\implies$ 
{\tiny
$\avmplus{\attvaltyp{G}{t2}}$}\\
{\bf t4} $\implies$ 
{\tiny
$\avmplus{\attvaltyp{G}{t5}}$}
\end{center}
(where {\bf t4} $\sqsubset$ {\bf t3} and thus 
{\bf t5} $\sqsubset$ {\bf t2})
and suppose that we have to convert the following {\sc tdfs} to a {\sc tfs}:
\begin{center}
{\tiny
$\avmplus{\att{t1}\\
\attval{F}{\avmplus{\att{t3$/$t4}\\
                  \attvaltyp{G}{t6$/$t7}}}}$}
\end{center}
If the appropriateness conditions on {\bf t3} or {\bf t4} induce a conflict
with the type on F$\cdot$G the result is potentially indeterminate. 
For example, assume
{\bf t2} is compatible with both {\bf t6} and {\bf t7},
{\bf t5} is compatible with {\bf t6} but 
$\mbox{\rm\bf t5}\sqcap\mbox{\rm\bf t7}=\bot$.  In this case, the 
{\sc tfs} which results from incorporating 
both defaults is not well-formed (\ref{conf}), but there multiple well-formed 
possibilities according to whether we accept {\bf t4} in preference to {\bf t7}
(\ref{t4}), {\bf t7} instead of {\bf t4} (\ref{t7}) or neither default type
(\ref{neither}).
\begin{examples}
\item \label{conf}
{\tiny
$\avmplus{\att{t1}\\
\attval{F}{\avmplus{\att{t4}\\
                  \attvaltyp{G}{t7}}}}$}
\item \label{t4}
{\tiny
$\avmplus{\att{t1}\\
\attval{F}{\avmplus{\att{t4}\\
                  \attvaltyp{G}{t6}}}}$}
\item \label{t7}
{\tiny
$\avmplus{\att{t1}\\
\attval{F}{\avmplus{\att{t3}\\
                  \attvaltyp{G}{t7}}}}$}
\item \label{neither}
{\tiny
$\avmplus{\att{t1}\\
\attval{F}{\avmplus{\att{t3}\\
                  \attvaltyp{G}{t6}}}}$}
\end{examples}

The result most in accord with our previous assumptions would be
(\ref{neither}), but this means that \mbox{{\em DefFill}} cannot be
computed without considering all the interactions of appropriateness
conditions, which becomes particularly complex when we consider
examples with reentrancy.  Thus, the interaction of constraints and
defaults is not straightforward, but we will not attempt to resolve
the problem here, since the options depend on the precise assumptions
made about typing, and are essentially independent of the $\ddunify$
operation itself, under the assumption that this is not required to
return a well-formed {\sc fs}.  The only definition of typed default
unification of which we are aware which does explicitly address the
issue of interaction of default and type constraints is that in
Copestake (1993).  This treats default unification as an operation to
be constrained by a type system, not integrated with it, and is in any
case somewhat inelegant.  We therefore leave open here the issue of
how to integrate our definition of persistent default unification
with a full type based constraint system. However, Lascarides and
Copestake (1995) propose an extension to persistent default
unification, which can be integrated in a straightforward manner with
such a system.

\section{The Logic of Persistent Default Unification}
\label{logic-operation}

The rest of the paper can be understood without reading this section.
However, specifying the logic which defines the operation $\ddunify$
allows us to prove that it meets the criteria we specified in
section~\ref{informal}.  We will translate {\sc tdfs}s into a modal
language with well-defined syntax and semantics; define the axioms of
the logic, and the accompanying logical consequence relation; define
the operation $\ddunify$ in terms of this logical consequence
relation; and then prove that $\ddunify$ has the properties specified
in section~\ref{informal}.

\subsection{Translating {\sc tdfs}s into a Modal Language}

We will use a conditional logic to axiomatise $\ddunify$.  We use a
modal language to describe the paths in the {\sc fs}s (cf.  Blackburn,
1992).  We introduce four conditionals into the language, which will
be used to represent: (i) indefeasible paths with values; (ii)
indefeasible reentrancies; (iii) defeasible paths with values; and
(iv) defeasible reentrancies.  Indefeasible paths will be translated
as: $1\leadsto\modal{\pi}a$, where 1 is the tag of the {\sc tdfs},
$\pi$ is a path, or sequence of features, and $a$ is a type.
Semantically this means that the {\sc tdfs} 1 indefeasibly entails the
path $\modal{\pi}a$, and for any path $\modal{\pi}b$ indefeasibly
entailed by this {\sc tdfs}, $a\sqsubseteq b$.  So in a sense,
$\modal{\pi}a$ is the $\modal{\pi}$-prime implicate.  Non-default
reentrancies will be translated as: $1\rightarrow
\modal{\pi}\approx\modal{\pi'}$, where $\rightarrow$ is the material
conditional, and $\approx$ is the Kasper-Rounds connective for
defining reentrancy (Kasper and Rounds, 1986).  Default paths will be
translated as $1\Rightarrow\modal{\pi}a$.  Semantically, this means
that the {\sc tdfs} 1 defeasibly entails $\modal{\pi}a$, and if it
defeasibly entails $\modal{\pi}b$, then $a\sqsubseteq b$.  Finally,
default reentrancies are translated as
$1>\modal{\pi}\approx\modal{\pi'}$. Semantically, this means that the
{\sc tdfs} 1 defeasibly entails the reentrancy between paths
$\modal{\pi}$ and $\modal{\pi'}$.  Note that this doesn't preclude
other reentrancies involving these paths also being entailed by the
{\sc tdfs}.

We first define the syntax and semantics of the modal language ${\cal
L}_{pdu}$, in which $\ddunify$ will be modelled.

\subsubsection*{The Syntax of ${\cal L}_{pdu}$}

\begin{enumerate}
\item   Types $t,t',a,b,\top,\bot\ldots$ are {\sc wff}s.\\
(Types in a {\sc tdfs} will be translated into these {\sc wff}s).
\item   Indices $1,2,\ldots$ are {\sc wff}s.\\
(The index in a {\sc tdfs} will be translated into these {\sc wff}s).
\item   If $1$ is an index, then $\tag{1}$ is a term.\footnotemark
\item   If $\pi$ is a path of features, and $a$ is a type, then
$\modal{\pi}a$ and $[\pi]a$ are {\sc wff}s.
\item   If $\pi$ and $\pi'$ are paths, then
$\modal{\pi}\approx\modal{\pi'}$ is a {\sc wff}.
\item   If $\phi$ and $\psi$ are {\sc wff}s, then so are ,
$\phi \wedge
\psi$, $\phi \rightarrow \psi$ and $\phi > \psi$.
\item   If $1$ is a tag and $\modal{\pi}a$ is a path, then
$1\Rightarrow \modal{\pi}a$ and $1\leadsto \modal{\pi}a$ are {\sc wffs}.
\end{enumerate}

\footnotetext{The term $\tag{1}$ will correspond to
the tag on a {\sc tdfs}.}

We will also occasionally use $\unify$ in the syntax of the language,
for notational convenience.  $a\unify b$ will be shorthand for that
value $c$ which is the value of $a\unify b$ according to the type
hierarchy $\langle \mbox{{\sf Type}},\sqsubseteq\rangle$.

A further notational convention we will use is: $A\not\leadsto B$ for
$(A\leadsto B)\rightarrow \bot$.\footnote{
Strictly speaking, the languge contains two $\bot$s; one which stands
for logical inconsistency---which is the one used in $A\not\leadsto
B$---and the other which stands for the most specific type in $\langle
\mbox{{\sf Type}},\sqsubseteq\rangle$.}
Similarly for $A\not\rightarrow B$,
$A\not\Rightarrow B$, and $A\not >B$.

We also use $\unify$ to refer to the infinum of sets of types.  For
example, if $X = \{a,b,c\}$, then we will write $\unify X$ for $a\unify
b\unify c$.  And if $Y=\{d,e\}$, then we will write $X\unify Y$ for
$a\unify b\unify c\unify d\unify e$.

\subsubsection*{The Semantics of ${\cal L}_{pdu}$}

A model for the language ${\cal L}_{pdu}$ is a tuple
$\langle W, *, R_F,R_G,\ldots,I\rangle$, where:
\begin{itemize}
\item   $W$ is a (non-empty) set of nodes;
\item   $*$ is a function from $W\times {\cal P}(W)$ to ${\cal P}(W)$,
where ${\cal P}(W)$ is the power set of $W$.\\
The constraints on $*$ will be determined by the axioms of the logic
that we define shortly.  These axioms will determine how defaults
behave during unification.
\item   $R_F, R_G,\ldots$ are accessibility relations on $W$ (one for
each feature in {\sf Feat}).\\  The constraints on these relations will
be determined by the axioms of the logic that we define shortly.  They
ensure that {\sc tdfs}s are double {\sc dag}s, for example.
\item   $I$ is the interpretation function, which assigns each type in
{\sf Type} and each tag in $N$ a member of ${\cal P}(W)$.
\end{itemize}
If $\pi$ is a sequence of features $F_1\ldots F_n$, then
$\modal{\pi}=\modal{F_1}\ldots\modal{F_n}$, and $R_{\pi}=
R_{F_1}\circ\ldots\circ R_{F_n}$ 

We now define the semantics of the {\sc wff}s of the language.
\begin{enumerate}
\item   Where $\phi$ is a type or tag $\sem{\phi}_M(n)=\mbox{{\em
      true}}$ 
iff $n\in
I(\phi)$. 
\item   For any feature $F$, 
$\sem{\modal{F}\phi}_M(n) = \mbox{{\em true}}$ iff \\there is an
$n'$ such that $n R_Fn'$ and $\sem{\phi}_M(n')=\mbox{{\em true}}$.
\item   For any paths $\pi$ and $\pi'$,
$\sem{\modal{\pi}\approx\modal{\pi'}}_M(n) = \mbox{{\em true}}$ iff 
$n'R_{\pi}n$ iff $n'R_{\pi'}n$, and \\
there exists an $n'$ such that
$n'R_{\pi}n$.  
\item   $\sem{\phi >
\psi}_M(n)=\mbox{{\em true}}$
just in case $*(n,\sem{\phi}_M) \subseteq \sem{\psi}_M$
\item   $\sem{1\leadsto \modal{\pi}a}(n)=\mbox{{\em true}}$ just in case
$\sem{1\rightarrow \modal{\pi}a}(n)=\mbox{{\em true}}$ 
 \\and if $\sem{1\rightarrow
\modal{\pi}b}(n)=\mbox{{\em true}}$ then $\sem{a}\subseteq \sem{b}$.
\item   $\sem{1\Rightarrow \modal{\pi}a}(n)=\mbox{{\em true}}$ just in case
$\sem{1> \modal{\pi}a}(n)=\mbox{{\em true}}$\\ and if $\sem{1>
\modal{\pi}b}(n)=\mbox{{\em true}}$ then $\sem{a}\subseteq \sem{b}$.
\end{enumerate}
The semantics of $\modal{\pi}\phi$ correspond exactly to that given in
Blackburn (1992), and the semantics of
$\modal{\pi}\approx\modal{\pi'}$ corresponds to that given in Kasper
and Rounds (1986).
These formulae can be used to define {\sc fs}s, as explained
in Blackburn (1992).  {\sc fs}s are a particular
kind of {\sc dag}, and formulae of the
form $\modal{\pi}\phi \wedge \modal{\pi'}\psi \wedge \ldots$ describe such
{\sc dag}s, as long as appropriate constraints are imposed on the
accessibility relations and $\approx$.  This is
because Kripke models are directed graphs.  For example, the
{\sc fs} in (\ref{krip})
describes a {\sc dag}, which is denoted by the formula
$\modal{F}a \wedge \modal{G}b
\wedge \modal{F}\approx\modal{G}$, under certain assumptions about
accessibility (such as $\modal{F}a$ entails $[F]a$).  
\begin{examples}
\item \label{krip}
{\tiny
$\avmplus{\attval{F}{\ind{1}\myvaluebold{a}}\\ \attval{G}{\ind{1}}}$}
\end{examples}
The necessary
axioms for ensuring this representation of {\sc fs}s is an accurate
one are defined below.


\subsection{The Translation of {\sc tdfs}s into ${\cal L}_{pdu}$}

The translation from {\sc tdfs}s into ${\cal L}_{pdu}$ is defined in
terms of two translation functions: one that takes reentrant nodes as
arguments, and the other that takes nodes which are assigned a type as
arguments.  The tails do not undergo a translation procedure.  Rather,
there will be definitions that explain how the tails are constructed,
both in the initial {\sc kb} and when default unification is
performed.  The tails will then play a part in defining the axioms on
the conditional $\Rightarrow$.  But the tails themselves are in
the metalanguage of ${\cal L}_{pdu}$.

The translation of the {\sc fs}s
is a bijection, and therefore has an inverse.  Each {\sc tdfs} is
translated into $\rightarrow$, $\leadsto$, $>$ and $\Rightarrow$
rules, with the tag in the antecedent.  For example:
\begin{enumerate}
\item   $1\rightarrow \modal{\pi}\approx\modal{\pi'}$
\item   $1\leadsto \modal{\pi}a$
\item   $1 > \modal{\pi}\approx\modal{\pi'}$
\item   $1 \Rightarrow \modal{\pi}a$
\end{enumerate}

When unifying two {\sc tdfs}s tagged, say, 1 and 2, we translate the
two {\sc tdfs}s into rules of the above form.  The axioms of the logic
will then generate new $\rightarrow$, $\leadsto$, $>$ and $\Rightarrow$
rules, with the tag $1\wedge 2$ in the antecedent (as before, we will
sometimes abbreviate the tag $1\wedge 2$ to 12).  Using the
inverse translation on these formulae, and the
definition of how a tail is transformed by the $\ddunify$ operation,
which is given below, we produce the
resulting {\sc tdfs}, $\mbox{{\sc tdfs}}_1 \ddunify \mbox{{\sc
tdfs}}_2$. 

The translation on nodes is defined as follows:

\begin{defn}
Let $\langle {\cal T}, i, Q, \langle r_1,r_2\rangle, 
\delta,\theta\rangle$ be a {\sc tdfs}.  Then the translation of this
{\sc tdfs} is defined in terms of two functions $\tau_1$ and $\tau_2$,
which are defined as follows:
\begin{itemize}
\item   $\tau_1:Q_1\longrightarrow {\cal L}_{pdu}$, where
\[
Q_1 =\{n\in Q: \exists \mbox{ paths } \pi,\pi' \mbox{ such that }
n = \delta(r_1,\pi) = \delta(r_1,\pi') \mbox{ or }
n = \delta(r_2,\pi) = \delta(r_2,\pi')\}
\]
and
\[
\tau_1(n) = 
\left \{
\begin{array}{l l}
\{i \rightarrow \modal{\pi}\approx\modal{\pi'}\} & \mbox{If } n =
\delta(r_1,\pi)= \delta(r_1,\pi')\\
\{i > \modal{\pi}\approx\modal{\pi'}\} & \mbox{If } n = \delta(r_2,\pi)=
\delta(r_2,\pi')
\end{array}
\right .
\]
\item   $\tau_2:Q_2\longrightarrow {\cal L}_{pdu}$ where 
\[
Q_2 = \{n\in Q: \theta(n) \mbox{ is defined.}\}
\]
and
\[
\tau_2(n) =
\left \{
\begin{array}{l l}
\{i \leadsto \modal{\pi}\theta(n): \delta(r_1,\pi) = n\} & \mbox{If }
n \mbox{ is a $\delta$-descendant of } r_1\\
\{i \Rightarrow \modal{\pi}\theta(n): \delta(r_2,\pi) = n\} & \mbox{If }
n \mbox{ is a $\delta$-descendant of } r_2
\end{array}
\right.
\]
\end{itemize}
\end{defn}

\subsubsection{An Example of Translation into ${\cal L}_{pdu}$}

The translation of the {\sc tdfs} (\ref{fs1}) is (\ref{fs1}$'$).
\begin{examples}
\item   \label{fs1}
{\tiny
$
\begin{array}{c}
\avmplus{\att{t$^1$}\\
        \attval{F}{\avmplus{\attval{G}{\myvaluebold{a}/\ind{2}}\\
                        \attval{/H}{\ind{2}}}}\\
        \attvaltyp{H}{b$/$c}}
\end{array}
$}
$
\left/
\{\langle F \cdot H,\{\langle a,t\rangle\}\rangle, 
\langle H,\{\langle c,t\rangle\}\rangle\} \right.
$

A tuple that describes this {\sc tdfs} is $\langle {\cal T}, 1, Q,
(n_1,n_5), \delta, \theta\rangle$, where:
\begin{enumerate}
\item   ${\cal T} = \{\langle F\cdot H, \{\langle a,t\rangle\}\rangle,
\langle H,\{\langle c,t\rangle\}\rangle\}$
\item   $Q= \{n_1,n_2,n_3,n_4,n_5,n_6,n_7,n_8\}$
\item   $\delta(n_1,F)=n_2$, $\delta(n_2,G)=n_3$, $\delta(n_1,H)=n_4$,
$\delta(n_5,F)=n_6$, $\delta(n_6,G)=n_7$, $\delta(n_6,H)=n_7$,
$\delta(n_5,H)=n_8$
\item   $\theta(n_1)=t$, $\theta(n_3) = a$,
$\theta(n_4) = b$, $\theta(n_5) = t$, 
$\theta(n_7)=a$, $\theta(n_8)=c$
\end{enumerate}
\item   [\ref{fs1}$'$]
$
\begin{array}[t]{r l}
F\cdot H^1= & \{\langle a,t\rangle\}\\
H^1= & \{\langle c,t\rangle\}\\
1 \leadsto & t\\
1 \leadsto & \modal{F}\modal{G}a\\
1 \leadsto & \modal{H}b\\
1 > & \modal{F}\modal{G} \approx\modal{F}\modal{H}\\
1 \Rightarrow & t\\
1 \Rightarrow & \modal{F}\modal{G}a\\
1 \Rightarrow & \modal{F}\modal{H}a\\
1 \Rightarrow & \modal{H}c
\end{array}
$
\end{examples}

\subsection{The Axioms of the Logic}

We now define the axioms of the logic, so that we can infer new
conditionals from the translations of the {\sc tdfs}s $\mbox{{\sc
tdfs}}_1$ and $\mbox{{\sc tdfs}}_2$ to be unified.  The new
conditionals, together with the new tail as defined below, will be the
translation of the {\sc tdfs} $\mbox{{\sc tdfs}}_1\ddunify \mbox{{\sc
tdfs}}_2$.  We will later see that one cannot take an arbitrary theory
of ${\cal L}_{pdu}$, and determine whether it specifies a {\sc tdfs};
although this won't matter given the way $\ddunify$ is defined.  See
section 4.4.

\subsubsection*{The Axioms on Features and Reentrancy}

The following axioms are consistent with those given in Blackburn
(1992), and Kasper and Rounds (1986):
\begin{itemize}
\item   [PN] {\tt A Possible path is a Necessary One}\\
$\vdash \langle F\rangle\phi \rightarrow [F]\phi$
\item   [ARE]   {\tt Adding Reentrancies}\\
$\vdash (\modal{\pi}\approx\modal{\pi'}
\wedge \modal{\pi'}\approx\modal{\pi''}) \rightarrow
\modal{\pi}\approx\modal{\pi''}$
\item   [RET]   {\tt Reentrancy and Top}\\
$\vdash \modal{\pi}\approx\modal{\pi'} \rightarrow
(\modal{\pi}\top\wedge \modal{\pi'}\top)$\\
$\vdash \modal{\pi}\approx\modal{\pi}\leftrightarrow \modal{\pi}\top$
\item   [REV]   {\tt Reentrancies and Values}\\
$\vdash (\modal{\pi}\phi \wedge \modal{\pi'}\psi \wedge
\modal{\pi}\approx\modal{\pi'})\rightarrow \\
\hspace*{0.3in}(\modal{\pi}(\phi \unify
\psi) \wedge \modal{\pi'}(\phi\unify \psi))$
\item   [ACL]   {\tt Acycles}\\
$\vdash (\modal{\pi_1\pi_2}\approx\modal{\pi_2}) \rightarrow \bot$
\end{itemize}

These ensure that the modal semantics does indeed describe the {\sc
fs}s in the definition of {\sc tdfs}s in the appropriate way.  For
example, as long as the accessibility relations are constrained so as
to model PN, each {\sc dag} in the model contains at most one
$\modal{\pi}$-arc---just like {\sc fs} {\sc dag}s); and by ARE,
reentrancies are transitive.  The semantic constraints corresponding
to RET and REV ensure the {\sc dag} in the Kripke model is isomorphic
to one containing node sharing, when the paths are reentrant.  And by
ACL, cycles are disallowed.

We also assume the axioms on $\rightarrow$, familiar from first order logic.

\subsubsection*{The Axioms of $\leadsto$}

The axioms on $\rightarrow$ and $\leadsto$ determine how the
indefeasible information in the {\sc tdfs}s combines under the
operation $\ddunify$.

The first axioms PI1 and PI1$'$ ensure that the path in the consequent of a
$\leadsto$ rule is the most specific path.  The last three axioms TU1,
TU2 and TU3 ensure that, together
with PI1 and PI1$'$, $\leadsto$ corresponds to typed unification.
\begin{itemize}
\item   [PI1]   {\tt The First Prime Implicate Axiom: Part I}\footnotemark\\
\begin{tabular}[t]{l}
$1\leadsto \modal{\pi}a$ \\ \hline
$(1\leadsto \modal{\pi}b) \rightarrow b=a$
\end{tabular}
\item   [PI1$'$]        {\tt The First Prime Implicate Axiom: Part
    II}\\
\begin{tabular}[t]{l}
$1\rightarrow \modal{\pi}a$\\
$(1\rightarrow \modal{\pi}b) \rightarrow (a\rightarrow b)$\\ \hline
$1\leadsto \modal{\pi}a$
\end{tabular}
\item   [TU1]   {\tt The First TU Axiom}\\
\begin{tabular}[t]{l}
$1 \leadsto \modal{\pi}a$\\
$(1\rightarrow \modal{\pi}\approx\modal{\pi'})\rightarrow
(2\not\rightarrow \modal{\pi'}\top)$\\ \hline
$(1\wedge 2) \rightarrow \modal{\pi}a$
\end{tabular}
\item   [TU2]   {\tt The Second TU Axiom}\\
\begin{tabular}[t]{l}
$1 \leadsto \modal{\pi}a$\\
$2 \leadsto \modal{\pi'}b$\\
$1\rightarrow \modal{\pi}\approx\modal{\pi'}$ \\ \hline
$(1\wedge 2) \rightarrow \modal{\pi}(a\unify b)$
\end{tabular}
\item   [TU3]   {\tt The Third TU Axioms}\\
\begin{tabular}[t]{l}
$1 \rightarrow \modal{\pi}\bot$\\ \hline
$1 \rightarrow \bot$
\end{tabular}
and
\begin{tabular}[t]{l}
$1 \rightarrow \bot$\\ \hline
$1 \rightarrow \modal{\pi}\bot$
\end{tabular}
\end{itemize}

\footnotetext{
One could replace $b=a$ in PI1 with $a\sqsubseteq b$; the resulting
axiom would be equivalent.}

TU1 and PI1$'$ ensure that the following holds:
\[
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attvaltyp{F}{a}}$}
\ddunify 
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attvaltyp{G}{b}}$}
=
\mbox{\tiny $\avmplus{\att{t$_1$ $\unify$ t$_2^{(1 \wedge 2)}$}\\
        \attvaltyp{F}{a}\\
        \attvaltyp{G}{b}}$}
\] 

TU2 and PI1$'$ ensure the following holds:

\[
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
\attval{F}{\ind{1}\myvaluebold{a}}\\
\attval{G}{\ind{1}}}$}
\ddunify
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
\attval{G}{\ind{2}\myvaluebold{b}}\\
\attval{H}{\ind{2}}}$}
=
\mbox{\tiny $\avmplus{\att{t$_1$ $\unify$ t$_2^{(1 \wedge 2)}$}\\
\attval{F}{\ind{1}\myvaluebold{a}\unify \myvaluebold{b}}\\
\attval{G}{\ind{1}}\\
\attval{H}{\ind{1}}}$}
\]

TU2, TU3 and PI1$'$ ensure the following holds: where $a\unify b=\bot$:
\[
\mbox{\tiny $\avmplus{\att{t$^1$}\\
        \attvaltyp{F}{a}}$}
\ddunify 
\mbox{\tiny $\avmplus{\att{t$^2$}\\
        \attvaltyp{F}{b}}$}
= \bot^{(1\wedge 2)}
\] 

These axioms ensure that step 1 in the informal description of
$\ddunify$ holds.  That is, the indefeasible part of $\mbox{{\em
FS}}_1\ddunify \mbox{{\em FS}}_2$ is $I_1\unify I_2$.

We now consider the axioms for $>$, the definition of tails, and
the axioms for $\Rightarrow$.  These will determine the default aspect
of the definition of $\ddunify$.

\subsubsection*{The Axioms on $>$}

Given the semantics of $>$, we have the following two axioms:
\begin{itemize}
\item   [CR]    {\tt Closure on the Right}\\
\begin{tabular}[t]{l} 
$A > B$ \\
$\vdash B\rightarrow C$\\ \hline
$A > C$
\end{tabular}
\item   [AND]   {\tt The And Condition}\\
\begin{tabular}[t]{l}
$A > B$\\
$A > C$\\ \hline
$A > (B \wedge C)$
\end{tabular}
\end{itemize}

In addition, we add the following, and a corresponding semantic
constraint on $*$:\footnote{For the purposes of brevity, we will not
define the semantic constraints on $*$ that correspond to
the axioms on $>$ and $\Rightarrow$.}
\begin{itemize}
\item   [RE1]   {\tt The First Reentrancy Axiom}\\
\begin{tabular}{l}
$1\rightarrow \modal{\pi}\approx\modal{\pi'}$\\ \hline
$1 > \modal{\pi}\approx\modal{\pi'}$
\end{tabular}
\end{itemize}
In other words, any reentrancy in the indefeasible {\sc dag} has a
corresponding reentrancy in the defeasible {\sc dag}.  This is in line
with the isomorphism constraint between the {\sc dag}s in the
definition of {\sc tdfs}s.

There is one more axiom involving $>$ and reentrancy, which will tell
us which defeasible reentrancies survive unification:
\begin{itemize}
\item   [RE2]   {\tt The Second Reentrancy Axiom}\\
\begin{tabular}{l}
$1 > \modal{\pi}\approx\modal{\pi'}$\\ \hline
$(1\wedge 2)>\modal{\pi}\approx\modal{\pi'}$
\end{tabular}
\end{itemize}
RE2 entails that the definition of $\ddunify$ will be one in which
default reentrancies always survive, even when there's incompatible
indefeasible information (in which case the default value on the
reentrant node is $\bot$).  
That is, it corresponds to step 2 in
the informal definition specified in \S\ref{informal}.
If the reentrancies in 1 and 2 produce a
cyle, then by RE2, ARE and CR, $(1\wedge 2)>\bot$.  The definition of a PDU
deduction below ensures that in this case, the defeasible part of the
unified {\sc tdfs} is $\bot$.

\subsubsection*{The Definition of Tails}

Tails are defined in the following manner:
\begin{itemize}
\item   Let the {\sc tdfs} {\sc tdfs}$_1$ be in the initial {\sc kb};
we call such {\sc tdfs}s  {\em basic} {\sc tdfs}s.  Then for any path
$\pi$ in {\sc tdfs}$_1$:
\[
\pi^1 =\{\langle a,t\rangle:\mbox{ where } 1\Rightarrow t,
1\Rightarrow \modal{\pi}a, 1\not\leadsto \modal{\pi}a\}
\]
That is, these tails record just the information that is defeasible but
{\em not} indefeasible, together with the root type (specificity).
\item   The following rule tells us how to construct new tails from
old ones, during unification:
\[
\pi^{1\wedge2} = \cup^{\pi'}_{(1\wedge
2)>\modal{\pi}\approx\modal{\pi'}}\pi'^1\cup \pi'^2
\]
This corresponds exactly to the instructions in step 3 of the
informal definition of $\ddunify$ given earlier.
\end{itemize}
When unifying {\sc tdfs}$_1$ with {\sc tdfs}$_2$, the $\pi$-part of
the new tail is formed by set union on the tails $\pi'^1$ and
$\pi'^2$, for all $\pi'$ that are reentrant with $\pi$.  So, in
particular, $\pi^1\cup\pi^2\subseteq \pi^{12}$ (since $\pi$ is
reentrant with itself).  These two definitions ensure that the tail of
a {\sc tdfs} contains all the strictly defeasible values on the {\em
original} {\sc tdfs}s that were used to build this {\sc tdfs},
together with the specificity information.  We will see that this
definition of tails guarantees the following result:
\[
\begin{array}{c}
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\
\attval{F}{/\ind{1}\myvaluebold{a}}\\
\attval{G}{/\ind{1}}\\
\attvaltyp{H}{b}}$}
\end{array}
\left/
\begin{array}{l}
\{\langle F,\{\langle a,t\rangle\}\rangle,\\
\langle G,\{\langle a,t\rangle\}\rangle\}
\end{array}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\
\attval{G}{/\ind{2}\myvaluebold{c}}\\
\attval{H}{/\ind{2}}}$}
\end{array}
\left/
\begin{array}{l}
\{\langle G,\{\langle c,t\rangle\}\rangle,\\
\langle H,\{\langle c,t\rangle\}\rangle\}
\end{array}
\right.\\
= 
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t}\\
\attval{F}{/\ind{1}\myvaluebold{a}\unify \myvaluebold{b}\unify \myvaluebold{c}}\\
\attval{G}{/\ind{1}}\\
\attval{H}{\myvaluebold{b}/\ind{1}}}$}
\end{array}
\left/
\begin{array}{l}
\{\langle F,\{\langle a,t\rangle\, \langle c,t\rangle\}\rangle,\\
\langle G,\{\langle a,t\rangle, \langle c,t\rangle\}\rangle\\
\langle H, \{\langle a,t\rangle, \langle c,t\rangle\}\rangle\}
\end{array}
\right.
\end{array}
\]
Note that in the above, $\langle H, \{\langle b,t\rangle\}\rangle$ is
not in the tail of the {\sc lhs} {\sc tdfs}, because the path $H:b$ is
indefeasible (as well as defeasible).  Because of this, it is not in
the tail of the result either.  But the values in the $F$, $G$ and $H$
parts of the tails are expanded in the result, because of the
reentrancy, which determines which sets to unify in the resulting
tail.  If we defined $\pi^{12}$ to be $\pi^1\cup \pi^2$, then in the
above, $F^{12}\neq H^{12}$.  So we would not get a well-defined {\sc
tdfs} in this example of $\ddunify$, because the axioms on
$\Rightarrow$, which are defined using the tails, would fail to see
that the default values on F, G, and H must agree.

\subsubsection*{The Axioms on $\Rightarrow$}

Having defined tails, we are finally in a position to define the
axioms on $\Rightarrow$, which will ultimately determine which default
paths in a {\sc tdfs} survive the $\ddunify$ operation.  There are
three axioms: the first ensures that the path in a consequent of a
$\Rightarrow$-rule is the most specific; the second and third define
the $\ddunify$ operation for default paths.

\begin{itemize}
\item   [PI2]   {\tt The Second Prime Implicate Axiom}\\
\begin{tabular}[t]{l}
$1\Rightarrow \modal{\pi}a$ \\ \hline
$(1\Rightarrow \modal{\pi}b) \rightarrow b=a$
\end{tabular}
\item   [CON]   {\tt Consistency}\\
\begin{tabular}[t]{l}
$1\Rightarrow \modal{\pi}a$\\
$(1>\modal{\pi}\approx\modal{\pi'}) \rightarrow (2\not>
\modal{\pi'}\top)$ \\ 
$(1\wedge 2)\not> \modal{\pi_1\pi_2}\approx\modal{\pi_2}$ \\ \hline
$(1\wedge 2)\Rightarrow \modal{\pi}a$
\end{tabular}
\item   [PDU]   {\tt The Persistent Default Unification Axiom}\\
\begin{tabular}[t]{l}
$1 \Rightarrow \modal{\pi}a$\\
$2 \Rightarrow \modal{\pi'}b$\\
$1 > \modal{\pi}\approx\modal{\pi'}$\\ 
$(1\wedge 2)\not> \modal{\pi_1\pi_2}\approx\modal{\pi_2}$ \\ \hline
$(1\wedge 2) \Rightarrow \modal{\pi}(\mbox{{\em Spec}}_{\pi}^{12} \unify
\mbox{{\em Comp}}_{\pi}^{12} \unify \psi)$
\end{tabular}

Where:

$\psi = \unify\{\psi_{\pi_i}: 1\wedge 2\leadsto \modal{\pi_i}\psi_{\pi_i}
\mbox{and } (1\wedge 2)> \modal{\pi}\approx\modal{\pi_i}\}$

$\mbox{{\em Spec}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall \langle\phi',t_{\phi'}\rangle\in
\pi^{12}, t_{\phi'}\not\sqsubset t_{\phi}
\mbox{ and } \phi\unify
\psi\neq \bot\}$

$\mbox{{\em Comp}}_{\pi}^{12} =\{\phi: \langle \phi,t_{\phi}\rangle \in
\pi^{12} \mbox{ and }
\forall v\in \mbox{{\em Spec}}_{\pi}^{12}, v\unify
\phi\neq \bot
\mbox{ and } \phi\unify
\psi\neq \bot\}$

$\mbox{{\em Spec}}$ stands for Specificity; and $\mbox{{\em Comp}}$
for Completeness.
\end{itemize}

CON and PDU are used to work out default values on paths, in the case
where the reentrancies didn't yield a cycle.
CON is analogous to TU1; it ensures that the result of the unification
operation  in (\ref{args}) is (\ref{arg1}) rather than (\ref{arg2}):
\begin{examples}
\item   \label{args}
{\tiny $\avmplus{\att{t$_1^1$}\\
        \attvaltyp{F}{$/$a}}$}
$\ddunify$ 
{\tiny $\avmplus{\att{t$_2^2$}\\
        \attvaltyp{G}{$/$b}}$}
\item   \label{arg1}
{\tiny $\avmplus{\att{t$_1$ $\unify$ t$_2^{(1 \wedge 2)}$}\\
        \attvaltyp{F}{$/$a}\\
        \attvaltyp{G}{$/$b}}$}
\item   \label{arg2}
{\tiny $\avmplus{\att{t$_1$ $\unify$ t$_2^{(1 \wedge 2)}$}\\
        \attvaltyp{F}{\boldmath $\top$}\\
        \attvaltyp{G}{\boldmath $\top$}}$}
\end{examples}

But why is the PDU axiom defined in the way it is?  Let's first look
at the sets $\mbox{{\em Spec}}_{\pi}^{12}$ and $\mbox{{\em
Comp}}_{\pi}^{12}$ (we will refer to these as $\mbox{{\em Spec}}$ and
$\mbox{{\em Comp}}$ when there is no confusion).  $\mbox{{\em
Spec}}_{\pi}^{12}$ picks all the values in the tail $\pi^{12}$ that
originated from the most specific {\sc tdfs}s, and that are compatible
with the indefeasible information.  This is equivalent to the set (b) in the
informal description of $\ddunify$ given earlier.  Note for now that
$\mbox{{\em Spec}}$ will help get the specificity results we require.
Suppose a tail contains $\langle a,t_a\rangle$ and $\langle
b,t_b\rangle$.  This means that the {\sc tdfs} with this tail resulted
from the default unification of (at least) the two {\sc tdfs}s which
contained respectively the strictly default information $\pi:a$ and
root type $t_a$, and strictly default information $\pi:b$ and root
type $t_b$.  Now suppose that $a\unify b=\bot$ and $t_a\sqsubset t_b$.
Then $b\not\in \mbox{{\em Spec}}$.  But $a$ will be in $\mbox{{\em
Spec}}$, as long as (i) $t_a$ was at least as specific as all the
other specificity information in the $\pi^{12}$, and (ii) $a$ is
compatible with the indefeasible information.  And if $a\in \mbox{{\em
Spec}}$, then $b\not\in
\mbox{{\em Comp}}$, since $a\unify b=\bot$.  So the PDU axiom will
ensure that $b$ will be overridden by $a$, as specificity requires.
The Nixon Diamond, therefore, will correspond to a case where
$\mbox{{\em Spec}}$ contains two elements that are incompatible.  They
must have been associated with types that were unordered with respect
to each other.  The result of $\ddunify$ in this case will be
$\modal{\pi}\bot$.

The set $\mbox{{\em Comp}}_{\pi}^{12}$ contains all the values in the
tail that are compatible with those in $\mbox{{\em
Spec}}_{\pi}^{12}$---i.e., the values associated with the most
specific types---and the indefeasible information.  This is equivalent
to the set (c) in the informal description of $\ddunify$ given earlier.
This enables a value that has been overridden previously by
specificity, to now be re-inherited into the result.  Therefore, a
specific value on a general type constraint can survive unification
when it is compatible with the most specific type constraints.  As
mentioned earlier, allowing this to happen is essential if $\ddunify$
is to reduce to typed unification when no conflicts arise.  It is also
essential for preserving order independence in the example in
\S\ref{informal} that illustrated that recording only specificity
information from the unification history is insufficient. 

In the definition of $\mbox{{\em Spec}}$ and $\mbox{{\em Comp}}$, we
remove all the values that are incompatible with $\psi$, in order to
ensure that indefeasible information always overrides defeasible
information, when there is conflict.  So, for example, if $a\unify b =
\bot$, then: 
\[
\begin{array}{c}
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a$/$c}}}}$}
\end{array}
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}$}
\end{array}\\
=
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^{(1\wedge 2)}$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a$/$c}}}}$}
\end{array}
\left/
\{\langle F\cdot G, \{\langle b,t_2\rangle, \langle c,t_1\rangle\}\rangle\}
\right.
\end{array}
\]

Suppose we didn't remove the information from $\mbox{{\em Spec}}$ and
$\mbox{{\em Comp}}$ that is incompatible with the indefeasible
information, and suppose $t_2\not\sqsubset t_1$ and $t_1\not\sqsubset
t_2$.  Then $\mbox{{\em Spec}}$ would be $\{b,c\}$, and so the PDU
axiom would give $(1\wedge 2)\Rightarrow \modal{F}\modal{G}\bot$,
rather than $(1\wedge 2)\Rightarrow \modal{F}\modal{G}c$.  Conflicts
between values of equal specificity would thus result in failure,
despite the indefeasible evidence which can resolve them.

Finally, the indefeasible information unifies with $\mbox{{\em Spec}}$
and $\mbox{{\em Comp}}$ ensuring that the result produces a
well-defined {\sc tdfs}.  This information is the unification of all
the indefeasible values on paths that, by default, are reentrant with
$\modal{\pi}$.  This looks mysterious at first.  The motivation for it
is illuminated by the following considerations.  First, we must unify
$\mbox{{\em Spec}}$ and $\mbox{{\em Comp}}$ with (at least) the
indefeasible information $\psi_{\pi}$ such that $(1\wedge 2)\leadsto
\modal{\pi}\psi_{\pi}$.  To see this consider the following:

\begin{center}

{\modsmalltree{3}{
{\node{a}{a}} & & {\node{b}{b}}\\
&& {\node{c}{c}}\\
& {\node{bot}{$\bot$}}}
\nodeconnect{a}{bot}
\nodeconnect{b}{c}
\nodeconnect{c}{bot}}

\vspace{0.1in}

$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$^1$}\\
\attvaltyp{F}{a}\\
\attvaltyp{G}{b}}$}
\end{array}
\left/
\{\}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$^2$}\\
\attval{F}{/\ind{1}\myvaluebold{c}}\\
\attval{G}{/\ind{1}}}$}
\end{array}
\left/
\{\langle F,\{\langle c,t\rangle\}\rangle, \langle G,\{\langle
c,t\rangle\}\rangle \}
\right.
$

\end{center}

If the PDU axiom were defined so that $(1\wedge 2)\Rightarrow
\modal{F}(\mbox{{\em Spec}}_{F}^{12}\unify
\mbox{{\em Comp}}_{F}^{12})$, then since in the above $F^{12} = \{\langle c,t\rangle\}$ and
$(1\wedge 2) \leadsto \modal{F}a$, $\mbox{{\em Spec}}^{12} =
\emptyset$ and $\mbox{{\em Comp}}^{12} =\emptyset$.  So $(1\wedge
2)\Rightarrow \modal{F}\top$.  But by PI2, $\top$ is the most specific
value on the defeasible $F$-path, and by REV, we must infer $(1\wedge
2)\Rightarrow \modal{G}\top$.  So for the result to translate back
into a well-defined {\sc tdfs}, we must have $\top\sqsubseteq a$, and
$\top\sqsubseteq b$, since the values on defeasible paths must entail
those on indefeasible paths.  Therefore, $\top \sqsubseteq a\unify b$.
So $\top \sqsubseteq \bot$.  This contradicts our type hierarchy.  So,
we must unify the indefeasible information $\psi_{\pi}$ with $\mbox{{\em
Spec}}$ and $\mbox{{\em Comp}}$ in the PDU axiom, to ensure the result
can be translated back into a well-defined {\sc tdfs}.

In fact, we unify much more with $\mbox{{\em Spec}}$ and $\mbox{{\em
Comp}}$.  The reason we need to unify $\mbox{{\em Spec}}$ and
$\mbox{{\em Comp}}$ with $\psi$ as defined above is because the value
on the default path must be more specific than {\em every}
indefeasible value on the paths with which it is reentrant.
Otherwise, the result again will not be a well-defined {\sc tdfs}.
Unifying $\mbox{{\em Spec}}$ and $\mbox{{\em Comp}}$ with just
$\psi_{\pi}$, such that $(1\wedge 2)\leadsto\modal{\pi}\psi_{\pi}$
does not guarantee this.  If PDU were defined so that $(1\wedge
2)\Rightarrow
\modal{F}(\mbox{{\em Spec}}_F^{12}\unify \mbox{{\em Comp}}_F^{12}\unify \psi_F)$, where $(1\wedge
2)\leadsto \modal{F}\psi_F$, then in the above example, we would infer
$(1\wedge 2)\Rightarrow \modal{F}\bot$, and $(1\wedge 2)\Rightarrow
\modal{G}c$.   So by REV and PI2, $c=\bot$, contradicting our
hypothesis about the type hierarchy.

To see that we must remove all values from $\mbox{{\em Spec}}$ and
$\mbox{{\em Comp}}$ that are inconsistent with $\psi$, consider the
above example of $\ddunify$, but with the following type hierarchy:

\begin{center}
{\modsmalltree{4}{
{\node{a}{a}} && {\node{b}{b}}\\
& {\node{d}{d}} && {\node{c}{c}}\\
&& {\node{e}{$\bot$}}}
\nodeconnect{a}{d}
\nodeconnect{b}{c}
\nodeconnect{b}{d}
\nodeconnect{d}{e}
\nodeconnect{c}{e}}
\end{center}

If we only removed values from $\mbox{{\em Spec}}_{\pi}^{12}$ and
$\mbox{{\em Comp}}_{\pi}^{12}$ that were incompatible with
$\psi_{\pi}$, then PDU would yield $(1\wedge 2)\Rightarrow
\modal{F}(a\unify b)$, and $(1\wedge 2)\Rightarrow\modal{G}(a\unify
b\unify c)$.  So, via REV and the prime implicate axiom PI2,
$d=\bot$, contradicting our hypothesis.

\subsubsection*{The Tag Axioms}

Finally, we need to provide axioms on the tags or indices, that ensure
that when the logic predicts that 1 and 2 have identical paths and
reentrancies, they are the same tag, and hence name the same {\sc
tdfs}.  This is done as follows:
\begin{itemize}
\item   [TAG]   {\tt The Tag Axiom}
\item   If for all $\pi$, $\pi'$ and for all $\phi$:\\
$(1 \leadsto \modal{\pi}\phi) \leftrightarrow (2 \leadsto \modal{\pi}\phi)$\\
$(1 \rightarrow \modal{\pi}\approx \modal{\pi'}) \leftrightarrow (2
\leadsto \modal{\pi}\approx \modal{\pi'})$\\
$(1 \Rightarrow \modal{\pi}\phi) \leftrightarrow (2 \Rightarrow
\modal{\pi}\phi)$\\
$(1 > \modal{\pi}\approx \modal{\pi'}) \leftrightarrow (2 >
\modal{\pi}\approx \modal{\pi'})$\\ 
Then\\
$\tag{1} = \tag{2}$
\end{itemize}
We require this, in order to ensure that $\ddunify$ is a function, and
is commutative, as we will demonstrate below.  The tag axioms ensure
that if the logic produces exactly the same paths, then the {\sc tdfs}
they correspond to is the same.

\subsection{Examples}
\label{examples}

In \S\ref{proofs} we will prove that the above axioms make $\ddunify$
order independent, and also ensure that $\ddunify$ reduces to $\unify$
when there's no conflict between the {\sc tdfs}s.  But first, we will
illuminate how the above logic works, by means of specific examples.
In each case, the task is to translate the {\sc tdfs}s to be unified
into the conditional logic, and then to use the above axioms to
generate new $\leadsto$, $\rightarrow$, $>$ and $\Rightarrow$ rules,
which will be translated back into {\sc tdfs} notation via the inverse
translation function.

To demonstrate the equivalence between the informal description of
$\ddunify$ given earlier and the formal specification given here, we
use the same examples as earlier.

\subsubsection*{The Defeat of Defeasible Modus Ponens}

Consider the following example of $\ddunify$:
Where $t_2 \sqsubset t_1$ and $a\unify b = \bot$

\[
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a}}}}$}
\left/
\{\}
\right.
\end{array}
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\right.
\]


The above {\sc tdfs}s are translated into
the following formulae of ${\cal L}_{pdu}$:
\[
\begin{array}{l l}
1 \leadsto & t_1\\
1 \leadsto & \modal{F}\modal{G}a\\
1 \Rightarrow & t_1\\
1 \Rightarrow &  \modal{F}\modal{G}a\\
2 \leadsto & t_2\\
2 \leadsto & \modal{F}\modal{G}\top\\
2 \Rightarrow & t_2\\
2 \Rightarrow &  \modal{F}\modal{G}b
\end{array}
\]

Using the axioms, we gain the following results:

\begin{tabular}{l l l}
$(1\wedge 2)\leadsto$ & $\modal{F}\modal{G}a$ & TU1 and PI1$'$
\end{tabular}

By the definition of tails, $\mbox{{\em Spec}}_{F\cdot G}^{12}$ and $\mbox{{\em Comp}}_{F\cdot G}^{12}$ we have:
\[
\begin{array}{r l}
F\cdot G^{12} = & \{\langle b,t_2\rangle\}\\
\mbox{{\em Spec}}_{F\cdot G}^{12} = \mbox{{\em Comp}}_{F\cdot G}^{12} = & \emptyset
\end{array}
\]

So\\
\begin{tabular}{l l l}
$(1\wedge2)\Rightarrow$ & $\modal{F}\modal{G}a$ & PDU
\end{tabular}

Therefore:
\[
\begin{array}{c}
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a}}}}$}
\end{array}
\left/
\{\}
\right.
\ddunify

\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\right.\\
=
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^{(1 \wedge 2)}$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{a}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\right.
\end{array}
\]


\subsubsection*{Specificity}

Consider the following example of $\ddunify$, where $t_2\sqsubset
t_1$, and $a\unify b = \bot$.

\[
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$a}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle a,t_1\rangle\}\rangle\}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\right.
\]
The above {\sc tdfs}s are translated into the following formulae of
${\cal L}_{pdu}$:
\[
\begin{array}{l l}
1 \leadsto & t_1\\
1 \leadsto & \modal{F}\modal{G}\top\\
1 \Rightarrow & t_1\\
1 \Rightarrow & \modal{F}\modal{G}a\\
2 \leadsto & t_2\\
2 \leadsto & \modal{F}\modal{G}\top\\
2 \Rightarrow & t_2\\
2 \Rightarrow & \modal{F}\modal{G}b\\
\end{array}
\]
And the tails are defined as follows:
\[
\begin{array}{l l}
F\cdot G^1 = & \{\langle a,t_1\rangle\}\\
F\cdot G^2 = & \{\langle b,t_2\rangle\} \mbox{ so }\\
F\cdot G^{12} = & \{\langle a,t_1\rangle, \langle
b,t_2\rangle\}\\
\mbox{{\em Spec}}_{F\cdot G}^{12} = & \{b\}\\
\mbox{{\em Comp}}_{F\cdot G}^{12} = & \{b\}
\end{array}
\]
Using the axioms, we gain the following results:

\begin{tabular}{l l l}
$(1\wedge 2) \leadsto$ &  $t_2$ & TU2 and PI1$'$\\
$(1\wedge 2)\leadsto$ &  $\modal{F}\modal{G}\top$ & TU2 and PI1$'$\\
$(1 \wedge 2) \Rightarrow$ &  $t_2$ & PDU\\
$(1\wedge 2)\Rightarrow$ & $\modal{F}\modal{G}b$ & PDU
\end{tabular}\\
Therefore:
\[
\begin{array}{c}
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$a}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle a,t_1\rangle\}\rangle\}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attval{F}{\avmplus{
                \attvaltyp{G}{$/$b}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle b,t_2\rangle\}\rangle\}
\right.\\
=
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^{(1\wedge 2)}$}\\
        \attval{F}{\avmplus{\attvaltyp{G}{$/$b}}}}$}
\end{array}
\left/
\{\langle F\cdot G,\{\langle a,t_1\rangle,\langle b,t_2\rangle\}\rangle\}
\right.
\end{array}
\]
\subsubsection*{General Values on Specific {\sc tdfs}s}

In \S\ref{informal} we gave an example to motivate the need to record
the original specificity information for each feature\,:\,value path
during the unification process.  Here we go through an equivalent case
in detail:

\begin{center}
(1)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
        \attvaltyp{F}{$/$a}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle\}\rangle\}
\right.
$
\hfill 
(2)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
        \attvaltyp{F}{$/$b}}$}
\end{array}
\left/
\{\langle F,\{\langle b,t_2\rangle\}\rangle\}
\right.
$\\
(3)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^3$}\\
        \attvaltyp{F}{c}}$}
\end{array}
\left/
\{\}
\right.
$

\vspace{0.1in}

$t_3\sqsubset t_2\sqsubset t_1$\\
$a\generalize b = c$\\
$a\unify b = \bot$
\end{center}

We now show that under the above definition of $\ddunify$, the result
is order independent.  We will calculate $(1 \ddunify 2) \ddunify 3$,
and $(1\ddunify 3)\ddunify 2$.

First, the translations of the above {\sc tdfs}s produce the following:

\[
\begin{array}{l l}
1 \Rightarrow & \modal{F}a\\
2 \Rightarrow & \modal{F}b\\
3 \leadsto & \modal{F}c
\end{array}
\]

And the tails are defined as follows:
\[
\begin{array}{l l}
F^{1} = & \{\langle a,t_1\rangle\}\\
F^2 = & \{\langle b, t_2\rangle\}\\
F^3 = & \emptyset
\end{array}
\]

We first calculate $1\ddunify 2$.  $F^{12} = \{\langle
a,t_1\rangle,\langle b,t_2\rangle\}$. And by TU2 and
PI1$'$, $(1\wedge 2)\leadsto
\modal{F}\top$; that is the path $F:\top$ is indefeasible information.
So $\mbox{{\em Spec}}_{F}^{12} = \{b\}$, and $\mbox{{\em
Comp}}_{F}^{12} = \{b\}$.  And therefore by the PDU axiom, $(1 \wedge
2)\Rightarrow \modal{F}b$.

Now we calculate $(1\ddunify 2)\ddunify 3$.  $F^{(12)3} = \{\langle
a,t_1\rangle,\langle b,t_2\rangle\}$, and by TU2 and PI1$'$
$((1 \wedge 2)\wedge 3) \leadsto \modal{F}c$.  So $\mbox{{\em Spec}}_{F}^{(12)3} = \{b\}$ and
$\mbox{{\em Comp}}_{F}^{(12)3}=\{b\}$, and by the PDU axiom $((1\wedge 2)\wedge 3)\Rightarrow
\modal{F}b$.  So:
\[
(1 \ddunify 2)\ddunify 3 = 
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^{(12)3}$}\\
        \attvaltyp{F}{c$/$b}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle,\langle b,t_2\rangle\}\rangle\}
\right.
\]

Now we calculate $(1 \ddunify 3)\ddunify 2$.
By the definition of tails, $F^{13} = \{\langle a,t_1\rangle\}$.  And
by TU2 and
PI1$'$, 
$(1\wedge 3)\leadsto \modal{F}c$.  So $\mbox{{\em Spec}}_{F}^{13} = \{a\}$,
and $\mbox{{\em Comp}}_{F}^{13} =
\{a\}$.  And so by PDU, $(1\ddunify 3) \Rightarrow \modal{F}a$.  

Now, $F^{(13)2} = \{\langle a,t_1\rangle, \langle b,t_2\rangle\}$.
And by TU2 and PI1$'$
$((1\wedge 3)\wedge 2) \leadsto \modal{F}c$.  So $\mbox{{\em
    Spec}}_{F}^{(13)2} = 
\{b\}$ (since $t_2\sqsubset t_1$), and $\mbox{{\em Comp}}_{F}^{(13)2} = \{b\}$.  So by the PDU
axiom, $((1\wedge 3)\wedge 2)\Rightarrow \modal{F}b$.  So again:
\[
(1 \ddunify 3)\ddunify 2 = 
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^{(12)3}$}\\
        \attvaltyp{F}{c$/$b}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle,\langle b,t_2\rangle\}\rangle\}
\right.
\]


\subsubsection*{Recording Specificity and Values}

We now turn to the example introduced in \S\ref{informal}, which
demonstrated that keeping track of only the specificity information of
the original default paths was insufficient to guarantee order
independence:

\begin{center}
(1)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^1$}\\
         \attvaltyp{F}{$/$a}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle\}\rangle\}
\right.
$
\hfill
(2)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_2^2$}\\
         \attvaltyp{F}{$/$b}}$}
\end{array}
\left/
\{\langle F,\{\langle b,t_2\rangle\}\rangle\}
\right.
$\\
(3)
$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^3$}\\
        \attvaltyp{F}{$/$d}}$}
\end{array}
\left/
\{\langle F,\{\langle d,t_3\rangle\}\rangle\}
\right.
$

\vspace{0.1in}

$t_3 \sqsubset t_1\sqsubset t_2$\\
$a\sqsubset b$\\
$d \unify b = c$\\
$d \unify a = \bot$
\end{center}


We show that our logic for $\ddunify$ guarantees order independence
for this example.  As before, we calculate $(1\ddunify 2)\ddunify
3$ and $(2\ddunify 3) \ddunify 1$.

First, the translations of the above {\sc tdfs}s produce the following:

\[
\begin{array}{l l}
1 \Rightarrow & \modal{F}a\\
2 \Rightarrow & \modal{F}b\\
3 \Rightarrow & \modal{F}d
\end{array}
\]

By the definition of tails, $F^{12} =\{\langle a,t_1\rangle,\langle
b,t_2\rangle\}$, and by TU2 and PI1$'$, 
$(1\wedge 2)\leadsto \modal{F}\top$.  So
$\mbox{{\em Spec}}_{F}^{12} = \{a\}$, and therefore $\mbox{{\em Comp}}_{F}^{12}=\{a,b\}$.  So by the PDU axiom,
$(1\wedge 2)\Rightarrow\modal{F}a$.

Now, $F^{(12)3}=\{\langle a,t_1\rangle, \langle b,t_2\rangle, \langle
d,t_3\rangle\}$, and by TU2 and PI1$'$, $((1\wedge 2)\wedge 3)\leadsto
\modal{F}\top$.  So $\mbox{{\em Spec}}_{F}^{(12)3} = \{d\}$ and therefore,
$\mbox{{\em Comp}}_{F}^{(12)3} = \{d,b\}$.  So by the PDU axiom, $((1\wedge 2)\wedge
3)\Rightarrow \modal{F}c$.

Now we calculate $(2\ddunify 3)\ddunify 1$.
By the definition of tails, 
$F^{23} = \{\langle b,t_2\rangle,\langle d,t_3\rangle\}$.  And by TU2
and PI1$'$,
$(2\wedge 3)\leadsto \modal{F}\top$.  So $\mbox{{\em Spec}}_{F}^{23} =
\{d\}$ and therefore, 
$\mbox{{\em Comp}}_{F}^{23} = \{b,d\}$.  So by the PDU axiom,
$(2\wedge 3)\Rightarrow \modal{F}c$.

Again by the definition of tails, $F^{(23)1} = \{\langle
b,t_2\rangle,\langle d,t_3\rangle, \langle 
a,t_1\rangle\}$. And by TU2 and PI1$'$, $((2\wedge 3)\wedge
1)\leadsto\modal{F}\top$.  So $\mbox{{\em Spec}}_{F}^{(23)1} = \{d\}$, and therefore,
$\mbox{{\em Comp}}_{F}^{(23)1} = \{b,d\}$.  So by the PDU axiom, $((2\wedge 3)\wedge
1)\Rightarrow \modal{F}c$.  Hence:

\[
(1\ddunify 2)\ddunify 3 = (2\ddunify 3)\ddunify 1 = 
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^{(13)2}$}\\
        \attvaltyp{F}{$/$c}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle,\langle b,t_2\rangle, \langle
d,t_3\rangle\}\rangle\}
\right.
\]

\subsubsection*{Reentrancy}

We now examine a simple example involving reentrancy:


\begin{center}
$a\unify b = \bot$

\[
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$^1$}\\
        \attvaltyp{F}{a}\\
        \attvaltyp{G}{b}}$}
\end{array}
\left/
\{\}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$^2$}\\
        \attval{F}{/\ind{1}}\\
        \attval{G}{/\ind{1}}}$}
\end{array}
\left/
\{\}
\right.
=
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$^{1\wedge 2}$}\\
        \attval{F}{\myvaluebold{a}/\ind{1}\mbox{\small\boldmath $\bot$}}\\
        \attval{G}{\myvaluebold{b}/\ind{1}}}$}
\end{array}
\left/
\{\}
\right.
\]

\end{center}

When translating the input {\sc tdfs}s, we obtain the following
formulae:
\[
\begin{array}{l l}
1\leadsto & \modal{F}a\\
1\leadsto & \modal{G}b\\
2 > & \modal{F}\approx\modal{G}
\end{array}
\]

And the tails are: $F^1=G^1=F^2=G^2=\emptyset$.  

The inferences are as follows:
\[
\begin{array}{l l}
(1 \wedge 2) >\modal{F}\approx\modal{G} & \mbox{RE2}\\
(1 \wedge 2) \leadsto \modal{F}a & \mbox{TU2 and PI1$'$}\\
(1 \wedge 2) \leadsto \modal{G}b & \mbox{TU2 and PI1$'$}
\end{array}
\]

Furthermore, calculating the $\delta$ such that $(1\wedge
2)\Rightarrow \modal{F}\delta$ involves applying the PDU axiom.  that
is, $\delta$ is calculated via the tails.
$F^{12}= G^{12} = \emptyset$.  So $\mbox{{\em Spec}}_F^{12} = \mbox{{\em Comp}}_F^{12} = \emptyset$.
So by the PDU axiom, $\delta = \mbox{{\em Spec}} \unify \mbox{{\em Comp}} \unify \psi$, where $\psi =
\unify \{a,b\}$.  Hence by PDU, $(1\wedge 2)\Rightarrow
\modal{F}\bot$.  Hence $1\ddunify 2$ is as defined above.

\subsection{Theorems and Proofs}
\label{proofs}

We have so far given the axioms of the  logic in which $\ddunify$ is
axiomatised, and we have illustrated how the logic works via some
simple examples.  We should now prove that the version of $\ddunify$
that the logic defines does indeed have the properties we desire.

First, we define precisely the logical consequence relation
$\pduprove$ in terms of which $\ddunify$ is defined:

\begin{defn}
{\bf PDU Deduction} $\pduprove$

A PDU deduction $T$ from the translation of 
two typed default feature structures $\mbox{{\em FS}}_1$ and
$\mbox{{\em FS}}_2$---written respectively as $\tau(\mbox{{\em FS}}_1)$ and
$\tau(\mbox{{\em FS}}_2)$---is a sequence of lines in which every line of
$\tau(\mbox{{\em FS}}_1)\cup\tau(\mbox{{\em FS}}_2)$ 
occurs and for every formula of the form $1
\Rightarrow \modal{\pi}\phi$ or $2\Rightarrow\modal{\pi}\phi$,
there is a formula of the form $(1\wedge
2) \Rightarrow 
\modal{\pi}\chi'$ as a line in $T$, and similarly for
$\rightarrow$, $\leadsto$ and $>$; or $(1 \wedge 2)>\bot$ and
$(1\wedge 2)\not\rightarrow \bot$ and the above conditions hold for
just $\rightarrow$ and $\leadsto$; or $(1\wedge 2)\rightarrow \bot$
and $(1\wedge 2)>\bot$.
\end{defn}

\begin{defn}
$\mbox{FS}_1\ddunify \mbox{FS}_2 = \mbox{FS}_3$ iff\\
$\tau(\mbox{FS}_1),\tau(\mbox{FS}_2)\pduprove \tau(\mbox{FS}_3)$.
\end{defn}

Note that $\pduprove$ is neither closed on the right, nor
supraclassical:
\begin{itemize}
\item   $\Gamma_1,\Gamma_2\pduprove \Gamma_3$ and $\Gamma_3\models
\Gamma_4$ doesn't entail that $\Gamma_1,\Gamma_2\pduprove\Gamma_4$.
\item   $\Gamma_1,\Gamma_2\models \Gamma_3$
doesn't entail that $\Gamma_1,\Gamma_2\pduprove\Gamma_3$.
\end{itemize}

Also note that if for one reason or another one can infer $(1\wedge
2)\rightarrow \bot$ or $(1 \wedge 2)>\bot$ (e.g., the reentrancies in
1 and 2 yield a cycle in the indefeasible part or defeasible part
respectively), then the corresponding {\sc tfs} in the result will be
$\bot$. 

Using the above definitions, we prove the following lemmas and
theorems:

\begin{lemma}
If $1\Rightarrow \modal{\pi}a$ then $a = \mbox{
    Spec}_{\pi}^1\unify \mbox{Comp}_{\pi}^1 
\unify \psi$ where\\ $\psi = \unify\{\psi':
1\leadsto\modal{\pi'}\psi' \mbox{ and } 1 >
\modal{\pi}\approx\modal{\pi'}\}$
\end{lemma}

Note that this lemma implies that if $(1\wedge 2)\Rightarrow
\modal{\pi}\delta$, then $\delta$ is determined by the tails, and not
the defeasible {\sc tfs} of the {\sc tdfs}s.  We now prove this lemma.

{\bf Proof}

By induction on the number of unifications to get 1.

{\bf Base case}: Where 1 is a {\sc tdfs} in the initial {\sc kb}, either:
\begin{enumerate}
\item $1\leadsto\modal{\pi}a$ and $\pi^1=\emptyset$; or
\item   $1\leadsto\modal{\pi}\psi_{\pi}$, $a\sqsubset \psi_{\pi}$, and
$\pi^1 = \{\langle a,t\rangle\}$, where $1\Rightarrow t$.
\end{enumerate}

Consider the first case.  Then $\psi = a$ because for all $\pi'$ such
that $1> \modal{\pi}\approx\modal{\pi'}$ and $1\leadsto
\modal{\pi'}\psi'$,
$a\sqsubseteq \psi'$. For suppose not, then there exists a $\psi'$, such
that $1\leadsto \modal{\pi'}\psi'$, $1\Rightarrow \modal{\pi'}a$ by
REV, and $a\not\sqsubseteq \psi'$.  This contradicts the definition of
{\sc tdfs}s, and the way they are translated into ${\cal L}_{pdu}$.
So $\psi = a$.  So since $\pi^1=\emptyset$, $a = \mbox{{\em Spec}}_{\pi}^1\unify
\mbox{{\em Comp}}_{\pi}^1 \unify \psi$, as required.

Now consider the second case.  Then by REV, the definition of {\sc
tdfs}s, and the translation of {\sc tdfs}s into ${\cal L}_{pdu}$, we
know that
for all $\psi'$ such that
$1\leadsto \modal{\pi'}\psi'$ and
$1>\modal{\pi}\approx\modal{\pi'}$, $a\sqsubseteq \psi'$.  So $a
\sqsubseteq \psi$.  And since $\pi^1 = \{\langle a,t\rangle\}$,
$\mbox{{\em Spec}}_{\pi}^1 = \mbox{{\em Comp}}_{\pi}^1 = \{a\}$.  So $a = \mbox{{\em Spec}}_{\pi}^1 \unify \mbox{{\em Comp}}_{\pi}^1
\unify \psi$, as required.

{\bf The Inductive Step}:  Assume the result holds for $n$
unifications, and 1 is obtained by $n+1$ unifications.  So $1 =
3\wedge 4$, where 3 and 4 where obtained by $\leq n$ unifications
each.  Now, $1\Rightarrow\modal{\pi}\delta$
must have been derived from 3 and 4 by CON or PDU.
If it was derived by PDU, then the result holds by the
definition of PDU.

So suppose 1 were derived by CON.  Then:
\[
\begin{array}{l}
3 \Rightarrow \modal{\pi}a\\
(3>\modal{\pi}\approx\modal{\pi'}) \rightarrow (4 \not >
\modal{\pi'}\top)\\
(3\wedge 4)\not>\modal{\pi_1\pi_2}\approx\modal{\pi_2}
\end{array} 
\]

So if $3> \modal{\pi}\approx\modal{\pi'}$, then $\pi'^4=\emptyset$,
and the reentrancies in 3 and 4 don't produce a cycle.

By the inductive hypothesis:
\[
\begin{array}{l}
a = \mbox{{\em Spec}}_{\pi}^3 \unify \mbox{{\em Comp}}_{\pi}^3 \unify \psi^3,\\
\mbox{where}\\
\psi^3 = \unify\{\psi'^3: 3\leadsto \modal{\pi'}\psi'^3 \mbox{ and }
3>\modal{\pi}\approx\modal{\pi'}\} 
\end{array}
\]
By definition:
\[
\pi^{34} = \cup^{\pi'}_{(3\wedge
4)>\modal{\pi}\approx\modal{\pi'}}\pi'^3 \cup \pi'^4
\]
We now show that  $(3 \wedge 4)
>\modal{\pi}\approx\modal{\pi'}$ iff
$3>\modal{\pi}\approx\modal{\pi'}$.  The if-condition follows from
RE2.  Now consider the only if condition.  
Suppose that $(3\wedge
4)>\modal{\pi}\approx\modal{\pi'}$ and $3\not
>\modal{\pi}\approx\modal{\pi'}$.  
By the following premise of
CON---$(3\wedge 4)\not>\modal{\pi_1\pi_2}\approx\modal{\pi_2}$---we
can assume that $3\wedge 4$ doesn't yield cyclic reentrancies.  So,
there must be a $\pi_1$ and
$\pi_2$, where $\pi_1\neq \pi_2$, and
$3>\modal{\pi}\approx\modal{\pi_1}$,
$4>\modal{\pi_1}\approx\modal{\pi_2}$, and
$3>\modal{\pi_2}\approx\modal{\pi'}$.  For otherwise by RE2, $(3\wedge
4)\not > \modal{\pi}\approx\modal{\pi'}$.  But this contradicts our
assumptions, because $3>\modal{\pi}\approx\modal{\pi_1}$, and
$4\Rightarrow\modal{\pi_1}\phi$, where $\phi\sqsubseteq \top$.  So
$(3\wedge 4)>\modal{\pi}\approx\modal{\pi'}$ only if
$3>\modal{\pi}\approx\modal{\pi'}$. 
So
\[
\{\pi': (3\wedge 4)>\modal{\pi}\approx\modal{\pi'}\} = \{\pi':
3>\modal{\pi}\approx\modal{\pi'}\}
\]
And by assumption, for all $\pi'$ such that
$3>\modal{\pi}\approx\modal{\pi'}$, $\pi'^4=\emptyset$.  So
\[
\pi^{34} = \cup^{\pi'}_{3>\modal{\pi}\approx\modal{\pi'}}\pi'^3 =
\pi^3
\]
Now consider $\pi'$ such that $3>\modal{\pi}\approx\modal{\pi'}$.
Then $(3\wedge 4) \leadsto\modal{\pi'}\psi'$ iff $3\leadsto
\modal{\pi'}\psi'$, because by the premises,
$4\not\rightarrow\modal{\pi'}\top$.  So:
\[
\begin{array}{l}
\{\psi':(3\wedge 4)\leadsto\modal{\pi'}\psi' \mbox{ and } (3\wedge
4)>\modal{\pi}\approx\modal{\pi'}\} = 
\{\psi':3\leadsto\modal{\pi'}\psi' \mbox{ and } 
3>\modal{\pi}\approx\modal{\pi'}\}\\
\mbox{{\em Spec}}_{\pi}^{34} =  \mbox{{\em Spec}}_{\pi}^3\\
\mbox{{\em Comp}}_{\pi}^{34} =  \mbox{{\em Comp}}_{\pi}^3
\end{array}
\]
So 
\[
a = \mbox{{\em Spec}}_{\pi}^1\unify \mbox{{\em Comp}}_{\pi}^1\unify \psi
\]
as required.  $\Box$


\begin{lemma}
$\ddunify$ is a function.  That is, $\Gamma_1\ddunify \Gamma_2$ is a unique
{\sc tdfs}.
\end{lemma}

{\bf Proof}

Suppose not.  Then $\tau(\Gamma_1)$ and $\tau(\Gamma_2)$ yield either
\begin{enumerate}
\item   $(1\wedge 2)>\modal{\pi}\approx\modal{\pi'}$ and $(1\wedge 2)\not >
\modal{\pi}\approx\modal{\pi'}$; or
\item   
$(1\wedge 2)\Rightarrow\modal{\pi}\phi$, $(1\wedge
2)\Rightarrow\modal{\pi}\psi$, 
and $\phi\neq \psi$; or
\item   $(1\wedge 2)\leadsto \modal{\pi}a$, $(1\wedge
2)\Rightarrow \modal{\pi}b$, and $b\not\sqsubseteq a$; or
\item   $(1\wedge 2)\rightarrow \modal{\pi}\approx\modal{\pi'}$ and
$(1\wedge 2)\not >\modal{\pi}\approx\modal{\pi'}$.
\end{enumerate}
Case 1 is impossible by the axioms of the logic. Case 2 isn't
possible by lemma 1.  Case 3 is  impossible by lemma 1, and case
4 is impossible by RE1.  $\Box$


\begin{lemma}
$\ddunify$ is commutative.
\end{lemma}

{\bf Proof}

PDU, CON, TU1, TU2 and the reentrancy axioms do not distinguish the
commutative order.  So for all $\pi$, $\pi'$, and $\phi$:
\[
\begin{array}{l l l}
(1\wedge 2)\Rightarrow \modal{\pi}\phi & \mbox{iff} & (2\wedge
1)\Rightarrow\modal{\pi}\phi \\
(1\wedge 2)> \modal{\pi}\approx\modal{\pi'} & \mbox{iff} & (2\wedge
1)> \modal{\pi}\approx\modal{\pi'} \\
(1\wedge 2)\leadsto \modal{\pi}\phi & \mbox{iff} & (2\wedge
1)\leadsto\modal{\pi}\phi \\
(1\wedge 2)\rightarrow \modal{\pi}\approx\modal{\pi'} & \mbox{iff} & (2\wedge
1)\rightarrow\modal{\pi}\approx\modal{\pi'}
\end{array}
\]
So by the tag axioms, $\widehat{1 \wedge 2} = \widehat{2
\wedge 1}$.  And
therefore $\Gamma_1\ddunify \Gamma_2$ and $\Gamma_2\ddunify \Gamma_1$
have identical paths, reentrancies and tags.

Furthermore,
\[
\begin{array}{r l}
\pi^{12} = & \cup^{\pi'}_{(1\wedge
2)>\modal{\pi}\approx\modal{\pi'}}\pi'^1\cup\pi'^2\\
= & \cup^{\pi'}_{(2\wedge
1)>\modal{\pi}\approx\modal{\pi'}}\pi'^2\cup\pi'^1\\
= & \pi^{21}
\end{array}
\]
So  $\Gamma_1\ddunify \Gamma_2$ and $\Gamma_2\ddunify \Gamma_1$ also
have identical tails.  Therefore 
$\Gamma_1\ddunify \Gamma_2 = \Gamma_2\ddunify \Gamma_1$. $\Box$

\begin{lemma}
$\ddunify$ is associative.
\end{lemma}

{\bf Proof}

We need to show:
\begin{enumerate}
\item   $((1 \wedge 2)\wedge 3)\leadsto\modal{\pi}\phi$ iff $(1\wedge
(2\wedge 3))\leadsto \modal{\pi}\phi$.
\item   $((1\wedge 2)\wedge 3)\rightarrow
\modal{\pi}\approx\modal{\pi'}$ iff $(1\wedge (2\wedge
3))\rightarrow\modal{\pi} \approx\modal{\pi'}$.
\item   $((1\wedge 2)\wedge 3)>
\modal{\pi}\approx\modal{\pi'}$ iff $(1\wedge (2\wedge
3))>\modal{\pi} \approx\modal{\pi'}$.
\item   $\pi^{(12)3}=\pi^{1(23)}$
\item   $((1\wedge 2)\wedge 3)\Rightarrow\modal{\pi}\phi$ iff
$(1\wedge (2\wedge 3))\Rightarrow\modal{\pi}\phi$.
\end{enumerate}
Cases 1 and 2 hold because typed unification is associative, and the
axioms on $\leadsto$ and $\rightarrow$ model typed
unification.

We now show Case 3: that the default reentrancies are associative.  
So,
suppose that\\
$((1\wedge 2)\wedge 3)>\modal{\pi}\approx\modal{\pi'}$.
Then by RE1 and RE2, this holds iff:
\begin{examples}
\item   [a]     $(1\wedge 2)>\modal{\pi}\approx\modal{\pi_1}$,
$3>\modal{\pi_1}\approx\modal{\pi_2}$, and $(1\wedge
2)>\modal{\pi_2}\approx\modal{\pi'}$; or
\item   [b]     $3>\modal{\pi}\approx\modal{\pi_1}$,
$(1\wedge 2)>\modal{\pi_1}\approx\modal{\pi_2}$, and 
$3>\modal{\pi_2}\approx\modal{\pi'}$.\footnotemark
\end{examples}
\footnotetext{We allow for the possibility here that there are
identities between $\pi$, $\pi_1$, $\pi_2$, and $\pi'$.}

Suppose Case (a).  Then since $(1\wedge 2)>
\modal{\pi}\approx\modal{\pi_1}$,
this holds iff:
\begin{examples}
\item   [a]
\begin{subexamples}
\item   [i]     $1>\modal{\pi}\approx\modal{\pi_3}$,
$2>\modal{\pi_3}\approx\modal{\pi_4}$, and
$1>\modal{\pi_4}\approx\modal{\pi_1}$; or
\item   [ii]    $2>\modal{\pi}\approx\modal{\pi_3}$,
$1>\modal{\pi_3}\approx\modal{\pi_4}$, and
$2>\modal{\pi_4}\approx\modal{\pi_1}$.
\end{subexamples}
\end{examples}
And also, since $(1\wedge 2) >\modal{\pi_2}\approx\modal{\pi'}$, case
(a) holds iff (iii) or (iv) hold:
\begin{examples}
\item [a]
\begin{subexamples}
\item [iii] $1>\modal{\pi_2}\approx\modal{\pi_5}$, $2 >
  \modal{\pi_5}\approx\modal{\pi_6}$ and $1 >
  \modal{\pi_6}\approx\modal{\pi'}$; or
\item [iv] $2>\modal{\pi_2}\approx\modal{\pi_5}$, $1 >
  \modal{\pi_5}\approx\modal{\pi_6}$ and $2 >
  \modal{\pi_6}\approx\modal{\pi'}$.
\end{subexamples}
\end{examples}

Suppose (i) and (iii) hold.  Then by RE2 and AND:
\[
(2\wedge
3)>(\modal{\pi_3}\approx\modal{\pi_4} \wedge
\modal{\pi_1}\approx\modal{\pi_2} \wedge
\modal{\pi_5}\approx\modal{\pi_6})
\]
And by RE2 and AND:
\[
\begin{array}{r l}
(1\wedge
(2\wedge 3))> ( & \modal{\pi}\approx\modal{\pi_3}\wedge
\modal{\pi_3}\approx\modal{\pi_4} \wedge
\modal{\pi_4}\approx\modal{\pi_1}\wedge \\
& \modal{\pi_1}\approx\modal{\pi_2} \wedge \modal{\pi_2}\approx
\modal{\pi_5} \wedge \modal{\pi_5}\approx\modal{\pi_6} \wedge
\modal{\pi_6}\approx\modal{\pi'}) 
\end{array}
\]
So by ARE and CR,
 $(1\wedge (2\wedge 3))>\modal{\pi}\approx\modal{\pi'}$.  

The other permutations of (i--iv) are symmetric to this case. 
And
the case for (b) is symmetric to case (a).  So
$((1\wedge 2)\wedge 3)>\modal{\pi}\approx\modal{\pi'}$ entails
$(1\wedge (2\wedge 3))>\modal{\pi}\approx\modal{\pi'}$.  The argument
that $(1\wedge (2\wedge 3))>\modal{\pi}\approx\modal{\pi'}$ entails
$((1\wedge 2)\wedge 3)>\modal{\pi}\approx\modal{\pi'}$ is similar.
Hence reentrancies are associative.

Now we prove 4: $\pi^{(12)3}=\pi^{1(23)}$
\[
\begin{array}{r l}
\pi^{(12)3}= & \cup^{\pi'}_{((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}} \pi'^{12} \cup \pi'^3\\
= & \cup^{\pi'}_{((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}} \pi'^3 \cup (\cup^{\pi''}_{(1\wedge
2)>\modal{\pi'}\approx\modal{\pi''}} \pi''^1 \cup\pi''^2)
\end{array}
\]
Now if $(1\wedge 2)>\modal{\pi'}\approx\modal{\pi''}$, then $((1\wedge
2)\wedge 3)>\modal{\pi'}\approx\modal{\pi''}$ by RE2.  So if in
addition $((1\wedge 2) \wedge 3)>\modal{\pi}\approx\modal{\pi'}$, then
by ARE and AND, $((1 \wedge 2)\wedge 3)>
\modal{\pi}\approx\modal{\pi''}$. So since $(1\wedge 2) >
\modal{\pi'}\approx\modal{\pi'}$, 
\[
\cup^{\pi'}_{((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}} \cup^{\pi''}_{(1\wedge
2)>\modal{\pi'}\approx\modal{\pi''}} \pi''^1 \cup\pi''^2 =
\cup^{\pi'}_{((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}} \pi'^1\cup \pi'^2
\]
Hence
\[
\pi^{(12)3}=  \cup^{\pi'}_{((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}} \pi'^1 \cup \pi'^2 \cup \pi'^3
\]
By a similar argument:
\[
\pi^{1(23)}= \cup^{\pi'}_{(1\wedge (2\wedge
3))>\modal{\pi}\approx\modal{\pi'}} \pi'^1 \cup \pi'^2 \cup \pi'^3
\]
But $\{\pi':((1\wedge 2)\wedge
3)>\modal{\pi}\approx\modal{\pi'}\} =
\{\pi':(1\wedge (2\wedge
3))>\modal{\pi}\approx\modal{\pi'}\}$.  So $\pi^{(12)3}=\pi^{1(23)}$.

Now we prove 5:
$((1\wedge 2)\wedge 3)\Rightarrow\modal{\pi}\phi$ iff
$(1\wedge (2\wedge 3))\Rightarrow\modal{\pi}\phi$.

Suppose $((1\wedge 2)\wedge 3)\Rightarrow\modal{\pi}\delta_1$ and
$(1\wedge (2\wedge 3))\Rightarrow\modal{\pi}\delta_2$.  Then
by lemma 1:
\[
\begin{array}{r l}
\delta_1 = & \mbox{{\em Spec}}^{(12)3}_{\pi} \unify \mbox{{\em Comp}}^{(12)3}_{\pi} \unify \{\psi_i:
((1\wedge 2)\wedge 3)>\modal{\pi}\approx\modal{\pi_i} \mbox{ and }
((1\wedge 2)\wedge 3)\leadsto\modal{\pi_i}\psi_i\}\\
= & \mbox{{\em Spec}}^{1(23)}_{\pi} \unify \mbox{{\em Comp}}^{1(23)}_{\pi} \unify 
\{\psi_i:
(1\wedge (2\wedge 3))>\modal{\pi}\approx\modal{\pi_i} \mbox{ and }
(1\wedge (2\wedge 3))\leadsto\modal{\pi_i}\psi_i\}\\
= & \delta_2
\end{array}
\]
So $\ddunify$ is associative.  $\Box$

\begin{theorem}
$\ddunify$ is an order independent function.
\end{theorem}

{\bf Proof}

Follows immediately from lemmas 2, 3 and 4.

\begin{theorem}
{\em The Typed Unification Property}\\
Suppose $(1\wedge 2)>\modal{\pi}\approx\modal{\pi_i}$, $1\leq i\leq n$
and if $(1\wedge 2)>\modal{\pi}\approx\modal{\pi'}$ then $\pi'= \pi_i$
for some $i$, $1\leq i\leq n$.\\  Let:
\[
\begin{array}{l l}
\phi = & \{x_i^1: 1\Rightarrow \modal{\pi_i}x_i^1, 1\leq i\leq n\} \cup\\
& \{x_i^2: 2\Rightarrow \modal{\pi_i}x_i^2, 1\leq i\leq n\}
\end{array}
\]
and
\[
(1\wedge 2)\Rightarrow\modal{\pi}\delta
\]
Then if $\delta \neq \bot$ and $\unify \phi \neq \bot$, then $\delta =
\unify \phi$.
\end{theorem}

{\bf Proof}

By lemma 1, $(1\wedge 2)\Rightarrow\modal{\pi}\delta$, where
\[
\begin{array}{l l}
\delta = & \mbox{{\em Spec}}^{12}_{\pi}\unify \mbox{{\em Comp}}^{12}_{\pi} \unify \psi \mbox{ where}\\
\psi = & \unify\{\psi_i: (1\wedge 2)\leadsto\modal{\pi_i}\psi_i, 1\leq
i\leq n\}
\end{array}
\]
Furthermore for $1\leq i\leq n$, by lemma 1:
\[
\begin{array}{l l}
x^1_i = & \mbox{{\em Spec}}^1_{\pi_i} \unify \mbox{{\em Comp}}^1_{\pi_i} \unify \chi^1_i \mbox{
where}\\
\chi^1_i = & \unify \{\zeta^1_j: 1 >\modal{\pi_i}\approx\modal{\pi_j}
\mbox{ and } 1\leadsto \modal{\pi_j}\zeta^1_j\} \mbox{ and}\\
x^2_i = & \mbox{{\em Spec}}^2_{\pi_i} \unify \mbox{{\em Comp}}^2_{\pi_i} \unify \chi^2_i \mbox{
where}\\
\chi^2_i = & \unify \{\zeta^2_j: 2 >\modal{\pi_i}\approx\modal{\pi_j}
\mbox{ and } 2\leadsto \modal{\pi_j}\zeta^1_j\}
\end{array}
\]
So by TU1, TU2 PI1$'$, ARE and REV:
\[
\psi = 
%\unify(\cup_{1\leq i\leq n}(\{\zeta^1_j: 1 >\modal{\pi_i}\approx\modal{\pi_j}
%\mbox{ and } 1\leadsto \modal{\pi_j}\zeta^1_j\}\cup
%\{\zeta^2_j: 2 >\modal{\pi_i}\approx\modal{\pi_j}
%\mbox{ and } 1\leadsto \modal{\pi_j}\zeta^1_j\}))\\
%=
\unify \{\chi^1_i,\chi^2_i: 1\leq i \leq n\})
\]
Now
\[
\pi^{12} = \cup_{1\leq i\leq n} \pi_i^1\cup \pi_i^2
\]
We now show $\mbox{{\em Spec}}^{12}_{\pi} \subseteq 
\cup_{1\leq i\leq n} \mbox{{\em Spec}}^1_{\pi_i} \cup \mbox{{\em Spec}}^2_{\pi_i}$.  
Suppose that $v\in \mbox{{\em Spec}}^{12}_{\pi}$. Then 
$\langle v,t_{v}\rangle \in \pi_i^1$ or $\langle v, t_{v}\rangle \in
\pi_i^2$
for some $i$,
such that $t_{v}$ is a most specific type in $\pi^{12}$.  Suppose
without loss of generality that $\langle v,t_{v}\rangle\in \pi_i^1$.
Then $t_{v}$ 
must be a most specific type in $\pi_i^1$.  And if $v\unify \chi_i^1 =\bot$,
then $v \unify \psi = \bot$, and so $v\not\in \mbox{{\em Spec}}^{12}_{\pi}$.  So
$v\unify \chi_i^1\neq \bot$.  Hence by definition, $v\in
\mbox{{\em Spec}}_{\pi_i}^1$.  So $\mbox{{\em Spec}}^{12}_{\pi} \subseteq \cup_{1\leq i\leq n}
\mbox{{\em Spec}}^1_{\pi_i} 
\cup \mbox{{\em Spec}}^2_{\pi_i}$.

Now consider $v\in \cup_{1\leq i\leq n} \mbox{{\em Spec}}_{\pi_i}^1 \cup \mbox{{\em Spec}}_{\pi_i}^2$
where $v\not\in \mbox{{\em Spec}}_{\pi}^{12}$.  Then since $\unify\phi\neq\bot$,
$v\unify \mbox{{\em Spec}}_{\pi}^{12}\neq \bot$, since by the above
$\mbox{{\em Spec}}_{\pi}^{12}\subseteq \phi$ and $v\in \phi$.  Furthermore, $v\unify
\{\chi_i^1,\chi_i^2: 1\leq i\leq n\} \neq \bot$, because otherwise
$\unify \phi= \bot$.  So $v\unify \psi \neq \bot$.  So by 
definition, $v\in \mbox{{\em Comp}}_{\pi}^{12}$.  So
\[
\cup_{1\leq i\leq n} \mbox{{\em Spec}}_{\pi_i}^1\cup \mbox{{\em Spec}}_{\pi_i}^2\subseteq \mbox{{\em Spec}}_{\pi}^{12}
\cup \mbox{{\em Comp}}_{\pi}^{12}
\]

Now consider $w\in \cup_{1\leq i\leq n} \mbox{{\em Comp}}_{\pi_i}^1\cup \mbox{{\em Comp}}_{\pi_i}^2$.
Suppose without loss of generality that $w\in \mbox{{\em Comp}}_{\pi_i}^1$.  Then if
$w\unify \mbox{{\em Spec}}_{\pi_j}^1 = \bot$ or $w\unify \mbox{{\em Spec}}_{\pi_j}^2 = \bot$ for some
$j$, $\unify \phi = \bot$, contradicting our assumption.  So $w \unify
\mbox{{\em Spec}}_{\pi}^{12} \neq \bot$.  Similarly, if $w\unify \chi_j^1=\bot$ or $w
\unify \chi_j^2=\bot$ for some $j$, then $\unify \phi = \bot$.  So
$w\unify \psi \neq \bot$.  So $w\in \mbox{{\em Comp}}_{\pi}^{12}$.  Hence:
\[
\cup_{1\leq i\leq n} \mbox{{\em Comp}}_{\pi_i}^1\cup \mbox{{\em Comp}}_{\pi_i}^2 \subseteq 
\mbox{{\em Comp}}_{\pi}^{12}
\]

Now choose $x\in \pi_i^1$.  Suppose $x\not\in \mbox{{\em Comp}}_{\pi_i}^1$.  Then
$x\unify \mbox{{\em Spec}}_{\pi_i}^1 = \bot$ or $x\unify \chi_i^1=\bot$.  

If $x\unify
\mbox{{\em Spec}}_{\pi_i}^1 = \bot$, then $x\unify \{\mbox{{\em Spec}}_{\pi_i}^1,\mbox{{\em Spec}}_{\pi_i}^2: 1\leq
i\leq n\} = \bot$.  But 
$\mbox{{\em Spec}}_{\pi}^{12} \unify \mbox{{\em Comp}}_{\pi}^{12} \sqsubseteq 
\unify \{\mbox{{\em Spec}}_{\pi_i}^1,\mbox{{\em Spec}}_{\pi_i}^2: 1\leq
i\leq n\}$, since 
$\mbox{{\em Spec}}_{\pi}^{12} \cup \mbox{{\em Comp}}_{\pi}^{12} \supseteq 
\{\mbox{{\em Spec}}_{\pi_i}^1,\mbox{{\em Spec}}_{\pi_i}^2: 1\leq
i\leq n\}$.  So $x\unify \delta = \bot$.  So if $x\in \mbox{{\em Comp}}_{\pi}^{12}$,
then $x\unify \delta = \delta =\bot$.  This contradicts our
hypothesis.  So $x\not\in \mbox{{\em Comp}}_{\pi}^{12}$.

If $x\unify \chi_i^1=\bot$, then $x\unify \psi = \bot$, and so
$x\unify \delta= \bot$.  Therefore, if $x\in \mbox{{\em Comp}}_{\pi}^{12}$, then
$x\unify \delta = \delta = \bot$.  So $x\not\in \mbox{{\em Comp}}_{\pi}^{12}$.

Hence $\cup_{1\leq i\leq n} \mbox{{\em Comp}}_{\pi_i}^1\cup \mbox{{\em Comp}}_{\pi_i}^2 \supseteq
\mbox{{\em Comp}}_{\pi}^{12}$.  So:
\[
\begin{array}{r l l}
\cup_{1\leq i\leq n} \mbox{{\em Comp}}_{\pi_i} ^1\cup \mbox{{\em Comp}}_{\pi_i}^2 = &
\mbox{{\em Comp}}_{\pi}^{12} & \mbox{ and therefore}\\
\cup_{1\leq i\leq n} \mbox{{\em Spec}}_{\pi_i}^1 \cup \mbox{{\em Comp}}_{\pi_i} ^1\cup \mbox{{\em Spec}}_{\pi_i}^2
\cup \mbox{{\em Comp}}_{\pi_i}^2 = & \mbox{{\em Spec}}_{\pi}^{12} \cup \mbox{{\em Comp}}_{\pi}^{12} &
\end{array}
\]
So, since $\unify \{\chi_i^1,\chi_i^2: 1\leq i \leq n\} = \psi$,
\[
\begin{array}{r l}
\unify \phi = & \mbox{{\em Spec}}_{\pi}^{12}\unify \mbox{{\em Comp}}_{\pi}^{12} \unify \psi\\
= & \delta
\end{array}
\]
$\Box$

The above theorem confirms that $\ddunify$ reduces to typed
unification when no conflict arises.  But `no conflict' doesn't mean
`no conflict in the {\sc fs} components of the {\sc tdfs}s'.
The crucial extra premise is: $(1\wedge
2)\Rightarrow\modal{\pi}\delta$ where $\delta\neq\bot$.  By lemma 1,
$\delta$ is defined by the tails, and not the {\sc fs}s.

Without this condition, the theorem would be one where $\ddunify$
reduces to $\unify$ when there is no conflict among the {\sc fs}
components of the {\sc tdfs}s.  But this is not a valid
result.  The following example illustrates this:

$
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_1^{1}$}\\
        \attvaltyp{F}{$/$a}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle,\langle c,t_2\rangle\}\rangle\}
\right.
\ddunify
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^{2}$}\\
        \attvaltyp{F}{$/$b}}$}
\end{array}
\left/
\{\langle F,\{\langle b,t_3\rangle\}\rangle\}
\right.
$

Where:
\begin{center}
$t_3\sqsubset t_1\sqsubset t_2$\\
$a\unify b = d$, $c\unify a = \bot$, $c \sqsubset b$

{\modsmalltree{4}{
{\node{a}{a}} && {\node{b}{b}}\\
& {\node{d}{d}} && {\node{c}{c}}\\
&& {\node{bot}{$\bot$}}}
\nodeconnect{a}{d}
\nodeconnect{b}{d}
\nodeconnect{b}{c}
\nodeconnect{d}{bot}
\nodeconnect{c}{bot}}
\end{center}

In the above, the {\sc fs}s components do not conflict, but the tails
do.  If the Typed Unification Property held in cases where there was
no conflict among the {\sc fs} components, then we should be able to
infer that $(1\wedge 2)\Rightarrow \modal{F}d$ from the axioms.

But this does not hold.  By the definition of tails, $\mbox{{\em
Spec}}$ and $\mbox{{\em Comp}}$, $\mbox{{\em Spec}}_{F}^{12} = \{b\}$,
$\mbox{{\em Comp}}_{F}^{12} = \{a,b,c\}$, and so $\mbox{{\em
Spec}}_{F}^{12}\unify \mbox{{\em Comp}}_{F}^{12} = \bot$ (and {\em
not} $d$).  Therefore:
\[
FS1\ddunify FS2 =
\begin{array}{c}
\mbox{\tiny $\avmplus{\att{t$_3^{12}$}\\
        \attvaltyp{F}{$/${\boldmath $\bot$}}}$}
\end{array}
\left/
\{\langle F,\{\langle a,t_1\rangle, \langle c, t_2\rangle,
\langle b,t_3\rangle\}\rangle\}
\right.
\]
We could define {\em Comp} in the PDU axiom, so that {\em Comp}
prioritises the defaults that are compatible with the values in {\em
Spec}.  Here, this would mean that $a$ would be in {\em Comp} but $c$
would not, because $c$ is associated with a more general type than $a$
is, and $c$ is incompatible with $a$ thereby yielding priority to $a$.
The defeasible result on the $F$ path would then be $d$ rather than
$\bot$.  However, this modification to the PDU axiom, while preserving
order independence, increases complexity.  It also does not ultimately
produce an operation more integrated with typing in general; the
reasons for this are discussed in detail in Lascarides and Copestake
(1995).  It does show, however, that the conditional logic approach to
defining order independent $\ddunify$ provides several options.

The Typed Unification Property is not guaranteed when the defeasible
{\sc fs} components do not conflict.  But the only added condition
here is that $\delta\neq \bot$, which is quite weak.  This permits
$\ddunify$ to reduce to $\unify$ in certain cases where the tails are
in conflict.

Because {\sc tdfs}s contain more information than the information in
the {\sc fs} components alone, the notion of `conflict' is more
complex than in Carpenter (1992, 1993) and Bouma (1992).  Their
definitions of default unification correspond to the situations where
we are unifying structures in the initial {\sc kb} (see
\S\ref{comparison}) and we can prove for these cases that the typed
unification property is one where $\ddunify$ reduces to $\unify$ when
there is no conflict among the {\sc fs} components:
\begin{corollary}
If {\sc tdfs}1 and {\sc tdfs2} are basic {\sc tdfs}s, and
$(1\wedge 2)>\modal{\pi}\approx\modal{\pi_i}$ for $1\leq i\leq n$, and \\if
$(1\wedge 2)>\modal{\pi}\approx\modal{\pi'}$, then $\pi' = \pi_i$ for
some $i$, \\and $\unify \phi \neq \bot$, where
\[
\begin{array}{l l}
\phi = & \{x_i^1: 1\Rightarrow \modal{\pi_i}x_i^1, 1\leq i\leq n\} \cup\\
& \{x_i^2: 2\Rightarrow \modal{\pi_i}x_i^2, 1\leq i\leq n\}
\end{array}
\]
Then $(1\wedge 2)\Rightarrow \modal{\pi}(\unify \phi)$
\end{corollary}

{\bf Proof}

By lemma 1, $x_i^1 = \mbox{{\em Spec}}_{\pi_i}^1 \unify \mbox{{\em Comp}}_{\pi_i}^1 \unify \psi_i^1$,
where\\ $\psi_i^1 =\{\chi_j^1: 1\leadsto \modal{\pi_j}\chi_j^1 \mbox{
and }
1\leadsto \modal{\pi_i}\approx\modal{\pi_j}\}$.  Similarly for 2.

And by lemma 1, $(1\wedge 2)\Rightarrow\modal{\pi}\delta$, where
$\delta = \mbox{{\em Spec}}_{\pi}^{12} \unify \mbox{{\em Comp}}_{\pi}^{12}\unify \psi$, and\\ $\psi =
\{\zeta_i, (1\wedge 2)\leadsto \modal{\pi_i}\zeta_i, 1\leq i\leq n\}$.

Since 1 is a basic {\sc fs}, $\pi_i^1 = \emptyset$, or $\pi_i^1 = x_i^1$,
and $x_i^1\sqsubseteq \psi_i^1$ by the definition of {\sc tdfs}s 
and their translation into ${\cal L}_{pdu}$, and the axiom REV.
Similarly for 2.

So
\[
\begin{array}{r l}
\pi^{12} = & \cup_{1\leq i\leq n} \pi_i^1\cup \pi_i^2\\
\subseteq & \{\langle x^1_i,t_1\rangle, \langle x_i^2,t_2\rangle: 1\leq
i \leq n\} 
\end{array}
\]
Where $t_1$ and $t_2$ are the root types of 1 and 2.   
So $\mbox{{\em Spec}}_{\pi}^{12} \unify \mbox{{\em Comp}}_{\pi}^{12} \sqsupseteq \unify \phi$.
Furthermore, by TU1, TU2 and REV, $\psi \sqsupseteq \unify
\{\psi_i^1,\psi_i^2: 1\leq i\leq n\}\sqsupseteq \unify \phi$.  So
$\mbox{{\em Spec}}_{\pi}^{12}\unify \mbox{{\em Comp}}_{\pi}^{12} \unify \psi \sqsupseteq \unify \phi$.
That is, $\delta\sqsupseteq \unify \phi$.
And since $\unify\phi\neq \bot$, $\delta\neq \bot$.  So by theorem 2
(The Typed Unification Property), $\delta
= \unify \phi$.  $\Box$


\subsection{Different Tails for Different Sublanguages}
\label{index}
% If we are going in for wholesale reorganisation, it might make sense
% to put this section after some linguistic examples and also
% after the discussion of complexity.  Since it isn't essential in
% order to understand any of the rest of the paper, it could go in as
% a concluding section.

If we restrict the kinds of {\sc tdfs}s that are permitted, then we
can reduce the length of tails, without sacrificing the properties we
have proved for $\ddunify$ --- namely, order independence and
reduction to monotonic typed unification where there are no conflicts.
There is a balance between restricting the language of {\sc tdfs}s,
and the potential length of tails.  The more restricted the language,
the less of the unification history needs to be recorded in order to
retain order independence.  The computational complexity of $\ddunify$ is
$O(nt^2)$ where $n$ is the number of nodes in the {\sc tdfs}s and $t$ is the
length of the tails, so reducing the length of the tails would bring
$\ddunify$ closer in actual complexity to monotonic typed
unification.

First, consider the following sublanguage: suppose that whenever
$t_1\sqsubset t_2$, then
for any {\sc tdfs}s of the forms below, either $a\unify b =\bot$,
or $a\sqsubseteq b$.
\[
\mbox{\tiny $\avmplus{\att{t$_1$}\\
\attvaltyp{F}{/a}}$}
\mbox{ and }
\mbox{\tiny $\avmplus{\att{t$_2$}\\
\attvaltyp{F}{/b}}$}
\]

With this sublanguage, we can reduce the amount of information in tails,
and yet the existing axioms will still produce an order independent
$\ddunify$ which reduces to typed unification where there is no
conflict.  The definition of tails for the base case remains the same.
The revised definition of how to construct new tails from old ones is
given below:
\[
\pi^{12} = \cup^{\pi'}_{(1\wedge 2)>\modal{\pi}\approx\modal{\pi'}}
\{\langle a,t\rangle: \langle a,t\rangle \in \pi'^1\cup
\pi'^2 \mbox{ and } \forall \langle a',t'\rangle\in \cup^{\pi'}
(\pi'^1\cup \pi'^2),
t'\not\sqsubset t\}
\]

Now, $\pi^{12}$ is not constructed by set union on $\pi^1$ and $\pi^2$,
and all the tails reentrant with $\pi$.  Rather, it just retains the
values associated with the most specific types.  Indeed, $\pi^{12}$ is
potentially shorter than $\pi^1$ or $\pi^2$.
For example, if $\pi^1=\{\langle a,t_1\rangle,\langle b,t_2\rangle\}$,
$\pi^2= \{\langle c,t_3\rangle\}$, where $t_3\sqsubset t_2$ and
$t_3\sqsubset t_1$, and there are no reentrancies with
$\pi$, then $\pi^{12} = \{\langle c,t_3\rangle\}$.  Whereas under the
old definition, $\pi^{12}$ was $\{\langle a,t_1\rangle, \langle
b,t_2\rangle, \langle c,t_3\rangle\}$.  

With this new definition of tails and the
existing axioms of the logic, all the above lemmas and theorems hold,
but only for the restricted language.\footnote{
The proof is left as an exercise for the reader.}  
In fact, this new definition of tails is analogous to the strategy for
defining $\ddunify$ that we mentioned in \S\ref{informal}, which
involved reasoning about a hierarchy of indices, which recorded the
specificity from which default paths originated.  The new definition
of tails, like the index strategy, records essentially only the most
specific defaults, and doesn't keep track of overridden values.
Recording this amount of information from the unification history is
sufficient for order independence on this restricted sublanguage.

This sublanguage might be appropriate for some linguistic
applications: for example, it is sufficient for defining the type
constraints given in Figure~\ref{final-eg}.  The problem is the
difficulty in ensuring that the extra condition holds.  In general, it
is highly desirable for usability of a formalism that any linguistic
description can be checked efficiently to ensure that it is
well-formed according to the language.  But even if we assume that
defaults are always introduced by the type hierarchy, and check that
the extra sublanguage condition holds of that, this does not ensure
that it will hold of any possible unification.  For example, suppose
that $t_1$ and $t_2$ have the following constraints (which do meet the
condition):\\
\begin{tabular}{l}
{\tiny $\avmplus{\att{t$_1$}\\
\attvaltyp{F}{$/$a}}$}
\hspace{0.2in}
{\tiny $\avmplus{\att{t$_2$}\\
\attvaltyp{F}{$/$b}}$}\\
where $t1 \sqsubset t2$, $a \sqsubset b$
\end{tabular}\\
If we also have $c$ such that $b\sqcap c = d$ and $d \sqcap a = e$ then
unifying a {\sc tdfs} of type $t_2$ with the strict information that the
value of $F$ is $c$ gives us the following {\sc tdfs}s which would not meet the
condition for the sublanguage if unified:\\
\begin{tabular}{l}
{\tiny $\avmplus{\att{t$_1$}\\
\attvaltyp{F}{$/$a}}$ }
\hspace{0.2in}
{\tiny $\avmplus{\att{t$_2$}\\
\attvaltyp{F}{c$/$d}}$}\\
$d \sqcap a \neq \bot$, $a \not \sqsubseteq d$
\end{tabular}\\
Other examples involving default information can be devised.  A more
stringent but statically checkable condition would be to require all
specified default values to be maximally specific.  This might be
suitable for some applications --- it is still adequate for the
example in Figure~\ref{final-eg} for instance --- but it is clearly
significantly less expressive.

We now consider a version of $\ddunify$ for the sublanguage used in
Young and Rounds (1993), assuming that multiple solutions are treated
as an error condition.  That is, we remove reentrancies, types, and
the subsumption relation on types.  Then we define tails as follows:
For the base case:
\[
\pi^1 =
\left\{
\begin{array}{l l}
\{a\} & \mbox{If } 1\Rightarrow\modal{\pi}a \mbox{ and }
1\not\leadsto\modal{\pi}a\\ 
\emptyset & \mbox{otherwise}
\end{array}
\right.
\]
We build tails as follows. Suppose 
$(1\wedge 2)\leadsto \modal{\pi}\psi$.  Then:
\[
\pi^{12} =
\left\{
\begin{array}{l l}
\pi^1\unify \pi^2 & \mbox{If } \pi^1\unify \psi\neq\bot \mbox{ and }
\pi^2\unify \psi\neq\bot\\
\pi^1 & \mbox{If } \pi^1\unify \psi \neq \bot \mbox{ and } \pi^2\unify\psi =
\bot\\
\pi^2 & \mbox{If } \pi^1\unify \psi = \bot \mbox{ and } \pi^2\unify\psi \neq
\bot\\
\emptyset & \mbox{If } \pi^1\unify \psi = \bot \mbox{ and } \pi^2\unify\psi =
\bot
\end{array}
\right.
\]
And we define:
\[
\mbox{{\em Spec}}_{\pi}^1 = \mbox{{\em Comp}}_{\pi}^1 = \pi^1
\]
Now, all tails are empty or singletons, and hence in general they are
smaller than they were for the general language.  But this new
definition of tails still produces an order independent version of
$\ddunify$.  Obviously now, we have to change the axioms slightly,
because default reentrancies must be removed.  So we remove RE2, and
modify CON and PDU to the more restricted versions given below:
\begin{itemize}
\item   [CON]   {\tt Consistency}\\
\begin{tabular}[t]{l}
$1\Rightarrow \modal{\pi}a$\\
$(1\rightarrow \modal{\pi}\approx\modal{\pi'}) \rightarrow 2\not >
\modal{\pi'}\top$ \\ 
$(1 \wedge 2)\not\rightarrow\modal{\pi_1\pi_2}\approx\modal{\pi_2}$\\ \hline
$(1\wedge 2)\Rightarrow \modal{\pi}a$
\end{tabular}
\item   [PDU]   {\tt The PDU Axiom}\\
\begin{tabular}[t]{l}
$1 \Rightarrow \modal{\pi}a$\\
$2 \Rightarrow \modal{\pi'}b$\\ 
$(1\rightarrow\modal{\pi}\approx\modal{\pi'})$ \\ 
$(1 \wedge 2)\not\rightarrow\modal{\pi_1\pi_2}\approx\modal{\pi_2}$\\ \hline
$(1\wedge 2) \Rightarrow \modal{\pi}(\mbox{{\em Spec}}_{\pi}^{12} \unify
\mbox{{\em Comp}}_{\pi}^{12} \unify \psi)$
\end{tabular}

Where:

$\psi = \unify\{\psi_{\pi_i}: 1\wedge 2\leadsto \modal{\pi_i}\psi_{\pi_i}
\mbox{and } (1\wedge 2)\rightarrow \modal{\pi}\approx\modal{\pi_i}\}$
\end{itemize}

This version of $\ddunify$ is equivalent to that given in Young and
Rounds (1993), assuming that multiple
extensions are treated as an error condition.  
So their version of persistent default unification is
a special case of the operation defined in \S3.5.  It can be
implemented more efficiently than $\ddunify$, but the lack of default
reentrancy and subsumption relationships on the types mean that it is
insufficiently expressive to model some of the phenomena we are
interested in.

\section{Linguistic Applications}
\label{applications}

Our illustrative lexical hierarchy concerning English inflectional
morphology was chosen because it is the simplest example capable of
demonstrating the inadequacies of existing definitions of default
unification and exemplifying the properties of persistent default
unification of {\sc tdfs}s. In this section, we discuss further
applications which we think provide better motivation for the
introduction of such an operation into constraint-based linguistic
theories.

There are many papers which argue for default inheritance of most
types of lexical property ranging from cases of inflectional
morphology of the type discussed above, through processes of
derivation, conversion and sense extension (see Daelemans \etal, 1992;
Briscoe, 1993 for reviews). In addition, default inheritance has been
argued to play a role in feature propagation for syntactic description
(Gazdar \etal, 1985; Shieber, 1986b), in the specification of
relations between constructions (Goldberg, 1992).  The
applications we briefly discuss involve treatments of paradigmatic
relations between lexical items and between constructions, processes
of regular sense extension and syntactic feature propagation.

\subsection{Lexical Semantic Specifications}

Briscoe \etal\ (1990), Boguraev and Pustejovsky (1990, 1993) and
Copestake and Briscoe (1992) argue that formalisation of
Pustejovsky's (e.g. 1991) approach to lexical semantics requires a
notion of default inheritance in the lexicon. For instance,
Pustejovsky argues on linguistic grounds that nouns denoting artifacts
must incorporate a representation of their telic role or `purpose' in
order to account for the interpretation of `logically' metonymic
constructions such as (\ref{1}).
\begin{examples}
\item   \label{1}
\begin{subexamples}
\item   John began a new book
\item   Jane finished her beer
\item   Bill enjoyed the film
\item   Mary likes hamburgers
\end{subexamples}
\end{examples}
In each case the noun phrase object denotes an artifact and the
(usual) interpretation of the verb phrase involves a `coercion' of the
artifact to a process or event involving the purpose of that artifact
-- reading books, drinking beer, watching films and eating
hamburgers. Pustejovsky emphasises that the assumption that certain
verbs cause such coercions has direct linguistic consequences for the
insightful representation of argument structure and complementation;
for example, {\it enjoy} can subcategorise for a complement
denoting a process in which the experiencer subject of {\it enjoy}
participates, capturing the relatedness in meaning between
(\ref{2}a) and (\ref{2}b).
\begin{examples}
\item   \label{2}
\begin{subexamples}
\item   John enjoyed the play
\item   John enjoyed watching the play
\end{subexamples}
\end{examples}

Once we accept the utility of representing telic roles, it is clear
that they are a natural candidate for an inheritance based treatment;
for example, the telic role of liquid artifacts will be {\it drink},
that of visual representation artifacts {\it watch}, and so forth. It
is also not difficult to show that inheritance must be default; for
example, the telic role of `literature' will be {\it read}, however
that of the subclass of reference books will be {\it refer-to}.
Briscoe \etal\ propose to express these observations in a
unification-based account by representing the lexicon in terms of
overwriting templates (e.g. Karttunen, 1986), and Copestake (1992,
1993) proposes using a non-associative version of default unification.
Boguraev and Pustejovsky (1990, 1993), Copestake and Briscoe (1992,
1994) and Vossen and Copestake (1993) discuss the extension of the
technique to the multiple orthogonal default inheritance of nominal
qualia structure (e.g. Pustejovsky, 1991), in general. In the current
framework these proposals can be incorporated directly without loss of
declarativity, using the type of lexical hierarchy introduced in
Figure~\ref{final-eg}.  The value of the {\sc telic} attribute will be
a complex {\sc fs} representing the semantics of specified (generic)
verbs with the artifact associated (usually) with the object argument
slot.  A fragment of such a hierarchy is shown in Figure~\ref{telic}.
The coercion process itself can be implemented as a unary rule (Briscoe
\etal 1990) or by monotonic 
type constraints (Copestake and Briscoe, 1994). 
\begin{figure}
\setlength{\unitlength}{0.5in}
\begin{center}
\begin{picture}(7,7.5)(-2,-1.5)
\thicklines
\put(3.5,5.5){\makebox(0,0){{\tiny $\avmplus{\att{artefact}\\
\attval{SEM ARG1}{\ind{1}}\\ 
\attval{QUALIA TELIC}{\avmplus{\attvaltyp{PRED}{event}\\
\attval{ARG2}{\avmplus{\attvaltyp{PRED}{/p-pat}\\
\attval{ARG1}{\ind{1}}}}}}}$}}}
\put(2.5,4.5){\line(-1,-1){1}}
\put(1,3){\makebox(0,0){{\tiny $\avmplus{\att{represent-art}\\ 
\attvaltyp{QUALIA TELIC PRED}{/perceive}}$}}}
\put(0.5,2.5){\line(-1,-1){1}}
\put(-1.3,1.0){\makebox(0,0){{\tiny $\avmplus{\att{visual-rep}\\ 
\attvaltyp{QUALIA TELIC PRED}{/watch}}$}}}
\put(1.5,2.5){\line(1,-1){1}}
\put(3.3,1.0){\makebox(0,0){{\tiny $\avmplus{\att{literature}\\ 
\attvaltyp{QUALIA TELIC PRED}{/read}}$}}}
\put(3.5,0.5){\line(1,-1){1}}
\put(5.0,-1.0){\makebox(0,0){{\tiny $\avmplus{\att{reference}\\ 
\attvaltyp{QUALIA TELIC PRED}{/refer\_to}}$}}}
\put(2.5,0.5){\line(-1,-1){1}}
\put(1.0,-1.0){\makebox(0,0){{\tiny $\avmplus{\att{fiction}}$}}}
\end{picture}
\end{center}
\vspace*{2mm}
\caption{Inheritance of Telic Roles}
\label{telic}
\end{figure}

It is clear that the examples in (\ref{1}) only have defeasible
interpretations involving the `usual purpose' readings. In suitable
discourse contexts, these readings can be replaced by ones involving
more specific processes, different qualia roles, and so forth, as
(\ref{3}) illustrates.
\begin{examples}
\item   \label{3}
\begin{subexamples}
\item   Coppola particularly enjoyed that film (watching $\leadsto$ making)
\item
You can see our neighbour, `Howard Hughes', really enjoying his new
car every Sunday in the drive, hose in hand (driving $\leadsto$ cleaning)
\item  Fido obviously enjoyed my new book (reading $\leadsto$ eating)
\end{subexamples}
\end{examples}
Briscoe \etal\ (1990) suggest that this can be accommodated by making
the rule of coercion which converts an object denoting NP into a
process or event denoting NP create a default specification of this
process or event, based on the telic role of the noun (if available).
In the present context of {\sc tdfs}s, this proposal makes more
formal sense since it reduces to making this aspect of the {\sc fs}
associated with the NP defeasible.  Thus, in contrast with the
morphology example shown in Figure~\ref{final-eg}, 
we do not assume that the default structure is incorporated into the
non-defeasible structure before non-lexical processing occurs.

The semantic translation we have provided for {\sc tdfs}s interprets a
defeasible specification such as $event/write$ as a default
conditional, providing the foundation for an interface with a theory
of discourse interpretation based on a default conditional logic (e.g.
Lascarides and Asher, 1993). Briscoe \etal\ (1990) argue on the basis
of corpus data that the notion of a lexically specified default
interpretation is motivated by the distribution of default and
non-default interpretations with verbs such as {\it enjoy} which make
available both an explicit (progressive VP) and implicit (NP)
complementation pattern for realising the intended meaning. Since the
implicit pattern is chosen mostly when the default interpretation is
correct or the discourse context is informationally rich, conflicting
and determinate, whilst the explicit pattern is chosen mostly when the
default reading would be inappropriate and the context is not
determinate, this suggests that language users structure their
utterances in a manner which supports assumption of the default
reading in the absence of conflicting information, but rejection of it
when additional conflicting information is made available. This view
of the interaction of semantic specification with discourse
interpretation is fully compatible with the principles of the {\sc
dice} framework (e.g. Lascarides and Asher, 1993, Asher and
Lascarides, 1994).

Lascarides (1995) shows how the defeasible pragmatic
information in {\sc dice} and defeasible results in {\sc pdu} can be
made to communicate in a perspicuous fashion, via just two {\sc dice}
axioms.  The details are beyond the scope of this paper, because it
would require a detailed discussion of the {\sc dice} framework.
However, we informally describe this approach.  The two axioms predict
when the {\sc pdu} default predictions survive in the discourse
context and when they are overridden.  They also guarantee that the
{\sc pdu} indefeasible results {\em always} survive, regardless of
what pragmatic information is stated.  The two axioms make essential
use, therefore, of the fact that defeasible results of {\sc pdu} are
`visibly' marked as such for the pragmatic component. Furthermore, we
would argue that default lexical specification could not be replaced
in this instance with, for example, a disjunction of alternative
values to be selected from pragmatically because of the open-ended
nature of the eventual interpretation. Similarly, we would argue that
not providing a default lexical specification and leaving the coercion
predicate underspecified is not compatible with the corpus-based
evidence summarised above from Briscoe \etal\ (1990), since this would
require the pragmatic component to provide a default interpretation
which is specified lexically and not in terms of contextual
information. 

The first axiom states that normally, default {\sc pdu} results
survive in the discourse context.  The second axiom ensures that when
there is discourse information that conflicts with the defeasible
results of {\sc pdu}, the discourse information wins, even if it's
defeasible.  In the case of metonymy, Lascarides (1995) demonstrates
how the axioms
predict different interpretations of (\ref{goat}a) and (\ref{goat}b).
\begin{examples}
\item   \label{goat}
\begin{subexamples}
\item   John enjoyed the book.
\item   The goat enjoyed the book.
\end{subexamples}
\end{examples}
(\ref{goat}a) is interpreted as John enjoyed reading the book, because
the {\sc pdu} expansion of the metonymy survives in this context.  In
contrast, this {\sc pdu} expansion of metonymy is blocked by the
second axiom in the interpretation of (\ref{goat}b), because of the
conflicting defeasible domain information that goats don't read.  We
refer the reader to Lascarides (1995) for further
details.

To summarise, we have sketched treatment of default inheritance of
lexical qualia roles which we argue improve on those presented in
Briscoe \etal (1990) in that they are declarative and can
persist beyond the lexicon, and can thus interact straightforwardly
with a theory of discourse interpretation grounded in default logic.

\subsection{Semantic Broadening}

Copestake and Briscoe (1994) argue for a systematic process of sense
modulation which they term {\it broadening} where sense usages are
available in context which appear to semantically subsume the basic
sense of a lexeme/sign.  Usually it appears that a quale, in
Pustejovsky's (1991) sense, which is specified in the basic sense
becomes overridden in context.  For example, the normal usages of {\it
bank} and {\it cloud} could be specified as stating both form and
composition (earth/water vapour).  However, both have usages where
alternative compositions are stated {\it bank of rhododendrons}, {\it
bank of clouds}/{\it cloud bank}, {\it cloud of mosquitoes}, {\it dust
cloud}.  In some comparable cases the broadened sense may appear more
metaphorical, for example {\it forest of hands}.  In many cases there
is evidence that broadening of meaning has taken place diachronically
and that the original senses tended to be specific and concrete (see
Sweetser 1990).  It seems appropriate to regard these examples in
terms of a modulation of sense rather than a complete shift, but this
modulation is most naturally expressed as being non-monotonic.  There
is a very strong preference for one particular sense and the
alternative interpretations are not conventionalised, but given by
context (there is no conventional interpretation of {\it cloud} as
{\it cloud of mosquitoes}).  This implies that non-default
interpretations will only be usual in contexts which explicitly give
the exceptional component (normally by compounding or
post-modification).

To represent broadening we make use of lexically specified persistent
default components of the qualia structure and allow these to be
overridden.  In the {\sc fs} for the lexical entry for {\it cloud} shown in
Figure~\ref{cloudfig} the qualia structure is stated to refer necessarily
to an individuated physical object of amorphous form, with a
composition that is also physical and refers cumulatively (i.e.~the
composition is either a mass or a plural object).  By default, {\it
cloud} is a natural object (as opposed to an artifact) and is composed
of water vapour.\footnote{This description has been somewhat
simplified but in any case we would not claim that it is completely
adequate.  It does not, for instance, cover the mass use of {\it
cloud}, found in (\ref{cloud}a), which seems to be available only with
the default usage (compare (\ref{cloud}b)):
\begin{examples}
\item   \label{cloud}
\begin{subexamples}
\item   We flew into dense cloud.
\item
* We walked into dense cloud of smoke.
\end{subexamples}
\end{examples}
Nor does it cover the metaphorical uses, such as {\it cloud of
suspicion}.}  Referring to the process of overriding the lexically
specified defaults as broadening is perhaps somewhat misleading, since
a more general {\sc fs} never actually exists in isolation according to this
treatment.  The intuition that the sense is broadened is reflected in
the non-defeasible components of the modified structure, however: for
example the semantic contribution of {\it cloud} to {\it cloud of
mosquitoes} could be represented as a {\sc fs} with unspecified composition.
\begin{figure}
{\centering
\tiny
$\avmplus{\att{lex-count-noun}\\
                  \attvaltyp{ORTH}{cloud}\\
                  \attvaltyp{CAT}{noun-cat}\\
                  \attvaltyp{SEM}{obj-noun-formula}\\
                  \attval{QUALIA}{\avmplus{\att{phys\_obj / natural\_obj}\\
                           \attval{FORM}{\avmplus{\att{nomform}\\
                                    \attvaltyp{RELATIVE}{individuated}\\
                                    \attvaltyp{ABSOLUTE}{amorphous}}}\\
                           \attvaltyp{CONSTITUENCY}{phys\_cum / water-vapour}}}}$

}
\caption{Lexical entry for {\it cloud}}
\label{cloudfig}
\end{figure}

Broadening and other kinds of sense modulation (Cruse, 1986) provide a
straightforward motivation for the persistence of default lexical
specifications into the syntagmatic plane. Persistent default
unification provides a natural mechanism for implementing interactions
of this kind between lexical semantic specification and syntactic and
compositional semantic rules.  The axioms specified in Lascarides
(1995) for predicting when defeasible results of $\ddunify$
ultimately survive into the interpretation would account for semantic
broadening, as well as the expansion of metonymy described earlier.
Alternative treatments, such as alternate entries for {\it cloud} and
{\it bank} which specify an indefeasible value for composition in the
absence of a complement and leave it underspecified with obligatory
complementation seem unsatisfactory since this would predict that in a
narrative such as (\ref{cow})
the second occurrence of {\it cloud} denotes a mass
composed of water vapour.
\begin{examples}
\item \label{cow}
The cow was engulfed by a cloud of flies,
flicking its tail ineffectually. As the cloud dissipated, we realised
it was injured.
\end{examples}
\subsection{Dative Constructions}
\label{dative}

Goldberg (1992), building on the frameworks of frame semantics and
construction grammar developed by Fillmore and his colleagues (e.g.
Fillmore \etal, 1988), argues that certain constructions should be
seen as related by `metaphorical or polysemous links'. For example,
she argues that there is a family of dative constructions which
exhibit the same syntactic properties and related semantic properties,
exemplified in (\ref{6}).
\begin{examples}
\item   \label{6}
\begin{subexamples}
\item
Mary gave Joe a present
\item
Joe painted Sally a picture
\item
The medicine brought him relief
\item
The music lent the party a festive air
\item
Jo gave Bob a punch
\item
He blew his wife a kiss
\end{subexamples}
\end{examples}
Goldberg argues that the core ditransitive construction involves a
volitional agent and willing recipient and carries the entailments
that the agent causes the recipient to receive the object denoted by
the patient argument, as in (\ref{6}a).  Under this interpretation,
(\ref{6}b) involves a shift in meaning where the recipient may or
may not receive the patient, but the agent acts with this intention.
Following Sanfilippo (1990, 1993) we might
represent these differences in the basic (abstract) meaning of the
construction in terms of entailments associated with proto thematic
roles (Dowty, 1989), so that `agent' becomes {\it p-agt-cause-transfer} in
(\ref{6}a) and {\it p-agt-cause-make-intend-transfer} in
(\ref{6}b). In the case of these first two examples it is plausible
to argue that there are lexical rules which relate the dative
construction with the alternative complementation patterns involving
{\it to} and {\it for} PP arguments, respectively, and that this rule
alters the proto-agent role of a `creation' verb such as {\it paint}
from {\it p-agt-cause-make} to {\it p-agt-cause-make-intend-transfer}.
Furthermore, we will represent the different entailments (willingness
and successful transfer) concerning the first object in (\ref{6}a)
and (\ref{6}b) as `recipient' and `benefactive', respectively.

As Goldberg argues, if we want to elegantly capture the similarity
between the dative constructions in these two rules it should only be
necessary to state the form of the construction once. Furthermore, it
should not be necessary to say that verbs of creation, such as {\it
paint} are lexically ambiguous between two and three -place
predicates; rather it is participation in the dative construction
itself which creates a third beneficiary argument for these inherently
two-place predicates. In what follows, we assume a lexically-based
theory of grammar in which bounded lexically-governed dependencies of
the type discussed by Goldberg are treated in terms of the
subcategorisation requirements of their heads (in this case verbs).
We also assume an approach to lexical rules, in which such rules
conditionally create derived lexical signs stated in terms of mappings
between (lexical) types (e.g. Pollard and Sag, 1987), and factor the
majority of information concerning the form of the types related into
their associated type constraints (e.g. Flickinger and Nerbonne,
1992). Thus, the core dative rule and benefactive dative rule could be
represented as in Figures~\ref{dative-lr} and~\ref{benef-dative-lr},
assuming the (inherited and specific) type constraints on `transfer'
ditransitive and `creation' transitive verbs and on the dative
construction (sign) given in Figures~\ref{ditrans-type},~\ref{trans-type}
and~\ref{dative-type}.\footnote{In this example and those that follow,
we make as few assumptions as possible concerning the exact
grammatical framework employed. The basic ideas are compatible with
HPSG, LFG or UCG -like treatments of the realisation of grammatical
relations, and the proto-role approach to thematic relations might be
linked to an event-based semantic framework (e.g. Parsons, 1990;
Sanfilippo, 1990, 1993) or to a LFG style treatment in terms of
mappings or projections to a semantic representation (Halvorsen and
Kaplan, 1988; Dalrymple \etal, 1993). We assume that proto-role
entailments create selection preferences on the semantic nature of
their arguments, but do not attempt to make these constraints
explicit. Similarly, we make no attempt to show how the
generalisations implicit in type constraints can be elegantly factored
out into constraints on supertypes (e.g. Pollard and Sag, 1987;
Sanfilippo, 1993).}
\hidden{
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{transfer-ditrans-ppto-verb}\\
          \attval{PHON}{\avmplus{
                  \attval {STEM} {\ind{1}}}}\\
          \attval{SYN}{\avmplus{
                     \attval{SUBJ}{\avmplus{
                                      \attval{SEM}{\ind{2}}}}\\
                     \attval{OBJ1}{\avmplus{
                                      \attval{SEM}{\ind{3}}}}\\
                     \attval{OBL1}{\avmplus{
                                      \attval{SEM}{\ind{4}}}}}}\\
          \attval{SEM}{\ind{5}}}$                 
}
$\mapsto$
{\tiny
$\avmplus{\att{recip-dative-verb}\\
          \attval{PHON}{\avmplus{
          \attval {STEM} {\ind{1}}}}\\      
          \attval{SYN}{\avmplus{
                     \attval{SUBJ}{\avmplus{
                                      \attval{SEM}{\ind{2}}}}\\
                     \attval{OBJ1}{\avmplus{
                                      \attval{SEM}{\ind{4}}}}\\
                     \attval{OBJ2}{\avmplus{
                                      \attval{SEM}{\ind{3}}}}}}\\
          \attval{SEM}{\ind{5}}}$
}\\[1mm]
$\mbox{{\bf recip-dative-verb}}\sqsubset \mbox{{\bf dative-sign}}$\\
%$\mbox{{\bf lit-transfer-ditrans-ppto-verb}}\sqsubset \mbox{{\bf
%transfer-ditrans-ppto-verb}}$
}
\caption{Dative Lexical Rule}
\label{dative-lr}
\end{figure}
}

\hidden{
\begin{figure}
{\tiny
$\avmplus{\att{create-dyadic-trans-verb}\\
          \attval{PHON}{\avmplus{
                  \attval{STEM}{\ind{1}}}}\\
          \attval{SYN}{\avmplus{
                     \attval{SUBJ}{\avmplus{
                                      \attval{SEM}{\ind{2}}}}\\
                     \attval{OBJ1}{\avmplus{
                                      \attval{SEM}{\ind{3}}}}}}\\ 
          \attval{SEM}{\avmplus{ 
                     \attval{PRED}{\ind{4}}}}}$\\                 
}
$\mapsto$
{\tiny
$\avmplus{\att{benef-dative-verb}\\
          \attval{PHON}{\avmplus{
                   \attval{STEM}{\ind{1}}}}\\      
          \attval{SYN}{\avmplus{
                     \attval{SUBJ}{\avmplus{
                                      \attval{SEM}{\ind{2}}}}\\
                     \attval{OBJ1}{\avmplus{
                                      \attval{SEM}{\ind{5}}}}\\
                     \attval{OBJ2}{\avmplus{
                                      \attval{SEM}{\ind{3}}}}}}\\
          \attval{SEM}{\avmplus{ 
                     \attval{PRED}{\ind{4}}\\
                     \attval{ARG1}{\avmplus{
                            \attvaltyp{PRED}{p-agt-cause-make-intend-transfer}\\
                            \attval{ARG}{\ind{2}}}}\\
                     \attval{ARG2}{\avmplus{
                            \attvaltyp{PRED}{p-pat-benef}\\
                            \attval{ARG}{\ind{5}}}}\\
                     \attval{ARG3}{\avmplus{
                            \attvaltyp{PRED}{p-pat-aff-obj}\\
                            \attval{ARG}{\ind{3}}}}}}}$
}

{\centering
$\mbox{{\bf benef-dative-verb}}\sqsubset \mbox{{\bf dative-sign}}$

}
\caption{Benefactive Dative Lexical Rule}
\label{benef-dative-lr}
\end{figure}
}

\hidden{
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{lit-transfer-ditrans-ppto-verb} \\
         \attval{PHON}{\avmplus{
                         \attvaltyp{STEM}{stem}}}\\
         \attval{SYN}{\avmplus{
                  \attvaltyp{CAT}{verb}\\
                  \attval{SUBJ}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{2}}}}\\
                  \attval{OBJ1}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{3}}}}\\
                  \attval{OBL1}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{pp}}}\\
                           \attval{SEM}{\ind{4}}}}}}\\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\avmplus{
                            \attvaltyp{PRED}{p-agt-cause-transfer}\\
                            \attval{ARG}{\ind{2}}}}\\
                  \attval{ARG2}{\avmplus{
                            \attvaltyp{PRED}{p-pat-recip}\\
                            \attval{ARG}{\ind{4}}}}\\
                  \attval{ARG3}{\avmplus{
                            \attvaltyp{PRED}{p-pat-aff-obj}\\
                            \attval{ARG}{\ind{3}}}}}}}$
}\\[1mm]
$\mbox{{\bf lit-transfer-ditrans-ppto-verb}}\sqsubset \mbox{{\bf
transfer-ditrans-ppto-verb}}$

}
\caption{Ditransitive Verb Type Constraint}
\label{ditrans-type}
\end{figure}
}


\hidden{
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{create-dyadic-trans-verb} \\
         \attval{PHON}{\avmplus{
                         \attvaltyp{STEM}{stem}}}\\
         \attval{SYN}{\avmplus{
                  \attvaltyp{CAT}{verb}\\
                  \attval{SUBJ}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{2}}}}\\
                  \attval{OBJ1}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{3}}}}}}\\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\avmplus{
                            \attvaltyp{PRED}{p-agt-cause-make}\\
                            \attval{ARG}{\ind{2}}}}\\
                  \attval{ARG2}{\avmplus{
                            \attvaltyp{PRED}{p-pat-aff-obj}\\
                            \attval{ARG}{\ind{3}}}}}}}$
}

}
\caption{Transitive Type Constraint}
\label{trans-type}
\end{figure}
}


\hidden{
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{dative-sign} \\
         \attval{PHON}{\avmplus{
                         \attvaltyp{STEM}{stem}}}\\
         \attval{SYN}{\avmplus{
                  \attvaltyp{CAT}{verb}\\
                  \attval{SUBJ}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{2}}}}\\
                  \attval{OBJ1}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{3}}}}\\
                  \attval{OBJ2}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{4}}}}}}\\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\avmplus{
                            \attvaltyp{PRED}{p-agt/p-agt-cause-transfer}\\
                            \attval{ARG}{\ind{2}}}}\\
                  \attval{ARG2}{\avmplus{
                            \attvaltyp{PRED}{p-pat/p-pat-recip}\\
                            \attval{ARG}{\ind{3}}}}\\
                  \attval{ARG3}{\avmplus{
                            \attvaltyp{PRED}{p-pat-aff-obj}\\
                            \attval{ARG}{\ind{4}}}}}}}$
}

}
\caption{Dative Type Constraint}
\label{dative-type}
\end{figure}
}

As {\bf benef-dative-verb} is a subtype of {\bf dative-sign}, the
benefactive dative lexical rule will create a new lexical entry for
`creation' verbs which inherits properties of the dative construction.
However, {\bf benef-dative-verb} overrides the specific default
thematic entailments associated with the basic construction.  Thus the
resulting sign will have the proto-roles {\bf
p-agt-cause-make-intend-transfer} and {\bf p-pat-benef}, rather than
{\bf p-agt-cause-transfer} and {\bf p-pat-recip}.\footnote{Note that
although for the sake of clarity we show the {\sc obj1} and the {\bf
p-pat-benef} role in Figure~\ref{benef-dative-lr}, this information is
inherited from the {\bf benef-dative-verb} subtype of the dative
construction and not stipulated directly in the rule.} On the other
hand, when the core (recipient) dative lexical rule is applied to a
sign of type {\bf lit-transfer-ditrans-ppto-verb}, the specifications
of the proto-roles as {\bf p-agt-cause-transfer} and {\bf p-pat-recip}
in the result will be indefeasible, in contrast to their defeasible
status in {\bf dative-sign}.  This is because they are indefeasible in
the type {\bf lit-transfer-ditrans-ppto-verb}.  The lexical rule also
specifies that the entire semantics of the derived sign is reentrant
with that of the basic sign.  These rules predict the correct
relationships between (\ref{6}a) and (\ref{6}b), and the corresponding
sentences with {\em to} and {\em for} complements.

Further support for this approach to the dative construction and
dative lexical rule(s) is provided by the other examples in (\ref{6}).
Goldberg argues that (\ref{6}c,d) are licensed by a metaphorical
extension of the transfer relation by which causal events are viewed
as transfers.  Causing an effect in an entity is understood as
transferring that effect to it.  We might capture this by altering the
entailments associated with verbs such as {\it lend} by the
proto-roles specified by {\bf lit-transfer-ditrans-ppto-verb} by a
lexical rule which created an entry of a sister type {\bf
met-transfer-ditrans-ppto-verb} which specified different proto-roles.
The dative lexical rule would also apply to this subtype, capturing
the fact that this metaphorical extension in the dative construction
parallels a similar extension of the same verb set in the oblique {\it
to} prepositional phrase construction.  Finally, (\ref{6}e,f) provide
evidence that certain quasi-idiomatic expressions need to be
associated directly with {\bf dative-sign} as they have no
counterparts in such oblique expressions.  We assume that
(quasi-)idioms are best represented as subtypes of lexical signs in
which not only the syntactic head but also other arguments are
severely constrained in terms of lexical selection. Thus Goldberg
claims the quasi-idiomatic expressions in (\ref{6}e,f) are licensed by
a metaphor which involves understanding actions intentionally directed
at another person as being entities transferred to that person.  As a
first approximation, we might represent this process in terms of the
subtype of {\bf dative-sign} shown in Figure~\ref{met-dative-type}, in
which we have overridden the default proto-role specifications with
entailments specific to the metaphor which we assume also serve to
constrain the range of acceptable arguments to the (transfer) verb.

\hidden{
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{met-dative-sign} \\
         \attval{PHON}{\avmplus{
                         \attvaltyp{STEM}{stem}}}\\
         \attval{SYN}{\avmplus{
                  \attvaltyp{CAT}{verb}\\
                  \attval{SUBJ}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{2}}}}\\
                  \attval{OBJ1}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{3}}}}\\
                  \attval{OBJ2}{\avmplus{
                           \attval{SYN}{\avmplus{
                                         \attvaltyp{CAT}{np}}}\\
                           \attval{SEM}{\ind{4}}}}}}\\
         \attval{SEM}{\avmplus{
                  \attvaltyp{PRED}{pred}\\
                  \attval{ARG1}{\avmplus{
                            \attvaltyp{PRED}{p-agt-cause-met-transfer}\\
                            \attval{ARG}{\ind{2}}}}\\
                  \attval{ARG2}{\avmplus{
                            \attvaltyp{PRED}{p-pat-met-recip}\\
                            \attval{ARG}{\ind{3}}}}\\
                  \attval{ARG3}{\avmplus{
                            \attvaltyp{PRED}{p-pat-transferred-ev}\\
                            \attval{ARG}{\ind{4}}}}}}}$
}

}
\caption{Metaphorical Dative Type Constraint}
\label{met-dative-type}
\end{figure}
}

To summarise, we have sketched a lexical treatment of dative
constructions intended to capture and formalise some of Goldberg's
observations concerning similarities and differences between related
versions of the same basic construction.  We have utilised a familiar
and standard notion of lexical rule, coupled with persistent default
unification of {\sc tdfs}s. In this formulation of this fragment of
data, there is no requirement for the default specifications to
persist outside the lexicon. However, a more adequate treatment of
proto-roles in this framework would probably involve persistent
default lexical specification of the entailments associated with
proto-roles which could be overridden at the compositional semantic or
pragmatic level. 

\subsection{Syntactic Feature Propagation}

Shieber (1986b) and Bouma (1992) discuss the unification-based
interpretation of the Head Feature Convention (HFC) of GPSG (Gazdar
\etal, 1985). The HFC is a default convention which equates the values
of head features on the mother and head daughter in a local tree
unless these features have acquired distinct values through
stipulation in immediate dominance rules. Most unification-based
approaches to GPSG either captured the default nature of the HFC and
related feature propagation principles through a non-unification-based
metagrammatical pre-compilation phase (e.g. Briscoe \etal, 1987) or
simplified it to a non-default reentrancy condition (Shieber,
1986a,b). Bouma (1992) presents a version of default unification which
he motivates as a technique for implementing the HFC in a
unification-based fashion. Bouma's version of default unification
is an asymmetric, non-associative operation which adds consistent
information from a defeasible {\sc fs} to an indefeasible {\sc fs}. Bouma
represents the HFC as a default reentrancy associated with each
underspecified rule, schematically of the form in (\ref{10}a), in
which mother and head daughter categories are {\sc fs}s and the head
daughter {\sc fs} is taken to be indefeasible.
\begin{examples}
\item   \label{10}
\begin{subexamples}
\item
$M(other) \rightarrow X\ H(ead)D(aughter)\ Y$
\item
$S \rightarrow NP\ H[BAR 1] $
\item
$[N -, V +, BAR 2] \rightarrow NP\ [BAR 1] $
\item
$[N -, V +, BAR 2] \rightarrow NP\ [N -, V +, BAR 1] $
\end{subexamples}
\end{examples}
The idea is that default unification can be used in a pre-compilation
phase to flesh out underspecified rules, so that a rule such as
(\ref{10}b) which contains the features in (\ref{10}c) will be
expanded out to (\ref{10}d), where {\sc bar} values remain distinct because
of the stipulation on the head daughter, though {\sc bar} is a head feature.
After compilation the expanded rule can be utilised for parsing using
monotonic unification. As rule expansion serves only to create a set of
fully specified (phrase-structure) rules, the overall approach remains
declarative because default unifications will never be `chained'.

A weakness of Bouma's approach is that it preserves the
declarativity of the overall grammar only by making strong assumptions
concerning the point at which such feature propagation principles are
applied (which are also at odds with those assumed in GPSG). If, for
example, it turned out that it was more efficient to apply such
unification-based constraints after the initial construction of
(underspecified) syntactic descriptions during parsing (see
e.g. Maxwell and Kaplan (1993) for evidence that this is true for some
types of grammar), then different results might be obtained depending
on whether the sequence of default unifications required to flesh out
a chain of mothers and head daughters in a syntactic description
was implemented top-down or bottom-up.

We might be able to utilise persistent default unification of {\sc tdfs}s in
order to formalise the HFC by making use of the flexibility in the
definition of specificity mentioned in \S\ref{incorp} and calculate
the inheritance relationship between head features on the basis of the
relationship given by the syntactic description, such that head
daughters were lower in the partial order than their mothers.  In this
case, if all head features had defeasible values, the HFC is given by
inheritance.  As this operation is order independent it can be
interpreted either in terms of rule pre-compilation or interleaved
with the construction of a syntactic description. However, there is a
potential problem with the persistency of defeasible specifications in
this context: whilst it is quite possible to view the {\it
propagation} of head features in terms of default inheritance, their
{\it application} to (fully-specified) lexical items must be
indefeasible.  Otherwise, lexical information may override head feature
specifications leading to analyses of many ungrammatical
sentences. Therefore, to make this approach work we would
need to ensure that the head features were only interpreted as
defeasible with respect to inheritance and were indefeasible with
respect to category matching.  Clearly, if we simply do this by
applying the {\it DefFill} operation discussed in \S\ref{incorp}, we
return to order dependence, because the result will be sensitive to
the point at which we transform the {\sc tdfs} to a {\sc tfs}.  
An alternative would be to regard all values as uniformly defeasible,
but only information which should be involved in the HFC would be in a
mutual specificity relationship, everything else would be unordered
(leading to inconsistency during matching of inappropriate categories).

Developing a satisfactory account of GPSG's HFC in terms of $\ddunify$ is,
however, beyond the scope of this paper since it would require
significant revisions to the syntactic theory in order to utilise the
concepts of typed {\sc fs}s and specificity in this fashion. Nevertheless,
although $\ddunify$ as defined in \S\ref{PDUdefn} will not give the precise
behaviour of the HFC in GPSG, Bouma's (1992) definition of default
unification suffers from taking this single specialised application as
the paradigm case. In order to capture the intent of `add
conservatively' (Shieber, 1986b) which was introduced solely to
capture specific effects of the HFC, Bouma defines default
unification to `weaken' reentrancy statements even in the absence of
conflicting defaults (see e.g. his (13)). This has the unfortunate
consequence that his definition does not reduce to monotonic
unification in the absence of conflict (Carpenter, 1993; Copestake,
1993), severely limiting its application to other problems.

\subsection{Lexical Rules}

The use of {\sc avm} boxed `reentrancy' notation between subparts of
{\sc fs}s in constraint-based formalisms such as HPSG in the statement
of lexical rules is quite arbitrary when viewed from the perspective
of information flow between signs and semantically incoherent since
the two {\sc fs}s involved cannot be treated as a single {\sc dag}.
The attraction of utilising default unification rather than reentrancy
to specify patterns of inheritance between signs (and their subparts)
is that some of this arbitrariness and incoherence in constraint-based
terms might be eradicated, because we could state that information is
shared {\it unless} stated to the contrary and that the derived
lexical sign is obtained by default unification of information from
the basic sign with that stipulated for the derived
one.\footnote{Note that Pollard and Sag~(1994) omit shared information
from their descriptions of lexical rules for notational 
convenience.}

We will briefly illustrate the point by defining a restricted notion
of lexical rule in terms of $\ddunify$. Throughout this paper we have
assumed a definition of lexical rule effectively equivalent to that of
Pollard and Sag (1987), in which information is `copied' from base
sign to derived sign by stipulation. A more natural and less arbitrary
definition might utilise default unification between base and derived
signs and stipulate modifications as far as possible through type
constraints on the derived sign. Then information flow between base
and derived sign will be a consequence of the persistent default
unification of the instantiated `antecedent' {\sc tfs} with the
specification of the `consequent' {\sc tfs}. For example, assuming a
lexical rule based treatment of English inflectional morphology, we
could represent the third person singular rule as in
Figure~\ref{3rd-sing}.
\begin{figure}
{\centering
{\tiny
$\avmplus{\att{base}\\
          \attval{PHON}{\avmplus{\attval{STEM}{\ind{1}}}}\\
          \attval{SYNSEM}{\ind{2}}}$
}
$\mapsto$
{\tiny
$\avmplus{\att{third-person-sing}\\
          \attval{PHON}{\avmplus{\attval{STEM}{\ind{1}}}}\\
          \attval{SYNSEM}{\ind{2}}}$
}

}
\caption{Third Person Singular Lexical Rule}
\label{3rd-sing}
\end{figure}
The intended interpretation of the rule, following Pollard and Sag
(1987) is that signs of type {\bf base} which unify with the
antecedent {\sc tfs} in the rule are used to create derived signs of
type {\bf third-person-sing}. The `reentrancies' indexed one and two
pass over information from the instantiated antecedent {\sc tfs} to
the consequent.  The value of SYNSEM given by the type {\bf base} is
assumed to be underspecified with respect to agreement, but the type
{\bf third-person-sing} will specify agreement and suffixation.

The interpretation of the rule violates the spirit of a
constraint-based formalism as there is no constraint-based connection
between the antecedent and consequent {\sc tfs}s. Thus, the
reentrancies between the two {\sc tfs}s do not have the same
interpretation as those which occur within a single {\sc tfs} but
rather function to copy information between distinct nodes of
different {\sc tfs}s. Linguistically, the rule is inelegant in that
what remains the same between base and derived entry must be
stipulated in addition to what changes.  As we will now describe, the
third-person-sing rule could be simplified to a simple statement of
the form \mbox{{\bf base} $\mapsto$ {\bf third-person-sing}}, by
reinterpreting $\mapsto$ in terms of $\ddunify$.

The operation of lexical rules involves a matching stage and creation
stage. Under the new formulation matching is trivial since the rule
specifies a type and any sign of this type or its subtypes will match
(unify with) the rule `antecedent'. The creation of a new sign could
be formalised as:
\[ \mbox{{\em DefFill}}(DefFilter(TDFS1, TDFS2) \ddunify TDFS2) \]
where TDFS1 is the matching `input' {\sc tdfs} and TDFS2 is the
`output' {\sc tdfs} and {\it DefFilter} is an operation which creates
a {\sc tdfs} of a type compatible with the type of TDFS2 (and with
features appropriate for that type) in which the information contained
in TDFS1 and appropriate for the type of TDFS2 is made default: that
is DefFilter outputs a {\sc tdfs} with no strict information and a
defeasible type which is the generalisation of the types of TDFS1 and
TDFS2 if those are incompatible.  It is necessary to filter the
information given in TDFS1 in this way because $\ddunify$ would
otherwise give a {\sc tdfs} with the default root node typed $\bot$.
DefFilter essentially involves removing all information from TDFS1
which is incompatible with the type of TDFS2 and with its
appropriateness conditions: we will not formalise it here, because the
details depend on the precise approach to typing taken.  Persistent
default unification of the new {\sc tdfs} with TDFS2 ensures that
modifications specified in the lexical rule override information from
the base sign, but for third-person-sing this would not be needed.
{\it DefFill} ensures that the resultant sign is indefeasible.

The effect of this formulation is that the `reentrancies' of
Figure~\ref{3rd-sing} are replaced by three steps, the first of which
removes incompatible information from the base sign, the second of
which persistent default unifies the result with the output {\sc tdfs}
specified in the rule, and the third of which makes the result
indefeasible.  The rule can thus be rewritten simply as:
\[ \mbox{\bf base} \mapsto \mbox{\bf third-person-sg} \]
A further slight complication is that in some cases we want to ignore
some parts of the base sign that would survive DefFilter.  We can
achieve this by making use of Kaplan and Wedekind's (1993) restriction
operator.  This formalisation considerably simplifies the stipulation
of most lexical rules.  For example, the dative lexical rule given in
Figure~\ref{dative-lr} above might be reformulated as follows:
\begin{quote}
{\bf transfer-ditrans-ppto-verb} \verb+\+ SYN $\mapsto$
{\bf recip-dative-verb}
\end{quote}
Here \verb+\+ SYN indicates that the feature SYN is ignored.

The account of lexical rules we have outlined is sufficient to handle
the rules proposed in this paper and in Copestake and Briscoe (1994). 
Because the components of lexical rules are constraints
on {\sc fs}s, it is possible to use (default)
inheritance 
to capture similarities and redundancies between families
of such rules (e.g. Copestake and Briscoe, 1992,1994).

The combination of the restriction, DefFilter and default unification
operators is not expressive enough to allow a direct implementation of
lexical rules which manipulate list-values of features, such as SUBCAT
in HPSG, in complex ways. In view of Carpenter's (1991) proof that
such rules considerably increase the generative power of otherwise
constrained grammatical formalisms, this may not be a bad result.
However, it remains to be seen whether this treatment of lexical rules
can be used to characterise passive and other valency-changing or
diathesis alternation rules in a linguistically motivated fashion. The
approach to the dative construction which we describe in
\S\ref{dative} together with the reformulation of the relevant lexical
rule in this section illustrates how, in principle, all such rules
might be reanalysed and reformulated. Detailed linguistic arguments
that this general approach would yield a more adequate account than
those offered in mainstream lexicalist theories can be found in Pinker
(1989) and Goldberg (1992) amongst others.

\section{Conclusion}

We have defined an order independent version of default unification on
typed feature structures.  The operation has several desirable
properties: it behaves like monotonic unification in the cases where
there are no conflicts among the {\sc tdfs}s; it never fails when the
indefeasible information is consistent; and it returns a single,
deterministic result.  It extends that of Young and Rounds (1993) in
two important respects.  First, it handles default reentrancies:
unifying paths with distinct values with a default reentrancy doesn't
lead to unification failure.  Second, it enables defaults on {\sc
tdfs}s with more specific types to override conflicting defaults on
more general types.

We extended the definition of typed feature structures given in
Carpenter (1992), so that a {\sc tdfs} carries with it, some
information from its unification history.  We showed that this
information is essential for order independence with the full
language, but we also described sublanguages for which less
information need be retained.  The semantics of the persistent default
unification operation are defined in a modal conditional logic.  This
allows us to formally link lexical defaults with pragmatic processing.
We left as future work some formal issues concerning the relationship
of type constraints and defaults: this will be undertaken in the
context of the particular approach to typing and constraints used in
the ACQUILEX LKB system (Copestake \etal, 1993).  We should also note
that although the nature of the problem of ensuring order independence
determined the basic framework of our definition of persistent default
unification (in particular the retention of the unification history in
the form of tails) there were some subsidiary decisions where
alternative options could be considered.  In particular, alternative
treatments of default reentrancy seem possible, although there would
be a cost in terms of conceptual complexity and computational
tractability, if we moved to a more expressive definition where
reentrancy could be overridden by default values.  As with the
definition of the sublanguages, the formal framework we have developed
makes it relatively straightforward to investigate variants on the
main definition presented here, if required for particular
applications.

We demonstrated the utility of persistent default unification in
several linguistic applications: inheritance in the lexicon, feature
propagation in syntax, semantic broadening of lexical items, the
dative construction and the formulation of lexical rules.  Moreover,
we argued that because default information persists as default under
the operation, defaults can survive the lexicon and potentially be
overridden by compositional semantic rules or by pragmatic information
at the discourse level.

\section*{Acknowledgements}

This work has been presented at the Centre for Cognitive Science,
University of Edinburgh; Rank Xerox Research Centre, Grenoble;
University of Pittsburgh; {\sc csli}, Stanford University; and the
Workshop on Universals in the Lexicon in Dagstuhl, Germany.  We are
grateful for the comments from the participants of these seminars.  In
addition, we would like to thank Chris Brew, Bob Carpenter, Gabriella
Crocco, Tomaz Erjavec, Roger Evans, Gerald Gazdar, Olivier Gasquet,
Ron Kaplan, Lauri Kartunnen and Carl Vogel and one anonymous reviewer
for helpful comments and advice.  This work was partly supported by
the ESPRIT Acquilex-II, project BR-7315, grant to Cambridge
University.  Xerox PARC very kindly provided Ann Copestake with
working facilities.

\section*{References}

\newcommand{\book}[4]{\item #1 (#4) {\it #2,} #3.}
\newcommand{\booknoauthor}[3]{\item #1 (#3) {\it #2,}}
\newcommand{\forthedbook}[4]{\item #1 (eds.) (#4, forthcoming) {\it #2,} #3.}
\newcommand{\unpub}[4]{\item #1 (#4) {\it #2,} #3.}
\newcommand{\bookart}[7]{\item #1 (#7) `#2' in #5 (eds.), {\it #4,} #6, pp.~#3.}
\newcommand{\bookartnopp}[6]{\item #1 (#6) `#2' in #4 (eds.), {\it #3,} #5.}
\newcommand{\forthart}[6]{\item #1 (#6, forthcoming) `#2' in #4 (eds.),
{\it #3,} #5.}
\newcommand{\journart}[6]{\item #1 (#6) `#2', {\it #3,} {\it vol.#4,}
#5.}
\newcommand{\journartnopp}[5]{\item #1 (#5) `#2', {\it #3,} {\it vol.#4,}}
\newcommand{\forthjournart}[4]{\item #1 (#4) `#2', {\it #3,}}
\newcommand{\procart}[6]{\item #1 (#6) `#2', {\it Proceedings of the
#3,} #4, pp.~#5.}
\newcommand{\forthprocart}[5]{\item #1 (#5) `#2', 
to appear in {\it Proceedings of the #3,} #4}
\newcommand{\procartnopp}[5]{\item #1 (#5) `#2', {\it Proceedings of the
#3,} #4.}

\begin{list}{}
   {\leftmargin 1.6em
    \itemindent -\leftmargin
    \itemsep 0pt plus 1pt
    \parsep 0pt plus 1pt}



\forthjournart{Asher, N. and A.~Lascarides}
        {Lexical Disambiguation in a Discourse Context}
        {Journal of Semantics}
        {1994, in press}        

\procart{Asher, N. and Morreau, M.}
        {Common Sense Entailment: A Modal Theory of Nonmonotonic
          Reasoning}
        {Proceedings of the 12th International Joint Conference on
          Artificial Intelligence}
        {Sydney Australia}
        {}
        {1991}



\journartnopp{Bird, S. and E.~Klein}
         {Phonological Analysis in Typed Feature Systems}
         {Computational Linguistics}
         {20.3}
         {1994}


\bookartnopp{Blackburn, P.}
{Modal Logic and Attribute Value Structures}
{Diamonds and Defaults}
{M.~de~Rijke}
{Studies in Logic, Language and Information. Kluwer, Dordrecht,
Holland (available as University of Amsterdam, ITLI, LP-92-02)} 
{1992}

\procart{Boguraev, B. and J.~Pustejovsky}
        {Lexical ambiguity and the role of knowledge representation in
lexicon design}
        {13th Int. Conf. on Comp. Ling. (COLING-90)}
        {Helsinki}
        {36--42} 
        {1990}


\procart{Bouma, G.}
{Defaults in unification grammar}
{28th Annual Meeting of the Association for Computational Linguistics (ACL-90)}
{Pittsburg, Pennsylvania} 
{165--173}
{1990}

\journart{Bouma, G.}
         {Feature structures and nonmonotonicity}
         {Computational Linguistics}
         {18.2}
         {183--204}
         {1992}

\book{Boutilier, C.}
        {Conditional Logics for Default Reasoning and Belief Revision}
        {PhD Thesis, The University of British Columbia, Technical
          Report 92-1}
        {1992}
\journart{Brewka, G.}
        {Cumulative Default Logic: In Defense of Nonmonotonic
Inference Rules}
        {Artificial Intelligence}
        {50}
        {}
        {1991}

\bookart{Briscoe, E.J.}
    {Introduction}
    {1--12}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\procart{Briscoe, E.J., C.~Grover, B.K.~Boguraev and J.~Carroll}
         {A Formalism and Environment for the Development of a Large 
          Grammar of English}  
         {10th Int. Joint Conf. on Artificial Intelligence (IJCAI-87)} 
         {Milan, Italy}
         {703--708}
         {1987}


\procart{Briscoe, E.J., A.~Copestake and B.K.~Boguraev}
    {Enjoy the paper: Lexical semantics via lexicology}
    {13th Int. Conf. on Comp. Ling. (COLING-90)}
    {Helsinki}
    {42--47} 
    {1990}

\bookartnopp{Briscoe, E.J., A.~Copestake and A.~Lascarides}
            {Blocking}
            {Computational Lexical Semantics}
            {P.~St.~Dizier, P. and E.~Viegas}            
            {Cambridge University Press, Cambridge, England}
            {1993, in press}


\procart{Calder, J.}
{Paradigmatic morphology}
{4th Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-89)}
{Manchester, England}
{58--65}
{1989}



\journart{Carpenter, R.}
      {The Generative Power of Categorial Grammars and Head-Driven
Phrase Structure Grammars with lexical Rules}
      {Computational Linguistics}
      {17.3}
      {301--314}
      {1991}

\book{Carpenter, R.}
{The logic of typed feature structures}
{(Tracts in Theoretical Computer Science), Cambridge University Press,
  Cambridge, England} 
{1992}

\bookart{Carpenter, R.}
           {Skeptical and credulous default unification with
application to templates and inheritance}
    {13--37}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}



\procart{Copestake, A.}
{The ACQUILEX LKB: representation issues in semi-automatic
acquisition of large lexicons}
{3rd Conference on Applied Natural Language Processing (ANLP-92)}
{Trento, Italy}
{88--96}
{1992}

\bookart{Copestake, A.}
    {Defaults in lexical representation}
    {223--245}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}


\bookart{Copestake, A. and E.J.~Briscoe}
     {Lexical Operations in a Unification Based Framework}
     {101--119}
     {Lexical Semantics and Knowledge Representation; Proceedings of
the 1st SIGLEX Workshop, Berkeley, California}
     {J.~Pustejovsky and S.~ Bergler}
     {Springer Verlag, Berlin}
     {1992}

\forthjournart{Copestake, A. and E.J.~Briscoe}
        {Semi-Productive Polysemy and Sense Extension}
        {Journal of Semantics}
        {1994, in press}

\bookart{Copestake, A., A.~Sanfilippo,
E.J.~Briscoe and V.~de~Paiva}
    {The ACQUILEX LKB: an Introduction}
    {148--163}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\book{Cruse, D.A.}
        {Lexical Semantics}
        {Cambridge University Press, Cambridge, England}
        {1986}

\procart{Daelemans, W.}
        {A tool for the automatic creation, extension and updating of
lexical knowledge bases}
{3rd Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-87)}
        {Copenhagen}
        {70--74}
        {1987}

\journart{Daelemans, W., K.~de Smedt and G.~Gazdar}
         {Inheritance in natural language processing}
         {Computational Linguistics}
         {18.2}
         {205--218}
         {1992}



\procart{Dalrymple, M., J.~Lamping and V.~Saraswat}
      {LFG semantics via constraints}
      {6th Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-93)}
      {Utrecht, The Netherlands}
      {97--105}
      {1993}

\journart{Delgrande, J. P.}
        {An Approach to Default Reasoning Based on First Order
          Conditional Logic: Revised Report}
        {Artificial Intelligence}
        {36, 1}
        {63--90}
        {1988}        

\bookart{Dowty, D.}
{On the semantic content of the notion `Thematic Role'.}
{69--129}
{Property Theory, Type Theory and Natural Language  Semantics}
{G.~Chierchia,  B.~Partee and R.~Turner}
{D. Reidel, Dordrecht, The Netherlands} 
{1989}

\procart{Evans, R. and G.~Gazdar}
{Inference in DATR}
{4th Conference of the European Chapter of the Association 
for Computational Linguistics (EACL-1989)}
{Manchester,  England}
{66--71}
{1989a}

\bookart{Evans, R. and G.~Gazdar}
{The semantics of DATR}
{79--87}
{Proceedings of the Seventh Conference of
  the Society for the Study of Artificial Intelligence and Simulation of
  Behavior (AISB)}
{A.~G.~Cohn}
{Pitman/Morgan Kaufmann, London}
{1989b}

\journart{Fillmore, C.,P.~ Kay and C.~O'Connor}
         {Regularity and idiomaticity in grammatical constructions}
         {Language}
         {64}
         {501--538}
         {1988}

\unpub{Flickinger,  D.}
        {Lexical Rules in the Hierarchical Lexicon}
        {PhD thesis, Stanford University} 
        {1987}


\procart{Flickinger, D., C.~Pollard and T.~Wasow}
        {Structure sharing in lexical representation}
        {23rd Annual Meeting of the Association for Computational
        Linguistics (ACL-85)}
        {University of Chicago}
        {262--268}
        {1985} 



\journart{Flickinger, D. and J.~Nerbonne}
{Inheritance and complementation: A case study of {\it easy}
adjectives and related nouns}
         {Computational Linguistics}
         {18.3}
         {269--310}
         {1992}

\bookart{Gazdar, G.}
  {Linguistic applications of default inheritance mechanisms}
  {37--68}
  {Linguistic Theory and Computer Applications}
 {P.~Whitelock, H.~Somers, P.~Bennett, R.~Johnson, and M.~McGee Wood}
  {Academic Press, London}
  {1987}

\book{Gazdar, G., E.~Klein, G.~Pullum and I.~Sag}
{Generalized Phrase Structure Grammar}
{Basil Blackwell, Oxford}
{1985}

\procartnopp{Gerdemann, D. and P.~King}
      {The Correct and Efficient Implementation of Appropriateness 
Specifications for Typed Feature Structures}
      {15th Int. Conf. on Comp. Ling. (COLING-94)}
      {Kyoto, Japan}
      {1994}

\unpub{Goldberg, A.}
      {Argument structure constructions}
      {PhD Thesis, UC Berkeley}
      {1992}

\procart{Grover, C., Brew, C., Manandhar, S. and Moens, M.}
{Priority Union and Generalization in Discourse Grammars}
{32nd Annual Meeting of the Association for Computational Linguistics}
{Las Cruces}
{17--24}
{1994}

\procart{Grover, C., Brew, C., Manandhar, S. and Moens, M.}
{Priority Union and Generalization in Discourse Grammars}
{Proceedings of the 32nd Annual Meeting of the Association for
Computational Linguistics}
{Las Cruces, New Mexico}
{35--41}
{1994}

\procart{Halvorsen, P.K. and R.~Kaplan}
        {Projections and semantic description in LFG}
        {Int. Conf. on 5th Generation Computer Systems}
        {Tokyo}
        {1116--1122}
        {1988}

\bookart{Kaplan, R.}
  {Three seductions of computational psycholinguistics}
  {149--188}
  {Linguistic Theory and Computer Applications}
  {P.~Whitelock, H.~Somers, P.~Bennett, R.~Johnson, and M.~McGee Wood}
  {Academic Press, London}
  {1987}

\procart{Kaplan, R. and J.~Wedekind}
        {Restriction and Correspondence-Based Translation}
        {6th Conference of the European Chapter of
        the Association for Computational Linguistics (EACL-93)}
        {Utrecht, The Netherlands}
        {193--202}
        {1993}

\procart{Karttunen, L.}
        {D-PATR: a development environment for unification-based
grammars}
        {11th Int. Conf. on Comp. Ling. (COLING-86)}
        {Bonn, Germany}
        {74--80}
        {1986}


\procart{Kasper, R.~T. and  W.~C. Rounds}
{A logical semantics for feature structures}
{24th Annual Conference of the Association for Computational
Linguistics}
{Columbia University}
{235--242}
{1986}


\unpub{Konolige, K.}
{Hierarchic Autoepistemic Theories for Nonmonotonic Reasoning:
Preliminary Report}
{Technical Note No. 446, {\sc sri} International}
{1988}


\bookart{Kreiger, H. and J.~Nerbonne}
    {Feature-based inheritance networks for computational lexicons}
    {90--136}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\unpub{Lascarides, A.}
        {The Pragmatics of Word Meaning}
        {{\em Proceedings of the AAAI Spring Symposium on Lexical
Semantics}, Stanford CA}
        {1995}

\journart{Lascarides, A. and N.~Asher}
{Temporal Interpretation, Discourse Relations and Common Sense Entailment}
{Linguistics and Philosophy}
{16}
{437--493}
{1993}

\unpub{Lascarides, A. and Copestake, A.}
        {A Logic for Order Independent Typed Default Unification}
        {{\sc acquilex} research report, also submitted to ACL95}
        {1995}


\journart{Maxwell, J.T. and R.~Kaplan}
      {The interface of functional and syntactic constraints}
      {Computational Linguistics}
      {19.4}
      {571--590}
      {1993}


\book{Morreau, M.}
        {Conditionals in Philosophy and Artificial Intelligence}
        {PhD Thesis, IMS, Universit\"at Stuttgart}
        {1992}

\bookart{de~Paiva, V.}
    {Types and Constraints in the LKB}
    {164--189}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}


\book{Parsons,  T.}
  {Events in the Semantics of English: a Study in Subatomic Semantics}
  {MIT Press, Cambridge, Massachusetts}
  {1990} 

\book{Pinker, S}
     {Learnability and Cognition: The Acquisition of Argument
Structure} 
     {MIT Press, Cambridge, MA}
     {1989}

\book{Pollard,  C. and I. Sag}
 {An information-based approach to syntax and semantics: 
Volume~1 fundamentals} 
 {CSLI Lecture Notes 13, Stanford CA}
 {1987} 

\book{Pollard,  C. and I. Sag}
     {??}
     {CSLI Lecture Notes, Stanford, CA}
     {1994}

\journart{Pustejovsky, J.}
    {The Generative Lexicon}
    {Computational Linguistics}
    {17.4}
    {409--441}
    {1991}

\journart{Pustejovsky, J. and B.~Boguraev}
      {Lexical knowledge representation and natural language processing}
      {Artificial Intelligence}
      {63}
      {193--223}
      {1993}



\journart{Reiter, R.}
{A Logic for Default Reasoning}
{Artificial Intelligence}
{13}
{81--132}
{1980}

\procart{Russell, G., J.~Carroll and  S.~Warwick}
{Multiple default
inheritance in a unification-based lexicon} 
{29th Annual Meeting of the Association for Computational 
Linguistics (ACL-91)}
{Berkeley, California}
{215--221}
{1991}

\bookart{Russell, G., A.~Ballim,
J.~Carroll and  S.~Warwick-Armstrong}
{A Practical Approach to Multiple Default Inheritance for Unification-based 
Lexicons}
    {137--147}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\unpub{Sanfilippo,  A.}
  {Grammatical Relations, Thematic Roles and Verb Semantics}
  {PhD thesis.  Centre for Cognitive
  Science,  University of Edinburgh}
  {1990} 

\bookart{Sanfilippo, A.}
    {LKB encoding of lexical knowledge}
    {190--222}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\book{Shieber, S.~M.}
{An introduction to unification-based approaches to grammar}
{CSLI Lecture Notes 4, Stanford CA}
{1986a}

\procart{Shieber, S.~M.}
{A simple reconstruction of GPSG}
{11th Int. Conf. on Comp. Ling. (COLING-86)}
{Bonn, Germany}
{211--215}
{1986b}


\journart{Smolka, G. and H.~A\"{\i}t-Kaci}
{Inheritance hierarchies: Semantics and unification}  
{Journal of  Symbolic Computation}
{7}
{343--370}
{1988}

\book{Sweetser, E.}
    {From etymology to pragmatics}
    {Cambridge University Press, Cambridge, England}
    {1990}

\bookart{Vossen, P. and A.~Copestake}
    {Untangling definition structure into knowledge representation}
    {246--274}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}


\procart{Young, M. and W.~Rounds}
        {A logical semantics for nonmonotonic sorts}
        {31st Annual Meeting of the Association for 
Computational Linguistics (ACL-93)}
        {Columbus, Ohio}
        {209--215}
        {1993}

\bookart{Zajac, R.}
    {Issues in the design of a language for representing linguistic
information based on inheritance and feature structures}
    {74--89}
    {Inheritance, Defaults and the Lexicon}
    {E.~J.~Briscoe, A.~Copestake and V.~de~Paiva}
    {Cambridge University Press, Cambridge, England}
    {1993}

\end{list}

\end{document}
