The LRSX Tool

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.

• The source-distribution is available here: lrsx-0.6.0.0.tar.gz
• 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.0.0.tar.gz
cd lrsx-0.6.0.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 help-text of the LRSX Tool.
• The executable lrsx can be installed via typing cabal install If this completes successfully you will have the lrsx-binary in ~/.cabal/bin.

Using LSRX

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 examples.
Two worked-out 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 LR can be found on this webpage.