Document Open Access Logo

A Generic Framework for Higher-Order Generalizations

Authors David M. Cerna, Temur Kutsia

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.10.pdf
  • Filesize: 0.53 MB
  • 19 pages

Document Identifiers

Author Details

David M. Cerna
  • FMV and RISC, Johannes Kepler University Linz, Austria
Temur Kutsia
  • RISC, Johannes Kepler University Linz, Austria

Funding

Supported by the Austrian Science Fund (FWF) under the project P 28789-N32.

Acknowledgements

We thank Tomer Libal for useful discussions on the early version of the paper.

Cite AsGet BibTex

David M. Cerna and Temur Kutsia. A Generic Framework for Higher-Order Generalizations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.10

Abstract

We consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Higher order logic
  • Theory of computation → Type theory
Keywords
  • anti-unification
  • typed lambda calculus
  • least general generalization

Metrics

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

References

  1. Hassan Aït-Kaci and Gabriella Pasi. Fuzzy Unification and Generalization of First-Order Terms over Similar Signatures. In Fabio Fioravanti and John P. Gallagher, editors, LOPSTR 2017, volume 10855 of LNCS, pages 218-234. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-94460-9_13.
  2. María Alpuente, Demis Ballis, Angel Cuenca-Ortega, Santiago Escobar, and José Meseguer. ACUOS2: A high-performance system for modular ACU generalization with subtyping and inheritance. In 16th European Conference on Logics in Artificial Intelligence, JELIA 2019, LNCS. Springer, 2019. To appear. Google Scholar
  3. María Alpuente, Santiago Escobar, Javier Espert, and José Meseguer. A modular order-sorted equational generalization algorithm. Inf. Comput., 235:98-136, 2014. URL: http://dx.doi.org/10.1016/j.ic.2014.01.006.
  4. Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  5. Adam D. Barwell, Christopher Brown, and Kevin Hammond. Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. Future Generation Comp. Syst., 79:669-686, 2018. URL: http://dx.doi.org/10.1016/j.future.2017.07.024.
  6. Alexander Baumgartner and Temur Kutsia. Unranked second-order anti-unification. Inf. Comput., 255:262-286, 2017. URL: http://dx.doi.org/10.1016/j.ic.2017.01.005.
  7. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A Variant of Higher-Order Anti-Unification. In Femke van Raamsdonk, 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 - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2013.113.
  8. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Higher-Order Pattern Anti-Unification in Linear Time. J. Autom. Reasoning, 58(2):293-310, 2017. URL: http://dx.doi.org/10.1007/s10817-016-9383-3.
  9. Cao Feng and Stephen Muggleton. Towards Inductive Generalization in Higher Order Logic. In Derek H. Sleeman and Peter Edwards, editors, Proceedings of the Ninth International Workshop on Machine Learning (ML 1992), Aberdeen, Scotland, UK, July 1-3, 1992, pages 154-162. Morgan Kaufmann, 1992. Google Scholar
  10. Kouichi Hirata, Takeshi Ogawa, and Masateru Harao. Generalization Algorithms for Second-Order Terms. In Rui Camacho, Ross D. King, and Ashwin Srinivasan, editors, Inductive Logic Programming, 14th International Conference, ILP 2004, Porto, Portugal, September 6-8, 2004, Proceedings, volume 3194 of Lecture Notes in Computer Science, pages 147-163. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30109-7_14.
  11. Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-unification for Unranked Terms and Hedges. J. Autom. Reasoning, 52(2):155-190, 2014. URL: http://dx.doi.org/10.1007/s10817-013-9285-6.
  12. 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 fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.26.
  13. José Meseguer. Symbolic Reasoning Methods in Rewriting Logic and Maude. In Lawrence S. Moss, Ruy J. G. B. de Queiroz, and Maricarmen Martínez, editors, WoLLIC 2018, volume 10944 of LNCS, pages 25-60. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-662-57669-4_2.
  14. Dale Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification. J. Log. Comput., 1(4):497-536, 1991. URL: http://dx.doi.org/10.1093/logcom/1.4.497.
  15. Frank Pfenning. Unification and Anti-Unification in the Calculus of Constructions. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 74-85. IEEE Computer Society, 1991. URL: http://dx.doi.org/10.1109/LICS.1991.151632.
  16. Brigitte Pientka. Higher-order term indexing using substitution trees. ACM Trans. Comput. Log., 11(1), 2009. URL: http://dx.doi.org/10.1145/1614431.1614437.
  17. Gordon D. Plotkin. A note on inductive generalization. Machine Intell., 5(1):153-163, 1970. Google Scholar
  18. John C. Reynolds. Transformational systems and the algebraic structure of atomic formulas. Machine Intell., 5(1):135-151, 1970. Google Scholar
  19. Reudismam Rolim, Gustavo Soares, Rohit Gheyi, and Loris D'Antoni. Learning Quick Fixes from Code Repositories. CoRR, abs/1803.03806, 2018. URL: http://arxiv.org/abs/1803.03806.
  20. Reudismam Rolim de Sousa. Learning syntactic program transformations from examples. PhD thesis, Universidade Federal de Campina Grande, Brazil, 2018. Google Scholar
  21. Martin Schmidt, Ulf Krumnack, Helmar Gust, and Kai-Uwe Kühnberger. Heuristic-Driven Theory Projection: An Overview. In Henri Prade and Gilles Richard, editors, Computational Approaches to Analogical Reasoning: Current Trends, volume 548 of Studies in Computational Intelligence, pages 163-194. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54516-0_7.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact