Type Constraints

[Code]
Our logical language of descriptions can be used with the type system in order to enforce constraints on feature structures of a particular type. Constraints are attached to types, and may consist of arbitrary descriptions. Their effect is to require every structure of the constrained type to always satisfy the constraint description.

Constraints are enforced using the cons operator, e.g.:

  bot sub [a,b].
    a sub []
      intro [f:b,g:b].
    b sub [].
  a cons (f:X,g:=\= X).

The constraint on the type a (which must occur within parentheses) requires all feature structures of type a to have non-token-identical values for features $f$ and $g$. Notice that the type b has no constraints expressed. This is equivalent to specifying the constraint:

  b cons bot.

which is satisfied by any feature structure (of type b). A type constraint may use any of the operators in the description language, including further type descriptions, which may themselves be constrained. The type, bot, may not have type constraints, nor may a_/1 atoms.

It is crucial that the type descriptions be finitely resolvable. Because simple depth-first search is used to evaluate constraints, infinite resolution paths will cause the system to hang. For example, the following signature should not contain the following constraints:

  bot sub [a,b].
    a sub [c]
      intro [f:bot].
      c sub [].
    b sub []
      intro [g:bot].
  a cons f:b.
  b cons g:c.

This is because a subsumes c. Notice, however, that type constraints can be used to provide additional information regarding value restrictions on appropriate features. In general, ALE performs more efficiently when restrictions are provided in the appropriateness conditions, rather than in general constraints; but type constraints can encode a greater variety of restrictions. Specifically, they allow constraints to express path equations and inequations, as well as deeper path restrictions. Constraints may include relational constraints, which are defined using definite clauses, which are discussed below. Type constraints are efficiently compiled in the same way as other descriptions. Also, like appropriateness conditions, they are only enforced once for any given structure.

It is also important to note that because of the delay in ALE's inequational enforcement, type constraints that involve recursion that terminates by an inequation failure may go into infinite loops due to this delay in enforcement. Because extensionality is only enforced before the answer to a top-level query is given, recursive type constraints that rely on the extensional identity of two feature structures to terminate on the basis of their type will not terminate.