10.4230/LIPICS.RTA.2011.283
Nishida, Naoki
Naoki
Nishida
Vidal, German
German
Vidal
Program Inversion for Tail Recursive Functions
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
term rewriting
program transformation
termination
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
2011
2011-04-26
2011-04-26
2011-04-26
en
urn:nbn:de:0030-drops-31253
10.4230/LIPIcs.RTA.2011
978-3-939897-30-9
1868-8969
10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA 2011
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
2013
10
24
283
298
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
10
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
16 pages
610334 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
Program inversion is a fundamental problem that has been addressed in
many different programming settings and applications. In the context
of term rewriting, several methods already exist for computing the
inverse of an injective function. These methods, however, usually
return non-terminating inverted functions when the considered function
is tail recursive. In this paper, we propose a direct and intuitive
approach to the inversion of tail recursive functions. Our new
technique is able to produce good results even without the use of an
additional post-processing of determinization or completion. Moreover,
when combined with a traditional approach to program inversion, it
constitutes a promising approach to define a general method for
program inversion. Our experimental results confirm that the new
technique compares well with previous approaches.
LIPIcs, Vol. 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), pages 283-298