Attribute-Value Logic

[Reference Manual]
[Code] Now that we have seen how the type system must be specified, we turn our attention to the specification of feature structures themselves. The most convenient and expressive method of describing feature structures is the logical language developed by Kasper and Rounds (1986), which we modify here in three ways. First, we replace the notion of path sharing with the more compact and expressive notion of variable due to Smolka (1988a). Second, we extend the language to types, following Pollard (in press). Finally, we add inequations.

The collection of descriptions used in ALE can be described by the following BNF grammar:

  <desc> ::= <type>
           | <variable>
           | (<feature>:<desc>)
           | (<desc>,<desc>)
           | (<desc>;<desc>)
           | (=\= <desc>)

As we have said before, both types and features are represented by Prolog constants. Variables, on the other hand, are represented by Prolog variables. As indicated by the BNF, no whitespace is needed around the feature selecting colon, conjunction comma and disjunction semi-colon, but any whitespace occurring will be ignored.

These descriptions are used for picking out feature structures that satisfy them. We consider the clauses of the definition in turn. A description consisting of a type picks out all feature structures of that type. A variable can be used to refer to any feature structure, but multiple occurrences of the same variable must refer to the same structure. A description of the form (<feature>:<desc>) picks out a feature structure whose value for the feature satisfies the nested description. An inequation =$\backslash$= <desc> is satisfied by those feature structures that are not token-identical to the feature structure described by <desc>. Inequations are discussed in more detail below.

There are two ways of logically combining descriptions: following Prolog, the comma represents conjunction and the semi-colon represents disjunction. A feature structure satisfies a conjunction of descriptions just in case it satisfies both conjuncts, while it satisfies a disjunction of descriptions if it satisfies either of the disjuncts.

We should also add to the above BNF grammar the following line:

  <desc> ::= (<path> == <path>)

This is an equational description, of which inequations are the negation. Equational or inequational descriptions are satisfied by the presence or absence, respectively, of token-identity. In particular, an inequation between two structurally-identical feature structures can be satisfied, while a path equation can only be satisfied by two structurally-identical feature structures, but is not necessarily satisfied.

All instances of equational descriptions can be captured by using multiple occurrences of variables. For example, the description:

  ([arg1]==[arg2])

is equivalent to the description:

  (arg1:X,arg2:X).

assuming there are no other occurrences of X.

Standard assumptions about operator precedence and association are followed by ALE, allowing us to omit most of the parentheses in descriptions. In particular, equational descriptions bind the most tightly, followed by feature selecting colon, then by inequations, then conjunction and finally disjunction. Furthermore, conjunction and disjunction are left-associative, while the feature selector is right-associative. For instance, this gives us the following equivalences between descriptions:

  a, b ; c, d ; e = (a,b);(c,d);e

  a,b,c = a,(b,c)
  
  f:g:bot,h:j = (f:(g:bot)),(h:j)

  f:g: =\=k,h:j = (f:(g: =\=(k))),(h:j)

  f:[g]==[h],h:j = (f:([g]==[h])),(h:j)

Note that a space must occur between =$\backslash$= and other operators such as :.

A description may be satisfied by no structure, a finite number of structures or an infinite collection of feature structures. A description is said to be satisfiable if it is satisfied by at least one structure. A description $\phi$ entails a description $\psi$ if every structure satisfying $\phi$ also satisfies $\psi$. Two descriptions are logically equivalent if they entail each other, or equivalently, if they are satisfied by exactly the same set of structures.

ALE is only sensitive to the differences between logically equivalent formulas in terms of speed. For instance, the two descriptions (tl:list,ne_list,hd:bot) and hd:bot are satisfied by exactly the same set of totally well-typed structures assuming the type declaration for lists given above, but the smaller description will be processed much more efficiently. There are also efficiency effects stemming from the order in which conjuncts (and disjuncts) are presented. The general rule for speedy processing is to eliminate descriptions from a conjunction if they are entailed by other conjuncts, and to put conjuncts with more type and feature entailments first. Thus with our specification for relations above, the description (arg1:a, binary_proposition) would be slower than (binary_proposition,arg1:a), since binary_proposition entails the existence of the feature arg1, but not conversely.^4.9

At run-time, ALE computes a representation of the most general feature structure that satisfies a description. Thus a description such as hd:a with respect to the list grammar is satisfied by the structure:

  ne_list
  HD a
  TL list

Every other structure satisfying the description hd:a is subsumed by the structure given above. In fact, the above structure is said to be a vague representation of all of the structures that satisfy the description. The type conditions in ALE were devised to obey the very important property, first noted by Kasper and Rounds (1986), that every non-disjunctive description is satisfied by a unique most general feature structure. Thus in the case of hd:a, there is no more general feature structure than the one above which also satisfies hd:a.

The previous example also illustrates the kind of type inference used by ALE. Even though the description hd:a does not explicitly mention either the feature TL or the type ne_list, to find a feature structure satisfying the description, ALE must infer this information. In particular, because ne_list is the most general type for which HD is appropriate, we know that the result must be of type ne_list. Furthermore, because ne_list is appropriate for both the features HD and TL, ALE must add an appropriate TL value. The value type list is also inferred, due to the fact that a ne_list must have a TL value which is a list. As far as type inference goes, the user does not need to provide anything other than the type specification; the system computes type inference based on the appropriateness specification. In general, type inference is very efficient in terms of time. The biggest concern should be how large the structures become.^4.10In contrast to a vague description, a disjunctive description is usually ambiguous. Disjunction is where the complexity arises in satisfying descriptions, as it corresponds operationally to non-determinism.^4.11For instance, the description hd:(a;b) is satisfied by two distinct minimal structures, neither of which subsumes the other:

  ne_list       ne_list
  HD a          HD b
  TL list       TL list

On the other hand, the description hd:atom is satisfied by the structure:

  ne_list
  HD atom
  TL list

Even though the descriptions hd:atom and hd:(a;b) are not logically equivalent (though the former entails the latter), they have the interesting property of being unifiable with exactly the same set of structures. In other words, if a feature structure can be unified with the most general satisfier of hd:atom, then it can be unified with one of the minimal satisfiers of hd:(a;b).

In terms of efficiency, it is very important to use vagueness wherever possible rather than ambiguity. In fact, it is almost always a good idea to arrange the type specification with just this goal in mind. For instance, consider the difference between the following pair of type specifications, which might be used for English gender:

  gender sub [masc,fem,neut].        gender sub [animate,neut].
    masc sub [].                       animate sub [masc,fem].
    fem sub [].                          masc sub [].
    neut sub [].                         fem sub [].
                                       neut sub [].

Now consider the fact that the relative pronouns who and which are distinguished on the basis of whether they select animate or inanimate genders. In the flatter hierarchy, the only way to select the animate genders is by the ambiguous description masc;fem. The hierarchy with an explicit animate type can capture the same possibilities with the vague description animate. An effective rule of thumb is that ALE does an amount of work at best proportional to the number of most general satisfiers of a description and at worst proportional to $2^n$, where $n$ is the number of disjuncts in the description. Thus the ambiguous description requires roughly twice the time and memory to process than the vague description. Whether the amount of work is closer to the number of satisfiers or exponential in the number of disjuncts depends on how many unsatisfiable disjunctive possibilities drop out early in the computation.

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^4.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.