Abstract
While higher-order pattern unification for the λ Π-calculus is decidable and unique unifiers exists, we face several challenges in practice: 1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification algorithm. 2) Many systems implement λ ΠΣ calculus and hence the known pattern unification algorithms for λ Π are too restrictive.
In this paper, we present a constraint-based unification algorithm for λ ΠΣ-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing Σ-types into problems only involving Π-types. We prove correctness of our algorithm and discuss its application.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Cervesato, I., Pfenning, F.: A linear spine calculus. Journal of Logic and Computation 13(5), 639–688 (2003)
Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Joint International Conference Logic Programming, pp. 259–273. MIT Press, Cambridge (1996)
Duggan, D.: Unification with extended patterns. Theoretical Computer Science 206(1-2), 1–50 (1998)
Elliott, C.: Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University (1990)
Fettig, R., Löchner, B.: Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 347–361. Springer, Heidelberg (1996)
Goguen, H.: Justifying algorithms for βη conversion. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 410–424. Springer, Heidelberg (2005)
Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science 13, 225–230 (1981)
McBride, C.: Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In: ACM SIGPLAN Workshop on Genetic Programming (WGP 2010), pp. 1–12. ACM, New York (2010)
Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, pp. 255–269. MIT Press, Cambridge (1991)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3), 1–49 (2008)
Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Technical Report 33D (2007)
Pfenning, F., Schürmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, CMU-CS-03-185 (2003)
Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (System Description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15–21. Springer, Heidelberg (2010)
Poswolsky, A., Schürmann, C.: System description: Delphin—a functional programming language for deductive systems. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008). ENTCS, vol. 228, pp. 135–141. Elsevier, Amsterdam (2009)
Reed, J.: Higher-order constraint simplification in dependent type theory. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2009 (2009)
Reed, J.: A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University (2009)
Schack-Nielson, A., Schürmann, C.: Pattern unification for the lambda calculus with linear and affine types. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010). EPTCS, vol. 34, pp. 101–116 (2010)
Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abel, A., Pientka, B. (2011). Higher-Order Dynamic Pattern Unification for Dependent Types and Records. In: Ong, L. (eds) Typed Lambda Calculi and Applications. TLCA 2011. Lecture Notes in Computer Science, vol 6690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21691-6_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-21691-6_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21690-9
Online ISBN: 978-3-642-21691-6
eBook Packages: Computer ScienceComputer Science (R0)