proof - 编程语言之间的形式等价

Question

我们有 2 种语言（非正式地）在语义上是等价的，但在语法上是不同的。一个是xml，另一个是基于脚本的。我怎样才能正式证明这两种语言实际上是等价的。脚本方法只是编写相同程序的便捷方式，而用 xml 编写会很乏味。

谢谢科坦

Answer 1

编写一个程序，将一种语言的程序作为其输入，并将另一种语言的等效程序作为其输出。

然后证明你刚刚编写的程序对于所有可能的输入都是正确的。

一个很好的方法是通过某种归纳。程序通常具有树结构；如果你可以证明翻译对于每个可能的叶子都是正确的，并且你可以证明它对于两棵正确树的每个可能组合都是正确的，那么通过归纳，你已经证明了整个事情。

Answer 2

您需要定义的第一件事是“等效”的含义

如果你的意思是“你可以用一种来做什么，你可以用另一种来做”，那么一种方法是证明两种语言都是图灵完备的。如果你能做到这一点，那么你将证明两种语言都可以执行相同类型的相互计算（以及任何其他图灵完备语言或设备）

如果您的意思是“它们具有相同的结构 - 只是指定元素的不同方式”，那么您将需要抽象语言以表明它们确实具有相同的结构。Backus Naur Form是这样做的一种方式。如果两种语言在 BNF 中具有相同的结构，只是终端不同，那么它们实际上只是相同抽象语法的两种不同表示。

“等效”显然还有其他可能的含义，因此您可以做其他事情。

您还需要定义“证明”的含义——您是指严格的数学证明还是“让我的同事相信脚本语言足够好”？如果你的意思是第一个，这将是艰难的。如果您指的是第二种，您可以定义这些语言需要能够做什么的规范，并演示每种语言的概念证明，以表明它们可以满足规范。

Answer 3

您可能会在这里获得一些灵感：http: //compcert.inria.fr/doc/index.html

Answer 4

如果它们是通用编程语言，请在每种语言中编写一个图灵机模拟器。如果他们不是，你有更多的问题。你有多确定这些语言是等价的？这是一种探索性的事情，还是你只是想证明你已经确定的事情？

一般来说，不可能证明语言之间的等价性。如果它们是独立编写的，那么最好的办法可能是证明基于脚本的语言可以完成您需要做的一切，而不是试图证明它与基于 XML 的语言等价。