This represents an older verion of the tool SubVariant. For all purposes I recommend the use of the new version.

SUBVARIANT

Abstract

SubVariant is a tool for computing a complete set of variants of any term modulo a subterm convergent rewrite system.

Subterm convergent rewrite systems were first introduced in [1] and their definition slightly extended in [2]. The tool SubVariant works for subterm convergent rewrite systems in the slightly larger sense of [2].

Finite variants and the finite variant property were introduced in [3].

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

As a bonus, SubVariant can be used to compute complete set of unifiers modulo any subterm convergent rewrite system in the sense of [2].

Using SubVariant

SubVariant is available as a Scheme source file.

SubVariant was written in Plt Racket (and is compatible with some older versions of Plt Scheme). In order to run SubVariant, you need to download and install Plt Racket (or an older version of Plt Scheme) from [5].

To run SubVariant on an input file variant.in, you should execute:

mzscheme subvariant.scm < variant.in

Example

Assume we have the following subterm convergent rewrite system:

dec(enc(x, y), y) -> x
fst(pair(x,y)) -> x
snd(pair(x,y)) -> y

and that we are trying to


 find the variants of pair(dec(x,y),dec(z,w))
 find a complete set of unifiers of the equation dec(x,y) = a

In the above terms, we have assumed that dec, enc and pair are binary function symbols, that fst and snd are unary function symbols, that a is a nullary function symbol (a constant) and that x, y, z and w are variables.

To have SubVariant answer the above two questions, we will construct the following input file example.in:

(rewrite
	((dec (enc x y) y) x)
	((fst (pair x y)) x)
	((snd (pair x y)) y))

(variants
	(pair (dec x y) (dec z w)))

(unifiers
	(dec x y)
	(a))

(exit)

The input file is given as a series of S-expressions as explained above. Terms are written as is expected in prefix form. Any symbol which appears in the non-head position of a list is assumed to be a variable. This means that constants must be written using parenthesis, as seen in the unification example.

To run SubVariant on the above example, simply launch the command:

mzscheme subvariant.scm < example.in

When run with the above input, SubVariant will provide the answers we are looking for:

Setting new rewrite system
(((dec (enc x y) y) x) ((fst (pair x y)) x) ((snd (pair x y)) y))


Computing finite variants of
(pair (dec x y) (dec z w))
The variants are:
(() ((y . _1) (x enc _0 _1)) ((w . _7) (z enc _6 _7)) ((y . _1) (x enc _0 _1) (w . _13) (z enc _12 _13)) ((w . _7) (z enc _6 _7) (y . _19) (x enc _18 _19)))




Computing unifiers of
(dec x y) and (a)
Unifiers:
(((y . _37) (x enc (a) _37)))


()

The

(exit)

command is required because SubVariant is usually used as an interactive tool. If you do not insert at the end of a file, you will get an error at the end but other than the uglyness of the error everything should be ok.

Contact

If you have questions/problems regarding SubVariant, please contact Ștefan Ciobâcă at name@lsv.ens-cachan.fr. Use "ciobaca" for name.

References

[1] Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under equational theories

[2] M. Baudet, V. Cortier and S. Delaune YAPA: A generic tool for computing intruder knowledge

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

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

[5] Download PLT Racket