Example Lneed+seq


Automated Proving Correctness of Transformations for the Program Calculus Lneed+seq
The calculus Lneed+seq is a minimalistic call-by-need lambda calculus with letrec and seq. The calculus and program transformations are modeled in the LRSX Tool by the following input files:

  • Description of the calculus (standard reductions and meta transformations): LNEED.inp
  • Overlap commands to compute answer and forking diagrams: lneed_fork.inp
  • Overlap commands to compute answer and commuting diagrams (i.e. forking diagrams for the reversed transformations): lneed_commute.inp

Some exemplary calls of the LRSX Tool are:

  • compute forking and answer diagrams and write them into file output with full proofs:

    lrsx join proofs bound=12 lneed_fork.inp > output_proofs

  • compute forking and answer diagrams and write them into file output in long format:

    lrsx join proofs bound=12 lneed_fork.inp > output.long

  • convert diagrams from long into short format, where the input is in file output.long and the output is written into output_short:

    lrsx convert long short output.long > output_short

  • compute commuting and answer diagrams and write them into file output in long format:

    lrsx join proofs bound=12 lneed_commute.inp > output.long

  • convert the commuting diagrams in file output.long into a TRS:

    lrsx convert long trs output.long > output_trs

  • perform the induction on diagrams in input.long where atppath contains AProVE and CeTA, the TRSs are written to outpath, termination proofs are written to proofs:

    lrsx induct atp-path=atppath output-to=outpath input.long > proofs
Output of the LRSX Tool
Contact
Dr. David Sabel
Computer Science Institute
Computer Science and Mathematics Department
Johann Wolfgang Goethe-University Frankfurt am Main
(c) 2016 PD Dr. David Sabel, Imprint, Last modified: $Author: sabel $, $Date: 2017/06/23 14:26:35 $