<p>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.</p>
<p>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 <span class="math-container">$L_1$</span> into <span class="math-container">$L_2$</span>, say, then
<span class="math-container">$L_2$</span> is at least as expressive as <span class="math-container">$L_1$</span>.</p>
<p>Unfortunately, things are not quite that easy.
By the <a href="http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis%E2%80%8E" rel="nofollow noreferrer">Church-Turing thesis</a> you know that you can
always find such translations
(for Turing-complete languages). So the very existence of
translations is not discriminating enough to distinguish
programming languages. And yet, everybody who has programmed in
different languages (e.g. Assembler vs Scala, Prolog, Haskell) knows that some
languages are easier to program than others.</p>
<p>This conundrum is
usually approached by putting <strong>restrictions</strong> 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.</p>
<p>In this sense e.g. the <span class="math-container">$\pi$</span>-calculus is very expressive because
we can often find translations meeting various restrictions when
translating from a language <span class="math-container">$L$</span> into the <span class="math-container">$\pi$</span>-calculus. Conversely,
purely functional languages are not so expressive, because when we
translate <span class="math-container">$L$</span> into a purely functional language, the translation functions
often violate various constraints.</p>
<p>Here is a far from exhausting list of popular restrictions
for this purpose (which are not equivalent):</p>
<ul>
<li><p>The translation should preserve <strong>termination</strong>.</p>
</li>
<li><p>The translation should preserve the structure of
programs (mathematically: translation should be a
homomorphism): <span class="math-container">$$trans(f(P_1, ..., P_n)) = trans(f)(trans(P_1),
  ..., trans(P_n)).$$</span> This constraint is usually referred to as
<strong>compositionality</strong> of the translation.</p>
</li>
<li><p>While compositionality can often not be achieved when we try to
compare very different languages <span class="math-container">$L_1$</span> and <span class="math-container">$L_2$</span>, A weaker form
almost always holds: (simplifying a bit) there is a fixed
program <span class="math-container">$Q$</span> for each constructor <span class="math-container">$f$</span> such that <span class="math-container">$$trans(f(P_1, ..., P_n)) = trans(f)(Q,
  trans(P_1), ..., trans(P_n)).$$</span> I like to call this
<strong>compositionality-up-to-OS</strong>, because the fixed program <span class="math-container">$Q$</span> acts
like an operating system.</p>
</li>
<li><p>The translation should preserve the (asymptotic space or time)
<strong>complexity</strong> 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.</p>
</li>
<li><p>The translation should exhibit <strong>operational correspondence</strong>: We
say an encoding <span class="math-container">$trans(.)$</span> is operationally corresponding if it is
Whenever <span class="math-container">$P →^* Q$</span> then <span class="math-container">$trans(P) →^*≈ trans(Q)$</span>. Moreover, whenever <span class="math-container">$trans(P) →^* Q$</span> then there is <span class="math-container">$P'$</span> such that <span class="math-container">$P
  →^* P'$</span> and <span class="math-container">$Q →^*≈ trans(P')$</span>. Here ≈ is the chosen notion of program
equality in the target language.</p>
</li>
<li><p><strong>Divergence reflection</strong>: this means that whenever <span class="math-container">$trans(P)$</span> diverges, then so does <span class="math-container">$P$</span>.</p>
</li>
<li><p><strong>Success sensitiveness</strong>: Given a criterion of program
success (e.g. the ability of output a chosen value) on both
source and target, an encoding <span class="math-container">$trans(.)$</span> is success sensitive if <span class="math-container">$P$</span>
is successful if and only iff <span class="math-container">$trans(P)$</span> is successful.</p>
</li>
<li><p><strong>Full abstraction</strong>, we want <span class="math-container">$P \simeq_1 Q$</span> iff <span class="math-container">$trans(P) \simeq_2 trans(Q)$</span>,
where <span class="math-container">$\simeq_1$</span> is the chosen notion of program equality in the source language
of the translation and <span class="math-container">$\simeq_2$</span> does that job in the target.</p>
</li>
<li><p>Preservation of <strong>program size</strong>:  the translation should not lead to substantial
increases in program size.</p>
</li>
<li><p><strong>Name invariance</strong>: 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'.</p>
</li>
</ul>
<p>The relationships between those criteria, like the whole field
of programming language expressiveness, is ill-understood.</p>
<p>A pioneering paper in the study of programming language expressiveness is</p>
<ul>
<li>M. Felleisen, <a href="http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz%E2%80%8E" rel="nofollow noreferrer">On the Expressive Power of Programming Languages.</a></li>
</ul>
<p>where key concepts from logic, such as conservative extension of
theories are generalised to programming languages.</p>

CC BY-SA 3.0
2014-04-02T14:29:48.463Z
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
CC BY-SA 3.0
2014-04-02T15:12:36.740Z
@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
CC BY-SA 3.0
2014-04-02T15:12:58.243Z
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
CC BY-SA 3.0
2014-04-02T15:17:00.587Z
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
CC BY-SA 3.0
2014-04-02T15:29:20.073Z
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
CC BY-SA 3.0
2014-04-02T16:01:15.320Z
The constraints I listed are not intended to be equal, they are just a list of constraints I have seen used for expressivity results. Operational correspondence is significant because it often holds and is often used as a stepping stone towards stronger results. BTW, I'm not sure what you mean by "visibility/hiding".
Martin Berger
CC BY-SA 3.0
2014-04-02T16:13:27.710Z
I do not mean you intended them equal, but I think useful to state
they may not be. Wrt operational correpondance, I remember that very
different programs may compute the same result, but possibly it does
not extend to languages??? Last, the organization of modularity and
visibility is an important part of expressivity. There is more than
the computation to a program, if semantic equivalence goes beyond a
Turing argument. For example, can it emphasize the architecture of a
problem? Can we abstract away subparts and still have something
meaningful, understandable?
babou
CC BY-SA 3.0
2014-04-02T16:32:54.623Z
I'm not sure I fully understand what you mean. Anyway, operational correspondence can be made to appl to individual pairs of programs,  but you usually want to show that it holds for the whole translation. Note also that operational correspondence is defined w.r.t. to a chosen notion of equivalence on the target language. One has to be careful here. For example if the source and target have very different levels of non-determinism, conventional notions of bisimululation may no longer work, and one has to move to e.g. coupled simulations.
Martin Berger
CC BY-SA 4.0
2014-03-30T11:18:37.333Z
2023-02-18T21:27:14.310Z
2023-02-18T21:27:14.310Z
Martin Berger
<p>I would like to compare two languages which are from different programming paradigms. Both languages are object oriented languages, but one of them a multiparadigm language because it supports functional programming style as well.</p>
<p>I wrote some example codes in imperative style and functional style which are absolutely different in syntax but equivalent in semantics.</p>
<p>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 definition about semantic equivalence of an imperative and a functional language.</p>
<p>I was looking for a clear and nice article about this topic on google scholar but i have not found any useful yet.</p>

CC BY-SA 3.0
2014-03-30T17:17:16.067Z
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
CC BY-SA 3.0
2014-03-31T05:57:18.227Z
@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
<reference-request><pl.programming-languages><semantics><equivalence>
How can I prove formally semantic equivalence of programming languages?
bitli
# How can I prove formally semantic equivalence of programming languages?

(Asked by: username_0 on 2014-03-30)

I would like to compare two languages which are from different programming paradigms. Both languages 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 definition about semantic equivalence of an imperative and a functional language.

I was looking for a clear and nice article about this topic on google scholar but i have not found any useful yet.

**Tags:** reference-request, pl.programming-languages, semantics, equivalence

> **Comments:**
> **username_1**: 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?  
> **username_2**: @username_1: 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.  

---

## 1 answers

### Answer by username_3 on 2014-03-30. Score: 14 | Accepted answer

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](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis%E2%80%8E) you know that you can
always find such translations
(for Turing-complete languages). So the very existence of
translations is not discriminating enough to distinguish
programming languages. And yet, everybody who has programmed in
different languages (e.g. Assembler vs Scala, Prolog, Haskell) 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 (which are not equivalent):

* 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

* M. Felleisen, [On the Expressive Power of Programming Languages.](http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz%E2%80%8E)

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

> **Comments:**
> **username_4**: 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.  
> **username_3**: @username_4 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.)  
> **username_3**: 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.  
> **username_3**: 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.  
> **username_4**: 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.  
> **username_3**: The constraints I listed are not intended to be equal, they are just a list of constraints I have seen used for expressivity results. Operational correspondence is significant because it often holds and is often used as a stepping stone towards stronger results. BTW, I'm not sure what you mean by "visibility/hiding".  
> **username_4**: I do not mean you intended them equal, but I think useful to state they may not be. Wrt operational correpondance, I remember that very different programs may compute the same result, but possibly it does not extend to languages??? Last, the organization of modularity and visibility is an important part of expressivity. There is more than the computation to a program, if semantic equivalence goes beyond a Turing argument. For example, can it emphasize the architecture of a problem? Can we abstract away subparts and still have something meaningful, understandable?  
> **username_3**: I'm not sure I fully understand what you mean. Anyway, operational correspondence can be made to appl to individual pairs of programs,  but you usually want to show that it holds for the whole translation. Note also that operational correspondence is defined w.r.t. to a chosen notion of equivalence on the target language. One has to be careful here. For example if the source and target have very different levels of non-determinism, conventional notions of bisimululation may no longer work, and one has to move to e.g. coupled simulations.  

---

