The LRSX Tool provides algorithms to syntactically reason on meta-expressions representing programs of program calculi with higher-order constructs and recursive and shared bindings (i.e. so-called letrec-expressions).
The underlying meta-language and the algorithms are designed to capture usual call-by-need lambda-calculi including their reduction strategies.
The core functionality are unification and a matching algorithm for those meta-expressions.
The extended functionality is to overlap reduction rules with program transformations on a given calculus description as input.
Using matching and symbolic alpha-renaming the LRSX Tool can be used to join the computed overlaps and thus to compute so-called 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 3-clause BSD-like LICENSE.
- Download and Building
The source-distribution is available here:
- A recent installation of the Glasgow Haskell Compiler, the base libraries, and Cabal-Install is required (see https://www.haskell.org/downloads)
To build lrsx unzip the archive, then run cabal, i.e.:
tar -xzf lrsx-0.6.1.0.tar.gz
This will create the executable
dist/build/lrsx/, e.g. type
to see the help-text of the LRSX Tool.
- The executable
lrsx can be installed via typing
If this completes successfully you will have the lrsx-binary in
The LRSX Tool prints several help-texts 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 from-format into to-format.
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.
The source distribution comes with several examples which can be found in
Two worked-out examples for program calculi can be found on the following webpages:
- Input and output for the calculus Lneed can be found on this webpage.
- Input and output for the calculus Lneed+seq can be found on this webpage.
- Input and output for the calculus LR can be found on this webpage.
Dr. David Sabel
Computer Science Institute
Computer Science and Mathematics Department
Johann Wolfgang Goethe-University Frankfurt am Main