SUBVARIANT

Abstract

SubVariant (*) is a tool for computing finite strongly complete set of variants modulo a convergent optimally reducing term rewriting system. SubVariant can also compute complete sets of equational unifiers for equational theories implemented by a convergent optimally reducing term rewriting system.

Complete sets of variants and the finite variant property were introduced in [1]. In [2], we define strongly complete sets of variants, which we argua to be more natural and more useful. Strongly complete sets of variants were motived by and used in the research tool AKISS, soon to be avaiable here. Chapter 3 in the PhD thesis of Ștefan Ciobâcă describes extensively the algorithms behind SubVariant. The PhD thesis will soon be available here.

The research report explaining the algorithm behind SubVariant is available [2].

Installing SubVariant

After installing the above dependencies, it is sufficient to type:

make

Running SubVariant

After succesfully compiling SubVariant, you can run it on an input such as the following input file "examples-variants/decenc.sub" found in SubVariant's distribution file:

$ cat examples-variants/decenc.sub 
var x, y, z;

rewrite dec(enc(x, y), y) -> x;

variants pair(dec(x, y), dec(z, y));

unify dec(x, y) and dec(z, y);

In the example file above, three variables x, y and z are declared as being variables. Everything else is treated as a function symbol. Then comes the definition of the rewrite system. In this case, there is only one rewrite rule (see the other examples for the syntax of multiple rewrite rules) which states that decryption (the function symbol "dec") cancels out encryption (the function symbol "enc") if the right key is used.

The example then features two queries: the first query asks for a strongly complete set of variants of the term

pair(dec(x, y), dec(z, y))

To run SubVariant on the above file, it is sufficient to run the following command:

$ ./subvariant.native < examples-variants/decenc.sub 
Strong variants of pair(dec(x, y), dec(z, y)):
pair(dec(x, y), dec(z, y)){  }
pair(dec(x, X2), X3){ y |-> X2, z |-> enc(X3, X2) }
pair(X5, dec(z, X4)){ y |-> X4, x |-> enc(X5, X4) }
pair(X5, X13){ y |-> X12, x |-> enc(X5, X12), X4 |-> X12, z |-> enc(X13, X12) }
pair(X9, X3){ y |-> X8, z |-> enc(X3, X8), X2 |-> X8, x |-> enc(X9, X8) }

Equational unifiers of dec(x, y) and dec(z, y):
{ y |-> X29, x |-> z }
{ y |-> X27, z |-> enc(dec(x, X27), X27) }
{ y |-> X25, x |-> enc(dec(z, X25), X25) }
{ y |-> X23, x |-> enc(X21, X23), z |-> enc(X21, X23) }

Note that neither the strongly complete set of variants nor the complete set of unifiers is minimal, in that the 4th or the 5th variant can be removed and the 4th equational unifier can be removed as well. Obtaining miminal sets is not the purpose of SubVariant. Minimality can be achieved by a post-processing step which checks if a variant/equational unifier is an instance of another variant/equational unifer.

Contact

References

[1] H. Comon-Lundh and S. Delaune The finite variant property: How to get rid of some algebraic properties

[2] Ștefan Ciobâcă Computing finite variants for subterm convergent rewrite systems

This webpage refers to SubVariant version 2, written in Ocaml. The first version of SubVariant was written in PLT Racket, is deprecated and is linked here for historical and archiving purposes.