Enforcement of Inequations

Inequations are persistent in that once that are created, they remain as long as one of the structures being inequated remains. Thus the following two descriptions are logically equivalent:

  f:(=\=c), f:c

  f:c, f:(=\=c)

Both will cause failure; but they are not operationally equivalent. An inequation is evaluated when it arises, and again after high-level unifications in the system; but inequations are not evaluated every time an inequated structure is modified. In an ideal system, inequations would be attached directly to structures so that they could be evaluated on-line during unification. As things stand, ALE represents a feature structure as a regular feature structure with a separate set of inequations. Also, the complexity is sensitive to the conjunctive normal form of inequations at the time at which it is evaluated, though this form may later be reduced.

These sets of inequations are evaluated at run-time at the point they are encountered, before answers are given to top-level queries, before any edge is added to ALE's parsing chart, after every daughter is matched to a description in an ALE grammar rule ^3.12, and after the head of an ALE definite clause has been matched to a goal. At compile-time, inequations are checked for every empty category, for every lexical entry, and after every lexical rule application.

Inequations are also symmetric. Thus the following two descriptions are logically equivalent:

  f:(=\= X),g:X

  f:X,g:(=\= X)

Both inequate the values of F and G. Again, these are not operationally equivalent. Because inequations are evaluated at the time they are encountered, the second ordering will normally detect an immediate failure sooner than the first.

An inequation between two feature structures is a requirement for them not to be token-identical. Thus, if a type is intensional, it is possible for two feature structures to be of that same type, and still satisfy an inequation between them. Thus, any attempt to inequate two structures that should be identical as a result of extensional typing will also cause failure. For instance, consider the following:

  s              s
  F [1] t        F [3]
    H [1]   +    G [4]           =  failure
  G [2] t        [3] =\= [4]
    H [1]

The values of the features F and G cannot be inequated because they are extensionally identical (assuming the type t is declared to be extensional and is only appropriate for the feature H.

When inequations are evaluated, they are reduced. This reduction consists, in part, of partial evaluation of extensionality checking, which is otherwise delayed in ALE. For instance, consider the following:

  F [1] s
    H bot
    J bot
  G [2] s
    H bot
    J bot
  [1] =\= [2]

If the type s is extensional and appropriate for the features H and J, then the inequation above is reduced to the following:

  F [1] s
    H [3] bot
    J [4] bot
  G [2] s
    H [5]
    J [6]
  [3] =\= [5] ; [4] =\= [6]

The set of inequations is stored in conjunctive normal form. The cost is some space over the re-evaluation of inequations. Of course, if the types on [3] and [4] were more refined than bot, then the inequations [3] =\= [5] and [4] =\= [6] would further reduce. In addition, when reducing inequations in this way, we eliminate those that are trivially satisfied. The ones that are printed are only the residue after reduction. For instance, consider the following structure:

  F [1] s
    H [3] a
    J bot
  G [2] s
    H [3]
    J bot
  [1] =\= [2]

Since the H values are token-identical, this structure reduces to the following.

  F s
    H [3] a
    J [4] bot
  G s
    H [3]
    J [5] bot
  [4] =\= [5]

If structures [4] and [5] had been of non-unifiable types, then there would be no residual inequation at all -- the original inequation would trivially be satisfied.

An important subcase is that of an inequation between extensional atoms. If an atom is extensional, then there is only one instance of it. Thus an inequation between two identical, extensional atoms always fails. For example, if a type signature includes:

  bot sub [..., a, b, ...].
  a sub [].
    intro [f:bot].
  b sub [].
  ...
  ext([..., b, ...]).

then the description:

  (a,f:=\= b)

is satisfied just in those cases where the value of F is not of type b. If b were intensional, then the inequation in this description would essentially have no effect. In fact, the only productive instances of inequations between two intensionally typed feature structures are those used with multiply occurring variables. In all other instances, there is no way for the inequation to be violated, since there is no way to render a structurally-identical copy of an intensionally typed feature structure token-identical to any other structure. ALE detects these trivially satisfied inequations and disposes of them.