Hello
We have 2 languages which are (informally) semantically equivalent but syntactically different. One is xml and 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.
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.
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.
Many thanks for your answers.
Erik, David
Yes, I do have a two way translator for the languages in question. In fact, the script based version has to be translated to its xml form for execution as the engine understands xml only. However, I am not sure how do I exhaustively check all possible combinations of features and translate them two-ways, that would be too much. About induction, I am not sure that paradigm of proof we can use for such a scenario. Are there any existing such proofs that you know of?
Dank Actually I need to show both and funny thing is that we have a proof that the xml based version is Turing complete and we have a complete EBNF grammar for the script-based version of the same language. I am thinking, it would be nice to do both ways and see where it goes.
By proof, indeed I mean a mathematical proof rigorous enough to be published in a scientific journal. :)
Thanks again for the replies and please post if you have any more insights. These answers have definitely got me started.
cheers Ketan
You may take some inspiration here: http://compcert.inria.fr/doc/index.html