Autowrite: A Tool for Term Rewrite Systems and Tree Automata
Résumé
Autowrite is an experimental software tool written in Common Lisp for handling term rewrite systems and bottom-up tree automata. A graphical interface has been written using McCLIM, (the free implementation of the CLIM specification) in order to free the user of any Lisp knowledge. Software and documentation can be found at http://dept-info.labri.u-bordeaux.fr/~idurand/autowrite Autowrite was initially designed to check call-by-need properties of term rewrite systems. For this purpose, it implements the tree automata constructions used in [J96,DM97,DM98,NT02] and many useful operations on terms, term rewrite systems and tree automata. In the first version of Autowrite [D02], only the call-by-need properties and a few other simple properties were available from the graphical interface. This new version of Autowrite includes many new functionalities. There are new functionalities related to TRSs, but the most interesting new feature is the possibility to directly handle (load, save, combine with boolean operations) bottom-up tree automata. In addition, we have added on-line timing information. Since the first version the run-times have been considerably improved due to better choices of data structures. The first version of Autowrite was used to check call-by-need for most of the examples presented in [DM01]. Most of the time no alternative proofs exists. The new features allowed testing many properties of examples presented in DM03 for which no easy proof can be written.