Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-25T18:54:08.628Z Has data issue: false hasContentIssue false
  • English
  • Français

Higher-order pattern generalization modulo equational theories

Published online by Cambridge University Press:  20 May 2020

David M. Cerna Open the ORCID record for David M. Cerna [Opens in a new window]  and
Temur Kutsia
David M. Cerna*
Affiliation:
RISC, Johannes Kepler University, Linz, Austria FMV, Johannes Kepler University, Linz, Austria
Temur Kutsia
Affiliation:
RISC, Johannes Kepler University, Linz, Austria
*
*Corresponding author. Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We consider anti-unification for simply typed lambda terms in theories defined by associativity, commutativity, identity (unit element) axioms and their combinations and develop a sound and complete algorithm which takes two lambda terms and computes their equational generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of such generalizations contains finitely many elements. We define the notion of optimal solution and investigate special restrictions of the problem for which the optimal solution can be computed in linear or polynomial time.

Keywords

Simply typed lambda calculusanti-unificationequational theorieshigher-order patterns
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Special Issue 6: Special Issue: Unification , June 2020 , pp. 627 - 663
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s) 2020. Published by Cambridge University Press

References

Alpuente, M., Escobar, S., Espert, J. and Meseguer, J. (2014). A modular order-sorted equational generalization algorithm. Information and Computation 235 98–136. doi: 10.1016/j.ic.2014.01.006.CrossRefGoogle Scholar
Alpuente, M., Ballis, D., Cuenca-Ortega, A., Escobar, S. and Meseguer, J. (2019). ACUOS2: A high-performance system for modular ACU generalization with subtyping and inheritance. In: Calimeri, F., Leone, N. and Manna, M. (eds.) Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7–11, 2019, Proceedings, Lecture Notes in Computer Science. vol. 11468. Springer, 171–181. ISBN 978-3-030-19569-4. doi: 10.1007/978-3-030-19570-0_11.Google Scholar
Barendregt, H. (1984). The Lambda Calculus. Its Syntax and Semantics. North Holland.Google Scholar
Barwell, A. D., Brown, C. and Hammond, K. (2018). Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. Future Generation Computing Systems 79 669–686. doi: 10.1016/j.future.2017.07.024.CrossRefGoogle Scholar
Baumgartner, A. (2015). Anti-Unification Algorithms: Design, Analysis, and Implementation. PhD thesis, Johannes Kepler University Linz.Google Scholar
Baumgartner, A. and Kutsia, T. (2014). A library of anti-unification algorithms. In: Fermé, E. and Leite, J. (eds.) Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8761, Springer, 543–557. ISBN 978-3-319-11557-3. doi: 10.1007/978-3-319-11558-0_38.Google Scholar
Baumgartner, A. and Kutsia, T. (2017). Unranked second-order anti-unification. Information and Computation 255 262–286. doi: 10.1016/j.ic.2017.01.005.CrossRefGoogle Scholar
Baumgartner, A., Kutsia, T., Levy, J., and Villaret, M.. A variant of higher-order anti-unification. In van Raamsdonk, F., editor, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, June 24-26, 2013, Eindhoven, The Netherlands, volume 21 of LIPIcs, pages 113–127. Schloss Dagstuhl, 2013. ISBN 978-3-939897-53-8. doi: 10.4230/LIPIcs.RTA.2013.113.Google Scholar
Baumgartner, A., Kutsia, T., Levy, J. and Villaret, M. (2017). Higher-order pattern anti-unification in linear time. Journal of Automated Reasoning 58 (2) 293–310. doi: 10.1007/s10817-016-9383-3.CrossRefGoogle ScholarPubMed
Besold, T. R., Kuehnberger, K. and Plaza, E. (2017). Towards a computational- and algorithmic-level account of concept blending using analogies and amalgams. Connection Science 29 (4) 387–413. doi:10.1080/09540091.2017.1326463 CrossRefGoogle Scholar
Cerna, D. M. and Kutsia, T. (2018). Higher-order equational pattern anti-unification. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, LIPIcs, vol. 108, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 12:1–12:17. ISBN 978-3-95977-077-4. doi: 10.4230/LIPIcs.FSCD.2018.12.Google Scholar
Cerna, D. M. and Kutsia, T. (2019a). A generic framework for higher-order generalizations. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., LIPIcs, vol. 131, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 10:1–10:19. ISBN 978-3-95977-107-8. doi: 10.4230/LIPIcs.FSCD.2019.10.Google Scholar
Cerna, D. M. and Kutsia, T. (2019b). Idempotent anti-unification. ACM Transactions on Computational Logic 21 (2) 10:1–10:32. https://doi.org/10.1145/3359060 (To appear).Google Scholar
Dowek, G. (2001). Higher-order unification and matching. In: Robinson, J. A. and Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier and MIT Press, 1009–1062. ISBN 0-444-50813-9.CrossRefGoogle Scholar
Eberhard, S. and Hetzl, S. (2015). Inductive theorem proving based on tree grammars. Annals of Pure and Applied Logic 166 (6) 665–700. doi: 10.1016/j.apal.2015.01.002.CrossRefGoogle Scholar
Eberhard, S., Ebner, G. and Hetzl, S. (2017). Algorithmic compression of finite tree languages by rigid acyclic grammars. ACM Transactions on Computational Logic 18 (4) 26:1–26:20. ISSN 1529-3785. doi: 10.1145/3127401.CrossRefGoogle Scholar
Ebner, G., Hetzl, S., Leitsch, A., Reis, G. and Weller, D. (2019). On the generation of quantified lemmas. Journal of Automated Reasoning 63 (1) 95–126.CrossRefGoogle Scholar
Hetzl, S., Leitsch, A., Reis, G. and Weller, D. (2014). Algorithmic introduction of quantified cuts. Theoretical Computer Science 549 1–16. doi: 10.1016/j.tcs.2014.05.018.CrossRefGoogle Scholar
Kutsia, T., Levy, J. and Villaret, M. (2014). Anti-unification for unranked terms and hedges. Journal of Automated Reasoning 52 (2) 155–190.CrossRefGoogle Scholar
Libal, T. and Steen, A. (2016). Towards a substitution tree based index for higher-order resolution theorem provers. In: Fontaine, P., Schulz, S. and Urban, J. (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning Co-located with IJCAR 2016, CEUR Workshop Proceedings, vol. 1635, CEUR-WS.org, 82–94. http://ceur-ws.org/Vol-1635/paper-08.pdf Google Scholar
Miller, D. (1991). A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation 1 (4) 497–536. doi: 10.1093/logcom/1.4.497.CrossRefGoogle Scholar
Pfenning, F. (1991). Unification and anti-unification in the calculus of constructions. In: LICS, IEEE Computer Society, 74–85.Google Scholar
Pientka, B. (2009). Higher-order term indexing using substitution trees. ACM TOCL 11 (1). doi: 10.1145/1614431.1614437.CrossRefGoogle Scholar
Rolim, R., Soares, G., Gheyi, R. and D’Antoni, L. (2018). Learning quick fixes from code repositories. CoRR, abs/1803.03806. http://arxiv.org/abs/1803.03806 Google Scholar
Schmid, U. (2003). Inductive Synthesis of Functional Programs, Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning, Lecture Notes in Computer Science, vol. 2654, Springer. ISBN 3-540-40174-1.Google Scholar
Schmidt, M., Krumnack, U., Gust, H. and Kühnberger, K. (2014). Heuristic-driven theory projection: An overview. In: Prade, H. and Richard, G. (eds.) Computational Approaches to Analogical Reasoning: Current Trends, Studies in Computational Intelligence, vol. 548, Springer, 163–194. ISBN 978-3-642-54515-3. doi: 10.1007/978-3-642-54516-0_7.CrossRefGoogle Scholar