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?
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.
functor $F$ describing the machine.
$\endgroup$
Commented
Jul 22, 2013 at 14:20
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.
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).
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.
