クイックソートは半順序でもソート可能であることをCoq/SSReflectで証明する - Qiita
はじめに 前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。 定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。 クイックソートを定義 SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。 そこでCoqでクイックソートを定義します。 まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義
関数の仕様を正しく実装していることをどう保証するのか - $shibayu36->blog;
静的型チェックがあったらテストはあまり書かなくて良いのか - $shibayu36->blog; で静的型チェックがあったとしても、テストをあまり書かなくて良いわけではないという話を書いた。するとブコメでいろいろ意見をもらえた。これらの意見から、関数の仕様を正しく実装していることをどう保証するのかについてもう少し深く考えてみようと思い、その考えがまとまってきたので、ブログに書いておく。 一応前提として、今回の話は自分の経験とこれまでの本を読んだ知識を元に自分で考えたものであり、何かの理論に則って話しているわけではない。この部分が違うなどあれば突っ込みを受けたい。 今回考える仕様 このようなことを考える時、非常にシンプルに考えたほうが理解がしやすいので、以下の様な仕様を持つ関数addNaturalIntを考える。 関数addNaturalIntは正の整数を二つ受け取り、足しあわせて正の整数を
型理論 なんて自分には関係ないと思っているあなたへ
This document contains definitions and proofs about natural numbers, functions, and theorems in Coq. It defines natural numbers as inductive types, defines addition as a recursive function, and proves theorems like 1+1=2. It also contains definitions for monads and proofs about monad bind being associative in Coq.Read less
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
