Programs and Outputs for Contextual Equivalence in a Probablistic Call-by-Need Lambda Calculus

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 probablistic call-by-need lambda calculus with recursive let

Calculus description as input for the LRSX tool

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

Forking Diagrams

Input

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

Output

• 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

Commuting Diagrams

Input

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

Output

• 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

TRSs for diagrams and termination proofs

(cp)

• 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

(cpx)

• 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

(lll)

• 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

(ucp) and (gc)

• 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 probablistic call-by-need lambda calculus with recursive let extended by case, constructors and seq

Calculus description as input for the LRSX tool

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.

Forking Diagrams

Input

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

Output

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!)

Commuting Diagrams

Input

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]

Output

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!)

Induction and adapted Diagrams

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

Transformation cpcx

• 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

Transformation cp

• 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

Transformation cpx

• 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

Transformation lll

• 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

Transformation ug [ucp and gc]

• 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

Transformation xch

• 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