Unification: a multidisciplinary survey
---
paper_title: The Design and Analysis of Computer Algorithms

paper_content:

From the Publisher: ::: With this text, you gain an understanding of the fundamental concepts of algorithms, the very heart of computer science. It introduces the basic data structures and programming techniques often used in efficient algorithms. Covers use of lists, push-down stacks, queues, trees, and graphs. Later chapters go into sorting, searching and graphing algorithms, the string-matching algorithms, and the Schonhage-Strassen integer-multiplication algorithm. Provides numerous graded exercises at the end of each chapter. ::: ::: ::: 0201000296B04062001
---
paper_title: A PROLOG Implementation of Lexical Functional Grammar

paper_content:

Lexical functional grammar (LFG) is an attempt to solve problems that arise in transformational grammar and ATN-formalisms (Bresnan, 1982). Another powerful formalism for describing natural languages follows from a method for expressing grammars in logic, due to Colmerauer (1970) and Kowalski (1974) called definite clause grammars(DCG) (Warren, Pereira, 1980). Both formalisms are a natural extension of context free grammars (CFG). ::: ::: The aim of this paper is to show -how LFG can be translated into DCG -that the procedural semantics of PROLOG provides an efficient tool for LFG-implementations in that it allows the construction of function structures (f-structures) directly during the parsing process. i.e. it is not necessary to have a separate component which first derives a set of functional equations from the parse tree, and secondly generates a f-structure by solving these equations.
---
paper_title: Nondestructive graph unification

paper_content:

Graph unification is sometimes implemented as a destructive operation, making it neccesary to copy the argument graphs before beginning the actual unification. Previous research on graph unification claimed that this copying is a computation sink, and has sought to correct this. ::: ::: In this paper I claim that the fundamental problem is in designing graph unification as a destructive operation. This forces it to both over copy and early copy. I present a nondestructive graph unification algorithm that minimizes over copying and eliminates early copying. This algorithm is significantly simpler than recently published solutions to copying problems, but maintains the essential efficiency gains of older techniques.
---
paper_title: Definite clause grammars for language analysis—A survey of the formalism and a comparison with augmented transition networks

paper_content:

Abstract A ciear and powerful formalism for describing languages, both natural and artificial, follows from a method for expressing grammars in logic due to Colmerauer and Kowalski. This formalism, which is a natural extension of context-free grammars, we call “definite clause grammars” (DCGs). A DCG provides not only a description of a language, but also an effective means for analysing strings of that language, since the DCG, as it stands, is an executable program of the programming language Prolog. Using a standard Prolog compiler, the DCG can be compiled into efficient code, making it feasible to implement practical language analysers directly as DCGs. This paper compares DCGs with the successful and widely used augmented transition network (ATN) formalism, and indicates how ATNs can be translated into DCGs. It is argued that DCGs can be at least as efficient as ATNs, whilst the DCG formalism is clearer, more concise and in practice more powerful.
---
paper_title: The Semantics Of Grammar Formalisms Seen As Computer Languages

paper_content:

The design, implementation, and use of grammar formalisms for natural language have constituted a major branch of computational linguistics throughout its development. By viewing grammar formalisms as just a special case of computer languages, we can take advantage of the machinery of denotational semantics to provide a precise specification of their meaning. Using Dana Scott's domain theory, we elucidate the nature of the feature systems used in augmented phrase-structure grammar formalisms, in particular those of recent versions of generalized phrase structure grammar, lexical functional grammar and PATR-II, and provide a denotational semantics for a simple grammar formalism. We find that the mathematical structures developed for this purpose contain an operation of feature generalization, not available in those grammar formalisms, that can be used to give a partial account of the effect of coordination on syntactic features.
---
paper_title: Complex indeterminates in Prolog and its application to discourse models

paper_content:

Complex indeterminates and their notation are introduced into Prolog. The syntax and semantics of the new language are described. The language builds in an extension to the usual unification. Detailed examples are given to demonstrate discourse models based on situation semantics in the proposed language. Discourse, connective and resource situations are included in the examples.
---
paper_title: Inheritance hierarchies: Semantics and unification

paper_content:

Inheritance hierarchies are introduced as a means of representing taxonomicallyorganized data. The hierarchies are built up from so-called feature types that are ordered by subtyping and whose elements are records. Every feature type comes with a set of features prescribing fields of its record elements. So-called feature terms are available to denote subsets of feature types. Feature unification is introduced as an operation that decides whether two feature terms have a nonempty intersection and computes a feature term denoting the intersection. We model our inheritance hierarchies as algebraic specifications in ordersortedequational logic using initial algebra semantics. Our framework integrates feature types whose elements are obtained as records with constructor types whose elements are obtained by constructor application. Unification in these hierarchies combines record unification with order-sorted term unification and is presented as constraint solving. We specify a unitary unification algorithm by a set of simplification rules and prove its soundness and completeness with respect to the model-theoretic semantics.
---
paper_title: Improving the Efficiency of Higher Order Unification

paper_content:

The sources of inefficiency in currently existing higher order unification algorithms are investigated. Aside from such theoretical difficulties as the undecidability of unification in third order logic, and the existence of infinite unifiers and the lack of a polynomial bound on the number of applications of the "imitation" rule even in the monadic subcase of second order unification, the current algorithms suffer from a built-in inefficiency due to their introduction and subsequent elimination of many auxiliary functional variables, and to the nondirected nature of the substitutions made by the "projection" rule. It i s argued that a procedure based on attempting to match the argument or arguments of a functional or predicate variable with the subterms of the other formula in the unification can decide the possibility of unification and generate the resulting unifiers much more directly than the theoretically complete algorithm.
---
paper_title: AUTOMATING HIGHER-ORDER LOGIC

paper_content:

An automated theorem-proving system called TPS for proving theorems of first or higher-order logic in automatic, semi-automatic, or interactive mode has been developed. As its logical language TPS uses Church's formulation of type theory with A-notation, in which most theorems of mathematics can be expressed very directly. As an interactive tool TPS has many features which facilitate writing formal proofs and manipulating and displaying formulas of logic in traditional notations. In automatic mode TPS combines theorem-proving methods for first-order logic with Huet's unification algorithm for typed A-calculus, finds acceptable general matings (which represent the essential syntactic combinatorial information implicit in proofs), and constructs proofs in natural deduction style. Among the theorems which can· be proved completely automatically is - 3G 'dF 3J [[G J] = F], which expresses Cantor's Theorem that a set ou 0' , has more subsets than members by asserting that there is no function G from individuals to sets which has every set F of individuals in its range. The computer substitutes for F the formula [AW - G W W], which denotes 0' L ou the set {W I W ~ G W} and expresses the key idea in the classical diagonal argument. The methods presently used by TPS in automatic mode are in principle complete for first-order logic, but not for higher-order logic. A recently proved extension of Herbrand's Theorem to type theory is presented. It is anticipated that this metatheorem will provide a basis for extending the capabilities of TPS.
---
paper_title: Order-sorted unification

paper_content:

This paper studies unification for order-sorted equational logic. This logic generalizes unsorted equational logic by allowing a partially ordered set of sorts, with the ordering interpreted as set-theoretic containment in the models; it also allows overloading of function symbols, such as + for integer and rational number addition, with the overloaded functions of greater rank interpreted in the models as extensions of those of smaller rank. Our presentation emphasizes semantic aspects, and gives a categorical treatment of unification that has substantial advantages in this context over the usual treatment of unifiers as endomorphisms of a single free algebra. Given system @C of equations and a set E of axioms that is sort-preserving and does not impose restrictions on the sorts of its variables, the main results characterize when an order-sorted signature has a minimal (or finite, or most general when @C is solvable) family of order-sorted E-unifiers for @C. In addition, for unitary signatures, where each solvable system of equations has a most general unifier, we give a quasi-linear algorithm for syntactic unification (i.e., for E= ) a la Martelli-Montanari, that is more efficient than the unsorted one for failures.
---
paper_title: Parallel algorithms for term matching

paper_content:

We present a new randomized parallel algorithm for term matching. Let n be the number of nodes of the directed acyclic graphs (dags) representing the terms to be matched, then our algorithm uses O(log2n) parallel time and M(n) processors, where M(n) is the complexity of n by n matrix multiplication. The number of processors is a significant improvement over previously known bounds. Under various syntactic restrictions on the form of the input dags only O(n2) processors are required in order to achieve deterministic O(log2n) parallel time. Furthermore, we reduce directed graph reachability to term matching using constant parallel time and O(n2) processors. This is strong evidence that in practice, taking M(n) to be n3, no deterministic algorithm can beat the processor bound of our randomized algorithm. We also improve the lower bound of [DKM] on the unification problem. We show that unification is logspace-complete in PTIME even if both input terms are linear, i.e., no variable appears more than once in each term.
---
paper_title: On the sequential nature of unification

paper_content:

Abstract The problem of unification of terms is log-space complete for P. In deriving this lower bound no use is made of the potentially concise representation of terms by directed acyclic graphs. In addition, the problem remains complete even if infinite substitutions are allowed. A consequence of this result is that parallelism cannot significantly improve on the best sequential solutions for unification. However, we show that for the problem of term matching, an important subcase of unification, there is a good parallel algorithm using O ( log 2 n ) time and n O(1) processors on a PRAM. For the O ( log 2 n ) parallel time upper bound we assume that the terms are represented by directed acyclic graphs; if the longer string representation is used we obtain an O ( log n ) parallel time bound.
---
paper_title: On unification: Equational theories are not bounded

paper_content:

We are interested in first-order unification problems and, more specifically, in the hierarchy of equational theories based on the cardinality of the set of most general unifiers. The following result is established in this paper: if T is a suitable first-order equational theory that is not unitary, then T is not bounded; that is, there is no integer n > 1 such that for every unification problem (s = t)"T, the cardinality of the set of most general unifiers for (s = t)"T is at most n. Hence, the class of (non-unitary) finitary theories cannot be decomposed into a hierarchy obtained by uniformly bounding the eardinalities of the sets of most general unifiers.
---
paper_title: Prolog - the language and its implementation compared with Lisp

paper_content:

Prolog is a simple but powerful programming language founded on symbolic logic. The basic computational mechanism is a pattern matching process (“unification”) operating on general record structures (“terms” of logic). We briefly review the language and compare it especially with pure Lisp. The remainder of the paper discusses techniques for implementing Prolog efficiently; in particular we describe how to compile the patterns involved in the matching process. These techniques are as incorporated in our DECsystem-10 Prolog compiler (written in Prolog). The code it generates is comparable in speed with that produced by existing DEC10 Lisp compilers. We argue that pattern matching is a better method for expressing operations on structured data than conventional selectors and constructors - both for the user and for the implementor.
---
paper_title: Login: a logic programming language with built-in inheritance

paper_content:

D An elaboration of the PROLOG language is described in which the notion of first-order term is replaced by a more general one. This extended form of terms allows the integration of inheritance-an IS-A taxonomy-directly into the unification process rather than indirectly through the resolutionbased inference mechanism of PROLOG. This results in more efficient computations and enhanced language expressiveness. The language thus obtained, called LOGIN, subsumes PROLOG, in the sense that conventional PROLOG programs are equally well executed by LOGIN. a
---
paper_title: An Efficient Context-Free Parsing Algorithm for Natural Languages

paper_content:

This thesis introduces an efficient context-free parsing algorithm and emphasizes its practical value in natural language processing. In the theoretical worst case analysis, the parsing algorithm occasionally takes more than O(n('3)) time with kinds of context-free grammars which are very unlikely to appear in natural languages. As far as practical natural language processing is concerned, on the other hand, the parsing algorithm seems more efficient than any existing algorithms including Earley's algorithm. Experiments with several English grammars and sample sentences show that our algorithm is 5 to 10 times faster than Earley's standard algorithm. ::: The parsing algorithm can be viewed as an extended LR parsing algorithm which embodies the concept of a "graph-structured stack." Unlike the standard LR, the algorithm is capable of handling arbitrary non-cyclic context-free grammars including ambiguous grammars, with little loss of LR efficiency. In particular, if its grammar is "close" to LR, most of the LR parsing efficiency can be preserved. Natural language grammars are, fortunately, considerably "close" to LR, compared with other general context-free grammars. ::: The algorithm is an all-path parsing algorithm; it produces all possible parse trees (a parse forest) in an efficient representation called a "shared-packed forest." This thesis also shows that Earley's forest representation has a defect and his representation cannot be used in natural language processing. ::: The last chapters of the thesis suggest practical applications of the algorithm. A concept of left-to-right on-line parsing is introduced, taking advantage of the fact that our algorithm parses a sentence strictly from left to right. Several benefits of on-line parsing are described, and its application to user-friendly natural language interface is discussed. This thesis also proposes a technique to disambiguate a sentence out of the shared-packed forest representation by asking the user questions interactively. Finally, a personal/interactive machine translation system is suggested.
---
paper_title: Transformational systems and the algebraic structure of atomic for-mulas

paper_content:

A semiconductor photovoltaic device is comprised of 2n layers of alternating p-type and n-type material having respective PN junctions between adjacent layers, wherein n is an integer greater than 1. Each layer has a thickness which is less than the diffusion length of a minority carrier therein. The PN junctions are excited by light which is incident on the device to thereby cause majority carriers to be accumulated in the respective layers so as to forward bias all of the PN junctions. As a result of this forward biasing, minority carriers are injected across a first PN junction fr0m one layer into an adjacent layer and then traverse the next PN junction into the next succeeding layer. The photovoltaic device thus is adapted to supply a voltage and a current to a load.
---
paper_title: A semantics of multiple inheritance

paper_content:

There are two major ways of structuring data in programming languages. The first and common one, used for example in Pascal, can be said to derive from standard branches of mathematics. Data are organized as Cartesian products (i.e., record types), disjoint sums (i.e., unions or variant types), and function spaces (i.e., functions and procedures). The second method can be said to derive from biology and taxonomy. Data are organized in a hierarchy of classes and subclasses, and data at any level of the hierarchy inherit all the attributes of data higher up in the hierarchy. The top level of this hierarchy is usually called the class of all objects; every datum is an object and every datum inherits the basic properties of objects, e.g., the ability to tell whether two objects are the same or not. Functions and procedures are considered as local actions of objects, as opposed to global operations acting over objects. These different ways of structuring data have generated distinct classes of programming languages, and induced different programming styles. Programming with taxonomically organized data is often called objectoriented programming, and has been advocated as an effective way of structuring programming environments, data bases, and large systems in general. The notions of inheritance and object-oriented programming first appeared in Simula 67 (Dahl, 1966). In Simula, objects are grouped into classes and classes can be organized into a subclass hierarchy. Objects are similar to records with functions as components, and elements of a class can appear wherever elements of the respective superclasses are expected. Subclasses inherit all the attributes of their superclasses. In Simula, the issues are somewhat complicated by the use of objects as coroutines, so that communication between objects can be implemented as message passing between processes. Smalltalk (Goldberg, 1983) adopts and exploits the idea of inheritance, with some changes. While stressing the message-passing paradigm, a
---

Title: Unification: A Multidisciplinary Survey

Section 1: INTRODUCTION
Description 1: This section introduces the unification problem across various fields of computer science and outlines the structure of the paper.

Section 2: THE UNIFICATION PROBLEM
Description 2: This section defines the unification problem, introduces formal definitions, and reviews efforts to improve the efficiency of unification algorithms.

Section 3: UNIFICATION AND THEOREM PROVING
Description 3: This section discusses the role of unification in resolution theorem proving and reviews research efforts in this area.

Section 4: UNIFICATION AND LOGIC PROGRAMMING
Description 4: This section details the application of unification in Prolog and other logic programming languages, highlighting efficient implementations and research.

Section 5: UNIFICATION AND HIGHER ORDER LOGIC
Description 5: This section explores the application and complexities of higher order unification in second-order and higher order logic systems.

Section 6: UNIFICATION AND FEATURE STRUCTURES
Description 6: This section introduces feature structures, their properties, and their use in unification, particularly in natural language processing.

Section 7: UNIFICATION AND NATURAL LANGUAGE PROCESSING
Description 7: This section describes the role of unification in parsing unification-based grammars in natural language processing systems.

Section 8: UNIFICATION AND EQUATIONAL THEORIES
Description 8: This section covers unification under equational theories, discussing various equational axioms like commutativity and associativity.

Section 9: GENERALIZATION
Description 9: This section introduces the concept of generalization as the dual of unification and describes its applications and algorithms.

Section 10: OTHER APPLICATIONS OF UNIFICATION
Description 10: This section reviews additional applications of unification in areas such as type inference, programming languages, and machine learning.

Section 11: CONCLUSION
Description 11: This section lists general properties of unification and summarizes trends in unification research.