0
$\begingroup$

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, 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?

$\endgroup$
2
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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.... $\endgroup$ – anil keshav May 13 '16 at 10:23
  • $\begingroup$ @anilkeshav The question of comparing programming languages and their expressivity is a deep one and far from understood. $\endgroup$ – Martin Berger May 13 '16 at 10:56
  • $\begingroup$ 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. $\endgroup$ – Martin Berger May 13 '16 at 11:02

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.