Evaluating Descriptions

[Code]
Descriptions can be evaluated in order to find their most general satisfiers. ALE provides the following form of query:

  | ?- mgsat tl:e_list.

  ne_list_quant
  HD quant
     RESTR proposition
     SCOPE proposition
     VAR individual
  TL e_list

  ANOTHER?  n.

  yes

Note that there must be whitespace between the mgsat and the description to be satisfied. The answer given above is the most general satisfier of the description tl:e_list using the signature in the categorial grammar in the appendix. It is important to note here that type inference is being performed to find most general satisfiers. In the case at hand, because lists in the categorial grammar are typed to have quantifiers as their HD values, the value of the HD feature in the most general satisfier has been coerced to be a quantifier.

Satisfiable non-disjunctive descriptions always have unique most general satisfiers as a consequence of the way in which the type system is constrained. But a description with disjunctions in it may have multiple satisfiers. Consider the following query:

  | ?- mgsat hit,hitter:(j;m).

  hit
  HITTEE individual
  HITTER j

  ANOTHER?  y.

  hit
  HITTEE individual
  HITTER m
  
  ANOTHER?  y.
  
  no

After finding the first most general satisfier to the description, the user is prompted as to whether or not another most general satisfier should be sought. As there are only two most general satisfiers of the description, the first request for another satisfier succeeds, while the second one fails. Failure to find additional solutions is indicated by the no response from Prolog.

Error messages will result if there is a violation of the type hierarchy in the query. For instance, consider the following query containing two type errors before a satisfiable disjunct:

  | ?- mgsat hd:j ; a ; j.

  add_to could not add incompatible type j to: 
       quant
       RESTR proposition
       SCOPE proposition
       VAR individual
  
  add_to could not add undefined type: a to
       bot
  
  MOST GENERAL SATISFIER OF: hd:j;a;j
  
  j
  
  ANOTHER?

Here the two errors are indicated, followed by a display of the unique most general satisfiers. The problem with the first disjunct is that lists have elements which must be of the quantifier type, which conflicts with the individual type of j, while the second disjunct involves an undefined type a. Note that in the error messages, there is some indication of how the conflict arose as well as the current state of the structure when the error occurred. For instance, the system had already figured out that the head must be a quantifier, which it determined before arriving at the incompatible type j. The conflict arose when an attempt was made to add the type j to the quant type object.

To explore unification, simply use conjunction and mgsat. In particular, to see the unification of descriptions D1 and D2, simply display the most general satisfiers of D1, D2, and their conjunction (D1,D2). To obtain the correct results, D1 and D2 must not share any common variables. If they do, the values of these will be unified across D1 and D2, a fact which is not represented by the most general satisfiers of either D1 or D2. Providing most general satisfiers also allows the user to test for subsumption or logical equivalence by visual inspection, by using mgsat/1 and comparing the set of solutions. Future releases should contain mechanisms for evaluating subsumption (entailment), and hence logical equivalence of descriptions.

mgsat can also be used to test functional descriptions, e.g., for the functional append on p. :

  | ?- mgsat append([bot],[bot,bot]).

ne_list
HD bot
TL ne_list
  HD bot
  TL ne_list
    HD bot
    TL e_list

ANOTHER?

The Prolog predicate iso_desc/2 can be used to discover whether two descriptions evaluate to the same feature structure. This can be useful for testing extensional type declarations.

  | ?- iso_desc(X,X).
 
  X = _A-bot ? 

  yes
  | ?- iso_desc((a_ atom),(a_ atom)).     % a_ atoms are extensional

  yes
  | ?- iso_desc(b,b).         % for b, intensional

  no
  | ?- iso_desc(a,a).         % for a, extensional, with feature f
 
  no
  | ?- iso_desc(f:(a_ at1),f:(a_ at1)).   % f approp. to a_ atoms
 
  yes
  | ?- iso_desc(f:(a_ at1),f:(a_ at2)).

  no