
 Synopsis

The LRSX Tool provides algorithms to syntactically reason on metaexpressions representing programs of program calculi with higherorder constructs and recursive and shared bindings (i.e. socalled letrecexpressions).
The underlying metalanguage and the algorithms are designed to capture usual callbyneed lambdacalculi including their reduction strategies.
The core functionality are unification and a matching algorithm for those metaexpressions.
The extended functionality is to overlap reduction rules with program transformations on a given calculus description as input.
Using matching and symbolic alpharenaming the LRSX Tool can be used to join the computed overlaps and thus to compute socalled complete sets of forking and commuting diagrams.
Finally, an induction proof using the diagrams can be used to prove correctness of program transformations.
The LRSX Tool automates this final step by transforming the induction proof into a termination proof of term rewrite systems which is then performed by automated termination provers.
The LRSX Tool is implemented in Haskell and packaged via Cabal and comes with
a 3clause BSDlike LICENSE.
 Download and Building


The sourcedistribution is available here:
lrsx0.6.1.0.tar.gz
 A recent installation of the Glasgow Haskell Compiler, the base libraries, and CabalInstall is required (see https://www.haskell.org/downloads)

To build lrsx unzip the archive, then run cabal, i.e.:
tar xzf lrsx0.6.1.0.tar.gz
cd lrsx0.6.1.0/
cabal configure
cabal build
This will create the executable lrsx in dist/build/lrsx/ , e.g. type
dist/build/lrsx/lrsx help
to see the helptext of the LRSX Tool.
 The executable
lrsx can be installed via typing cabal install
If this completes successfully you will have the lrsxbinary in ~/.cabal/bin .
 Documentation

Using LSRX
The LRSX Tool prints several helptexts by calling lrsx help or more command specific help by typing lrsx command help .
The main commands of the LRSX Tool are:
 Unification equations with constraints:
For input files call lrsx unify file, where file contains the input.
LRSX will unify the input and print the output to stdout.
 Matching equations with constraints:
For input files call lrsx match file, where file contains the input.
LRSX will perform matching on the input and print the output to stdout.
 Program calculus descriptions and overlap commands:
lrsx overlap file computes the overlaps as requested by the commands in file.
lrsx join file computes the overlaps and joins to compute forking and answer diagrams, as requested the commands in file.
lrsx convert from to file converts the representation of joins in file from fromformat into toformat.
lrsx induct file uses the diagrams from file and performs automated induction with them (requires an appropriate installation of termination provers).
lrsx interactive start the interactive mode of the LRSX tool.
 Examples
The source distribution comes with several examples which can be found in examples .
Two workedout examples for program calculi can be found on the following webpages:
 Input and output for the calculus L_{need} can be found on this webpage.
 Input and output for the calculus L_{need}^{+seq} can be found on this webpage.
 Input and output for the calculus LR can be found on this webpage.
 Contact

Dr. David Sabel
Computer Science Institute
Computer Science and Mathematics Department
Johann Wolfgang GoetheUniversity Frankfurt am Main
