|
|
- Automated Proving Correctness of Transformations for the Program Calculus Lneed
-
The calculus Lneed is a minimalistic call-by-need lambda calculus with letrec.
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
-
David Sabel
|