VDMからIsabelle/HOLへの再帰関数の翻訳

この記事では、VDMというシステムからIsabelle/HOLという別のシステムへ再帰的定義を翻訳する方法について話してるよ。目的は、VDMのいろんな定義に自動で対応できるテンプレートを作ること。翻訳が明確で、できるだけ証明プロセスを自動化することに重点を置いてる。

VDMとIsabelle/HOLにはいくつかの違いがあって、特に再帰関数の終了の概念の扱い方に違いがあるんだ。終了は重要で、関数が永遠に止まらずに動き続けないことを保証してくれるからね。この記事では、これらの違いを考慮しながら再帰的定義を翻訳する方法を議論するよ。

この翻訳方法を使って、VDM定義をIsabelle/HOLに変換するのを助ける既存のツールに拡張を加えているよ。Isabelleでは、ユーザーが仕様、証明、文書を一箇所で書けるから便利。ソースや証明の詳細は特定のツールキットのリポジトリにあるよ。

次のセクションでは、VDMとIsabelleの背景情報を提供した後、基本的な型、再帰、全体の翻訳戦略について議論する予定だよ。

#背景

VDMからIsabelle/HOLへの翻訳器は、VDMに見られる広範な構造をカバーしてる。いろんな表現、パターン、型、仕様を管理できるんだ。目的は、VDMのほとんどのパターンが効果的に翻訳できるようにすることで、できない場合はそれらを表現する同等の方法を用意すること。

この翻訳で特に注目しているのは、再帰的定義された関数の扱いだよ。VDMでは、ユーザーは再帰が終了することを保証するために測度関数を定義しなきゃいけない。この測度関数は、再帰が意図通りに動くことを確認するための証明義務を生成するんだ。

ここで使う翻訳戦略は、サイズ変更終了（SCT）という特定のアプローチに従ってる。このアプローチでは、再帰関数が生成する値に基づいて終了を証明できるかどうかをチェックするんだ。すべての計算が小さい値に繋がるなら、再帰は最終的に止まるってことを保証できるよ。

#IsabelleのVDM基本型

Isabelleでは、自然数はゼロと1を加える後続関数の2つの部分からなるデータ型として表現されてる。Isabelleでは、これらの自然数を使って整数や他の数値型も定義してるよ。型変換があって、ユーザーが型を移行するのを助けるけど、自動で型を広げる暗黙のルールはないんだ。

VDMでは、自然数や整数のような基本型には特定の広がりルールがあることを考慮しなきゃいけない。例えば、両方の型が自然数なら、結果は整数になるかもしれない。私たちの翻訳戦略では、VDMの自然数をIsabelleの型同義語として扱うことで、プロセスを簡素化し、複雑な型の強制を避ける手助けをしてるよ。

でも、自然数を使って再帰関数をエンコードするのは予想以上に複雑になるかもしれない、IsabelleとVDMの表現が違うからね。

これらの複雑さがあっても、VDMの整数、集合、またはマップに対する再帰はまだ発生するよ、これらの型はIsabelleに明確な構成的定義がないからね。

#VDMとIsabelleの再帰

再帰的定義には、終了することを正当化する方法が必要だよ。さもないと、再帰は無限ループに陥るかもしれない。VDMでは、この正当化は再帰的測度から来ていて、再帰的定義と同じ入力を受け取って、各再帰呼び出しで減少しなきゃいけない自然数を返すんだ。

例えば、自然数の階乗を計算するシンプルな再帰関数を考えてみて。測度関数は入力自体を使って、入力がゼロに達した時に再帰が止まるんだ。この場合、VDMはIsabelleで確認しなきゃいけない3つの証明義務を生成する。

一方、Isabelleでは原始再帰や証明義務を生み出す一般的な関数定義を通じて再帰的定義を許可してる。課題は、パラメータが定義されたパターンに一致することと、再帰呼び出しが適切に終了することを保証することだよ。

Isabelleの再帰関数定義は、終了を自動で証明しようとする構文と、ユーザーが手動で終了の証明を提供する必要がある構文の2種類で表現できる。後者は、再帰関数がもっと複雑な場合に必要になることが多いんだ。

終了関係もよく構造化されてないといけなくて、それが終了することを保証するための秩序立った構造を持ってる必要がある。この要件が翻訳プロセスにさらに複雑さを加えてるよ。

#VDM再帰翻訳戦略

翻訳戦略の目標は、基本型、集合、列、マップに関連する再帰の問題を扱うこと、そして相互再帰も含めることだよ。最初に、明示的な測度なしでもVDMのすべての再帰関数にタグを付けて、Isabelleの関数を使って翻訳を促進するんだ。

もしIsabelleが必要な終了を自動で証明できなかったら、ユーザーはよく構造化された測度関係を定義する注釈を提供できる。これが再帰呼び出しの関係を確立し、翻訳が成功するのを保証するんだ。

翻訳中は、注釈が正しく定義されているかを確認するためにツールがチェックする。このプロセスには、終了の証明をサポートするために注釈をIsabelleの定義に翻訳することが含まれるよ。

翻訳戦略では、VDMのチェックが明示的に述べられることが求められる。例えば、VDMの集合は有限でなければならないし、その型不変条件はすべての要素に対して成立しなきゃいけない。

#VDM基本型の再帰

自然数のような基本型に対して、翻訳戦略は最初にパラメータが有効な型であることを要求する前提条件を設定するよ。次に、再帰関数を定義して、前提条件が失敗した場合は未定義の値を返すんだ。パターンの互換性と完全性の証明は、標準のIsabelleメソッドに従って確立される。

再帰のよく構造化されていることは、Isabelleの既存の仕組みを使って簡単に確立できることが多いから、このプロセスはスムーズになるよ。私たちは証明発見を助けるために新しい補題も定義して、ユーザーの負担を減らしてる。

#VDM集合の再帰

翻訳戦略の次のステップは、VDM集合の処理を含むよ。よくある例が、集合の要素を合計する関数だ。関数は合計を進める前に集合が空でないかチェックして、再帰に使う任意の要素を選ぶんだ。

関数の前提条件を定義して、集合が有効な数だけを含んでいて有限であることを確保するよ。基本型と同じように、Isabelleで再帰関数を確立して、合計を実行する前に前提条件をチェックする。

測度関係は関与するプロセスを反映する必要があって、Isabelleのツールを使って関係のよく構造化されていることを検証できる。終了の証明も前提条件やフィルタリング条件に基づいて構築されるよ。

#VDMマップの再帰

マップに関する再帰も集合に関する再帰と似てる。マップの値を合計する関数は、マップが空かどうかをチェックして、空でない場合はキーを選んでその値を合計する技術を使うんだ。

これまでと同様に、前提条件はマップのドメインとレンジの両方が必要な特性を満たすことを保証する。翻訳プロセスでは、よく構造化されているかのコア条件をチェックして、終了の証明をサポートするための適切な測度関係を構築するよ。

#複雑な測度を含む再帰

同じ翻訳アプローチをもっと複雑な再帰的定義にも適用できるよ。でも、これらの定義はユーザーにより詳細な注釈や追加の補題を定義することを要求することが多いんだ。

例えば、よく知られたAckermann関数を考えてみて、これは複雑な再帰で有名だよ。この関数は、両方のパラメータを特定の方法で処理する必要があって、VDMで定義しなきゃいけない追加の測度が関与するんだ。ユーザーは、Isabelleが再帰呼び出しの間の関係を正しく推論できるように注釈を提供しなきゃいけない。

VDM版で使われる測度は、通常Isabelleで見るものとは違ってるから、翻訳がうまくいくためには両者の明確なつながりを確立することが重要だよ。

#難しい例

いくつかの例はもっと難しくて、証明のためにより複雑な設定が必要だよ。例えば、置換関数は減少するパラメータの間で置換できることを示していて、Takeuchi関数は内再帰を示してる。

これらの複雑な例は、証明システムが要求することの違いを明らかにすることが多い。ユーザーは特定の測度を提供し、Isabelleが必要な証明を生成するのを助けるために手動で介入することが多いんだ。

#相互再帰

最後に、翻訳は相互再帰も考慮してるよ。VDMでは、定義が互いに呼び出すことを許可しているんだ。VDMの型チェッカーからのアルゴリズムを使って、これらの関係を特定して必要な測度を導き出すことができる。

もし再帰グラフが自動的に発見できない場合は、ユーザーは互いに再帰的な定義の一つに注釈を付けて、関与する関数名を示さなきゃいけないんだ。

要するに、これらの相互作用は、すべての関連関数が一緒に定義されて、証明のセットアップで適切にリンクされることを保証する必要があるよ。

#結論

この記事では、VDMからIsabelle/HOLへの再帰関数の翻訳方法を概説して、基本型、集合、マップ、相互再帰に焦点を当ててる。議論された戦略は、複雑な例を含む多様な再帰定義を可能にするよ。今後もこの翻訳戦略を洗練させていくことで、VDM定義をIsabelle/HOLに変換するユーザーにとって価値のあるツールになるはず。今後の作業は、既存のツールにこれらの戦略をさらに実装して、ユーザーの利便性と自動化を高めることに取り組むよ。