Document Open Access Logo

E-Unification for Second-Order Abstract Syntax

Author Nikolai Kudasov

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2023.10.pdf
  • Filesize: 0.92 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • E-unification
  • higher-order unification
  • second-order abstract syntax

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Higher-order unification (HOU) concerns unification of (extensions of) λ-calculus and can be seen as an instance of equational unification (E-unification) modulo βη-equivalence of λ-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to λ-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce E-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general E-unification. We prove that the procedure is sound and complete.

Cite As Get BibTex

Nikolai Kudasov. E-Unification for Second-Order Abstract Syntax. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.10

Author Details

Nikolai Kudasov
  • Innopolis University, Tatarstan Republic, Russia

Acknowledgements

I thank Nikolay Shilov for encouragement and fruitful discussions about the contents of the paper. I also thank Alexander Chichigin, Violetta Sim, Timur Fayzrahmanov, Alexey Stepanov, and Dale Miller for discussions of early versions of this work. I thank Alexander Chichigin, Timur Fayzrahmanov, and Ikechi Ndukwe for proofreading the paper. Finally, I thank the anonymous reviewers of FSCD-2023 for their valuable and detailed comments.

References

  1. Franco Barbanera, Maribel Fernández, and Herman Geuvers. Modularity of strong normalization in the algebraic-λ-cube. J. Funct. Program., 7(6):613-660, November 1997. URL: https://doi.org/10.1017/S095679689700289X.
  2. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP '08, pages 143-156, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1411204.1411226.
  3. Jacek Chrząszcz and Daria Walukiewicz-Chrząszcz. Towards Rewriting in Coq, pages 113-131. Springer-Verlag, Berlin, Heidelberg, 2007. Google Scholar
  4. Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 2:1-2:27, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.2.
  5. Jesper Cockx. 1001 representations of syntax with binding. https://jesper.sikanda.be/posts/1001-syntax-representations.html, November 2021. Accessed: 2023-01-21. Google Scholar
  6. Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434341.
  7. Denis Cousineau and Gilles Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, volume 4583 of Lecture Notes in Computer Science, pages 102-117. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73228-0_9.
  8. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Higher Order Unification via Explicit Substitutions. Inf. Comput., 157(1-2):183-235, 2000. URL: https://doi.org/10.1006/inco.1999.2837.
  9. Marcelo Fiore and Dmitrij Szamozvancev. Formal Metatheory of Second-Order Abstract Syntax. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498715.
  10. Marcelo P. Fiore and Chung-Kil Hur. Second-Order Equational Logic (Extended Abstract). In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 320-335. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_26.
  11. Jean H. Gallier and Wayne Snyder. Complete sets of transformations for general E-unification. Theor. Comput. Sci., 67(2&3):203-260, 1989. URL: https://doi.org/10.1016/0304-3975(89)90004-2.
  12. Warren D. Goldfarb. The Undecidability of the Second-Order Unification Problem. Theor. Comput. Sci., 13:225-230, 1981. URL: https://doi.org/10.1016/0304-3975(81)90040-2.
  13. Adam Michael Gundry. Type inference, Haskell and dependent types. PhD thesis, University of Strathclyde, Glasgow, UK, 2013. URL: http://oleg.lib.strath.ac.uk/R/?func=dbin-jump-full&object_id=22728.
  14. Michael Hoche and Peter Szabó. Essential unifiers. J. Appl. Log., 4(1):1-25, 2006. URL: https://doi.org/10.1016/j.jal.2004.12.001.
  15. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. URL: https://doi.org/10.1016/0304-3975(75)90011-0.
  16. D. C. Jensen and Tomasz Pietrzykowski. Mechanizing ω-order type theory through unification. Theor. Comput. Sci., 3(2):123-171, 1976. URL: https://doi.org/10.1016/0304-3975(76)90021-9.
  17. Claude Kirchner and Christophe Ringeissen. Higher-Order Equational Unification via Explicit Substitutions. In Michael Hanus, Jan Heering, and Karl Meinke, editors, Algebraic and Logic Programming, 6th International Joint Conference, ALP '97 - HOA '97, Southampton, UK, Spetember 3-5, 1997, Proceedings, volume 1298 of Lecture Notes in Computer Science, pages 61-75. Springer, 1997. URL: https://doi.org/10.1007/BFb0027003.
  18. Edward Kmett. Rotten bananas. http://comonad.com/reader/2008/rotten-bananas/, March 2008. Accessed: 2023-01-21. Google Scholar
  19. Edward Kmett. Bound. https://www.schoolofhaskell.com/user/edwardk/bound, December 2015. Accessed: 2023-01-21. Google Scholar
  20. Nikolai Kudasov. Functional Pearl: Dependent type inference via free higher-order unification, 2022. URL: https://arxiv.org/abs/2204.05653.
  21. Tomer Libal and Dale Miller. Functions-as-Constructors Higher-Order Unification. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 26:1-26:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.26.
  22. Francesco Mazzoli and Andreas Abel. Type checking through unification. CoRR, abs/1609.09709, 2016. URL: https://arxiv.org/abs/1609.09709.
  23. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput., 1(4):497-536, 1991. URL: https://doi.org/10.1093/logcom/1.4.497.
  24. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  25. Tobias Nipkow and Christian Prehofer. Higher-order rewriting and equational reasoning. In W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications. Volume I: Foundations, volume 8 of Applied Logic Series, pages 399-430. Kluwer, 1998. Google Scholar
  26. Werner Nutt. Unification in monoidal theories is solving linear equations over semirings. In SciDok - Der Wissenschaftsserver der Universität des Saarlandes, volume 92-01 of Research report / Deutsches Forschungszentrum für Künstliche Intelligenz. SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz, 1992. URL: https://doi.org/10.22028/D291-24991.
  27. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Richard L. Wexelblat, editor, Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988, pages 199-208. ACM, 1988. URL: https://doi.org/10.1145/53990.54010.
  28. Wayne Snyder. Higher order E-unification. In Mark E. Stickel, editor, 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, volume 449 of Lecture Notes in Computer Science, pages 573-587. Springer, 1990. URL: https://doi.org/10.1007/3-540-52885-7_115.
  29. Mark-Oliver Stehr. The open calculus of constructions (part I): an equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundam. Informaticae, 68(1-2):131-174, 2005. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi68-1-2-05.
  30. Mark-Oliver Stehr. The open calculus of constructions (part II): an equational type theory with dependent types for programming, specification, and interactive theorem proving. Fundam. Informaticae, 68(3):249-288, 2005. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi68-3-04.
  31. Peter Szabó and Jörg H. Siekmann. E-Unification based on Generalized Embedding. Math. Struct. Comput. Sci., 31(8):898-917, 2021. URL: https://doi.org/10.1017/S0960129522000019.
  32. Peter Szabó, Jörg H. Siekmann, and Michael Hoche. What Is Essential Unification? In Eugenio G. Omodeo and Alberto Policriti, editors, Martin Davis on Computability, Computational Logic, and Mathematical Foundations, volume 10 of Outstanding Contributions to Logic, pages 285-314. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41842-1_11.
  33. Val Tannen. Combining algebra and higher-order types. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988, pages 82-90. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/LICS.1988.5103.
  34. Petar Vukmirovic, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. Log. Methods Comput. Sci., 17(4), 2021. URL: https://doi.org/10.46298/lmcs-17(4:18)2021.
  35. Daria Walukiewicz-Chrząszcz. Termination of rewriting in the calculus of constructions. J. Funct. Program., 13(2):339-414, March 2003. URL: https://doi.org/10.1017/S0956796802004641.
  36. Geoffrey Washburn and Stephanie Weirich. Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program., 18(1):87-140, 2008. URL: https://doi.org/10.1017/S0956796807006557.
  37. Beta Ziliani and Matthieu Sozeau. A unification algorithm for Coq featuring universe polymorphism and overloading. In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 179-191. ACM, 2015. URL: https://doi.org/10.1145/2784731.2784751.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact