波打つ

コンピュータサイエンス、特に自動定理証明において、リップリング^{[1]は、主に}エディンバラ大学情報学部の数学的推論グループで開発されたメタレベルのヒューリスティックスのグループを指し、自動定理証明システムで帰納的証明を導くために最も一般的に使用されています。リップリングは、書き換えシステムの制限された形式と見なすことができます。書き換えシステムでは、書き換えの完了時に受精を確実にするために特別なオブジェクトレベルの注釈が使用され、測定値が減少する要件によって、任意の書き換えルールと表現のセットの終了が保証されます。

レイモンド・オービンは、1976年にエディンバラ大学で博士論文^[2]を執筆中に「波及」という用語を初めて使用した人物である。彼は、帰納的証明の書き直し段階で共通の動きのパターンを認識した。アラン・バンディは後にこの概念を覆し、波及を副作用ではなくこの動きのパターンであると定義した。^[要出典]

それ以来、「横に波打つ」、「内側に波打つ」、「過去に波打つ」という言葉が造語され、この用語は「波打つ」に一般化されました。^[要出典] 2007 年現在、エディンバラやその他の場所で波打つ現象が開発され続けています。

リップリングは、ブレッドソーの極限定理^{[引用が必要]や、}マイケル・J・C・ゴードンとケンブリッジ大学のチームによって開発された小型コンピュータであるゴードン・マイクロプロセッサ^{[引用が必要]}の証明など、帰納的定理証明コミュニティでは伝統的に難しいと考えられてきた多くの問題に適用されてきました。

多くの場合、命題を証明しようとすると、ソース式とターゲット式が与えられますが、それらの違いは、いくつかの追加の構文要素が含まれていることだけです。

これは特に帰納的証明において当てはまります。帰納的証明では、与えられた式が帰納的仮説、目的の式が帰納的結論とみなされます。通常、仮説と結論の違いは、帰納変数の周囲に後続関数 (例: +1) が含まれる程度の小さな違いしかありません。

リップルの開始時に、リップル用語でウェーブフロントと呼ばれる 2 つの式の違いが識別されます。通常、これらの違いは証明の完了を妨げるため、「削除」する必要があります。ターゲット式には、2 つの式間のウェーブフロント (違い) とスケルトン (共通の構造) を区別するための注釈が付けられます。その後、ウェーブ ルールと呼ばれる特別なルールを終了方式で使用して、ソース式を使用して証明を完了できるようになるまで、ターゲット式を操作できます。

自然数の加算が可換であることを示すことが目的です。これは基本的な性質であり、証明は日常的な帰納法で行えます。しかし、そのような証明を見つけるための探索空間はかなり大きくなる可能性があります。

通常、帰納的証明の基本ケースはリップル以外の方法で解決されます。このため、ここではステップ ケースに焦点を当てます。ステップ ケースは次の形式をとり、帰納変数として x を使用することにしました。

また、補題、帰納的定義などから導き出された、波規則を形成するために使用できるいくつかの書き換え規則が存在する場合もあります。次の 3 つの書き換え規則があるとします。

これらに注釈を付けると、次のようになります。

これらの注釈付きルールはすべてスケルトン (最初のケースでは x + y = y + x、2 番目/3 番目のケースでは x + y) を保持していることに注意してください。ここで、帰納的ステップのケースに注釈を付けると、次のようになります。

これでリップルを実行する準備が整いました。

最終的な書き換えによりすべての波面が消え、帰納的仮説の適用である受精を適用して証明を完了できることに注意してください。

• David A. Basin および Toby Walsh (1996)。「リップルの計算と終了」(PDF)。Journal of Automated Reasoning。16 ( 1–2): 147–180。doi : 10.1007/BF00244462。S2CID 14427821  。