[B! sort] kirakkingのブックマーク

kirakking id:kirakking

sortに関するkirakkingのブックマーク (2)

[KMP77] を読んでみた - d.y.d.
17:53 14/12/22 ソートの逆流れクイックソートってあるじゃないですか、クイックソート。配列、たとえば [4,2,1,7,0,6,5,3] があったときに、小さい方を左に、大きい方を右にまず適当に集める。この「小さい方」と「大きい方」への二分割を、いわゆる再帰的に、分かれたブロック両方で同じ事を繰り返していくと… なんと、小さい順に並んだ配列 [0,1,2,3,4,5,6,7] が出来上がるというアルゴリズムです。逆向き！このデータの流れを「逆向きに」見てみたい。つまり、ソートが終わった最終状態から話が始まります。しかも、さっきから説明なしで意味ありげにくっついていた、「入力配列で元々どの位置にあったか」を表す値に注目していきます。 0の上に[4]がくっついているのは、最初は値0は配列のインデックス[4]の位置にあった、ということを意味しています。（上のソート
kirakking 2014/12/22
sort

algorithm
リンク
推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─ - λx. x K S K ＠はてな
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です．元々このネタは，後学期の3年生向けの実験でCoqを教える際に提示した「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです．このため，ここで紹介するプログラムや証明は，タクティクの種類やライブラリの利用が必要最低限に絞られているので，もしかしたら Coq 初心者の方にも参考になるかもしれません (各タクティクの作用を明確に理解してもらうため，敢えて auto も使いませんでした)． Coq 上級者には冗長な証明が気になるかもしれませんが，その点は予めご了承ください．はじめに比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ，クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します (逆に比較ソー
kirakking 2013/12/25
coq

proof

prover

sort
リンク
1