Autowrite is now part of TRAG

What is Autowrite

Autowrite is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autowrite is an experimental tool written in Common Lisp for checking properties of term rewrite systems and handling bottom-up term (tree) automata. It is written in Steele Bank Common Lisp ( SBCL). It was initially designed to check call-by-need (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata constructions (determinization, minimization, union, intersection, emptimess,...) and many operations on terms. Recently, fly-automata have been added to the implementation. The transition function of a fly-automaton is a (Lisp) transition function instead of a table of transitions. Fly-automata may be used when the transition table is too big to be stored and can also be infinite in two ways (infinite signature, infinite number of states). A graphical interface interface written using FreeCLIM , the free implementation of the CLIM specification frees the user from any Lisp knowledge. From this interface, one can handle term rewrite systems, term automata and build many term automata related to TRSs and graphs represented as terms; one can check membership to call-by-need classes for the different considered approximations of a given system.

Main features of Autowrite

The principal features of Autowrite are:

• Terms and term rewrite systems. Given a term t and a term rewrite system R over a signature F
  • check whether: R is left-linear, overlapping, orthogonal, constructor
  • check whether: R is forward-branching
  • compute approximations of R (strong-approximation, nv-approximation, linear-growing-approximation, growing-approximation)
  • decide whether R is in CBN_alpha (for the different approximations alpha) and exhibits an alpha-free term in the negative case.
  • Check whether NF(R) (the set of normal forms) is empty
  • Check whether ENF(R) (the set of external normal forms) is empty
  • If F is the signature consisting of the terms appearing in R and G be F extended by a fresh constant symbol, decide whether the set of terms in T(F) normalizable with (R,F), WN(R,F), is different (strictly included) into the set of terms in T(F) normalizable with (R,F), WN(R,G,F). The same check can be done with R extended with the rule o -> o.
  • Check whether the current approximation S is arbitrary i.e. if there exists a term t in T(F) such that t -*->(R,FU{@}) @
• Term automata. Given term automata A and a term t
  
  • decide whether t is in L(A)
  • decide whether L(A) is empty
  • compute a deterministic version of A
  • compute a reduced version of A
  • compute the complement of A
  • compute the minimized version of A
  • given another automaton B compute the union or the intersection of A and B
• Automata and term rewrite systems.
  
  • given a set of ground terms S: compute a term automaton A_S such that L(A_S) = S
  • given a set of linear terms S: compute a term automaton A_S such that L(A_S) recognizes the set of instances of S
  • given the set of left-handsides of a left-linear TRS R: compute an automaton A_NF(R) such that L(A_NF(R)) = NF(R)
  • given term automaton A and a left-linear growing term rewrite system:
    compute an automaton C_[R,A] such that L(C_[R,A]) = (-*->)[L(A)]
  • given a left-linear growing extended term rewrite system R: compute an automaton D_R such that L(D_R) is empty if and only if R is in CBN.
• Fly-automata.
  Fly-(Term)-automata are (non necessarily finite) Term Automata whose transitions are given by a transition function instead of a transition table; a fly-automaton has also a final state predicate which indicates whether a state returned by the transition is final. A fly-automaton can be infinite in two ways: it can have an infinite (countable) signature and/or an infinite (countable) set of states. When finite (finite signature and finite set of states), a fly-automaton be compiled into a table-automaton (when the resulting term automaton is not too big).

A collection of examples of term rewrite systems to use with Autowrite is included in the Data directory of the distribution.

Installing Autowrite

Download the relevant Autowrite.tgz tar file

• tar xzvf Autowrite.tgz
  
• cd Autowrite
  
• ./INSTALL
  

Running Autowrite

• ./autowrite

 git clone https://idurand@bitbucket.org/idurand/trag.git