pouya/coalgebraic-simulation
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

list

Browse Source
This commit is contained in:
partowp
2026-07-31 15:57:22 +01:00
parent e4ac0c6797
commit 3090215662
1 changed files with 7 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
list
+7
View File
@@ -0,0 +1,7 @@
Introduce HJ-simulation in relator-form, show uniqness of wittnesses.
Prove a general theorem that symmetric simulation for symmetrized relator yields similarity that is sound and complete for behavioral equivalence (use "Relators and Notions of Simulation Revisited" soundness and compteleness criterion).
Elaborate this for powerset
When is symmetrized relator the Barr relator (definition is in "Relators and Notions of Simulation Revisited")?
At least, try to prove it for the Jacobs-Hughes relator
Introduce notions of simulation, diverging from HJ-simulation. Do we need two of them (with normalization and without)? How are all of them related?
Can we separate Hughes-Jacobs relator from one-sided lax relator?