The Static Cut

The Static Cut defines nodes in a mother^6.1 that carry no relevant information with respect to the unification with a daughter. Intuitively, these nodes can be ``left out'' while computing the unification.

Definition 6.1   For a mother $M$ and a daughter $D$ that are unifiable before parsing, the static cut is defined as $StaticCut(M,D)=RigidCut(M,D) \cup VariableCut(M,D)$.

The $RigidCut$ is defined first, representing nodes that can be ``left out'' because neither they, nor one of their ancestors, can have their type values changed by means of external sharing.

Definition 6.2   $RigidCut(M,D)=\{x\in Q_M \vert \{[y]_{\bowtie} \in Q_{M\sqcup D} \vert \exists... ...qcup D}(\pi, [y]_{\bowtie})= [x]_{\bowtie}\} \cap Ext(M\sqcup D) = \emptyset \}$, where $\bowtie$ is the equivalence relation from the definition of typed feature structure unification with respect to $M\sqcup D$.

The $VariableCut$ is now defined as nodes that are either externally shared, or have an ancestor that is externally shared, but still can be ``left out''. The name VariableCut is inspired by the fact that variables in descriptions are the source for external sharing between most general satisfiers, as described in Section 3.2.2.

Definition 6.3   $VariableCut(M,D)$ is the largest subset of $\{x\in Q_M\}$ such that:

1. $x\notin RigidCut(M,D)$
2. $\forall s\sqsupseteq \theta(x), \forall t\sqsupseteq \theta([x]_{\bowtie} \cap Q_D) . s\sqcup t\downarrow$

Basically, definition 6.3 is saying that a node can be left out even if it is externally shared (or has an externally shared ancestor) if all possible types this node can have unify with all possible types its corresponding nodes in $M\sqcup D$ can have. The first condition can also be written as follows: $\exists y\in Ext(M\sqcup D) . \exists \pi . \delta^*_{M\sqcup D}(\pi, [y]_{\bowtie})= [x]_{\bowtie}$.

Definition 6.4   $M^{\textrm{\Cutleft}}= \langle Q',\overline{Q'}, \theta,\delta \rangle$ is the Statically Cut typed feature structure (symbolized as $M^{\textrm{\Cutleft}_D}$) of a mother $M=\langle Q,\overline{q}, \theta, \delta\rangle$ with respect to a daughter $D$ iff $Q'=Q\setminus StaticCut(M,D)$.

It should be mentioned that $M^{\textrm{\Cutleft}_D}$ is created after the mother $M$ is created (i.e., after the rule is completed). Only the nodes in $M$ that are accessible before parsing can be included in the $RigidCut$ or in the $VariableCut$.

Intuitively, the nodes in the Statically Cut typed feature structure of $M$ after the rule is completed (symbolized as $\widehat{M}^{\textrm{\Cutleft}_D}$) are mappings of the nodes in $M^{\textrm{\Cutleft}_D}$ before rule is completed.

Definition 6.5   $\widehat{M}^{\textrm{\Cutleft}_D}= \langle Q',\overline{Q'}, \theta,\delta \rangle$ is the Statically Cut typed feature structure of a mother $M=\langle Q,\overline{q}, \theta, \delta\rangle$ with respect to a daughter $D$ after $M$'s rule is completed iff

• $M$'s rule represented as an MRS is $R=\langle \dots, M\rangle$, and $M^{\widehat{n}}$ is the mother of the same rule after the rule is completed: $R^{\widehat{n}}=\langle \dots, M^{\widehat{n}}\rangle$ (where $n$ is the length of $R$),
• $Q'$ is the largest set of nodes $\{\widehat{x} \in Q_{M^{\widehat{n}}} \vert \exists x\in ([\widehat{x}]^{-1}\cap Q), x\notin StaticCut(M,D)\}$.

In the above definition, the set $[\widehat{x}]^{-1}$ must be intersected with $Q$ in order to exclude from $Q'$ daughters' nodes that, by means of structure sharing, are mapped into $\widehat{x}$ during parsing.

Figure 6.1: Static Cut - An Example. The dotted lines pointing to nodes $x_2$, $y_3$, and $y_7$ represents external structure sharing (caused by active external variables.) After the static analysis is performed, $StaticCut(M,D)=\{x_1, x_3, x_5,x_6\}$.

Figure 6.1 presents an example of a mother $M$ and a daughter $D$ that are unifiable before parsing. Nodes $x_1, x_6, y_1$ and $y_2$ have the following types assigned initially: $\theta(x_1)=t_1, \theta(x_6)=t_7, \theta(y_1)=t_2, \theta(y_2)=t_3$. Type values for the rest of the nodes are drawn from the appropriateness specifications: $\theta(x_2)=t_2, \theta(x_3)=t_5, \theta(x_4)=t_1, \theta(x_5)=t_6, \theta(x_7... ...ta(y_4)=t_1, \theta(y_5)=t_6, \theta(y_6)=t_6, \theta(y_7)=t_1, \theta(y_8)=t_1$. The following equivalence relations exist between nodes from $M$ and from $D$: $x_1\bowtie y_1$, $x_2 \bowtie y_2$, $x_3\bowtie y_3$, $x_4\bowtie y_4$, $x_5\bowtie y_5$, $x_6\bowtie y_6$ $x_7\bowtie y_7$.

Given the type hierarchy, the initial type assignments, the types from appropriateness, and the equivalence relations between nodes from $M$ and from $D$, the static analysis on $M$ and $D$ produces $StaticCut(M,D)=\{x_1, x_3, x_5,x_6\}$. For each node in $M$, the static analysis produced the results as follows:

$x_1$:

Since there is no external structure sharing on $x_1$ or $y_1$, $x_1\in RigidCut(M,D)$.

$x_2$:

There is external structure sharing on $x_2$. $\theta(x_2)=t_2$ (through appropriateness specification for feature $F$), and $\theta(y_2)=t_3$. Since $t_2$ has $t_4$ as a subtype, Condition 2 of Definition 6.3 is not satisfied ( $t_4 \sqcup t_3\uparrow$). Therefore, $x_2\notin VariableCut(M,D)$.

$x_3$:

$x_3\notin RigidCut(M,D)$ since its ancestor $x_2$ is in an external structure sharing. However, $x_3\in VariableCut(M,D)$ since Condition 2 is satisfied for $x_3$ and $y_3$ ( $\theta(x_3)=t_5$ and $\theta(y_3)=t_5$.)

$x_4$:

Similar to $x_2$, $x_4\notin StaticCut(M,D)$, with the difference that the external sharing is on $D$'s side (on node $y_4$.)

$x_5$:

Condition 2 is satisfied for $x_5$ and $y_5$ ( $\theta(x_5)=t_6$ and $\theta(y_5)=t_6$), therefore $x_5\in VariableCut(M,D)$.

$x_6$:

No external sharing is on $x_6$ or $y_6$ (or any of their ancestors), therefore $x_6\in RigidCut(M,D)$.

$x_7$:

The most interesting example is $x_7$. Even though its ancestors have no external sharing, its corresponding $y_7$ ( $x_7\bowtie y_7$) does, by being shared between two paths (one of them being $K:G$, which does not appear in $M$). $\theta(x_7)=t_3$ (by unifying the appropriateness for $I$ and $G$) and $\theta(y_7)=t_1$. Since $t_5\sqsupseteq t_1$, and $t_5\sqcup t_3\uparrow$, Condition 2 fails, and therefore, $x_7\notin StaticCut(M,D)$. This is indeed justified, because $\theta(y_8)$ can promote from $t_1$ to any subtype of $t_1$, including $t_5$. But for $t_5$, appropriateness promotes the type restriction of feature $G$ to $t_5$, thus promoting $\theta(y_7)$ from $t_1$ to $t_5$, which no longer unifies with $\theta(x_7)$.

Proposition 6.1   For a mother $M$ and a daughter $D$, if $M\sqcup D\downarrow$ before parsing, and $\widehat{M}$ and $\widehat{D}$ exist (after completion), then after completion:

1. $\widehat{M}^{\textrm{\Cutleft}_D} \sqcup \widehat{D}\downarrow \textrm{\mbox{$=\!\!\!>$}}\widehat{M}\sqcup \widehat{D}\downarrow$,
2. $\widehat{M}^{\textrm{\Cutleft}_D} \sqcup \widehat{D}\uparrow \textrm{\mbox{$=\!\!\!>$}}\widehat{M}\sqcup \widehat{D}\uparrow$.

In the above proposition, the notation $\widehat{D}$ symbolizes the daughter ${D_i}^{\widehat{i-1}}$ in a rule $R^{\widehat{i-1}}=\langle {D_1}^{\widehat{i-1}},\dots,{D_i}^{\widehat{i-1}},\dots \rangle$ (i.e., the rule $R=\langle D_1,\dots,D_i,\dots \rangle$ during completion, after daughters $D_1,\dots,D_{i-1}$ are unified with edges from the chart.)

Proof. Follows from the proof of Proposition 6.6. $\qedsymbol$