推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─ - λx. x K S K ＠はてな
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です． 元々このネタは， 後学期の3年生向けの実験でCoqを教える際に提示した 「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです． このため，ここで紹介するプログラムや証明は， タクティクの種類やライブラリの利用が必要最低限に絞られているので， もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため，敢えて auto も使いませんでした)． Coq 上級者には冗長な証明が気になるかもしれませんが，その点は予めご了承ください． はじめに 比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ， クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソー
定理証明系 Haskell
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
