May 20, 2022

This website links to the source code, inputs and outputs for the automated diagram generation and automated induction for our paper â€˜Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculusâ€™.

The source code of the LRSX tool is in this Git-Repository. It computes overlaps and forking and commuting diagrams for program calculi. For automated induction on the diagrams external tools are required like AProVE, CeTA, TTT2.

- The examples, computations, and outputs are generated for two program calculi:
- a probablistic call-by-need lambda calculus with recursive let
- an extension of the calculus by case-expressions, data constructors and a seq-operator

The description of the syntax, the standard reduction, and of a set of program transformations as input for the LRSX tool are in file LNEED.inp

The overlap-computation for the forking diagrams is controlled by file lneed_fork.inp.

- The overlaps are in: lneed_fork.overlaps
- The overlaps with joins (=diagrams) including the poofs are in: lneed_fork.inp.proofs
- The forking diagrams are long version without unions: lneed_fork.long
- The forking diagrams in short version without unions: lneed_fork.short

- The overlap-computation for the commuting diagrams is controlled by lneed_commute.inp.

- The overlaps are in: lneed_commute.overlaps
- The overlaps with joins (=diagrams) including the poofs are in: lneed_commute.inp.proofs
- The commuting diagrams are long version without unions: lneed_commute.long
- The commuting diagrams in short version without unions: lneed_commute.short

- TRS for cp (commuting) cp-comm.trs
- Termination proof (using TTT2): cp-comm.TTT2.out.txt
- Termination proof (using TTT): cp-comm.TTT.html
- TRS for cp (forking) cp-fork.trs
- Termination proof (using TTT2): cp-fork.TTT2.out.txt
- Termination proof (using TTT): cp-fork.TTT.html

- TRS for cpx (commuting) cpx-comm.trs
- Termination proof (using TTT2) cpx-comm.TTT2.out.txt
- TRS for cpx (forking) cpx-fork.trs
- Termination proof (using TTT2) cpx-fork.TTT2.out.txt

- TRS for lll (commuting) lll-comm.trs
- Termination proof (using TTT2) lll-comm.TTT2.cpf
- Termination proof (using TTT) lll-comm.TTT.html
- TRS for lll (forking) lll-fork.trs
- Termination proof (using TTT2) lll-fork.TTT2.cpf
- Termination proof (using TTT) lll-fork.TTT.html

- TRS for ucp and gc (commuting) ucp-comm.trs
- Termination proof (using AProVE) ucp-comm.trs.proof.html
- TRS for ucp and gc (forking) ucp-fork.trs
- Termination proof (using AProVE) ucp-fork.trs.proof.html

The description of the standard reduction reduction rules is in file LR-StandardReductions.inp, weak head normal forms are defined in file LR-Answers.inp, contexts are defined in file LR-Contexts.inp, and of a set of program transformations as input for the LRSX tool are in LR-Transformations.inp. Unions of transformations are define in files LR-Unions.inp and LR-MoreUnions.inp.

The overlap-computation for the forking diagrams is controlled by this file.

The overlaps are in: LR-FORK.overlaps.gz The overlaps with joins (=diagrams) including the poofs are in: LR-FORK.inp.proofs.gz The forking diagrams are long version without unions: LR-FORK.long.gz The forking diagrams in short version without unions: LR-FORK.short

(Note that some files are compressed due to their size!)

The overlap-computation for the commuting diagrams is controlled by this file which imports several other files [LR-COMMUTE.abs.gc.ucp.inp,LR-COMMUTE.cpcx-e.inp,LR-COMMUTE.cpcx-in.inp,LR-COMMUTE.gc.ucp.inp ,LR-COMMUTE.lbeta.cp.lll.inp,LR-COMMUTE.seq.case.xch.cpx.inp]

The overlaps are in: LR-COMMUTE.overlaps.gz The overlaps with joins (=diagrams) including the poofs are in: LR-COMMUTE.inp.proofs.gz The commuting diagrams are long version without unions: LR-COMMUTE.long.gz The commuting diagrams in short version without unions: LR-COMMUTE.short

(Note that some files are compressed due to their size!)

The following files show the diagrams (which were adapted by hand and compressed) and the corresponding proofs of termination.

- Commuting diagrams: LR-COMMUTE.cpcx.ed.short
- TRS for commuting diagrams: LR-COMMUTE.cpcx.ed.short.out.cpcx.trs
- Termination proof: LR-COMMUTE.cpcx.ed.short.out.cpcx.trs.proof.html
- Forking diagrams: LR-FORK.cpcx.ed.short
- TRS for forking diagrams: LR-FORK.cpcx.ed.short.out.cpcx.trs
- Termination proof: LR-FORK.cpcx.ed.cpcx.short.out.trs.proof.html

- Commuting diagrams: LR-COMMUTE.cp.ed.short
- TRS for commuting diagrams: LR-COMMUTE.cp.ed.short.out.cp.trs
- Termination proof: LR-COMMUTE.cp.ed.short.out.cpd.trs.proof.html
- Forking diagrams: LR-FORK.cp.ed.short
- TRS for forking diagrams: LR-COMMUTE.cp.ed.short.out.cp.trs
- Termination proof: LR-FORK.cp.ed.short.out.cpd.trs.proof.html

- Commuting diagrams: LR-COMMUTE.cpx.ed.short
- TRS for commuting diagrams: LR-COMMUTE.cpx.ed.short.out.cpx.trs
- Termination proof: LR-COMMUTE.cpx.ed.short.out.cpx.trs.proof.html
- Forking diagrams: LR-FORK.cpx.ed.short
- TRS for forking diagrams: LR-FORK.cpx.ed.short.out.cpx.trs
- Termination proof: LR-FORK.cpx.ed.short.out.cpx.trs.proof.html

- Commuting diagrams: LR-COMMUTE.lll.ed.short
- TRS for commuting diagrams: LR-COMMUTE.lll.ed.short.out.llet.trs
- Termination proof: LR-COMMUTE.lll.ed.short.out.llet.trs.proof.html
- Forking diagrams: LR-FORK.lll.ed.short
- TRS for forking diagrams: LR-FORK.lll.ed.short.out.llet.trs
- Termination proof: LR-FORK.lll.ed.short.out.llet.trs.proof.html

- Commuting diagrams: LR-COMMUTE.ug.ed.short
- TRS for commuting diagrams: LR-COMMUTE.ug.ed.short.out.ucp.trs
- Termination proof: LR-COMMUTE.ug.ed.short.out.ucp.trs.proof.html
- Forking diagrams: LR-FORK.ug.ed.short
- TRS for forking diagrams: LR-FORK.ug.ed.short.out.ucp.trs
- Termination proof: LR-FORK.ug.ed.short.out.ucp.trs.proof.html

- Commuting diagrams: LR-COMMUTE.xch.ed.short
- TRS for commuting diagrams: LR-COMMUTE.xch.ed.short.out.xch.trs
- Termination proof: LR-COMMUTE.xch.ed.short.out.xch.trs.proof.html
- Forking diagrams: LR-FORK.xch.ed.short
- TRS for forking diagrams: LR-FORK.xch.ed.short.out.xch.trs
- Termination proof: LR-FORK.xch.ed.short.out.xch.trs.proof.html