Type System

As we mentioned in the introduction, what distinguishes ALE from other approaches to feature structures and most other approaches to terms, is that there is a strong type discipline enforced on feature structures. We have already demonstrated how to define a type hierarchy, but that is only half the story with respect to typing. The other component of our type system is a notion of feature appropriateness, whereby each type must specify which features it can be defined for, and furthermore, which types of values such features can take. The notion of appropriateness used here is similar to that found in object-oriented approaches to typing. For instance, if a feature is appropriate for a type, it will also be appropriate for all of the subtypes of that type. In other words, appropriateness specifications are inherited by a type from its supertypes. Furthermore, value restrictions on feature values are also inherited. Another important consideration for ALE's type system is the notion of type inference, whereby types for structures which are underspecified can be automatically inferred. This is a property our system shares with the functional language ML, though our notion of typing is only first-order. To further put ALE's type system in perspective, we note that type inheritance must be declared by the user at compile time, rather than being inferred. Furthermore, types in ALE are semantic, in Smolka's (1988b) terms, meaning that types are used at run-time. Even though ALE employs semantic typing, the type system is employed statically (at compile-time) to detect type errors in grammars and programs.

As an example of an appropriateness declaration, consider the simple type specification for lists with a head/tail encoding:

  bot sub [list,atom].
    list sub [e_list,ne_list].
      e_list sub [].
      ne_list sub []
              intro [hd:bot,
                     tl:list].
  atom sub [a,b].
    a sub [].
    b sub [].

This specification tells us that a list can be either empty (e_list) or non-empty (ne_list). It implicitly tells us that an empty list cannot have any features defined for it, since none are declared directly or inherited from more general types. The declaration also tells us that a non-empty list has two features, representing the head and the tail of a list, and, furthermore, that the head of a list can be anything (since every structure is of type bot), but the tail of the list must itself be a list. Note that features must also be Prolog constants, even though the output routines convert them to all caps. The appropriateness declaration, intro, can be specified along with subsumption, as shown above, or separately; but for any given type, all features must be declared at once. If no intro declaration is given for a type, it is assumed that that type introduces no appropriate features. If an intro declaration is made for a type that does not occur on either side of a sub declaration, that type is assumed to be an immediate subtype of bot with no subtypes of its own. If a value restrictor (such as list above for feature tl) does not occur on either side of a sub declaration, it too is assumed to be maximal and an immediate subtype of bot.

In ALE, every feature structure must respect the appropriateness restrictions in the type declarations. This amounts to two restrictions. First, if a feature is defined for a feature structure of a given type, then that type must be appropriate for the feature. Furthermore, the value of the feature must be of the appropriate type, as declared in the appropriateness conditions. The second condition goes the other way around: if a feature is appropriate for a type, then every feature structure of that type must have a value for the feature. A feature structure respecting these two conditions is said to be totally well-typed in the terminology of Carpenter (1992, Chapter 6).^4.4For instance, consider the following feature structures:

  list
  HD a
  TL bot

  ne_list
  HD bot
  TL ne_list
     HD atom
     TL list

  ne_list
  HD [0] ne_list
     HD [0]
     TL [0]
  TL e_list

The first structure violates the typing condition because the type list is not appropriate for any features, only ne_list is. But even if we were to change its type to ne_list, it would still violate the type conditions, because bot is not an appropriate type for the value of TL in a ne_list. On the other hand, the second and third structures above are totally well-typed. Note that the second such structure does not specify what kind of list occurs at the path TL TL, nor does it specify what the HD value is, but it does specify that the second element of the list, the TL HD value is an atom, but it doesn't specify which one.

To demonstrate how inheritance works in a simple case, consider the specification fragment from the categorial grammar in the appendix:

  functional sub [forward,backward]
             intro [arg:synsem,
                    res:synsem].
    forward sub [].
    backward sub [].

This tells us that functional objects have ARG and RES features. Because forward and backward are subtypes of functional, they will also have ARG and RES features, with the same restrictions.

There are a couple of important restrictions placed on appropriateness conditions in ALE. The most significant of these is the acyclicity requirement. This condition disallows type specifications which require a type to have a value which is of the same or more specific type. For example, the following specification is not allowed:

  person sub [male,female]
         intro [father:male,
                mother:female].
    male sub [].
    female sub [].

The problem here is the obvious one that there are no most general feature structures that are both of type person and totally well-typed.^4.5This is because any person must have a father and mother feature, which are male and female respectively, but since male and female are subtypes of person, they must also have mother and father values. It is significant to note that the acyclicity condition does not rule out recursive structures, as can be seen with the example of lists. The list type specification is acceptable because not every list is required to have a head and tail, only non-empty lists are. The acyclicity restriction can be stated graph theoretically by constructing a directed graph from the type specification. The nodes of the graph are simply the types. There is an edge from every type to all of its supertypes, and an edge from every type to the types in the type restrictions in its features. Type specifications are only acceptable if they produce a graph with no cycles. One cycle in the person graph is from male to person (by the supertype relation) and from person to male (by the FATHER feature). On the other hand, there are no cycles in the specification of list.

The second restriction placed on appropriateness declarations is designed to limit non-determinism in much the same way as the bounded completeness condition on the inheritance hierarchy. This second condition requires every feature to be introduced at a unique most general type. In other words, the set of types appropriate for a feature must have a most general element. Thus the following type declaration fragment is invalid:

  a sub [b,c,d].
    b sub []
      intro [f:w,
             g:x].
    c sub []
      intro [f:y,
             h:z].
    d sub [].

The problem is that the feature F is appropriate for types b and c, but there is not a unique most general type for which it's appropriate. In general, just like the bounded completeness condition, type specifications which violate the feature introduction condition can be patched, without violating any of their existing structure, by adding additional types. In this case, we add a new type between a and the types b and c, producing the equivalent well-formed specification:

  a sub [e,d].
    e sub [b,c]
      intro [f:bot].
      b sub []
        intro [f:w,
               g:x].
      c sub []
        intro [f:y,
               h:z].
    d sub [].

This example also illustrates how subtypes of a type can place additional restrictions on values on features as well as introducing additional features.

As a further illustration of how feature introduction can be obeyed in general, consider the following specification of a type system for representing first-order terms:

  sem_obj sub [individual,proposition].
    individual sub [a,b].
      a sub []. 
      b sub [].
  proposition sub [atomic_prop,relational].
    atomic_prop sub [].
    relational_prop sub [unary_prop,transitive_prop]
                    intro [arg1:individual].
      unary_prop sub [].
      transitive_prop sub [binary_prop,ternary_prop]
                      intro [arg2:individual].
        binary_prop sub [].
        ternary_prop sub []
                     intro [arg3:individual].

In this case, unary propositions have one argument feature, binary propositions have two argument features, and ternary propositions have three argument features, all of which must be filled by individuals.