Document Open Access Logo

Nominal Anti-Unification

Authors Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2015.57.pdf
  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Nominal Anti-Unification
  • Term-in-context
  • Equivariance

Metrics

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

Abstract

We study nominal anti-unification, which is concerned with computing
least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.

Cite As Get BibTex

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.57

Author Details

Alexander Baumgartner
Temur Kutsia
Jordi Levy
Mateu Villaret

References

  1. María Alpuente, Santiago Escobar, José Meseguer, and Pedro Ojeda. A modular equational generalization algorithm. In Michael Hanus, editor, LOPSTR, volume 5438 of LNCS, pages 24-39. Springer, 2008. Google Scholar
  2. Alexander Baumgartner and Temur Kutsia. A library of anti-unification algorithms. In Eduardo Fermé and João Leite, editors, Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, volume 8761 of Lecture Notes in Computer Science, pages 543-557. Springer, 2014. Google Scholar
  3. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A variant of higher-order anti-unification. In Femke van Raamsdonk, editor, RTA, volume 21 of LIPIcs, pages 113-127. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. Google Scholar
  4. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. Technical Report 15-03, RISC, JKU Linz, April 2015. Google Scholar
  5. Christophe Calvès. Complexity and Implementation of Nominal Algorithms. PhD thesis, King’s College London, 2010. Google Scholar
  6. Christophe Calvès and Maribel Fernández. A polynomial nominal unification algorithm. Theor. Comput. Sci., 403(2-3):285-306, 2008. Google Scholar
  7. Christophe Calvès and Maribel Fernández. Matching and alpha-equivalence check for nominal terms. J. Comput. Syst. Sci., 76(5):283-301, 2010. Google Scholar
  8. James Cheney. Relating nominal and higher-order pattern unification. In Laurent Vigneron, editor, UNIF'05, LORIA A05-R-022, pages 105-119, 2005. Google Scholar
  9. James Cheney. Equivariant unification. JAR, 45(3):267-300, 2010. Google Scholar
  10. Gilles Dowek, Murdoch J. Gabbay, and Dominic P. Mulligan. Permissive nominal terms and their unification. In 24th Italian Conference on Computational Logic, CILC'09, 2009. Google Scholar
  11. Gilles Dowek, Murdoch James Gabbay, and Dominic P. Mulligan. Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. Logic Journal of the IGPL, 18(6):769-822, 2010. Google Scholar
  12. Cao Feng and Stephen Muggleton. Towards inductive generalization in higher order logic. In Derek H. Sleeman and Peter Edwards, editors, ML, pages 154-162. Morgan Kaufmann, 1992. Google Scholar
  13. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Asp. Comput., 13(3-5):341-363, 2002. Google Scholar
  14. Murdoch J. Gabbay. A Theory of Inductive Definitions with alpha-Equivalence. PhD thesis, University of Cambridge, UK, 2000. Google Scholar
  15. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In LICS, pages 214-224. IEEE Computer Society, 1999. Google Scholar
  16. 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, Australian Conference on Artificial Intelligence, volume 4830 of LNCS, pages 273-282. Springer, 2007. Google Scholar
  17. Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-unification for unranked terms and hedges. In Manfred Schmidt-Schauß, editor, RTA, volume 10 of LIPIcs, pages 219-234. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  18. Jordi Levy and Mateu Villaret. Nominal unification from a higher-order perspective. In Andrei Voronkov, editor, RTA, volume 5117 of LNCS, pages 246-260. Springer, 2008. Google Scholar
  19. Jordi Levy and Mateu Villaret. An efficient nominal unification algorithm. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 209-226. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. Google Scholar
  20. Jordi Levy and Mateu Villaret. Nominal unification from a higher-order perspective. ACM Trans. Comput. Log., 13(2):10, 2012. Google Scholar
  21. Jianguo Lu, John Mylopoulos, Masateru Harao, and Masami Hagiya. Higher order generalization and its application in program verification. Ann. Math. Artif. Intell., 28(1-4):107-126, 2000. Google Scholar
  22. Frank Pfenning. Unification and anti-unification in the calculus of constructions. In LICS, pages 74-85. IEEE Computer Society, 1991. Google Scholar
  23. Gordon D. Plotkin. A note on inductive generalization. Machine Intel., 5(1):153-163, 1970. Google Scholar
  24. Luc De Raedt. Logical and Relational Learning. Springer, 2008. Google Scholar
  25. John C. Reynolds. Transformational systems and the algebraic structure of atomic formulas. Machine Intel., 5(1):135-151, 1970. Google Scholar
  26. Ute Schmid. Inductive Synthesis of Functional Programs, Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning, volume 2654 of LNCS. Springer, 2003. Google Scholar
  27. Christian Urban. Nominal techniques in Isabelle/HOL. J. Autom. Reasoning, 40(4):327-356, 2008. Google Scholar
  28. Christian Urban and James Cheney. Avoiding equivariance in alpha-prolog. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, volume 3461 of LNCS, pages 401-416. Springer Berlin Heidelberg, 2005. Google Scholar
  29. Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay. Nominal unification. In Matthias Baaz and Johann A. Makowsky, editors, CSL, volume 2803 of LNCS, pages 513-527. Springer, 2003. Google Scholar
  30. Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay. Nominal unification. Theor. Comput. Sci., 323(1-3):473-497, 2004. Google Scholar
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