Abstract
Higher-order patterns are simply typed λ-terms in η-long form where free variables F only occur in the form F(x 1,...,x k ) with x 1, ...,x k being distinct bound variables. It has been proved in [6] that in the simply typed λ-calculus unification of higher-order patterns modulo α, β and η reductions is decidable and unifiable higher-order patterns have a most general unifier.
In this paper a unification algorithm for higher-order patterns is presented, whose time and space complexities are proved to be linear in the size of input.
Research partially supported by ESPRIT Basic Research WG COMPASS 6112.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley Publishing Company, 1974.
W. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.
G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4(2):258–282, 1982.
A. Martelli and U. Montanari. Unification in linear time and space: A structured presentation. Technical Report, Internal Rep. B76-16, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy, 1976.
D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
D. Miller. Unification of simply typed lambda-terms as logic programming. In P. K. Furukawa, editor, Proc. 1991 Joint Int. Conf. on Logic Programming, MIT Press, 1991.
G. Nadathur and D. Miller. An overview of λProlog. In R. A. Kowalski and K. A. Bowen, editors, Proc. 5th Int. Logic Programming Conference, MIT Press, 1988.
T. Nipkow. Higher-order critical pairs. In Proc. 6th LICS, pages 342–349, 1991.
T. Nipkow. Practical Unification of Higher-Order Patterns. Draft, Technische Universität München, 1991.
M. Paterson and M. Wegman. Linear unification. J. Computer and System Sciences, 16:158–167, 1978.
L. Paulson. Isabelle: the next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385, Academic Press, 1990.
F. Pfenning. Elf: a language for logic definition and verified meta-programming. In Proc. 4th LICS, pages 313–322, IEEE Computer Society Press, June 1989.
F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. D. Plotkin, editors, Logical Frameworks, Cambridge University Press, 1991.
F. Pfenning. Unification and anti-unification in the Calculus of Constructions. In Proc. 6th LICS, pages 74–85, IEEE Computer Society Press, July 1991.
Z. Qian. Unification of Higher-Order Patterns in Linear Time and Space. Technical Report, Forschungsbericht 5/92, FB3 Informatik, Universtät Bremen, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qian, Z. (1993). Linear unification of higher-order patterns. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_78
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_78
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive