Compiling Appropriateness Conditions

[User's Manual]
[Code]
The closed Boolean semiring, $B_{OR}$, suffices for processing simple partial orders of types with no features, often called type hierarchies. For type signatures with feature appropriateness conditions and value restrictions on those features, this is not enough however.

We can think of 0 and 1 in $B_{OR}$ as constituting a very small type hierarchy, as shown in Figure 3.8. If $\top$ corresponds to 1, and $\bot$ to 0, then unification in this hierarchy corresponds to Boolean OR. We can also write this as in Figure 3.9, in which the trivial type hierarchy, consisting of just $\bot$, has been bottom-lifted to add a new bottom, $\underline{\bot}$. Because bottom-lifting preserves meet-semi-latticehood, we can trivially extend unification, $\sqcup$, to any $P\cup\{\underline{\bot}\}$ where $P$ is a finite meet semi-lattice. Now, we need something to correspond to AND:

$$a\underline{\sqcup}b = \left\{ \begin{array}{ll} \underlin... ...{\bot}\\ a\sqcup b & \mathrm{otherwise} \end{array} \right.$$

Figure 3.8: The Boolean type hierarchy

top$\top$

bot$\bot$

topbot

Figure 3.9: The trivial type hierarchy lifted to produce the Boolean hierarchy

bot1$\bot$

bbot $\underline{\bot}$

bot1bbot

Definition 7   Let $\langle P, \sqsubseteq\rangle$ be a finite meet semi-lattice. Then $Q(P) = \langle P\cup\{\underline{\bot}\},\sqcup,\underline{\sqcup},\underline{\bot},\bot\rangle$, is the closed semiring induced by $P$.

Notice that we can define this for all $P$, not just the trivial type hierarchy, because in all type hierarchies, $\sqcup$ and therefore its extension to $P\cup\{\underline{\bot}\}$ and to $\underline{\sqcup}$, are total functions, and there is a least element. As can easily be verified:

Proposition 1   For all finite meet semi-lattices $P$ with a greatest element, $Q(P)$ is a closed semi-ring.

The existence of a greatest element ensures that $\sqcup$ and $\underline{\sqcup}$ are closed in $P\cup\{\underline{\bot}\}$. Without loss of generality, we can assume that the greatest element, $\top$, does not explicitly appear in $P$, and that it does not occur anywhere else in the signature, e.g., in appropriateness conditions. $\top$ can be smashed onto any such $P$, and is typically implemented as type unification failure in the original signature. Figure 3.10 shows the type hierarchy in Figure 3.1 $\underline{\bot}$-lifted and $\top$-smashed to form its induced closed semiring.

The benefit of using $P(Q)$ is that it allows us to generalize to other computations on signatures that require matrices with types in them rather than just 0s and 1s. The subsumption matrix of $P$ can still be constructed using $\underline{\bot}$ and $\bot$ in place of 0 and 1, respectively.

Figure 3.10: The induced closed semiring, $Q(P)$, constructed from Figure 3.1

Feature Introduction

[Code]
In the logic of typed feature structures, appropriateness conditions take the form of a restriction on which types can bear a particular feature, and which types that feature's value can have.

Definition 8   A type signature is a quadruple, $\langle P,\sqsubseteq,F,A\rangle$, where $\langle P, \sqsubseteq\rangle$ is a finite meet semi-lattice, $F$ is a set of features, and $A: F \times P \rightharpoonup P$ is a partial function such that:

• (Feature Introduction)
  for every $\mbox{\sc f}\in F$, there is a most general type $\mathit{intro}(\mbox{\sc f})\in P$ such that $A(\mbox{\sc f},\mathit{intro}(\mbox{\sc f}))\mathord{\downarrow}$,^3.2 and
• (Upward Closure / Right Monotonicity)
  if $A(\mbox{\sc f},t)\mathord{\downarrow}$ and $t\sqsubseteq u$, then $A(\mbox{\sc f},u)\mathord{\downarrow}$ and $A(\mbox{\sc f},t)\sqsubseteq A(\mbox{\sc f},u)$.

$A(\mbox{\sc f},t)$ is defined on those types, $t$, that can bear the feature F, and its value is a type that must subsume the type of the value of F at $t$.

Feature Introduction eliminates a source of disjunction in inferring types from feature names in descriptions. By having a unique introducing type, it is possible to apply appropriateness in the other direction immediately to infer some of the other features that must also exist, along with the types of their values.

In practice, signature declarations specify appropriateness only by declaring (1) where a feature is introduced, along with the type its value must have and (2) where a feature takes on a value whose type cannot be inferred to be the least type that satisfies Upward Closure and/or Right Monotonicity given its value on supertypes. The type to which a feature's value is constrained is called a value restriction. Figure 3.11, for example, is Figure 3.1 with appropriateness declarations added.

Figure 3.11: An example type signature

F is appropriate to a, for example, with value restriction, $\bot$. Because F is appropriate to a, it is also appropriate to b, c and e, although b refines the value restriction to c. b has two appropriate features because it also introduces G. e has two appropriate features by Upward Closure because H was introduced at d.

In order to enforce this view of appropriateness conditions on $P$, we can build a matrix over $Q(P)$ for these declarations:

Definition 9   Given a set of types, $P$, a set of features, $F$, and a partial function of appropriateness declarations $D: F\times P\rightharpoonup P$, the value declaration matrix for $D$ over $F$ and $P$ is a $\mathord{\mid} P\/ \mathord{\mid}\times \mathord{\mid} F\/ \mathord{\mid}$ matrix, $V$, over $Q(P)$, in which $V_{i,j} = u$ if there exists a $u\in P$ such that $D(\mbox{\sc f}_{j},t_{i})=u$, and $V_{i,j}= \underline{\bot}$ if there is no such $u$.

The uniqueness of $u$, when it exists, is guaranteed by the fact that $D$ is a partial function. The value declaration matrix for Figure 3.11 is shown in Figure 3.12. The entry for type $d$, feature H is $b$ because H is declared as appropriate to $d$ with its value restricted to $b$.

Figure 3.12: The value declaration matrix of Figure 3.11

Notice that $\underline{\bot}$ is being used here as a place-holder for pairs of type, t and feature, F, for which F is not appropriate to t. We use $\underline{\bot}$ rather than $\top$ so that feature introduction (with a value restriction of $\bot$ or greater) still respects Right Monotonicity.

Definition 10   The value restriction matrix of $P$ is $R = S^{T}\cdot V$.

Premultiplying $V$ by the transpose of $S$ closes the appropriateness declarations under subsumption. $V_{i,j}$ is thus something other than $\underline{\bot}$ iff feature $j$ is appropriate to type $i$. The value restriction matrix of Figure 3.11 is shown in Figure 3.13. Notice that the entry for type e, feature H is also b because e inherits H from d.

Figure 3.13: The value restriction matrix of Figure 3.11

Using the value restriction matrix, we can then express the condition on Feature Introduction:

Definition 11   $\delta: P\cup \{\underline{\bot}\} \rightarrow \{\underline{\bot},\bot\}$ is the characteristic function for $P$, such that:

$$\delta(t) = \left\{ \begin{array}{ll} \bot & \mbox{if $t\i... ...ne{\bot}& \mbox{if $t=\underline{\bot}$} \end{array} \right.$$

Proposition 2   $R$ satisfies the feature introduction restriction iff for all $i$, there exists a $j$, such that $\vec{\delta}(R^{T}_{i})=S_{j}$.

$\delta$ projects the elements of $Q(P)$ back onto the closed Boolean semi-ring, according to whether they belong to $P$. Feature Introduction is satisfied iff, after component-wise projection, every column of $R$ is the same as some row of $S$. Rows of $S$ encode types as the upward closed sets that they subsume. The columns of $R$ have non- $\underline{\bot}$ values for the types to which a feature, F, is appropriate; and we know that that set is upward-closed, having left-multiplied by $S^{T}$. If that set is one of the rows of $S$, then that row corresponds to a least type, which is $intro($F$)$.

Along the way, we can also compute those introducing types:

Definition 12   The introduction matrix, $I$, of $P$ is a $\mathord{\mid} P\/ \mathord{\mid}\times \mathord{\mid} F\/ \mathord{\mid}$ matrix in which $I_{j,i}=V_{j,i}$ when $j$ is the $j$ specified for $i$ in Proposition 2, and $\underline{\bot}$ elsewhere.

The introduction matrix for Figure 3.11 is given in Figure 3.14.

Figure 3.14: The introduction matrix of Figure 3.11

The entry for type b, feature F is $\underline{\bot}$ because, although b places a non-inferable value restriction on F, it does not introduce F.

Value Restriction Consistency

[Code]
Because of Right Monotonicity, join-reducible types can not only multiply inherit features, but also inherit value restrictions on the same feature from two or more different branches; and these must be consistent. Figure 3.15 shows an example of this.

Figure 3.15: A type signature with consistent value restrictions

Right Monotonicity from b and c requires F to be appropriate to d with a value of both f and g. In Figure 3.15, this is consistent--the value of F at d must be of type h. Without h, it would not be consistent. We can use value restriction matrices to enforce this consistency check as well.

Proposition 3   The value restrictions of $P$ are consistent iff there is no $i$,$j$ for which $R_{i,j}=\top$.

$\top$ corresponds to inconsistency in the original signature.

The value declaration matrix for Figure 3.15 is given in Figure 3.16.

Figure 3.16: The value declaration matrix of Figure 3.15

The value restriction matrix of Figure 3.15 is given in Figure 3.17.

Figure 3.17: The value restriction matrix of Figure 3.15

Without h, the entry for d would have been $\top$.

Appropriateness Cycles

All types must have a finite most general satisfier, a finite least informative feature structure of that type that respects appropriateness conditions. This means that appropriateness conditions may not conspire so as to require a feature structure of type t to have a proper substructure of type either t or a subtype of t. Very often, the appropriateness conditions will allow a subtype of t to occur, but that is not the same thing. Non-empty lists, for example, have a tail appropriate to lists, of which non-empty lists are a subtype. That makes lists a recursive data type, but lists still have finite most general satisfiers. The former kind of appropriateness cycle can very naturally be described using $R$.

Definition 13   The convolution matrix of $R$, $C$, is a $\mathord{\mid} P\/ \mathord{\mid}\times \mathord{\mid} P\/ \mathord{\mid}$ matrix over $Q(P)$ such that $C_{i,j}=\bot$ if there exists a $k$ such that $R_{i,k}=t_{j}$, and $C_{i,j}=\underline{\bot}$ otherwise.

Proposition 4   $P$ has an appropriateness cycle iff there exists an $i$ such that $C^{*}_{i,i}= \bot$, where $C^{*}$ is the (non-reflexive) transitive closure of $C$.

$C_{i,j}=\bot$ means that type $t_{j}$ is accessible as a substructure by some feature from structures of type $t_{i}$. By transitively closing $C$, we extend that accessibility to finite paths of features, and so can detect whether $t_{i}$ is accessible from $t_{i}$. Because we convoluted $C$ from $R$, which was upward closed by left-multiplication with $S^{T}$, we detect accessibility to subtypes of $t_{i}$ as well. The convolution of Figure 3.17 is given in Figure 3.18 (0 and 1 are used for readability).

Figure 3.18: The convolution of Figure 3.17

The entry for row $b$, column $f$ is $\bot$, because $f$ is accessible from $b$ along the feature F. In this case, the transitive closure of $C$ is the same as $C$ itself, because all types that occur as value restrictions of features are atomic, i.e., they have no features of their own.

In practice, this transitive closure can be computed directly from $R$, without explicitly constructing $C$.

Join Preservation Condition

Not all type signatures are statically typable. This means that there are some signatures for which the result of unifying two feature structures that obey appropriateness must be reverified as obeying appropriateness. Although these signatures are technically valid ones, systems that process with LTFS normally check for static typability because of the computational cost of this run-time verification. Signatures that are not statically typable are those that do not satisfy the following condition:

Definition 14   A signature, $\langle P,\sqsubseteq,F,A\rangle$, satisfies the join preservation condition iff for all consistent $t,u\in P$ and $\mbox{\sc f}\in F$:

$$\begin{eqnarray*} \lefteqn{A(\mbox{\sc f},t\sqcup u) =}\\ & & \hspace*{-.5cm}\l... ...row}\\ \mbox{anything} & \mbox{otherwise} \end{array} \right. \end{eqnarray*}$$

Proposition 5   $\langle P,\sqsubseteq,F,A\rangle$ satisfies the join preservation condition iff for all $i,j$ for which $J_{i,j}=\bot$, and $U_{i,j}=t_{k}$, $R_{i}\vec{\sqcup} R_j \vec{\sqcup} (S^{T}I)_k = R_k$.

Viewed in terms of $R$, join preservation is a linear dependence condition among consistent types--recall that in $Q(P)$, $\sqcup$ corresponds to the additive operator. In a join-preserving signature, joins cannot add new information to the system, apart from introducing new features.