<p>I have an answer to this question which is possibly novel.  In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet.</p>

<p>The general thesis is that relational reasoning principles like "logical relations", "simulations", and even "invariants" are manifestations of data abstraction or information hiding.  Wherever there is information hiding, these principles crop up.</p>

<p>The first people to discover it were automata theorists.  Automata have hidden state.  So you need relational reasoning to talk about their equivalence.  Automata theorists struggled with homomorphisms for a while, gave up, and came up with a notion called "relational covering", which is a form of simulation relations.</p>

<p>Milner picked up the idea in a little-known but very fundamental paper called "<a href="http://ijcai.org/Past%20Proceedings/IJCAI-1971/PDF/044.pdf">An algebraic notion of simulation between programs</a>" in 1971.  Hoare knew it and used it in coming up with "<a href="http://dx.doi.org/10.1007/BF00289507">Proof of correctness of data representations</a>" in 1972 (but used abstraction functions instead of relations because he thought they were "simpler").  He later retracted the simplicity claim and went back to using relations in "<a href="http://dx.doi.org/10.1007/3-540-16442-1_14">Data refinement refined</a>".  Reynolds used relational reasoning in "<a href="http://repository.cmu.edu/compsci/1280/">Craft of Programming</a>", Chapter 5 (1981).  He thought relations were more natural and general than abstraction functions.  If you go back and read this chapter, you will find relational parametricity ideas lurking around, waiting to be discovered.  Sure enough, two years later, Reynolds published "Types, abstraction and parametric polymorphism" (1983).</p>

<p>It looks like all these ideas have nothing to do with types, but they really do.  Stateful languages and models have <i>built-in</i> data abstraction.  You don't need to define an "abstract data type" to get information hiding.  You just declare a local variable and hide it.  We can teach it to first year students in Java classes in the first few weeks.  No sweat.</p>

<p>Functional languages and models, on the other hand, have to get their information hiding via <em>types</em>.  Functional models don't have built-in data abstraction.  We have to add it on explicitly, using $\forall$ or $\exists$.  So, if you translate a stateful language into a functional language, you will notice all the local state getting translated into type variables.  For an explicit description of how this works, see my paper "<a href="http://www.cs.bham.ac.uk/~udr/papers/objects-and-classes.pdf">Objects and classes in Algol-like languages</a>", but the ideas really come from Reynolds 1981 ("The Essence of Algol"). We are just understanding those classic ideas better now.</p>

<p>Take two machines $M$ and $M'$ that you want to prove equivalent.  Milner 1971 says, define a relation between the states of $M$ and $M'$ and show that the two machines preserve the relation.  Reynolds parametricity says, think of the states of the machines as belonging to types $X$ and $X'$.  Define a relation $R$ between them.  If the machines are of type $F(X)$ and $F(X')$, parameterized by the types of their states, then check that the two machines are related by the relation $F(R)$.  </p>

<p>So, <em>simulations and relational parametricity are essentially the same idea</em>.  It is not merely a superficial resemblance.  The former is made for stateful languages where there is built-in data abstraction.  The latter is made for stateless languages where data abstraction is obtained via type variables.  </p>

<p>What about logical relations then?  On the surface, logical relations appear to be a more general idea.  Whereas parametricity talks about how to relate type variables within the same model, logical relations appear to relate types across different models.  (Dave Clarke wrote a brilliant exposition of this earlier.)  But my feeling is (and it still needs to be demonstrated) that this is an instance of some form of higher-type parametricity which hasn't yet been formulated.  Stay tuned for more progress on that front.</p>

<hr>

<p>[Note added] The connection between logical relations and simulations is discussed in our recent paper <a href="http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf">Logical relations and parametricty: A Reynolds programme for Category Theory and Programming Languages</a>.</p>

CC BY-SA 3.0
2013-07-22T14:20:12.013Z
I was wondering whether it would be true to say that the relation $F(R)$ mentioned above is the so-called relation lifting of $R$ given `functor` $F$ describing the machine.
Dave Clarke
CC BY-SA 3.0
2013-07-22T14:49:27.450Z
@DaveClarke Yes, it is the same idea.  In the Reynolds style of definition, each type constructor $F$ comes equipped with a *relation action* that associates, to each relation $R : X \leftrightarrow X'$, a corresponding relation $F(R): F(X) \leftrightarrow F(X')$ satisfying some axioms.  In some other communities, they would like to derive $F(R)$ from other principles, whence they call them *relation liftings*.  The $F(R)$ they produce by this process would be a relation action in the Reynolds sense.
Uday Reddy
CC BY-SA 3.0
2012-02-27T22:55:02.717Z
2014-01-19T02:41:29.957Z
2014-01-19T02:41:29.957Z
Uday Reddy
<p>One of the key differences is that logical relations are used as a technique for showing that a class of programs (eg, input to a compiler) correspond to another class of programs (eg, the output of the compiler), whereas simulation relations are used to show the correspondence between two programs.</p>

<p>The similarity between the two notions is that they both define a relation used to show the correspondence between two different entities. In some sense, one can think of a logical relation as a simulation relation that is defined inductively on the syntax of types. But different kinds of simulation relations exist.</p>

<p>Logical relations can used to show the correspondence between a language such as ML and its translation into assembly language, as in the paper you read. A logical relation is defined inductively on the type structure. A logical relation provides a compositional means for showing, for example, that a translation is correct, by showing that the translation is correct for each type constructor. At function types the correctness condition condition would say something like, the translation of this function takes well-translated input to well-translated output.</p>

<p>Logical relations are a versatile technique for languages based on the lambda calculus.
Other applications of logical relations include (from <a href="http://homepages.inf.ed.ac.uk/gdp/publications/laxlr.pdf">here</a>): characterising lambda definability, relating denotational semantic definitions, characterising parametric polymorphism, modelling abstract interpretation, verifying data representations, defining fully abstract semantics and modelling local state in higher-order languages.</p>

<p>Simulation relations are generally used to show the equivalence of two programs. Typically such programs produce some kind of observation, such as sending messages on channels. One program P simulates another Q if P can do everything that Q can do, though perhaps more.</p>

<p>Bisimulation, roughly, is two simulation relations put together. You show that program P and simulate program Q and that program Q can simulate program P and you have a bisimulation, though additional conditions are generally present. Wikipedia's entry on <a href="http://en.wikipedia.org/wiki/Bisimulation">bisimulation</a> is a good (more precise) starting point. Thousands of variants of the idea exist, but it is a fundamental idea that has been reinvented in more or less the same form computer science, modal logic and model theory. Sangiorgi's <a href="http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf">article</a> gives a wonderful history of the idea.</p>

<p>One paper establishing a relationship between the two notions is <a href="http://www.cl.cam.ac.uk/~amp12/papers/notlrb/notlrb.pdf">A Note on Logical Relations Between Semantics and Syntax</a> by Andy Pitts which uses logical relations, ultimately a semantic notion defined syntactally, to prove a certain property about <em>applicative bisimulation</em>, which is a purely syntactic notion.</p>

CC BY-SA 3.0
2011-04-27T19:52:19.010Z
are you sure about the statement "You show that program P and simulate program Q and that program Q can simulate program P and you have a bisimulation."?  Let A=(a.(b+c)) + (a.b+a.c) and B=a.b+a.c when as far as I can tell A is similar to B, B is similar to A, but A and B are not bisimilar.
András Salamon
CC BY-SA 3.0
2011-04-27T20:26:50.930Z
@András: You are right. My statement is not precise enough. The difference is abstracted away by the phrase "Some additional conditions may be present".
Dave Clarke
CC BY-SA 3.0
2011-04-28T04:58:40.990Z
Hennessy and Milner defined three kinds of equivalence relations in [their original paper for bisimulation](http://portal.acm.org/citation.cfm?id=2455.2460) and gave some examples to illustrate their differences. Your original statement is actually the medium one in their paper, which is weaker than bisimulation and stronger than trace equivalence. I'm not sure which equivalence is better. Maybe it depends on practical use.
Hongjin Liang
CC BY-SA 2.5
2011-03-13T02:09:34.703Z
Thanks a lot for your detailed explanation! I will read your references and try to figure out deep connections/differences between the two.
Hongjin Liang
CC BY-SA 3.0
2012-03-04T22:47:44.577Z
Simulation is also used as a proof technique to establish data refinement between two data types. Every single one of those simulation proofs relates whole classes of programs. See e.g.[1] for details. This suggests that the distinction between the two concepts is even blurrier.  

[1]: CAR Hoare, He J, and JW Sanders. Prespecification in data refinement. *Information Processing Letters*, 25:71-76, 1987.
Kai
CC BY-SA 3.0
2011-03-12T15:02:00.887Z
2011-04-27T20:34:53.823Z
2011-04-27T20:34:53.823Z
Dave Clarke
<p>The two types of relations appear to be used in different contexts. Logical simulations for typed languages and simulation relations when dealing with process calculi or modal logics interpreted over transition systems. Dave Clarke has provided much intuitive explanation, so I will just add a few pointers that may help. </p>

<p>There has been work on characterising both notions using abstract interpretation. It may not be what you want, but at least both notions are treated in the same mathematical framework.</p>

<p>Samson Abramsky used logical relations to prove soundness and termination of strictness analysis for the lazy Lambda calculus (<a href="http://logcom.oxfordjournals.org/content/1/1/5.abstract" title="Abstract Interpretation, Logical Relations, and Kan Extensions">Abstract Interpretation, Logical Relations, and Kan Extensions</a>). He also showed that the logical relations define abstraction functions in the Galois connection sense of abstract interpretation. More recently, Backhouse and Backhouse showed how to construct Galois connections for higher-order types from Galois connections for base types and that these constructions can be equivalently described using logical relations (<a href="http://www.springerlink.com/content/kpv52g3k48n8tpgc/">Logical Relations and Galois Connections</a>). Thus, in the specific context of typed functional languages, the two notions are equivalent. </p>

<p>Simulation relations characterise property preservation between Kripke structures for various modal and temporal logics. Instead of types, we have modalities in a logic. Simulation relations also define Galois connections and hence, abstractions. One can ask if these abstractions have special properties.  The answer is that standard abstractions are sound and simulation relation-based abstractions are complete. The notion of completeness is with respect to Galois connections, which may not concur with ones intuitive interpretation. This line of work has been developed by David Schmidt (<a href="http://www.springerlink.com/content/h51ncq7vuvflfx70/">Structure-Preserving Binary Relations for Program Abstraction</a>), and Francesco Ranzato and Francesco Tapparo (<a href="http://arxiv.org/abs/cs/0401016">Generalized Strong Preservation by Abstract Interpretation</a>). </p>

CC BY-SA 2.5
2011-03-13T02:19:48.907Z
Your answer is very helpful that connecting the concepts with abstract interpretation. Thank you!
Hongjin Liang
CC BY-SA 3.0
2015-03-11T10:49:26.580Z
A sincere question: I'm no expert, but doesn't Reynolds (1983, "Types, abstraction and parametric polymorphism") already define logical relations that are Galois connections (Sec. 6)? The only differences I notice: he doesn't say the term "Galois connection" but only the equivalent "adjoint functors between partial orders regarded as categories", and he restricts to domains. OTOH, Backhouse and Backhouse cite Reynolds but don't discuss this claim, one way or the other.
Blaisorblade
CC BY-SA 2.5
2011-03-13T00:10:11.570Z
2011-03-13T00:10:11.570Z
Vijay D
<p>I'd say that the two concepts are somewhat vague. Both are about binary relations of computational mechanisms which somehow embody a notion of equality. Logical relations are defined by induction of type-structure, while simulations can be defined however you want, but the term alludes to coinduction.</p>

<p>It is misleading to say that logical relations are restrictied to lambda-calculi or sequential languages, although that's where logical relations originated. For example in our <a href="http://www.informatics.sussex.ac.uk/users/mfb21/publications/fossacs03/index.html">work on fully abstract models for System F</a>, we defined logical relations for typed $\pi$-calculi.</p>

CC BY-SA 3.0
2011-04-28T05:27:02.817Z
Your reference is really nice! I haven't heard logical relations for concurrent programs before. Thank you! 
I guess the difficulty of defining a logical relation is in finding the type structure. With the same type structure, a logical relation can be defined between different programming languages. On the other hand, a simulation requires modelling programs by a state transition system, which might be uneasy if the programs are written for different state models.
Hongjin Liang
CC BY-SA 3.0
2011-04-28T08:11:15.940Z
Hello! Yes, finding an appropriate type-structure might not always be easy.

You can define simulations using different transition systems for the two calculi you want to compare.  One could argue that the definition of weak simulation does just that. All you really need to define simulations is a relation for comparing transition labels.
Martin Berger
CC BY-SA 3.0
2011-04-27T07:48:49.683Z
2011-04-27T07:48:49.683Z
Martin Berger
<p>I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused about these two techniques.</p>

<p>I only know logical relations are inductively defined while simulations are based on coinduction. Why are they defined in such ways? What are their pros and cons respectively? Which one should I choose in different situations? </p>

CC BY-SA 2.5
2011-03-12T02:31:29.450Z
You might want to provide links to these papers you've read.  This would make it clearer which specific examples are confusing you.
Marc Hamann
CC BY-SA 2.5
2011-03-12T04:52:31.717Z
For logical relations, I've read Hur and Dreyer's recent paper "A Kripke logical relation between ML and assembly"(POPL'11). Also I've read the classical chapters in Pierce's book "Advanced Topics in Types and Programming Languages". I find logical relations are defined inductively on the type structure of the language, but what if the language does not have a type structure (such as C)? (It seems another question, I guess.)
Hongjin Liang
CC BY-SA 2.5
2011-03-12T04:54:08.487Z
For simulations, I've read the original paper "Algebraic laws for nondeterminism and concurrency" by Hennessy and Milner. Koutavas and Wand's "Small bisimulations for reasoning about higher-order imperative programs"(POPL'06) is incomprehensible to me and I'm not sure why they called their method "bisimulation".
Hongjin Liang
CC BY-SA 2.5
2011-03-12T04:55:08.517Z
I'd admit that I haven't well understood these papers. I'm wondering that if both these two techniques are powerful, can they replace each other anytime? Or does each one have its own optimal applications?
Hongjin Liang
CC BY-SA 2.5
2011-03-13T12:32:21.497Z
it would be better if you include the information you have provided in the comments in the post. You can edit your question by clicking on the edit link under the question.
Kaveh
CC BY-SA 3.0
2014-03-24T18:10:39.293Z
@HongjinLiang: If you don't have a type structure (or if you have recursive types), you can use step-indexed logical relations - with logical relations you use induction on types, with step-indexing you do induction on observation steps.
You'll find pointers in Amal Ahmed's research statement:
http://www.ccs.neu.edu/home/amal/ahmed-research.pdf.
(Another overview on research on logical relations is [this talk](http://www.mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf) from Derek Dreyer and in his research statement: http://www.mpi-sws.org/~dreyer/research.pdf).
Blaisorblade
CC BY-SA 4.0
2020-05-13T05:17:04.597Z
A relatively new relevant paper: [Bisimulation As A Logical Relation](https://arxiv.org/pdf/2003.13542.pdf)
Łukasz Lew
<lo.logic><pl.programming-languages><logical-relations><parametricity>
What are the differences between logical relations and simulations?
Hongjin Liang
# What are the differences between logical relations and simulations?

(Asked by: username_0 on 2011-03-11)

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused about these two techniques.

I only know logical relations are inductively defined while simulations are based on coinduction. Why are they defined in such ways? What are their pros and cons respectively? Which one should I choose in different situations?

**Tags:** lo.logic, pl.programming-languages, logical-relations, parametricity

> **Comments:**
> **username_1**: You might want to provide links to these papers you've read.  This would make it clearer which specific examples are confusing you.  
> **username_0**: For logical relations, I've read Hur and Dreyer's recent paper "A Kripke logical relation between ML and assembly"(POPL'11). Also I've read the classical chapters in Pierce's book "Advanced Topics in Types and Programming Languages". I find logical relations are defined inductively on the type structure of the language, but what if the language does not have a type structure (such as C)? (It seems another question, I guess.)  
> **username_0**: For simulations, I've read the original paper "Algebraic laws for nondeterminism and concurrency" by Hennessy and Milner. Koutavas and Wand's "Small bisimulations for reasoning about higher-order imperative programs"(POPL'06) is incomprehensible to me and I'm not sure why they called their method "bisimulation".  
> **username_0**: I'd admit that I haven't well understood these papers. I'm wondering that if both these two techniques are powerful, can they replace each other anytime? Or does each one have its own optimal applications?  
> **username_2**: it would be better if you include the information you have provided in the comments in the post. You can edit your question by clicking on the edit link under the question.  
> **username_3**: @HongjinLiang: If you don't have a type structure (or if you have recursive types), you can use step-indexed logical relations - with logical relations you use induction on types, with step-indexing you do induction on observation steps. You'll find pointers in Amal Ahmed's research statement: http://www.ccs.neu.edu/home/amal/ahmed-research.pdf. (Another overview on research on logical relations is [this talk](http://www.mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf) from Derek Dreyer and in his research statement: http://www.mpi-sws.org/~dreyer/research.pdf).  
> **username_4**: A relatively new relevant paper: [Bisimulation As A Logical Relation](https://arxiv.org/pdf/2003.13542.pdf)  

---

## 4 answers

### Answer by username_5 on 2012-02-27. Score: 24

I have an answer to this question which is possibly novel. In fact, I am still thinking through it for the last 6 months or so, and it hasn't been written about in papers yet.

The general thesis is that relational reasoning principles like "logical relations", "simulations", and even "invariants" are manifestations of data abstraction or information hiding. Wherever there is information hiding, these principles crop up.

The first people to discover it were automata theorists. Automata have hidden state. So you need relational reasoning to talk about their equivalence. Automata theorists struggled with homomorphisms for a while, gave up, and came up with a notion called "relational covering", which is a form of simulation relations.

Milner picked up the idea in a little-known but very fundamental paper called "[An algebraic notion of simulation between programs](http://ijcai.org/Past%20Proceedings/IJCAI-1971/PDF/044.pdf)" in 1971. Hoare knew it and used it in coming up with "[Proof of correctness of data representations](http://dx.doi.org/10.1007/BF00289507)" in 1972 (but used abstraction functions instead of relations because he thought they were "simpler"). He later retracted the simplicity claim and went back to using relations in "[Data refinement refined](http://dx.doi.org/10.1007/3-540-16442-1_14)". Reynolds used relational reasoning in "[Craft of Programming](http://repository.cmu.edu/compsci/1280/)", Chapter 5 (1981). He thought relations were more natural and general than abstraction functions. If you go back and read this chapter, you will find relational parametricity ideas lurking around, waiting to be discovered. Sure enough, two years later, Reynolds published "Types, abstraction and parametric polymorphism" (1983).

It looks like all these ideas have nothing to do with types, but they really do. Stateful languages and models have *built-in* data abstraction. You don't need to define an "abstract data type" to get information hiding. You just declare a local variable and hide it. We can teach it to first year students in Java classes in the first few weeks. No sweat.

Functional languages and models, on the other hand, have to get their information hiding via *types*. Functional models don't have built-in data abstraction. We have to add it on explicitly, using $\forall$ or $\exists$. So, if you translate a stateful language into a functional language, you will notice all the local state getting translated into type variables. For an explicit description of how this works, see my paper "[Objects and classes in Algol-like languages](http://www.cs.bham.ac.uk/~udr/papers/objects-and-classes.pdf)", but the ideas really come from Reynolds 1981 ("The Essence of Algol"). We are just understanding those classic ideas better now.

Take two machines $M$ and $M'$ that you want to prove equivalent. Milner 1971 says, define a relation between the states of $M$ and $M'$ and show that the two machines preserve the relation. Reynolds parametricity says, think of the states of the machines as belonging to types $X$ and $X'$. Define a relation $R$ between them. If the machines are of type $F(X)$ and $F(X')$, parameterized by the types of their states, then check that the two machines are related by the relation $F(R)$.

So, *simulations and relational parametricity are essentially the same idea*. It is not merely a superficial resemblance. The former is made for stateful languages where there is built-in data abstraction. The latter is made for stateless languages where data abstraction is obtained via type variables.

What about logical relations then? On the surface, logical relations appear to be a more general idea. Whereas parametricity talks about how to relate type variables within the same model, logical relations appear to relate types across different models. (username_6 wrote a brilliant exposition of this earlier.) But my feeling is (and it still needs to be demonstrated) that this is an instance of some form of higher-type parametricity which hasn't yet been formulated. Stay tuned for more progress on that front.

---

[Note added] The connection between logical relations and simulations is discussed in our recent paper [Logical relations and parametricty: A Reynolds programme for Category Theory and Programming Languages](http://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf).

> **Comments:**
> **username_6**: I was wondering whether it would be true to say that the relation $F(R)$ mentioned above is the so-called relation lifting of $R$ given `functor` $F$ describing the machine.  
> **username_5**: @DaveClarke Yes, it is the same idea.  In the Reynolds style of definition, each type constructor $F$ comes equipped with a *relation action* that associates, to each relation $R : X \leftrightarrow X'$, a corresponding relation $F(R): F(X) \leftrightarrow F(X')$ satisfying some axioms.  In some other communities, they would like to derive $F(R)$ from other principles, whence they call them *relation liftings*.  The $F(R)$ they produce by this process would be a relation action in the Reynolds sense.  

---

### Answer by username_6 on 2011-03-12. Score: 16

One of the key differences is that logical relations are used as a technique for showing that a class of programs (eg, input to a compiler) correspond to another class of programs (eg, the output of the compiler), whereas simulation relations are used to show the correspondence between two programs.

The similarity between the two notions is that they both define a relation used to show the correspondence between two different entities. In some sense, one can think of a logical relation as a simulation relation that is defined inductively on the syntax of types. But different kinds of simulation relations exist.

Logical relations can used to show the correspondence between a language such as ML and its translation into assembly language, as in the paper you read. A logical relation is defined inductively on the type structure. A logical relation provides a compositional means for showing, for example, that a translation is correct, by showing that the translation is correct for each type constructor. At function types the correctness condition condition would say something like, the translation of this function takes well-translated input to well-translated output.

Logical relations are a versatile technique for languages based on the lambda calculus.
Other applications of logical relations include (from [here](http://homepages.inf.ed.ac.uk/gdp/publications/laxlr.pdf)): characterising lambda definability, relating denotational semantic definitions, characterising parametric polymorphism, modelling abstract interpretation, verifying data representations, defining fully abstract semantics and modelling local state in higher-order languages.

Simulation relations are generally used to show the equivalence of two programs. Typically such programs produce some kind of observation, such as sending messages on channels. One program P simulates another Q if P can do everything that Q can do, though perhaps more.

Bisimulation, roughly, is two simulation relations put together. You show that program P and simulate program Q and that program Q can simulate program P and you have a bisimulation, though additional conditions are generally present. Wikipedia's entry on [bisimulation](http://en.wikipedia.org/wiki/Bisimulation) is a good (more precise) starting point. Thousands of variants of the idea exist, but it is a fundamental idea that has been reinvented in more or less the same form computer science, modal logic and model theory. Sangiorgi's [article](http://www.cs.unibo.it/~sangio/DOC_public/history_bis_coind.pdf) gives a wonderful history of the idea.

One paper establishing a relationship between the two notions is [A Note on Logical Relations Between Semantics and Syntax](http://www.cl.cam.ac.uk/~amp12/papers/notlrb/notlrb.pdf) by Andy Pitts which uses logical relations, ultimately a semantic notion defined syntactally, to prove a certain property about *applicative bisimulation*, which is a purely syntactic notion.

> **Comments:**
> **username_0**: Thanks a lot for your detailed explanation! I will read your references and try to figure out deep connections/differences between the two.  
> **username_7**: are you sure about the statement "You show that program P and simulate program Q and that program Q can simulate program P and you have a bisimulation."?  Let A=(a.(b+c)) + (a.b+a.c) and B=a.b+a.c when as far as I can tell A is similar to B, B is similar to A, but A and B are not bisimilar.  
> **username_6**: @András: You are right. My statement is not precise enough. The difference is abstracted away by the phrase "Some additional conditions may be present".  
> **username_0**: Hennessy and Milner defined three kinds of equivalence relations in [their original paper for bisimulation](http://portal.acm.org/citation.cfm?id=2455.2460) and gave some examples to illustrate their differences. Your original statement is actually the medium one in their paper, which is weaker than bisimulation and stronger than trace equivalence. I'm not sure which equivalence is better. Maybe it depends on practical use.  
> **username_8**: Simulation is also used as a proof technique to establish data refinement between two data types. Every single one of those simulation proofs relates whole classes of programs. See e.g.[1] for details. This suggests that the distinction between the two concepts is even blurrier.    [1]: CAR Hoare, He J, and JW Sanders. Prespecification in data refinement. *Information Processing Letters*, 25:71-76, 1987.  

---

### Answer by username_9 on 2011-03-13. Score: 10

The two types of relations appear to be used in different contexts. Logical simulations for typed languages and simulation relations when dealing with process calculi or modal logics interpreted over transition systems. username_6 has provided much intuitive explanation, so I will just add a few pointers that may help.

There has been work on characterising both notions using abstract interpretation. It may not be what you want, but at least both notions are treated in the same mathematical framework.

Samson Abramsky used logical relations to prove soundness and termination of strictness analysis for the lazy Lambda calculus ([Abstract Interpretation, Logical Relations, and Kan Extensions](http://logcom.oxfordjournals.org/content/1/1/5.abstract "Abstract Interpretation, Logical Relations, and Kan Extensions")). He also showed that the logical relations define abstraction functions in the Galois connection sense of abstract interpretation. More recently, Backhouse and Backhouse showed how to construct Galois connections for higher-order types from Galois connections for base types and that these constructions can be equivalently described using logical relations ([Logical Relations and Galois Connections](http://www.springerlink.com/content/kpv52g3k48n8tpgc/)). Thus, in the specific context of typed functional languages, the two notions are equivalent.

Simulation relations characterise property preservation between Kripke structures for various modal and temporal logics. Instead of types, we have modalities in a logic. Simulation relations also define Galois connections and hence, abstractions. One can ask if these abstractions have special properties. The answer is that standard abstractions are sound and simulation relation-based abstractions are complete. The notion of completeness is with respect to Galois connections, which may not concur with ones intuitive interpretation. This line of work has been developed by David Schmidt ([Structure-Preserving Binary Relations for Program Abstraction](http://www.springerlink.com/content/h51ncq7vuvflfx70/)), and Francesco Ranzato and Francesco Tapparo ([Generalized Strong Preservation by Abstract Interpretation](http://arxiv.org/abs/cs/0401016)).

> **Comments:**
> **username_0**: Your answer is very helpful that connecting the concepts with abstract interpretation. Thank you!  
> **username_3**: A sincere question: I'm no expert, but doesn't Reynolds (1983, "Types, abstraction and parametric polymorphism") already define logical relations that are Galois connections (Sec. 6)? The only differences I notice: he doesn't say the term "Galois connection" but only the equivalent "adjoint functors between partial orders regarded as categories", and he restricts to domains. OTOH, Backhouse and Backhouse cite Reynolds but don't discuss this claim, one way or the other.  

---

### Answer by username_10 on 2011-04-27. Score: 7

I'd say that the two concepts are somewhat vague. Both are about binary relations of computational mechanisms which somehow embody a notion of equality. Logical relations are defined by induction of type-structure, while simulations can be defined however you want, but the term alludes to coinduction.

It is misleading to say that logical relations are restrictied to lambda-calculi or sequential languages, although that's where logical relations originated. For example in our [work on fully abstract models for System F](http://www.informatics.sussex.ac.uk/users/mfb21/publications/fossacs03/index.html), we defined logical relations for typed $\pi$-calculi.

> **Comments:**
> **username_0**: Your reference is really nice! I haven't heard logical relations for concurrent programs before. Thank you!  I guess the difficulty of defining a logical relation is in finding the type structure. With the same type structure, a logical relation can be defined between different programming languages. On the other hand, a simulation requires modelling programs by a state transition system, which might be uneasy if the programs are written for different state models.  
> **username_10**: Hello! Yes, finding an appropriate type-structure might not always be easy.  You can define simulations using different transition systems for the two calculi you want to compare.  One could argue that the definition of weak simulation does just that. All you really need to define simulations is a relation for comparing transition labels.  

---

