Document Open Access Logo

Anti-Unification of Unordered Goals

Authors Gonzague Yernaux , Wim Vanhoof

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.37.pdf
  • Filesize: 0.76 MB
  • 17 pages

Document Identifiers

Author Details

Gonzague Yernaux
  • Faculty of Computer Science, University of Namur, Belgium
  • Namur Digital Institute, Belgium
Wim Vanhoof
  • Faculty of Computer Science, University of Namur, Belgium
  • Namur Digital Institute, Belgium

Cite AsGet BibTex

Gonzague Yernaux and Wim Vanhoof. Anti-Unification of Unordered Goals. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.37

Abstract

Anti-unification in logic programming refers to the process of capturing common syntactic structure among given goals, computing a single new goal that is more general called a generalization of the given goals. Finding an arbitrary common generalization for two goals is trivial, but looking for those common generalizations that are either as large as possible (called largest common generalizations) or as specific as possible (called most specific generalizations) is a non-trivial optimization problem, in particular when goals are considered to be unordered sets of atoms. In this work we provide an in-depth study of the problem by defining two different generalization relations. We formulate a characterization of what constitutes a most specific generalization in both settings. While these generalizations can be computed in polynomial time, we show that when the number of variables in the generalization needs to be minimized, the problem becomes NP-hard. We subsequently revisit an abstraction of the largest common generalization when anti-unification is based on injective variable renamings, and prove that it can be computed in polynomially bounded time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Anti-unification
  • Logic programming
  • NP-completeness
  • Time complexity
  • Algorithms
  • Inductive logic programming

Metrics

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

Related Versions

References

  1. María Alpuente, Santiago Escobar, Javier Espert, and José Meseguer. A Modular Order-Sorted Equational Generalization Algorithm. Information and Computation, 235:98-136, 2014. Special issue on Functional and (Constraint) Logic Programming. URL: https://doi.org/10.1016/j.ic.2014.01.006.
  2. 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 Computer Systems, 79:669-686, 2018. URL: https://doi.org/10.1016/j.future.2017.07.024.
  3. Alexander Baumgartner and Temur Kutsia. Unranked second-order anti-unification. Information and Computation, 255:262-286, 2017. WoLLIC 2014. URL: https://doi.org/10.1016/j.ic.2017.01.005.
  4. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Higher-order pattern anti-unification in linear time. Journal of Automated Reasoning, 58(2):293-310, February 2017. URL: https://doi.org/10.1007/s10817-016-9383-3.
  5. Peter E. Bulychev, Egor V. Kostylev, and Vladimir A. Zakharov. Anti-unification Algorithms and Their Applications in Program Analysis. In Amir Pnueli, Irina Virbitskaite, and Andrei Voronkov, editors, Perspectives of Systems Informatics, pages 413-423, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  6. Jochen Burghardt. E-generalization using grammars. Artificial Intelligence, 165(1):1-35, 2005. URL: https://doi.org/10.1016/j.artint.2005.01.008.
  7. Jochen Burghardt. An improved algorithm for e-generalization. arXiv, 2017. URL: http://arxiv.org/abs/1709.00744.
  8. Dirk G. Cattrysse and Luk N. [Van Wassenhove]. A survey of algorithms for the generalized assignment problem. European Journal of Operational Research, 60(3):260-272, 1992. URL: https://doi.org/10.1016/0377-2217(92)90077-M.
  9. David M. Cerna and Temur Kutsia. Higher-order pattern generalization modulo equational theories. Mathematical Structures in Computer Science, 30(6):627-663, 2020. URL: https://doi.org/10.1017/S0960129520000110.
  10. Philippe Codognet and Daniel Diaz. Boolean Constraint Solving Using CLP(FD). In International Logic Programming Symposium, page 15 pages, Vancouver, British Columbia, Canada, 1993. Google Scholar
  11. Danny De Schreye, Robert Glück, Jesper Jørgensen, Michael Leuschel, Bern Martens, and Morten Heine Sørensen. Conjunctive partial deduction: foundations, control, algorithms, and experiments. The Journal of Logic Programming, 41(2):231-277, 1999. URL: https://doi.org/10.1016/S0743-1066(99)00030-8.
  12. Melvin Fitting. Fixpoint Semantics for Logic Programming A Survey. Theoretical Computer Science, 278(1):25-51, 2002. Mathematical Foundations of Programming Semantics 1996. URL: https://doi.org/10.1016/S0304-3975(00)00330-3.
  13. J. P. Gallagher. Tutorial on Specialisation of Logic Programs. In Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM '93, pages 88-98, New York, NY, USA, 1993. ACM. URL: https://doi.org/10.1145/154630.154640.
  14. Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Sondergaard, and Peter Stuckey. Horn Clauses as an Intermediate Representation for Program Analysis and Transformation. Theory and Practice of Logic Programming, 15, July 2015. URL: https://doi.org/10.1017/S1471068415000204.
  15. Peter Idestam-Almquist. Generalization of Clauses under Implication. Journal of Artificial Intelligence Research, November 1995. URL: https://doi.org/10.1613/jair.194.
  16. Joxan Jaffar, Michael Maher, Kim Marriott, and Peter Stuckey. The Semantics of Constraint Logic Programs. The Journal of Logic Programming, 37(1):1-46, 1998. URL: https://doi.org/10.1016/S0743-1066(98)10002-X.
  17. Laura Ildikó Kovács and Tudor Jebelean. An Algorithm for Automated Generation of Invariants for Loops with Conditionals. In Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), 25-29 September 2005, Timisoara, Romania, pages 245-249, 2005. URL: https://doi.org/10.1109/SYNASC.2005.19.
  18. Ulf Krumnack, Angela Schwering, Helmar Gust, and Kai-Uwe Kühnberger. Restricted Higher-Order Anti-Unification for Analogy Making. In Mehmet A. Orgun and John Thornton, editors, AI 2007: Advances in Artificial Intelligence, pages 273-282, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  19. Frédéric Mesnard, Étienne Payet, and Wim Vanhoof. Towards a Framework for Algorithm Recognition in Binary Code. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 202-213, 2016. URL: https://doi.org/10.1145/2967973.2968600.
  20. Stephen Muggleton and Luc de Raedt. Inductive Logic Programming: Theory and methods. The Journal of Logic Programming, 19-20:629-679, 1994. Special Issue: Ten Years of Logic Programming. URL: https://doi.org/10.1016/0743-1066(94)90035-3.
  21. Stephen Muggleton and Cao Feng. Efficient Induction of Logic Programs. In New Generation Computing. Academic Press, 1990. Google Scholar
  22. S. H. Nienhuys-Cheng and R. de Wolf. Least Generalizations and Greatest Specializations of Sets of Clauses. arXiv e-prints, page cs/9605102, April 1996. URL: http://arxiv.org/abs/cs/9605102.
  23. Alberto Pettorossi and Maurizio Proietti. Program Specialization via Algorithmic Unfold/Fold Transformations. ACM Comput. Surv., 30(3es):6, 1998. URL: https://doi.org/10.1145/289121.289127.
  24. F. Pfenning. Unification and Anti-Unification in the Calculus of Constructions. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74-85, July 1991. URL: https://doi.org/10.1109/LICS.1991.151632.
  25. Gordon D. Plotkin. A Note on Inductive Generalization. Machine Intelligence, 5:153-163, 1970. Google Scholar
  26. Reudismam Rolim, Gustavo Soares, Rohit Gheyi, Titus Barik, and Loris D'Antoni. Learning quick fixes from code repositories, 2018. URL: http://arxiv.org/abs/1803.03806.
  27. Morten H. Sørensen and Robert Glück. An Algorithm of Generalization in Positive Supercompilation. In Proceedings of ILPS'95, the International Logic Programming Symposium, pages 465-479. MIT Press, 1995. Google Scholar
  28. Wim Vanhoof and Gonzague Yernaux. Generalization-Driven Semantic Clone Detection in CLP. In Maurizio Gabbrielli, editor, Logic-Based Program Synthesis and Transformation, pages 228-242, Cham, 2020. Springer International Publishing. Google Scholar
  29. Gonzague Yernaux and Wim Vanhoof. Anti-unification in Constraint Logic Programming. Theory and Practice of Logic Programming, 19(5-6):773-789, 2019. URL: https://doi.org/10.1017/S1471068419000188.
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