Feature Graphs and Abstract Data Types: A Unifying Approach

Feature Graphs and Abstract Data Types: A Unifying Approach Christoph BEIERLE and Udo PLETAT IBM Deutschland GmbH Science and Technology - LILOG P.O. Box 80 08 80 7000 Stuttgart 80, West Germany (electronic mail on EARN/BITNET: BEIERLE at DS#LILOG, PLETAT at DS#LILOG) Abstract: Feature graphs appearing in unification--based grammar formalisms and algebraic specifications of abstract data types (ADTs) are both used for defining a collection of objects together with functions between these object sets. Starting from this observation we define an algebraic semantics for feature graphs by assigning an algebraic specification to each feature graph. This opens the rich world of semantical foundations for abstract data types to the area of feature graphs and thus to unification grammar formalisms. Using results from ADT theory we define a sim~le and fast syntactic decision procedure testing the usual consistency conditions on feature graphs like constant consistency, constant/complex consistency and acyclicity on the algebraic specification assigned to a feature graph. With this machinery at hand feature graph unification becomes union of feature graph specifications followed by the consistency test. 1. Introduction Unification-based grammar formalisms have become a popular field o'f research. The subject has attracted the interest not only of (computer) linguists but also of computer scientists, especially in the area of logic programming, see e.g. [Pe 87]. Due to the formality of grammars we also observe activities developing foundations for the formal semantics of various approaches on unification grammars, e.g. [PS 84], [KR 86], [RK 86], [Pe 87], [Jo 87]. In this paper we investigate the relationship between feature graphs on the one hand and algebraic specifications of abstract data types (ADTs) on the other hand. There is a natural correlation between both these areas since a feature graph as well as an abstract data type defines a collection of objects together with functions relating the objects. We present a formal semantics for feature graphs by assigning to each feature graph G an equational ADT specification ~(G), called fg--specification. This opens the rich world of ma'thematical foundations of ADT specifications (e.g [GTW 78], [EM 85]) in order to obtain a better - not only - formal understanding of the nature of feature graphs. In particular, we provide a model-theoretic characterization of various consistency conditions for feature graph specifications reflecting the consistency concepts usually imposed on feature graphs such as clash-freeness and acyclicity. These 40 model-theoretic characterizations have proof-theoretic counterparts in terms of syntactic conditions on the deductive closure of the set of equations of r(G)o Although the proof-theoretic consistency characterizations are of syntactic nature, a test of their validity requires to examine the deductive closure of the set of equations of a fg-specification. Our objective is to restrict consistency checks to equations explicitly mentioned in a fg-specificationo In the ADT-world there is a well-known tool for such tasks: the Knuth-Bendix algorithm ([KB 70]). We present a Knuth-Bendix like completion procedure transforming any fg-specification into a reduced normal form. We show that the model-theoretic consistency characterizations for G are equivalent to the presence …

Content truncated to 500 words