Formal Equivalence between programming languages

We have 2 languages which are (informally) semantically equivalent but syntactically different. One is xml an开发者_开发问答d another is script based. How can I go about formally proving that both languages are in fact equivalent. Script approach is just a convenient way to write a same program that would be tedious to write in xml.

Thanks Ketan

---

Write a program which takes as its input a program in one language, and gives as its output the equivalent program in the other language.

Then prove that the program you just wrote is correct for all possible inputs.

A good way to do that is by some sort of induction. Programs usually have a tree structure to them; if you can prove that the translation is correct for every possible leaf, and you can prove that it is correct for every possible combination of two correct trees, then by induction, you've proven the whole thing.

---

The first thing you need to define is what you mean by 'equivalent'

If you mean 'what you can do with one, you can do with the other' then one approach would be to prove that both languages are Turing complete If you can do this then you will have shown that both languages can perform the same kinds of computations as each other (and any other Turing complete language or device)

If you mean 'they have the same structure - just different ways of specifying elements' then you will need to abstract the languages to show that they do indeed share the same structure. Backus Naur Form is one way of doing this. If two languages have the same structure in BNF with just the terminals being different then really they are just two different representations of the same abstract syntax.

There are obviously other possible meaning of 'equivalent' and thus other things you could do.

You also need to define what you mean by 'proving' - do you mean a rigorous mathematical proof or 'convince my co workers that the scripting language is good enough'? If you mean the first, it's going to be tough. If you mean the second, you could define a specification for what thse languages need to be able to do and demonstrate proof of concepts in each language to show that they can meet the specification.

---

If they're general-purpose programming languages, write a Turing machine simulator in each. If they're not, you've got more of a problem. How sure are you that the languages are equivalent? Is this an exploratory sort of thing, or are you just trying to prove what you're already sure of?

In general, it's not possible to prove equivalence between languages. If they were written independently, your best bet might be to prove the script-based language does everything you need done, rather than to try to prove its equivalence to the XML-based one.

---

You may take some inspiration here: http://compcert.inria.fr/doc/index.html