29
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ You might want to provide links to these papers you've read. This would make it clearer which specific examples are confusing you. $\endgroup$ – Marc Hamann Mar 12 '11 at 2:31
  • 1
    $\begingroup$ 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.) $\endgroup$ – Hongjin Liang Mar 12 '11 at 4:52
  • 1
    $\begingroup$ 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". $\endgroup$ – Hongjin Liang Mar 12 '11 at 4:54
  • 3
    $\begingroup$ 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. $\endgroup$ – Kaveh Mar 13 '11 at 12:32
  • 1
    $\begingroup$ @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: ccs.neu.edu/home/amal/ahmed-research.pdf. (Another overview on research on logical relations is this talk from Derek Dreyer and in his research statement: mpi-sws.org/~dreyer/research.pdf). $\endgroup$ – Blaisorblade Mar 24 '14 at 18:10
20
$\begingroup$

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" in 1971. Hoare knew it and used it in coming up with "Proof of correctness of data representations" 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". Reynolds used relational reasoning in "Craft of Programming", 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", 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. (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.


[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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Dave Clarke Jul 22 '13 at 14:20
  • $\begingroup$ @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. $\endgroup$ – Uday Reddy Jul 22 '13 at 14:49
14
$\begingroup$

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): 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 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 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 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.

$\endgroup$
  • $\begingroup$ Thanks a lot for your detailed explanation! I will read your references and try to figure out deep connections/differences between the two. $\endgroup$ – Hongjin Liang Mar 13 '11 at 2:09
  • $\begingroup$ 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. $\endgroup$ – András Salamon Apr 27 '11 at 19:52
  • $\begingroup$ @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". $\endgroup$ – Dave Clarke Apr 27 '11 at 20:26
  • $\begingroup$ Hennessy and Milner defined three kinds of equivalence relations in their original paper for bisimulation 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. $\endgroup$ – Hongjin Liang Apr 28 '11 at 4:58
  • $\begingroup$ 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. $\endgroup$ – Kai Mar 4 '12 at 22:47
8
$\begingroup$

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.

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). 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). 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), and Francesco Ranzato and Francesco Tapparo (Generalized Strong Preservation by Abstract Interpretation).

$\endgroup$
  • $\begingroup$ Your answer is very helpful that connecting the concepts with abstract interpretation. Thank you! $\endgroup$ – Hongjin Liang Mar 13 '11 at 2:19
  • $\begingroup$ 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. $\endgroup$ – Blaisorblade Mar 11 '15 at 10:49
6
$\begingroup$

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, we defined logical relations for typed $\pi$-calculi.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Hongjin Liang Apr 28 '11 at 5:27
  • $\begingroup$ 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. $\endgroup$ – Martin Berger Apr 28 '11 at 8:11

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.