<p>Let me clarify the setting, which has nothing to do with $\pi$-calculus or bisimulation.</p>

<p>The first thing you have to realise that it does not make much sense to talk about a programming language without reference to the notion of program equivalence you intend to impose on the language. That's because </p>

<ul>
<li><p>We usually identify certain programs (e.g. <code>f(x:int) = { x+1 }</code> is considered the same as  <code>f(y:int) = { y+1 }</code>).</p></li>
<li><p>The notion of program equivalence to be used depends highly on what you are doing with these languages, e.g. sometimes we care about program time- or space complexity, sometimes we don't.</p></li>
</ul>

<p>So the general setup you are interested in is this: you are given 3 language $(A, \cong_A)$, $(B, \cong_B)$ and $(T, \cong_T)$, each comprising of a set of programs ($A$, $B$ and $T$)  with associated notions of program equivalence ($\cong_A$, ...). In addition, you have two mappings:</p>

<ul>
<li><p>$trans_A : A \rightarrow T$.  </p></li>
<li><p>$trans_B : B \rightarrow T$.</p></li>
</ul>

<p>They map ("compile") from source languages $A$ and $B$ to target $T$. Typically you want these two translation functions to be at least sound. That means that for all $A$-programs $P, Q$, we have: $trans_A(P) \cong_T trans_A(Q) \Rightarrow P \cong_A Q$, and likewise for $trans_B$. </p>

<p>Now you want to argue that $(A, \cong_A)$ and $(B, \cong_B)$ are equivalent as languages. That's what you use the target $(T, \cong_T)$ for. There are <strong>many</strong> ways that this can be done, details depend on what concept of language equivalence you are interested in. One approach could be to say</p>

<ul>
<li><p>For each $A$-program $P_A$ there is a $B$-program $P_B$ such that $trans_A(P_A) \cong_T trans_B(P_B)$.</p></li>
<li><p>Vice versa.</p></li>
</ul>

<p>None of the above is $\pi$-calculus specific, but you
 can instantiate $T$ with $\pi$-calculus and $\cong_T$ with any chosen notion of equivalence on $\pi$-calculus such as strong or weak bisimulation, maximum consistent theory, reduction congruence, or whatever else makes sense for your application.</p>

<p>I said that there are many alternative ways of doing this. You could for example impose constraints on $trans_A$ and $trans_B$ so the translation preserves chosen constraints (e.g. termination, or compositionality).</p>

CC BY-SA 3.0
2016-05-13T10:23:32.380Z
Thanks @Martin Berger, that made a lot of sense to me coming from a pure computer science background and not from the mathematical logic arena....
anil keshav
CC BY-SA 3.0
2016-05-13T10:56:59.247Z
@anilkeshav The question of comparing programming languages and their expressivity is a deep one and far from understood.
Martin Berger
CC BY-SA 3.0
2016-05-13T11:02:52.293Z
The $\pi$-calculus is an especially good target because it's very expressive, but also very regular, so it's a good tool for comparing programming languages.
Martin Berger
CC BY-SA 3.0
2016-05-12T11:16:35.933Z
2016-05-12T14:26:48.053Z
2016-05-12T14:26:48.053Z
Martin Berger
<p>I am relatively new to the field of language semantics. However i had a question pertaining to language equivalence (i did read about the <a href="https://cs.stackexchange.com/questions/38236/how-do-you-prove-two-languages-are-equivalent-using-the-definition-of-acceptance">question</a>, however my approach is slightly different and hence this question). </p>

<p>If i have two languages $A$ and $B$ and both languages can be expressed using a model a computation like $\pi$-Calculus. If i have to prove that the 2 languages are equivalent, then would it be need to show that the 2 $\pi$-Calculus constructs (starting from the most atomic elements of the language to then the composition of the elements etc) of the two languages are equivalent, is this correct?</p>

<p>How do we prove equivalence between two $\pi$-Calculus representation of the languages?. Can i use bisimulation in $\pi$-Calculus to prove the same or have i missed something and is there another formal proof to do the same?</p>

<fl.formal-languages><pi-calculus><proof-techniques>
Semantic equivalence using a model of computation of two languages
anil keshav
# Semantic equivalence using a model of computation of two languages

(Asked by: username_0 on 2016-05-12)

I am relatively new to the field of language semantics. However i had a question pertaining to language equivalence (i did read about the [question](https://cs.stackexchange.com/questions/38236/how-do-you-prove-two-languages-are-equivalent-using-the-definition-of-acceptance), however my approach is slightly different and hence this question).

If i have two languages $A$ and $B$ and both languages can be expressed using a model a computation like $\pi$-Calculus. If i have to prove that the 2 languages are equivalent, then would it be need to show that the 2 $\pi$-Calculus constructs (starting from the most atomic elements of the language to then the composition of the elements etc) of the two languages are equivalent, is this correct?

How do we prove equivalence between two $\pi$-Calculus representation of the languages?. Can i use bisimulation in $\pi$-Calculus to prove the same or have i missed something and is there another formal proof to do the same?

**Tags:** fl.formal-languages, pi-calculus, proof-techniques

---

## 1 answers

### Answer by username_1 on 2016-05-12. Score: 2 | Accepted answer

Let me clarify the setting, which has nothing to do with $\pi$-calculus or bisimulation.

The first thing you have to realise that it does not make much sense to talk about a programming language without reference to the notion of program equivalence you intend to impose on the language. That's because

* We usually identify certain programs (e.g. `f(x:int) = { x+1 }` is considered the same as `f(y:int) = { y+1 }`).
* The notion of program equivalence to be used depends highly on what you are doing with these languages, e.g. sometimes we care about program time- or space complexity, sometimes we don't.

So the general setup you are interested in is this: you are given 3 language $(A, \cong\_A)$, $(B, \cong\_B)$ and $(T, \cong\_T)$, each comprising of a set of programs ($A$, $B$ and $T$) with associated notions of program equivalence ($\cong\_A$, ...). In addition, you have two mappings:

* $trans\_A : A \rightarrow T$.
* $trans\_B : B \rightarrow T$.

They map ("compile") from source languages $A$ and $B$ to target $T$. Typically you want these two translation functions to be at least sound. That means that for all $A$-programs $P, Q$, we have: $trans\_A(P) \cong\_T trans\_A(Q) \Rightarrow P \cong\_A Q$, and likewise for $trans\_B$.

Now you want to argue that $(A, \cong\_A)$ and $(B, \cong\_B)$ are equivalent as languages. That's what you use the target $(T, \cong\_T)$ for. There are **many** ways that this can be done, details depend on what concept of language equivalence you are interested in. One approach could be to say

* For each $A$-program $P\_A$ there is a $B$-program $P\_B$ such that $trans\_A(P\_A) \cong\_T trans\_B(P\_B)$.
* Vice versa.

None of the above is $\pi$-calculus specific, but you
can instantiate $T$ with $\pi$-calculus and $\cong\_T$ with any chosen notion of equivalence on $\pi$-calculus such as strong or weak bisimulation, maximum consistent theory, reduction congruence, or whatever else makes sense for your application.

I said that there are many alternative ways of doing this. You could for example impose constraints on $trans\_A$ and $trans\_B$ so the translation preserves chosen constraints (e.g. termination, or compositionality).

> **Comments:**
> **username_0**: Thanks @Martin Berger, that made a lot of sense to me coming from a pure computer science background and not from the mathematical logic arena....  
> **username_1**: @anilkeshav The question of comparing programming languages and their expressivity is a deep one and far from understood.  
> **username_1**: The $\pi$-calculus is an especially good target because it's very expressive, but also very regular, so it's a good tool for comparing programming languages.  

---

