Document Open Access Logo

Nominal Anti-Unification with Atom-Variables

Authors Manfred Schmidt-Schauß , Daniele Nantes-Sobrinho

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.7.pdf
  • Filesize: 0.88 MB
  • 22 pages

Document Identifiers

Author Details

Manfred Schmidt-Schauß
  • Goethe Universität, Frankfurt am Main, Germany
Daniele Nantes-Sobrinho
  • Department of Computing, Imperial College London, UK
  • Department of Mathematics, University of Brasília, Brazil

Funding

  • Nantes-Sobrinho, Daniele: partially funded by the EPSRC Fellowship 'VeTSpec: Verified Trustworthy Software Specification' (EP/R034567/1) and Edital DPI/DPG n. 03/2020.

Cite AsGet BibTex

Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho. Nominal Anti-Unification with Atom-Variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.7

Abstract

Anti-unification is the task of generalizing a set of expressions in the most specific way. It was extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately, when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in nominal anti-unification does not exist, in general. In this paper, we present a more general approach to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants of freshness constraints: NL_A-constraints (with atom-variables), and Eqr-constraints based on Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation increases its application potential: we provide an algorithm that is finitary for the NL_A-freshness constraints, and for Eqr-freshness constraints it computes a unique least general generalization. There is a price to pay in the general case: checking freshness constraints and other related logical questions will require exponential time. The setting of Baumgartner et al. is improved by the atom-only case, which runs in polynomial time and computes a unique least general generalization.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Generalization
  • anti-unification
  • nominal algorithms
  • higher-order deduction

Metrics

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

References

  1. Franz Baader. Unification, weak unification, upper bound, lower bound, and generalization problems. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, Como, Italy, April 10-12, 1991, Proceedings, volume 488 of Lecture Notes in Computer Science, pages 86-97. Springer, 1991. URL: https://doi.org/10.1007/3-540-53904-2_88.
  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 Gener. Comput. Syst., 79:669-686, 2018. URL: https://doi.org/10.1016/j.future.2017.07.024.
  3. 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. URL: https://doi.org/10.1007/978-3-319-11558-0_38.
  4. Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal anti-unification. In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications, RTA 2015, June 29 to July 1, 2015, Warsaw, Poland, volume 36 of LIPIcs, pages 57-73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.RTA.2015.57.
  5. Peter E. Bulychev, Egor V. Kostylev, and Vladimir A. Zakharov. Anti-unification algorithms and their applications in program analysis. In Amir Pnueli, Irina B. Virbitskaite, and Andrei Voronkov, editors, Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers, volume 5947 of Lecture Notes in Computer Science, pages 413-423. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-11486-1_35.
  6. Christophe Calvès and Maribel Fernández. A polynomial nominal unification algorithm. Theor. Comput. Sci., 403(2-3):285-306, 2008. URL: https://doi.org/10.1016/j.tcs.2008.05.012.
  7. David M. Cerna and Temur Kutsia. Higher-order equational pattern anti-unification. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.12.
  8. David M. Cerna and Temur Kutsia. Higher-order pattern generalization modulo equational theories. Math. Struct. Comput. Sci., 30(6):627-663, 2020. URL: https://doi.org/10.1017/S0960129520000110.
  9. James Cheney. Toward a general theory of names: Binding and scope. In MERLIN 2005, pages 33-40. ACM, 2005. Google Scholar
  10. Hubert Comon. Sufficient completness, term rewriting systems and "anti-unification". In Jörg H. Siekmann, editor, 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, volume 230 of Lecture Notes in Computer Science, pages 128-140. Springer, 1986. URL: https://doi.org/10.1007/3-540-16780-3_85.
  11. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341-363, 2002. URL: https://doi.org/10.1007/s001650200016.
  12. Haskell. Haskell, an advanced, purely functional programming language, 2019. URL: https://www.haskell.org.
  13. Boris Konev and Temur Kutsia. Anti-unification of concepts in description logic EL. In Chitta Baral, James P. Delgrande, and Frank Wolter, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016, pages 227-236. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12880.
  14. 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, 20th Australian Joint Conference on Artificial Intelligence, Gold Coast, Australia, December 2-6, 2007, Proceedings, volume 4830 of Lecture Notes in Computer Science, pages 273-282. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76928-6_29.
  15. Yunus D. K. Kutz and Manfred Schmidt-Schauß. Rewriting with generalized nominal unification. Math. Struct. Comput. Sci., 30(6):710-735, 2020. URL: https://doi.org/10.1017/S0960129520000122.
  16. Jean-Louis Lassez and Kim Marriott. Explicit representation of terms defined by counter examples. J. Autom. Reason., 3(3):301-317, 1987. URL: https://doi.org/10.1007/BF00243794.
  17. Jordi Levy and Mateu Villaret. Nominal unification from a higher-order perspective. In 19th RTA, volume 5117 of Lecture Notes in Computer Science, pages 246-260. Springer, 2008. Google Scholar
  18. Jordi Levy and Mateu Villaret. An efficient nominal unification algorithm. In Christopher Lynch, editor, Proc. 21st RTA, volume 6 of LIPIcs, pages 209-226. Schloss Dagstuhl, 2010. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.209.
  19. 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. URL: https://doi.org/10.1023/A:1018952121991.
  20. Simon Marlow, editor. Haskell 2010 - Language Report. Haskell.org, 2010. Google Scholar
  21. Gordon D. Plotkin. A note on inductive generalization. Machine Intel., 5(1):153-163, 1970. Google Scholar
  22. Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal unification of higher order expressions with recursive let. In Manuel V. Hermenegildo and Pedro López-García, editors, Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, volume 10184 of LNCS, pages 328-344. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-63139-4_19.
  23. Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, and Yunus Kutz. Nominal unification and matching of higher order expressions with recursive let. Fundamenta Informaticae, 2022. to be published in volume 185 issue 03. Google Scholar
  24. Manfred Schmidt-Schauß, David Sabel, and Yunus D. K. Kutz. Nominal unification with atom-variables. J. Symb. Comput., 90:42-64, 2019. URL: https://doi.org/10.1016/j.jsc.2018.04.003.
  25. Christian Urban, Andrew M. Pitts, and Murdoch Gabbay. Nominal unification. In 17th CSL, 12th EACSL, and 8th KGC, volume 2803 of LNCS, pages 513-527. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_41.
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