Descriptions and Most General Satisfiers

Descriptions are used to logically describe specific feature structures. While AVMs can be used to graphically describe feature structures, descriptions can be seen as a ``way to talk about feature structures'' [Carpenter1992] through the use of a logical language. This section provides a short summary of the complete presentations of descriptions and satisfiability found in [Carpenter1992] and [Penn2000].

Definition 2.13   The set of descriptions, over a set of types Type, set of variables Vars, and set of features Feat, is the least set Desc such that:

• $\sigma\in Desc$, for all $\sigma\in Type$,
• $x\in Desc$, $\forall x\in Vars$,
• $\pi :\phi\in Desc$, for all paths $\pi\in Feat^*$ and $\phi\in Desc$,
• $\pi\doteq\pi' \in Desc$, if $\pi, \pi'\in Desc$,
• $\phi\wedge\psi\in Desc$, if $\phi\in Desc$ and $\psi\in Desc$.

Definition 2.14   The satisfaction relation $\models$ between feature structures and descriptions is the least relation such that:

• $F\models\sigma$ if $\sigma\in Type$ and $\sigma\sqsubseteq\theta(\overline{q})$,
• $F\models\pi:\phi$ if $F@\pi\models\phi$,
• $F\models\pi\doteq\pi'$ if $\delta(\pi,\overline{q})=\delta(\pi',\overline{q})$,
• $F\models\phi\wedge\psi$ if $F\models\phi$ and $F\models\psi$,

While in [Carpenter1992] disjunctions are used in the description language, in this thesis, the description language has no disjunction defined. One can consider a disjunction in a description as specifying two distinct descriptions.

Every satisfiable description is logically satisfied by a most general feature structure. This most general feature structure of a description $\phi$ is called $MGSat(\phi)$, and $MGSat(\phi)\sqsubseteq F$, for every $F$ that satisfies $\phi$. The Most General Satisfier provides a way of mapping a description to a feature structure.