Solving equations, also called unification, has made impressive progress during the past decade. Described as existentially quantified formulae over =, unification problems are usually transformed step by step until a solved form is reached from which a most general unifier can be obtained. Kirchner showed how to compute transformation rules for theories having a syntactic presentation, for which a proof of an arbitrary equation uses at most one top equality step. Comon generalized to the case where negation is added, yielding disequations. Both sets of rules may not necessarily terminate. Kirchner gave sufficient proof-theoretic conditions for checking syntacticness, and was improved upon by Rémy, and Nipkov. As an application, a complete type inference algorithm for polymorphic records in CAML was obtained by Rémy. Recently, Kirchner and Klay showed that all finitary unifying theories without collapse axioms were syntactic, a result generalized by Comon, Contejean and Jouannaud to arbitrary finitary unifying and finitary matching theories. In particular, the associative and commutative theory of one operator has a syntactic presentation made of seven axioms. This paper surveys these results which show an intriguing relationship between unification and syntacticness, and suggests some directions for future research.
Unable to display preview. Download preview PDF.
- H. Comon. Unification et Disunification: Théorie et Applications. Thèse de Doctorat, I.N.P. de Grenoble, France, 1988.Google Scholar
- N. Dershowitz and J.-P. Jouannaud. Rewrite systems. 1989. To appear in the Handbook of Theoretical Computer Science.Google Scholar
- E. Diday and Y. Kodratoff. 2èmes journées symbolique numérique pour l'apprentissage de connaissances à partir de données. Research Report, LRI, June 1989.Google Scholar
- M. Fay. First order unification in equational theories. In Proc. 4th Conf. on Automated Deduction, Austin, LNCS, July 1979.Google Scholar
- J. Herbrand. Recherches sur la théorie de la démonstration. Thèse d'Etat, Univ. Paris, 1930. Also in: Ecrits logiques de Jacques Herbrand, PUF, Paris, 1968.Google Scholar
- H. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. 14th ICALP, Karlsruhe, LNCS 267, Springer-Verlag, July 1987. Available as INRIA Research Report 678.Google Scholar
- J.-P. Jouannaud and C. Kirchner. Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. To appear in Festschrift for Robinson, JL. Lassez and G. Plötkin ed., MIT press, 1990.Google Scholar
- J.-P. Jouannaud and Y. Kodratoff. Program synthesis from examples of behaviour. In A. W. Bierman and G. Guiho, editors, Computer Program Synthesis Methodologies, D. Reidel, 1983.Google Scholar
- C. Kirchner. Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories equationnelles. Thèse d'Etat, Univ. Nancy, France, 1985.Google Scholar
- C. Kirchner and F. Klay. Syntactic theories and unification. In Proc. 5th IEEE Symposium on Logic in Computer Science, Philadelphia, June 1990.Google Scholar
- A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.Google Scholar
- T. Nipkov. Proof transformations for equational theories. In Proc. 5rth IEEE Symp. Logic in Computer Science, June 1990.Google Scholar
- D. Rémy. Algèbres touffues. Application au typage polymorphe des objets enregistrements dans les langage fonctionnels. Thèse de Doctorat, Université Paris 7, France, 1990.Google Scholar