Higher-Order Dynamic Pattern Unification for Dependent Types and Records

  • Andreas Abel
  • Brigitte Pientka
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


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.


Free Variable Deductive System Logical Framework Typing Rule Pattern Fragment 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cervesato, I., Pfenning, F.: A linear spine calculus. Journal of Logic and Computation 13(5), 639–688 (2003)CrossRefzbMATHGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Duggan, D.: Unification with extended patterns. Theoretical Computer Science 206(1-2), 1–50 (1998)CrossRefzbMATHGoogle Scholar
  4. 4.
    Elliott, C.: Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University (1990)Google Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    Goguen, H.: Justifying algorithms for βη conversion. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 410–424. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science 13, 225–230 (1981)CrossRefzbMATHGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Miller, D.: Unification of simply typed lambda-terms as logic programming. In: Eighth International Logic Programming Conference, pp. 255–269. MIT Press, Cambridge (1991)Google Scholar
  10. 10.
    Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3), 1–49 (2008)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Pientka, B.: Tabled higher-order logic programming. PhD thesis, Department of Computer Science, Carnegie Mellon University, CMU-CS-03-185 (2003)Google Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    Reed, J.: A Hybrid Logical Framework. PhD thesis, School of Computer Science, Carnegie Mellon University (2009)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Andreas Abel
    • 1
  • Brigitte Pientka
    • 2
  1. 1.Institut für InformatikLudwig-Maximilians-UniversitätMünchenGermany
  2. 2.School of Computer ScienceMcGill UniversityMontrealCanada

Personalised recommendations