REPIUS: REwrite-Program Inversion and Unraveling System

Ver. 1.1c

News

June 27, 2012

MSV is correct for constructor TRSs w.r.t. constructor-based reduction.

---

Contents

• What is REPIUS?
• History
• Web interface
• Download
• How to use
• Input files
• Benchmarks
• References
• Contact

---

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 [NV12b] 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 [NV12b] and unraveling transformations were added.

Ver. 1.0 (January 11, 2012)

Adapted to du operator.

---

Web Interface

---

Download

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.

• standard (containing the latest approach, without any options)

  java -jar repius.jar filename

• full inversion based on our previous full inversion method [NSS05b]

  java -jar repius.jar -ieice05 [--sp] filename

  The suboption --sp provides the special rules for each inverses.
• Other options:

  -noinversion

  The inversion phase is skipped if this option is specified. This option enables the system to perform the MST transformation or unravelings transformations.

  -msv [--depthn]

  The MSV transformation is applied to inverted CTRSs if this option is specified. The suboption --depthn specifies the depth of leftmost innermost basic narrowing trees used in the transformation, e.g., --depth1. The default depth is 2 * m + 1 where m is the maximum number of conditions in rewrite rules.

  -U [--original | --optimized]

  One unraveling transformations for DCTRSs is applied to the final result, i.e., this is used after applying the MSV transformation if -msv is specified. The default is Ohlebusch's one. Marchiori's original one is used if the suboption --original is specified, and the optimized one is used if the suboption --optimized is used.

  -version

  The version is shown if this option is specified.

  -verbose

  Intermediate results are shown as comments in .trs format if this option is specified.

• Any other options -opt are ignored.

---

Input Files

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

• the CTRSs are constructor systems, except for du operator (see pack.trs)
• du is used in conditional parts, with one of the following forms:
  • du(single(t1)) -> pair(u1,u2),
  • du(pair(t1,t2)) -> single(u1), or
  • du(pair(t1,t2)) -> pair(u1,u2),
  where u1, u2 are constuctor terms.
• ...

---

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 [NV12a]

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]

[NV12a]

Naoki Nishida and Germán Vidal
Conversion to First-Order Tail Recursion for Improving Program Inversion
Submitted to a conference.

[NV12b]

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]

---

Contact

Naoki Nishida (Nagoya University)

nishida @ is.nagoya-u.ac.jp

---