Haskell関数の正しさを証明/モデル検査/検証することは可能か？

質問

でのアイデアの続きです。 証明可能な実世界の言語はあるのでしょうか？

あなたはどうか知りませんが、私は 保証できないコードを書くのにうんざりしています。

上記の質問をし、驚異的な応答を得た後 (みんなありがとう!)、私は証明可能で実用的な、次のようなアプローチのために私の検索を狭めることに決めました。 ハスケル . 私が Haskell を選んだのは、それが実際に有用だからです (そこには が多い ウェブ フレームワーク のために書かれたもので、これは良いベンチマークと思われます) と 十分厳しいと思います。 機能的に であり、証明可能であるか、少なくとも不変量のテストを可能にするかもしれません。

私が欲しいものはこれです。 (そして見つけることができなかった)

psudocodeで書かれたHaskellの関数、addを見ることができるフレームワークが欲しい。

add(a, b):
    return a + b

- で、ある種の不変量がすべての実行状態にわたって保持されるかどうかをチェックします。私は何らかの正式な証明を希望しますが、モデルチェッカーのようなものに落ち着くでしょう。

この例では、不変性とは、与えられた値 a と b の場合、返り値は常に合計 a+b .

これは単純な例ですが、このようなフレームワークが存在することが不可能だとは思えません。確かに、テストできる関数の複雑さには上限があるでしょうが (関数への 10 文字列の入力は確かに長い時間がかかるでしょう!)、これは関数の設計をより慎重にすることを奨励し、他の形式的手法を使用することと変わりません。ZやBを使うとき、変数や集合を定義するときに、可能な限り小さな範囲を変数に与えるようにすることを想像してください。例えば、INTが100を超えることがないのであれば、必ずそのように初期化します。このようなテクニックと適切な問題分解によって、Haskell のような純粋関数型言語でも満足のいくチェックができるようになると思います。

私はまだ、形式手法やHaskellの経験があまりありません。私の考えが正しいかどうか、あるいはHaskellが適していないと思われるかどうか教えてください。他の言語を提案する場合は、それが "has-a-web-framework" テストに合格していることを確認し、原文を読んでください。 質問 :-)

どのように解決するのですか？

さて、Haskellのルートを取っているのだから、まずはいくつかのことを。

• をよくご存知ですか？ カレー・ハワード通信 ? これに基づいて機械的にチェックされた証明に使われるシステムがありますが、これは多くの点で、非常に強力な型システムを持つ単なる関数型プログラミング言語なのです。

• Haskellのコードを分析するために有用な概念を提供する抽象的な数学の領域に詳しいですか？代数のさまざまなフレーバーとカテゴリ理論のいくつかのビットがよく出てきます。

• Haskellは、すべてのチューリング完全言語と同様に、常に非終了の可能性を持っていることを心に留めておいてください。一般的に、あるものが次のようになることを証明するのははるかに困難です。 常に が真であることを証明するのは、何かが真であること、または非終端値に依存することのどちらかを証明することよりもはるかに困難です。

もしあなたが本気で 証明 でなく、単に テスト というようなことを念頭に置いています。基本的なルールはこうです。無効な状態がコンパイラのエラーの原因になるようにする。無効なデータが最初にエンコードされないようにし、面倒な部分は型チェッカに任せましょう。

さらに先に進みたいのであれば、記憶が私に役立つのであれば、証明の補助として Coq には、臨界関数に関する任意のプロパティを証明し、その証明を Haskell コードに変換することができる、quot;extract to Haskell" 機能があります。

Haskellで直接派手な型システムに関することをするためのもの。 Oleg Kiselyovがグランドマスターです。 . 彼のサイトでは、以下のような巧妙なトリックの例を見ることができます。 配列境界チェックの静的証明のための高ランク多相性型 .

より軽量なものについては、次のようなことができます。 タイプレベルの証明書を使って のように、データの一部が正しいかどうかチェックされたことをマークすることができます。しかし、他のコードは少なくとも、あるデータが実際にチェックされたことを知ることに依存することができます。

軽量な検証や派手な型システムのトリックから構築できるもう一つのステップは、Haskellが埋め込み用のホスト言語としてうまく機能するという事実を利用することです。 ドメイン固有言語 まず、慎重に制限されたサブ言語（理想的にはチューリング完全ではないもの）を構築し、それについて有用な特性をより簡単に証明することができます。そして、そのDSLでプログラムを使用して、プログラム全体のコア機能の重要な部分を提供します。たとえば、2 つの引数を持つ関数が連想的であることを証明し、その関数を使用してアイテムのコレクションを並列削減することを正当化できます (関数アプリケーションの順序は重要ではなく、引数の順序のみであるため)。

ああ、最後にもうひとつ。Haskellが含んでいる落とし穴を回避するためのいくつかのアドバイスがあります。ここでのあなたの不倶戴天の敵は 一般的な再帰 であり IO モナド であり、かつ 部分関数 :

• 最後は比較的簡単に避けることができます。書かないこと、そして使わないことです。パターンマッチのすべてのセットがすべての可能なケースを処理することを確認し、決して error や undefined . 唯一厄介なのは、エラーを引き起こす可能性のある標準ライブラリ関数を避けることです。いくつかは明らかに安全でないもので、例えば fromJust :: Maybe a -> a や head :: [a] -> a などがありますが、他のものはもっと微妙かもしれません。もし、本当に、本当に、ある入力値に対して何もできない関数を書いていることに気づいたら、入力タイプによってエンコードされる無効な状態を許可しているので、まず、それを修正する必要があります。

• 2つ目は表面的なレベルで簡単に回避できることで、様々な純粋な関数を通してものを散らし、それを IO 式から使用されます。それよりも、できるだけプログラム全体を純粋なコードに移動し、実際の入出力以外のすべてで独立して評価できるようにする方がよいでしょう。これは、外部入力によって駆動される再帰が必要な場合にのみ、大抵は厄介なことになります。

• 賢者への言葉 根拠のある再帰性 そして 生産的な重回帰 . 再帰的関数は常に、ある出発点から既知の基本ケースに向かうか、要求に応じて一連の要素を生成していることを確認してください。純粋なコードでは、これを行う最も簡単な方法は、有限のデータ構造を再帰的に折りたたむことです（例．または、遅延データ構造（例えば、ある値に対する近似値のリスト）を再帰的に生成することですが、この2つを直接混在させないように注意してください（例えば、ある条件を満たすストリーム内の最初の要素を単に" 見つけるのではなく、それは存在しないかもしれません。その代わりに、ある最大深度までストリームから値を取り、それから有限のリストを検索し、見つからないケースを適切に処理します）。

• 最後の2つの項目を組み合わせると、本当に必要な部分については IO を必要とする部分については、プログラムをインクリメンタルなコンポーネントとして構築し、すべての厄介な部分を単一の "ドライバ" 関数に凝縮してください。例えば、GUIイベントループを次のような純粋な関数で書くことができます。 mainLoop :: UIState -> Events -> UIState のような純粋な関数でGUIイベントループを書き、終了テストは quitMessage :: Events -> Bool 保留中のイベントを取得するための関数 getEvents :: IO Events そして、アップデート機能 updateUI :: UIState -> IO () のような一般化された関数で実際に動かしてみてください。 runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO () . これは複雑な部分を本当に純粋に保ち、イベントスクリプトでプログラム全体を実行し、その結果のUI状態をチェックすることができます。一方、厄介な再帰的入出力部分は単一の抽象関数に分離され、理解しやすく、多くの場合 パラメトリック .