proof - プログラミング言語間の形式的等価性

Question

（非公式に）意味的には同等ですが、構文的には異なる2つの言語があります。1つはxmlで、もう1つはスクリプトベースです。両方の言語が実際に同等であることを正式に証明するにはどうすればよいですか。スクリプトアプローチは、xmlで書くのが面倒な同じプログラムを書くための便利な方法です。

ありがとうケタン

Answer 1

ある言語のプログラムを入力として受け取り、他の言語の同等のプログラムを出力として与えるプログラムを作成します。

次に、作成したプログラムがすべての可能な入力に対して正しいことを証明します。

それを行う良い方法は、ある種の誘導によるものです。プログラムには通常、ツリー構造があります。翻訳がすべての可能な葉に対して正しいことを証明でき、それが2つの正しい木のすべての可能な組み合わせに対して正しいことを証明できれば、誘導によって、すべてを証明したことになります。

Answer 2

最初に定義する必要があるのは、「同等」の意味です

「一方を使ってできることは、もう一方を使ってもできる」という意味であれば、1 つのアプローチは、両方の言語がチューリング完全であることを証明することです。これができれば、両方の言語が同じ種類のことを実行できることを示したことになります。相互の計算 (およびその他のチューリング完全言語またはデバイス)

「それらは同じ構造を持っています-要素を指定する方法が異なるだけです」という意味であれば、言語を抽象化して、それらが実際に同じ構造を共有していることを示す必要があります。Backus Naur Formは、これを行う 1 つの方法です。2 つの言語が BNF で同じ構造を持ち、端子が異なるだけである場合、実際には、それらは同じ抽象構文の 2 つの異なる表現にすぎません。

「同等」の他の可能な意味が明らかにあり、したがって他のことができます。

また、「証明する」とは何を意味するのかを定義する必要があります。厳密な数学的証明を意味するのでしょうか、それとも「スクリプト言語が十分に優れていることを同僚に納得させる」ことを意味するのでしょうか? 最初のことを意味すると、それは難しいでしょう。2 番目の場合は、これらの言語ができる必要があることの仕様を定義し、各言語で概念の証明を示して、仕様を満たすことができることを示すことができます。

Answer 3

ここでインスピレーションを得ることができます: http://compcert.inria.fr/doc/index.html

Answer 4

汎用プログラミング言語の場合は、それぞれにチューリング マシン シミュレーターを記述します。そうでない場合は、さらに問題が発生します。言語が同等であることをどの程度確信していますか? これは探索的なものですか、それともすでに確信していることを証明しようとしているだけですか?

一般に、言語間の同等性を証明することはできません。それらが独立して書かれている場合、最善の策は、XML ベースの言語と同等であることを証明しようとするよりも、スクリプトベースの言語が必要なことをすべて実行できることを証明することです。