Updated: Oct 21, 2015

REPIUS: REwrite-Program Inversion and Unraveling System

Ver. 1.2a


News

December 16, 2014
The conversion to tail-recursion was incorporated by Takayuki Kuroda.
June 27, 2012
MSV is correct for constructor TRSs w.r.t. constructor-based reduction.

Contents


What is REPIUS?

REPIUS is a tool that (fully or partially) inverts a constructor TRS written in a .trs file and unravels the resulting inverse CTRS. The prototype (Ver. 0.x) was developed following the approach in [NSS05a] and optionally employs unraveling transformations as a post-process of inversion. The current version was wholly implemented, introducing a new approach to tail-recursive functions into the previous approach to full inversion [NSS05b]. The MSV transformation [NV12] can be optionally applied to inverted systems. The partial inversion approach [NSS05a] will be implemented as an extension.

The current implementation is based on the technique in [NV11].


History

Ver. 1.1c (June 27, 2012)
MSV transformation was completed.
Ver. 1.1b (January 25, 2012)
The options -noinversion, -version and -verbose were added.
Ver. 1.1 (January 24, 2012)
The MSV transformation [NV12] and unraveling transformations were added.
Ver. 1.0 (January 11, 2012)
Adapted to du operator.

Web Interface


Download

!! The download version is now outdated. !!

This is written in OCaml and compiled by OCaml-Java (ocamljava 1.4).

repius.jar (Jun 27, 2012)

How to Use

Note: Java 1.6 is required.


Input Files

Repius recognizes .trs format files, CTRSs in which satisfy all of the following:


Benchmarks

Original ones from Glück and Kawabe's papers [APLAS 2003, Fundam. Inform. 66(4), and PADL 2005]

name .fct style .trs style remarks wui
snoc snoc.fct snoc.trs
reverse reverse.fct reverse.trs
snocrev snocrev.fct snocrev.trs
double double.fct double.trs
mirror mirror.fct mirror.trs
zip zip.fct zip.trs
inc inc.fct inc.trs
unbin unbin.fct unbin.trs
octbin octbin.fct octbin.trs
treelist treelist.fct treelist.trs
treepaths treepaths.fct treepaths.trs
pack pack.fct pack.trs
pack-bin packbin.fct packbin.trs
print-sexp printsexp.fct printsexp.trs
print-xml printxml.fct printxml.trs

Variants of original ones [NV11]

name .fct style .trs style remarks wui
reverse2 reverse2.fct reverse2.trs
unbin2 unbin2.fct unbin2.trs
unbin3 unbin3.fct unbin3.trs
treelist2 treelist2.fct treelist2.trs

Ones obtained from the above by applying the inversion method [NV11]

name .fct style .trs style remarks wui
inv-reverse inv-reverse.fct inv-reverse.trs
inv-unbin inv-unbin.fct inv-unbin.trs
inv-treepaths inv-treepaths.fct inv-treepaths.trs

Ones obtained from the original and variants above by applying LRinv (Glück and Kawabe's method) [APLAS 2003, Fundam. Inform. 66(4), and PADL 2005]

name .fct style .trs style remarks wui
lrinv-reverse lrinv-reverse.fct lrinv-reverse.trs
lrinv-unbin lrinv-unbin.fct lrinv-unbin.trs
lrinv-treepaths lrinv-treepaths.fct lrinv-treepaths.trs

Ones obtained from the original by transforming into tail recursion [NV14]

name .fct style .trs style remarks wui
snoc-tail snoc-tail.fct snoc-tail.trs
reverse-tail reverse-tail.fct reverse-tail.trs
snocrev-tail snocrev-tail.fct snocrev-tail.trs
double-tail double-tail.fct double-tail.trs
mirror-tail mirror-tail.fct mirror-tail.trs
zip-tail zip-tail.fct zip-tail.trs
inc-tail inc-tail.fct inc-tail.trs
unbin-tail unbin-tail.fct unbin-tail.trs
octbin-tail octbin-tail.fct octbin-tail.trs
treepaths-tail1 treepaths-tail1.fct treepaths-tail1.trs
treepaths-tail2 treepaths-tail2.fct treepaths-tail2.trs
pack-tail pack-tail.fct pack-tail.trs
pack-bin-tail packbin-tail.fct packbin-tail.trs
print-sexp-tail1 printsexp-tail1.fct printsexp-tail1.trs
print-sexp-tail2 printsexp-tail2.fct printsexp-tail2.trs
print-xml-tail1 printxml-tail1.fct printxml-tail1.trs
print-xml-tail2 printxml-tail2.fct printxml-tail2.trs
print-xml-tail3 printxml-tail3.fct printxml-tail3.trs

Ones from Matsuda's papers

name .fct style .trs style remarks wui
exp exp.fct exp.trs

References

[NSS01]
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Generation of Inverse Term Rewriting Systems for Pure Treeless Functions
In Yoshihito Toyama, editor, Proceedings of the International Workshop on Rewriting in Proof and Computation,
pp. 188-198, Sendai, Japan, Octber 2001.

[NSS02]
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Generation of a TRS Implementing the Inverses of Pure Treeless Functions
Computer Software, Vol. 19, No. 1, pp. 29-33, January 2002 (in Japanese).

[NSS05a]
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Partial Inversion of Constructor Term Rewriting Systems
In Jürgen Giesl, editor, Proceedings of the 16th International Conference on Rewriting Techniques and Applications,
Vol. 3467 of Lecture Notes in Computer Science, pp. 264-278. Springer, April 2005.

[NSS05b]
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe
Generation of Inverse Computation Programs of Constructor Term Rewriting Systems
The IEICE Transactions on Information and Systems, Vol. J88-D-I, No. 8, pp. 1171-1183, August 2005 (in Japanese).

[NS09]
Naoki Nishida and Masahiko Sakai
Completion after Program Inversion of Injective Functions
In Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming,
Vol. 237 of Electronic Notes in Theoretical Computer Science, pp. 39-56, April 2009.
(This is a revised version of the preproceeding for WRS'08.)
[experimental results]

[NS10]
Naoki Nishida and Masahiko Sakai
Proving Injectivity of Functions via Program Inversion in Term Rewriting
In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Proceedings of the 10th International Symposium on Functional and Logic Programming,
Vol. 6009 of Lecture Notes in Computer Science, pp. 288-303, Springer, April 2010.

[NV11]
Naoki Nishida and Germán Vidal
Program Inversion for Tail Recursive Functions
In Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), Vol. 10 of LIPIcs, pp. 283-298, 2011.
[LIPIcs, paper]

[NV12]
Naoki Nishida and Germán Vidal
More Specific Term Rewriting Systems
In Proceedings of the 21st International Workshop on Functional and (Constraint) Logic Programming (WFLP 2012), 15 pages, 2012.
[pdf]

[NV14]
Naoki Nishida and Germán Vidal
Conversion to tail recursion in term rewriting
The Journal of Logic and Algebraic Programming, Vol. 83, Issue 1, pp. 53-63, January 2014.
[link]


Contact

Naoki Nishida (Nagoya University)
nishida @ is.nagoya-u.ac.jp