LIPIcs.FSCD.2020.26.pdf
- Filesize: 0.62 MB
- 20 pages
Document
Unital Anti-Unification: Type and Algorithms
Authors
-
Part of:
Volume:
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-28
Cite AsGet BibTex
David M. Cerna and Temur Kutsia. Unital Anti-Unification: Type and Algorithms. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.26
https://doi.org/10.4230/LIPIcs.FSCD.2020.26
Abstract
Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions.
Subject Classification
ACM Subject Classification
- Theory of computation → Rewrite systems
- Theory of computation → Tree languages
- Theory of computation → Equational logic and rewriting
Keywords
- Anti-unification
- tree grammars
- unital theories
- collapse theories
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- María Alpuente, Santiago Escobar, Javier Espert, and José Meseguer. A modular order-sorted equational generalization algorithm. Inf. Comput., 235:98-136, 2014. URL: https://doi.org/10.1016/j.ic.2014.01.006.
- Franz Baader and Wayne Snyder. Unification theory. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 445-533. North-Holland, Amsterdam, 2001. URL: https://doi.org/10.1016/B978-044450813-3/50010-2.
- Johannes Bader, Andrew Scott, Michael Pradel, and Satish Chandra. Getafix: learning to fix bugs automatically. Proc. ACM Program. Lang., 3(OOPSLA):159:1-159:27, 2019. URL: https://doi.org/10.1145/3360585.
- 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: https://doi.org/10.1016/j.future.2017.07.024.
- Alexander Baumgartner. Anti-Unification Algorithms: Design, Analysis, and Implementation. PhD thesis, Johannes Kepler University Linz, 2015. Available from URL: http://www.risc.jku.at/publications/download/risc_5180/phd-thesis.pdf.
- Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal anti-unification. In Maribel Fernández, editor, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland, volume 36 of LIPIcs, pages 57-73. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.57.
-
Armin Biere. Normalisation, unification and generalisation in free monoids. Master’s thesis, University of Karlsruhe, 1993. (in German).
- David Cerna and Temur Kutsia. Idempotent anti-unification. ACM Trans. Comput. Logic, 21(2), November 2019. URL: https://doi.org/10.1145/3359060.
-
David M. Cerna and Temur Kutsia. Higher-order pattern generalization modulo equational theories. Mathematical Structures in Computer Science, 2020. Accepted.
- Stefan Kühner, Chris Mathis, Peter Raulefs, and Jörg H. Siekmann. Unification of idempotent functions. In Raj Reddy, editor, Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, MA, USA, August 22-25, 1977, page 528. William Kaufmann, 1977. URL: http://ijcai.org/Proceedings/77-1/Papers/092.pdf.
- Sonu Mehta, Ranjita Bhagwan, Rahul Kumar, Chetan Bansal, Chandra Maddila, B. Ashok, Sumit Asthana, Christian Bird, and Aditya Kumar. Rex: Preventing bugs and misconfiguration in large services using correlated change analysis. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 435-448, Santa Clara, CA, February 2020. USENIX Association. URL: https://www.usenix.org/conference/nsdi20/presentation/mehta.
-
Gordon D. Plotkin. A note on inductive generalization. Machine Intell., 5(1):153-163, 1970.
-
John C. Reynolds. Transformational systems and the algebraic structure of atomic formulas. Machine Intel., 5(1):135-151, 1970.
- 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.
-
Ute Schmid. Inductive Synthesis of Functional Programs, Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning, volume 2654 of Lecture Notes in Computer Science. Springer, 2003.
- Jörg H. Siekmann. Unification theory. J. Symb. Comput., 7(3/4):207-274, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80012-4.
- Erik Tidén and Stefan Arnborg. Unification problems with one-sided distributivity. J. Symb. Comput., 3(1/2):183-202, 1987. URL: https://doi.org/10.1016/S0747-7171(87)80026-3.