Abstract
We present a new class of second-order unification problems, which we have called linear. We deal with completely general second-order typed unification problems, but we restrict the set of unifiers under consideration: they instantiate free variables by linear terms, i.e. terms where any λ-abstractions bind one and only one occurrence of a bound variable. Linear second-order unification properly extends context unification studied by Comon and Schmidt-Schauß. We describe a sound and complete procedure for this class of unification problems and we prove termination for three different subcases of them. One of these subcases is obtained requiring Comon's condition, another corresponds to Schmidt-Schauß's condition, (both studied previously for the case of context unification, and applied here to a larger class of problems), and the third one is original, namely that free variables occur at most twice.
This work was partially supported by the ESPRIT Basic Research Action CCL and the project DISCOR (TIC 94-0847-C02-01) funded by the CICYT
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
H. Comon. Completion of rewrite systems with membership constraints, part I: Deduction rules and part II: Constraint solving. Technical report, CNRS and LRI, Université de Paris Sud, 1993. (To appear in J. of Symbolic Computation).
J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40:273–326, 1990.
W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.
W. E. Gould. A Matching Procedure for ω-Order Logic. PhD thesis, Princeton Univ., 1966.
G. Huet. The undecidability of unification in third-order logic. Information and Control, 22(3):257–267, 1973.
G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
D. C. Jensen and T. Pietrzykowski. Mechanizing ω-order type theory through unification. Theoretical Computer Science, 3:123–171, 1976.
J. Levy and J. Agustí. Bi-rewriting, a term rewriting technique for monotonic order relations. In 4th Int. Conf. on Rewriting Techniques and Applications, RTA'93, volume 690 of LNCS, pages 17–31, Montreal, Canada, 1993.
J. Levy and J. Agustí. Bi-rewriting systems. J. of Symbolic Computation, 1995. (To be published).
C. Loría-Sáenz. A Theoretical Framework for Reasoning about Program Construction based on Extensions of Rewrite Systems. PhD thesis, Univ. Kaiserslautern, 1993.
C. L. Lucchesi. The undecidability of the unification problem for third-order languages. Technical Report CSRR 2059, Dept. of Applied Analysis and Computer Science, Univ. of Waterloo, 1972.
O. Lysne and J. Piris. A termination ordering for higher-order rewrite systems. In 6th Int. Conf on Rewriting Techniques and Applications, RTA'95, volume 914 of LNCS, Kaiserslautern, Germany, 1995.
D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1:497–536, 1991.
T. Nipkow. Functional unification of higher-order patterns. In 8th IEEE Symp. on Logic in Computer Science, LICS'93, pages 64–74, Montreal, Canada, 1993.
T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333–364, 1973.
C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. PhD thesis, Technische Universität München, 1995.
M. Schmidt-Schauß. Unification of stratified second-order terms. Technical Report 12/94, Johan Wolfgang-Goethe-Universität, Frankfurt, Germany, 1995.
K. U. Schulz. Makanin's algorithm, two improvements and a generalization. Technical Report CIS-Bericht-91-39, Centrum für Informations und Sprachverarbeitung, Universität München, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Levy, J. (1996). Linear second-order unification. In: Ganzinger, H. (eds) Rewriting Techniques and Applications. RTA 1996. Lecture Notes in Computer Science, vol 1103. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61464-8_63
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_63
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61464-7
Online ISBN: 978-3-540-68596-8
eBook Packages: Springer Book Archive