3
$\begingroup$

Leroy uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step semantics such that initial states are related, and the relation is preserved under a single step in the first semantics by a finite sequence of steps (or sometimes none) in the second. This can be augmented with notions of trace inclusion, and then determinism proofs allow trace equivalence to be shown from the existence of a simulation.

Chlipala covers this in his text (which is where I first learned about it), but there are no citations, and I'm not sure whether the method is due to Leroy or if it has earlier origins.

Improve this question
$\endgroup$
5
  • 4
    $\begingroup$ I have not had time to check in detail, but at a guess: this comes from Robin Milner, in particular his [17]. Milner has numerous publication that study various notions of equivalence. $\endgroup$ – Martin Berger Jul 27 '20 at 11:49
  • 2
    $\begingroup$ @MartinBerger Thanks! (Can't upvote comments since this is a fresh account.) I found "An algebraic notion of simulation between programs" (1971) which applies simulation to programs within the same semantics which seems to be the earliest notion of this. $\endgroup$ – denotational Jul 27 '20 at 12:53
  • 1
    $\begingroup$ @p0llard Milner's notion of simulation is quite natural, and I imagine (but don't know) that several other authors independently stumbled on it, maybe without naming it. E.g. Milner's coinductive notion of bisimulation turns out also to have been invented independently multiple times: in philosophical logic (more precisely modal logic), in set theory (more precisely in the study of non-well-founded sets) and in model theory (Ehrenfeucht-Fraïsse games). See On the Origins of Bisimulation and Coinduction. $\endgroup$ – Martin Berger Jul 27 '20 at 13:27
  • 1
    $\begingroup$ My memory may be playing tricks on me again but I do seem to remember that Milner's (typically bi-) simulations are unnecessarily strong for ordinary compiler correctness. This changes only when compilers are expected to preserve non-trace properties such as non-interference. A decent reference on the classical compiler correctness literature should be in Müller-Olm's thesis (LNCS 1283). As an aside, Leroy unfortunately confuses the rest of the world by swapping names of his simulations compared to just about every precursor. $\endgroup$ – Kai Jul 29 '20 at 10:47
  • $\begingroup$ @Kai > "Müller-Olm's thesis (LNCS 1283)" Wow, this is a great resource, thanks for pointing it out to me! $\endgroup$ – denotational Jul 29 '20 at 12:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.