与えられた文法の正しさを証明するには？

Question

私は、プログラミング言語開発者がどのように文法が正しいかを検証し、証明する方法を知っています。私が新しいlangaugeのための新しい文法を作ったとします。私は、さまざまな種類のテストプログラムを提供することによって、単位テストツールで文法をテストできます。しかし、私は文法が正しいことを決して100％保証しません。どのようにして言語デベロッパーは文法が現実世界で正しいことを保証しますか？

たとえば、鉛筆と紙を使って新しい言語の文法を作成しました。しかし、私は間違いを犯し、文法は2 + 2 +のような+で終わる式を受け入れます。私は間違いを見つけなければ、この誤った文法を使って自分の言語を実装します。実装とユニットテストの後、私はエラーを見つけることができます。実装を開始する前にそれを見つけることは可能でしょうか？

間違いなく、鉛筆と紙（派生など）を使っていくつかのサンプル入力を使って文法を試すことができますが、いくつかのコーナーケースが見逃されることがあります。実際の言語開発者が文法をテストする上で、より良いアプローチがありますか？

Answer 1

校正は、クレームの真実を示す論理的な議論です。問題を考える方法があるので、何かを証明する方法はたくさんあります。離散構造（文法など）について物事を証明する一般的な方法は、数学的帰納法を使用しています。基本的には、可能な限り単純なケースで何かが真であることを示してから、あるサイズのすべてのケースで真であれば、次のサイズのケースで真でなければならないことを示します。

私たちの場合、あなたの文法が単語の最後に+を生成しなかったことを証明したかったとします。言語で文字列を作成する際に使用されるプロダクションの数について誘導を行うことができます。すべての関連する基本事例を特定し、これらの文字列のプロパティ保持を表示し、最後に+を得ることができないように長い文字列を構築することを示します。ここに例があります。

S：= S + S | （S）| x

ベースケース：言語の中で最短の文字列がxで、S - > xとして生成されます。 +で終わるわけではありません。

帰納仮説：k個までのプロダクションを使用して生成されたすべての文字列が+で終わらないと仮定します。

誘導ステップ：k個以上のプロダクションを使用して生成された文字列を+で終わらないように表示する必要があります。 Sから生成された任意の文字列にルール（S）を適用すると、そのプロパティが保持する+を追加しません。 Sから生成されたストリングにS + Sを適用すると、S + Sの最後のシンボルは、Sによって生成されたより短いストリング（少なくとも2シンボル短く）の最後のシンボルになります。誘導仮説によって、 、どちらもこれをしません。他のプロダクションは存在しないため、言語の文字列は+で終わりません。 QED