# How can I prove formally semantic equivalence of programming languages?

I would like to compare two languages which are from different programming paradigms. Both langauges are object oriented languages, but one of them a multiparadigm language because it supports functional programming style as well.

I wrote some example codes in imperative style and functional style which are absolutely different in syntax but equivalent in semantics.

I have some experiences about operational semantics, the WHILE language and so on from my university studies and I was wondering how I could give a formal definiton about semantic equivalence of an imperative and a functional language.

Thanks for helping!

-
its an undecidable problem in general to prove two programs written in Turing complete languages are equivalent... when you say "equivalent in semantics" dont you mean they have equivalent inputs/outputs over all inputs/outputs? –  vzn Mar 30 at 17:17
@vzn: One can prove that one programming language is equivalent to another by providing a translation of one to another and back again. One can reason about the expressive power of languages by considering the complexity change this translation induces or whether it requires "nonlocal" information to be recorded. –  Dave Clarke Mar 31 at 5:57

Comparing two programming languages is difficult is a difficult problem, and far from being solved. The key issue is that there are many different ways languages can be compared, and none of them is compelling.

The most widely used approach, coming from logic, is to consider translations between the languages to be compared. The general idea is as follows: if we have a translation into from $L_1$ into $L_2$, say, then $L_2$ is at least as expressive as $L_1$.

Unfortunately, things are not quite that easy. By the Church-Turing thesis you know that you can always find such translations (for Turing-complete languages). So the very existence of translations is not discreminating enough to distinguish programming languages. And yet, everybody who has programmed in different languages (e.g. Assembler vs Scala) knows that some languages are easier to program than others.

This conundrum is usually approached by putting restrictions on what counts as a translation functions. The idea here is that the translation functions 'measure' how much 'rearrangement' is necessary when translating from one language to the other: the more 'rearrangement' required, the less expressive the target language. Restrictions on translations control what kind of 'rearrangement' we consider. If we can show that no translation exists that satisfies a bunch of restrictions, then the languages are substantially different in expressivity.

In this sense e.g. the $\pi$-calculus is very expressive because we can often find translations meeting various restrictions when translating from a language $L$ into the $\pi$-calculus. Conversely, purely functional languages are not so expressive, because when we translate $L$ into a purely functional language, the translation functions often violate various constraints.

Here is a far from exhausting list of popular restrictions for this purpose:

• The translation should preserve termination.

• The translation should preserve the structure of programs (mathematically: translation should be a homomorphism): $$trans(f(P_1, ..., P_n)) = trans(f)(trans(P_1), ..., trans(P_n)).$$ This constraint is usually referred to as compositionality of the translation.

• While compositionality can often not be achieved when we try to compare very different languages $L_1$ and $L_2$, A weaker form almost always holds: (simplifying a bit) there is a fixed program $Q$ for each constructor $f$ such that $$trans(f(P_1, ..., P_n)) = trans(f)(Q, trans(P_1), ..., trans(P_n)).$$ I like to call this compositionality-up-to-OS, because the fixed program $Q$ acts like an operating system.

• The translation should preserve the (asymptotic space or time) complexity of programs. (The Slot and van Emde Boas thesis says that polynomial-time translations are always possible, so we might need finer distinctions than preservation of run-time up to a polynomial factor.) The theory of NP-completeness can be seen in this light.

• The translation should exhibit operational correspondence: We say an encoding $trans(.)$ is operationally corresponding if it is Whenever $P →^* Q$ then $trans(P) →^*≈ trans(Q)$. Moreover, whenever $trans(P) →^* Q$ then there is $P'$ such that $P →^* P'$ and $Q →^*≈ trans(P')$. Here ≈ is the chosen notion of program equality in the target language.

• Divergence reflection: this means that whenever $trans(P)$ diverges, then so does $P$.

• Success sensitiveness: Given a criterion of program success (e.g. the ability of output a chosen value) on both source and target, an encoding $trans(.)$ is success sensitive if $P$ is successful if and only iff $trans(P)$ is successful.

• Full abstraction, we want $P \simeq_1 Q$ iff $trans(P) \simeq_2 trans(Q)$, where $\simeq_1$ is the chosen notion of program equality in the source language of the translation and $\simeq_2$ does that job in the target.

• Preservation of program size: the translation should not lead to substantial increases in program size.

• Name invariance: each program has a finite number of 'interaction points' that the outside can use to interact with the program, e.g. free variables. We can require that encodings commut with injective renamings of 'interaction points'.

The relationships between those criteria, like the whole field of programming language expressiveness, is ill-understood.

A pioneering paper in the study of programming language expressiveness is

where key concepts from logic, such as conservative extension of theories are generalised to programming languages.

-
One well known and widely used type of translator is called a compiler. How to they behave with respect to the properties a translation should satisfy? I guess that may be a new question by itself. One objection is naturally that compilers are not concerned with expressiveness. Also some of these criteria seem more related to semantic similarity (similarity of expression) than to expressiveness per se. And this is certainly not expected from a compiler. Still, it might be an interesting test. –  babou Apr 2 at 14:29
@babou Compilers don't directly fit in this picture for another reason: stricly speaking, they don't translate from $L_1$ to $L_2$ but from strings to, depending how you look at it, $L_2$ or to strings. As inputs are strings which may or may not represent valid programs, compilation can fail to lex, to parse or to type-check. If we ignore this detail, then compilers do fit into the picture. We generally expect a compiler to deliver a sound translation, preserving and reflecting termination and divergence. (Continued below.) –  Martin Berger Apr 2 at 15:12
However, because the target language of a compilation is usually much more fine-grained than the source, we typically don't get full abstraction. Moreover, as the aim of a compiler is not to establish or disprove expressivity claims, but rather to deliver high-performance code, they often take all manner of shortcuts which are not compositional (e.g. global program optimisation). If one throws types at the target language (e.g. G. Morrisett et al's typed assembly language) something like full abstraction could conceivably hold. –  Martin Berger Apr 2 at 15:12
Regarding the dichotomy between "semantic similarity" and "expressiveness": the constraints are a collection of constraints that seek to formalise the notion of expressiveness. They have all been used to show that certain languages are different in expressiveness. If you have very different criteria, please put them forward. –  Martin Berger Apr 2 at 15:17
Thanks for the answer. I think the correctness/WFF part of compiling can be ignored (I did). I think considering compilers makes a distinction with requirement concerning denotational equivalence (a minimum to be expected) and others that are more concerned with expressivity equivalence ... whatever that means. My feeling, regarding your excellent post, is that your criteria were not born equal. I am wondering about importance of "operational correspondance". And I would love something about visibility/hiding. –  babou Apr 2 at 15:29