Towards fast nominal anti-unification of Letrec-expressions
File(s)
Published version
Author(s)
Schmidt-Schauss, Manfred
Nantes Sobrinho, Daniele
Type
Chapter
Abstract
This paper describes anti-unification algorithms for computing least general generalizations of two expressions in a functional programming language with recursive let. First, by exploring a semantic approach to the problem, we argue for an improvement of the technique used in previous papers which avoids infinite chains of properly descending generalizations. Second, we present a (non-deterministic) nominal general anti-unification algorithm applicable to general expressions, which is complete, terminating and requires polynomial time. Third, we propose a specialized anti-unification algorithm applicable to two or more garbage-free ground expressions that produces a single least general generalization in polynomial time, and which can also exploit further semantically correct equivalences. Our results have potential applications in finding clones in functional programs.
Editor(s)
Pientka, B
Tinelli, C
Date Issued
2023-09-02
Citation
Automated Deduction - CADE 29, 2023, 14132, pp.456-473
ISBN
978-3-031-38498-1
Publisher
Springer International Publishing
Start Page
456
End Page
473
Journal / Book Title
Automated Deduction - CADE 29
Lecture Notes in Artificial Intelligence
Volume
14132
Copyright Statement
© The Author(s) 2023. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Subjects
Anti-Unification
Computer Science
Computer Science, Artificial Intelligence
Computer Science, Theory & Methods
Functional Programming
Generalization
Mathematics
Mathematics, Applied
Nominal Techniques
Physical Sciences
Recursive Let
Science & Technology
Technology
Publication Status
Published
Date Publish Online
2023-09-02