Related, I am more familiar with application of step-indexed logical relations to compiler verification for compositional compiler correctness/multi-language systems. You mention that you prefer to use them here rather than e.g. forward simulation - what motivates this preference?
I want to compare using logical relations for program equivalence with (bi)simulations. To understand (bi)simulations better, I found several definitions.
(bi)-simulations in the context of LTS's (labeled transition systems) in 1-5, in the case of $\lambda$-calculus, small-step operational semantics
applicative bisimulations as in 6-7, which seem to be a form of logical relations. In the case of
In plutus-cert, we use big-step semantics. Bisimulation in the sense of 1. and 2. only consider labeled transition systems (or reduction systems in PLFA). Perhaps logical relations are more suitable for big-step?
Hrutvik writes:
I want to compare using logical relations for program equivalence with (bi)simulations. To understand (bi)simulations better, I found several definitions.
1. PLFA - Bisimulations (Wadler): the relation is preserved over evaluation.
one step to multi-step
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/5d6b697b-75ee-4fc8-9969-8a0cf242472c)2. Wikipedia - Simulation
lock-step
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/9f7d8fe3-d7ab-4e0f-a2be-bdd8730f8817)3. Automata and process theory (eindhoven lecture notes)
lock-step, possibly between different labeled-transition-systems one step to multi-step
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/7ff1aa83-d70b-43cf-a52a-02b74d25d53a) ![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/4c75bd83-07f0-44fd-8a42-523c0132676c)4. Lecture Notes Types and Programming Languages (Pfenning)
defines weak and strong bisimulation
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/27900fe9-1d16-4b84-ab6b-6703fc84be32)5. [Modelling Computing Systems (Moller & Struth), chapter 12]
lock-step
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/5d6b697b-75ee-4fc8-9969-8a0cf242472c)6. The lazy lambda calculus p.5 (Abramsky)
(applicative bisimulation): Very much like a logical relation, except that functions are applied to equal arguments
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/c5738c1a-7855-4fe7-bbe7-5ca19ef7050a)7. Purecake
uses the same notion as in [6]
Definition
![image](https://github.com/jaccokrijnen/plutus-cert/assets/4022046/5177502f-c87f-49e4-a6a2-e3648ae77a63)There seems to be a distinction between
In plutus-cert, we use big-step semantics. Bisimulation in the sense of 1. and 2. only consider labeled transition systems (or reduction systems in PLFA). Perhaps logical relations are more suitable for big-step?