Abstract
We develop a higher-order unification algorithm for a restricted class of simply typed lambda terms with function space and product type constructors. It is based on an inference system manipulating so called higher-order product-patterns which is proven to be sound and complete. Allowing tuple constructors in lambda binders provides elegant notations. We show that our algorithm terminates on each input and produces a most general unifier if one exists. The approach also extends smoothly to a calculus with terminal type.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Y. Akama. On Mints' reductions for ccc-Calculus. In Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 1–12, 1993.
R. Di Cosmo. Isomorphisms of Types. Birkhäuser, 1995.
R. Di Cosmo and D. Kesner. A confluent reduction for the extensional typed λs-calculus with pairs, sums, recursion, and terminal object. In A. Lingas et al., editors, ICALP, volume 697 of LNCS, pages 645–656, 1993.
D. Duggan. Unification with Extended Patterns. Technical Report CS-93-37, University of Waterloo, 1993. To appear in Theoretical Computer Science.
W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225–230, 1981.
G. P. Huet. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science, 1:27–57, 1975.
C. B. Jay and N. Ghani. The virtues of eta-expansion. J. Functional Programming, 5(2):135–154, April 1995.
T. Johnsson. Fold-unfold transformations on state monadic interpreters. In K. Hammond et al., editors, Functional programming, Glasgow, Workshops in Computing. Springer-Verlag, 1994.
D. Kesner. Reasoning about Layered, Wildcard and Product Patterns. In G. Levi and M. Rodnguez-Artalejo, editors, Algebraic and Logic Programming, volume 850 of LNCS, pages 253–268, 1994.
J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, 1986.
D. Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. Logic Comp., 1(4):497–536, 1991.
T. Nipkow. Higher-order critical pairs. In Proc. sixth annual IEEE Symposium on Logic in Computer Science, pages 342–349, 1991.
T. Nipkow. Functional unification of higher-order patterns. In Proc. eighth annual IEEE Symposium on Logic in Computer Science, pages 64–74, 1993.
G. Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. Notre Dame J. of Formal Logic, 22(3):264–268, 1981.
W. Snyder and J. Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation, 8:101–140, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fettig, R., Löchner, B. (1996). Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. 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_64
Download citation
DOI: https://doi.org/10.1007/3-540-61464-8_64
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