Agda で挿入ソートする
概要
Agda2 で挿入ソート関数を定義して、それがほんとにリストをソートすることを証明してみました。試すには Agda の標準ライブラリ(The Agda Wiki - Standard Library)が必要です。
冗長な証明になっている可能性は大いにあります。Agda のサンプルコードはあんまり見ない気がするので、誰かの参考になれば幸いです。
関数定義
インサート関数 insert と、リストをソートする関数 insertSort をごく普通に定義します。
"≤?" は Coq で言うところの SumBool 型の値を返す不等号演算子です。たぶん。こちらを使うと、条件分岐した先でその条件が仮定として使えるようになるので、後の証明がしやすくなります。
insert : ℕ → List ℕ → List ℕ insert x [] = [ x ] insert x (x' ∷ xs) with x ≤? x' insert x (x' ∷ xs) | yes p = x ∷ x' ∷ xs insert x (x' ∷ xs) | no ¬p = x' ∷ (insert x xs)
insertSort : List ℕ → List ℕ
insertSort =
insertSort (x ∷ xs) = insert x (insertSort xs)
ごく自然に ℕ とか使ってるあたりがきもいですね。標準ライブラリがそうなってるんだから仕方ないんです。ちなみに ℕ は agda-mode で \bn と入力すると打てます。
変な記号を打ちたい場合には id:mzp に教えてもらったサイト(Detexify LaTeX handwritten symbol recognition)もお使いください。
ゴール
まずは"ソート済み"という性質を表す sorted を定義します。
sorted : List ℕ → Set
sorted = ⊤
sorted (x ∷ ) = ⊤
sorted (x ∷ x' ∷ xs) = (x ≤ x') × (sorted (x' ∷ xs))
今回の証明の1つめのゴールは "ソート済みのリストに要素を insert してもソート済みのリストのままである" です。
{- 'insert' dosen't mess up the list -}
thmInsert : ∀ {x xs} → sorted xs → sorted (insert x xs)
2つめのゴールは "insertSort するとどんなリストもソート済みのリストになる" です。
{- 'insertSort' does sort the list -}
thmInsertSort : ∀ xs -> sorted (insertSort xs)
補題
"m が n 以下でない" ならば "n は m 以下である"
m≰n-n≤m : ∀ {x y} → (x ≤ y → ⊥) → y ≤ x
m≰n-n≤m {zero} {zero} p = z≤n
m≰n-n≤m {zero} {suc n} p = ⊥-elim (p z≤n)
m≰n-n≤m {suc n} {zero} p = z≤n
m≰n-n≤m {suc n} {suc n'} p = s≤s (m≰n-n≤m (λ x → p (s≤s x)))
"m が n 以下" であり "n が o 以下" であるなら "m は o 以下" である(不等号の推移律)
≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
≤-trans {zero} p q = z≤n
≤-trans {suc n} (s≤s m≤n) (s≤s m≤n') = s≤s (≤-trans m≤n m≤n')
ソート済みのリストの tail 部分はソート済みのリストである
leSubSorted : ∀ {x xs} → sorted (x ∷ xs) → sorted xs
leSubSorted {x} {[]} p = p
leSubSorted {x} {_ ∷ _} (_ , y) = y
自然数 x はリスト xs 内のどの自然数よりも小さいか等しい
_⊑_ : ∀ (x : ℕ) (xs : List ℕ) -> Set x ⊑ [] = ⊤ x ⊑ (y ∷ xs) = x ≤ y × x ⊑ xs
ソート済みのリスト xs の先頭に、xs 内のどの自然数よりも小さいか等しい自然数 x を追加したものは、ソート済みのリストである
leCons : ∀ x xs -> x ⊑ xs -> sorted xs -> sorted (x ∷ xs) leCons x [] p q = p leCons x (x' ∷ xs) (x0 , y) q = x0 , q
ソート済みのリストの先頭要素は、後ろのリスト内のどの自然数よりも小さいか等しい
leHeadIsMin : ∀ x xs -> sorted (x ∷ xs) -> x ⊑ xs
leHeadIsMin x p = p
leHeadIsMin x (x' ∷ xs) (x0 , y) =
x0 , lemma {x} {x'} {xs} x0 (leHeadIsMin x' xs y)
where lemma : ∀ {x y xs} -> x ≤ y -> y ⊑ xs -> x ⊑ xs
lemma {x} {y} {} p q = q
lemma {x} {y} {x' ∷ xs} p (x0 , y') =
(≤-trans p x0) , (lemma {x} {y} {xs} p y')
"insert x x' xs" は、"x' ≤ x" の場合には "x' :: insert x xs" と評価される。このとき x' が xs に x をインサートしてできるリスト内のどの要素よりも小さい
leConsToInsertedList : ∀ x x' xs -> x' ≤ x -> x' ⊑ xs -> x' ⊑ (insert x xs) leConsToInsertedList x x' [] p q = p , q leConsToInsertedList x x' (x0 ∷ xs) p (x1 , y) with x ≤? x0 leConsToInsertedList x x' (x0 ∷ xs) p' (x1 , y) | yes p = p' , (x1 , y) leConsToInsertedList x x' (x0 ∷ xs) p (x1 , y) | no ¬p = x1 , ih where ih = leConsToInsertedList x x' xs p y
証明
{- 'insert' dosen't mess up the list -}
thmInsert : ∀ {x xs} → sorted xs → sorted (insert x xs)
thmInsert {x} {[]} p = p
thmInsert {x} {x' ∷ xs} p with x ≤? x'
... | yes q = q , p
... | no ¬q = leCons x' (insert x xs)
(leConsToInsertedList x x' xs x'≤x (leHeadIsMin x' xs p)) ih
where x'≤x = m≰n-n≤m ¬q
ih = thmInsert {x} {xs} (leSubSorted {x'} {xs} p)
{- 'insertSort' does sort the list -}
thmInsertSort : ∀ xs -> sorted (insertSort xs)
thmInsertSort [] = tt
thmInsertSort (x ∷ xs) = thmInsert {x} {insertSort xs} (thmInsertSort xs)
感想
たかが挿入ソートですが、証明にはものすごい手間がかかりました。Agda に慣れていないというのが原因だとは思うのですが。ともあれ非常におもしろかったです。
あと Coq のタクティックのありがたみがわかりました :)
全ソース
tmiyaさんの練習問題をラムダ式で解いてみた
2010-09-26 を見て同じ命題を Agda2 で証明してみた。
Functional Programming Memo: [Coq] Coq-99 : Part 1
agda-mode が証明するのを手伝ってくれるのでお気楽です。
module Practice1 where data True : Prop where tt : True data False : Prop where data _∧_ (P Q : Prop) : Prop where ∧-intro : P → Q → P ∧ Q ∧-eliml : ∀ {P Q} → P ∧ Q → P ∧-eliml (∧-intro y y') = y ∧-elimr : ∀ {P Q} -> P ∧ Q -> Q ∧-elimr (∧-intro y y') = y' data _∨_ (P Q : Prop) : Prop where ∨-introl : P -> P ∨ Q ∨-intror : Q -> P ∨ Q ∨-elim : ∀ {P Q R : Prop} -> (P ∨ Q) -> (P -> R) -> (Q -> R) -> R ∨-elim (∨-introl y) a b = a y ∨-elim (∨-intror y) a b = b y ~_ : Prop -> Prop ~ p = p -> False infixl 10 _∧_ infixl 9 _∨_ lemma01 : ∀ (A B C : Prop) → (A → B → C) → (A → B) → A → C lemma01 a b c d e f = d f (e f) lemma02 : ∀ A B C → A ∧ (B ∧ C) → (A ∧ B) ∧ C lemma02 a b c d = ∧-intro (∧-intro (∧-eliml d) (∧-eliml (∧-elimr d))) (∧-elimr (∧-elimr d)) lemma03 : ∀ A B C D → (A → C) ∧ (B → D) ∧ A ∧ B → C ∧ D lemma03 a b c d e = ∧-intro (∧-eliml (∧-eliml (∧-eliml e)) (∧-elimr (∧-eliml e))) (∧-elimr (∧-eliml (∧-eliml e)) (∧-elimr e)) lemma04 : ∀ A → ~(A ∧ (~ A)) lemma04 a b = ∧-elimr b (∧-eliml b) lemma05 : ∀ A B C → A ∧ (B ∨ C) → (A ∨ B) ∨ C lemma05 a b c d = ∨-introl (∨-introl (∧-eliml d)) lemma06 : ∀ A → ~(~(~ A)) → ~ A lemma06 a b c = b (λ x → x c) lemma07 : ∀ A B → (A → B) → ~ B → ~ A lemma07 a b c d e = d (c e) lemma08 : ∀ (A B : Prop) → ((((A → B) → A) → A) → B) → B lemma08 a b c = c (λ x → x (λ x' → c (λ _ -> x'))) lemma09 : ∀ A → ~(~(A ∨ (~ A))) lemma09 a b = b (∨-intror (λ x → b (∨-introl x)))
とりあえず JapanTimes と NYTimes をクーリエ・ジャポンみたいに見るブックマークレット(超適当)
iPad 買いました。おもしろいです。土日は iPad を持って外出してましたが、電池切れになることはありませんでした。あとは Evernote をプレミアムアカウントにしてローカルにファイルを保存できるようにすれば、今週は寮に MacBook を持ってく必要がないかもしれない！
で、iPad で JapanTimes とかを読んでみたのですが、僕は英語が苦手なので、画面いっぱいにアルファベットが表示されると読む気が失せてしまうのです。そこで前に感動したクーリエ・ジャポンの UI みたいなのを実現するブックマークレットを書いてみました。ブックマークレットを読み込むと本文の最初のパラグラフをハイライトして、暗い部分をタッチすると次のパラグラフにスクロールします。
ただ、ものっそい適当です。ハイライトのスクロールが遅いし、いろいろずれるし。まぁこれからしばらく使ってみて、いい感じなら改良していくことにします。
(function(){ const db = { "search.japantimes.co.jp":"#mainbody > p", "www.nytimes.com":"#article p" }; const duration = 0.4; const paragraphs = document.querySelectorAll(db[window.location.hostname]); function createCover(pos){ var cover = document.createElement("div"); cover.className = "couriercover"; cover.style.position = "absolute"; cover.style.left = "0px"; cover.style.width = "100%"; cover.style.zIndex = 65535; cover.style.backgroundColor = "black"; cover.style.opacity = "0.5"; if (pos == "upper") { cover.style.WebkitTransitionProperty = "height"; cover.style.WebkitTransitionDuration = ""+duration+"s"; cover.style.top = "0px"; cover.style.height = "0px"; } else if (pos == "lower") { cover.style.WebkitTransitionProperty = "top"; cover.style.WebkitTransitionDuration = ""+duration+"s"; cover.style.top = ""+(window.pageYOffset+window.innerHeight)+"px"; cover.style.height = ""+(document.body.scrollHeight- (window.pageYOffset+window.innerHeight))+"px"; } document.body.appendChild(cover); return cover; } var upperCover = createCover("upper"); var lowerCover = createCover("lower"); function getRect(element){ function loop(element){ var top = element.offsetTop; var left = element.offsetLeft; if (element.offsetParent) { var rect = loop(element.offsetParent); return {top:rect.top+top, left:rect.left+left}; } return {top:top, left:left}; } var rect = loop(element); rect.top = rect.top; rect.left = rect.left; rect.width = element.offsetWidth; rect.height = element.offsetHeight; rect.bottom = rect.top+rect.height; rect.right = rect.left+rect.width; return rect; } function smartScrollTo(element){ var rect = getRect(element); if (rect.bottom > window.pageYOffset+window.innerHeight || rect.top < window.pageYOffset) { window.scrollTo(0, rect.top-10); } } function forcusTo(element){ smartScrollTo(element); var rect = getRect(element); upperCover.style.top = ""+window.pageYOffset+"px"; upperCover.style.height = ""+(rect.top-window.pageYOffset)+"px"; lowerCover.style.top = ""+rect.bottom+"px"; setTimeout(function(){ lowerCover.style.height = ""+(window.innerHeight-(rect.bottom-window.pageYOffset))+"px"; }, duration*1000); } var counter = 0; function next(){ if(counter<paragraphs.length) forcusTo(paragraphs[counter++]); } function prev(){ if(counter>0) forcusTo(paragraphs[--counter]); } upperCover.addEventListener("touch",prev,false); upperCover.addEventListener("click",prev,false); lowerCover.addEventListener("touch",next,false); lowerCover.addEventListener("click",next,false); next(); })()
Project Euler: Problem27
f(n) = n*n + an + b, |a|<1000, |b|<1000 である f に対し、 n に 0 から順に代入していったとき、素数が連続して最も長く出現するような a, b の値を求めよ。
こっちもがっちり C で。何も考えなくても Haskell より速い。素敵。
#include <stdio.h> #define MAX 1000 int isPrime(int x){ int i; for (i=2;i<x;i++) if (x%i==0) return 0; if (x<=1) return 0; return 1; } int euler(int a, int b, int n){ return n*n+a*n+b; } int main(){ int a,b,n; int max_a=0, max_b=0, max_n=0; for(a=-MAX+1;a<MAX;a++) { for(b=-MAX+1;b<MAX;b++) { for(n=0;;n++) if (!isPrime(euler(a,b,n))) break; if (n>max_n) { max_n = n; max_a = a; max_b = b; } } } printf("%d,%d:%d\n", max_a, max_b, max_n); return 0; }
Project Euler: Problem23
現在は工場実習中で毎日肉体労働をしてるので、休日くらいはプログラムを書きたくなります。というわけで超久しぶりに Project Euler をやってみたよ。
問題23。正の整数 n の約数の和が n をより大きいとき、 n を過剰数(abundant number)という。2つの過剰数の和で表すことができない正の整数の和を求めよ。ただし28123より大きい整数は2つの過剰数の和で表せることがわかっている。
Haskell で適当に書いたら止まらなかったので C で書き直した。
#include <stdio.h> #define MAX 28123 int sumOfFactors(int n){ int x,r; for (x=1,r=0;x<n;x++) if (n%x==0) r += x; return r; } int main(){ char abundands[MAX]; char result[MAX]; unsigned int sum = 0; int i,j; for (i=0;i<MAX;i++) result[i] = 0; for (i=0;i<MAX;i++) abundands[i] = sumOfFactors(i) > i; for (i=0;i<MAX/2;i++) if (abundands[i]) for (j=i;j+i<MAX;j++) if (abundands[j]) result[i+j] = 1; for (i=0;i<MAX;i++) if (!result[i]) sum += i; printf("%u\n", sum); return 0; }
twitter.com を改善する拡張を書いた
背景
修論で追い詰められた学生が、「twitter クライアントはたくさんあるけど、実際ブラウザで十分なんじゃね。他の拡張と組み合わせれば、かえって操作性が上がるかもしれない。」と思いつき、嫌だ力を駆使して集中力が切れるたびに少しずつ書いた拡張機能です。
機能
今のところの機能は
- "in reply to" が付いてる tweet をクリックすると、一連のやりとりが表示される
- 自動再読み込みっぽいもの
だけです。そのうち適当なキーバインドを付けたいですね。
果たして修論が終わったあともやる気がでるかどうか！
感想
- 他の拡張と組み合わせると、tweet 内のリンクを開いたりするのが便利
- 無事に卒業したい
LablGTK で遊ぶ
LablGTK(http://wwwfun.kurims.kyoto-u.ac.jp/soft/lsl/lablgtk.html) は、OCaml のための GUI ライブラリです。素敵です。
背景
インストール
ドキュメント
公式のドキュメントはLablGTKにあります。あとは、http://alohakun.blog7.fc2.com/blog-entry-579.htmlからリンクをたどって参考にしました。いくつかサンプルを見て、あとは公式のドキュメントを睨めばなんとかなる。
ソースコード
やんごとなき事情により、研究用に書いたコードは事情を知らない人にはとっても読みにくいことに今気がついた。
でもここまで書いたのにざっくり消すのは悲しいので、とりあえず簡単なアプリケーションを書いてみた。
ボタンを交互に押し込むだけのもぐらたたきアプリケーションだ！
open Event open GMain let change_availavility obj b = obj#misc#set_sensitive b;; let set_disable obj = change_availavility obj false;; let set_enable obj = change_availavility obj true;; let main _ = (* レイアウト設定 *) let window = GWindow.window ~border_width:5 ~title: "mogura-tataki" () in let layout = GPack.vbox ~spacing:5 ~packing:window#add () in let text = GEdit.entry ~editable:false ~packing:layout#add () in let buttons = GPack.hbox ~packing:layout#add () in let mogura1 = GButton.button ~label:"(*-*)" ~packing:buttons#add () in let mogura2 = GButton.button ~label:"(*-*)" ~packing:buttons#add () in text#set_text "COUNT: 0"; set_disable mogura2; let count = ref 0 in (* イベントハンドラ設定 *) window#connect#destroy ~callback:Main.quit; mogura1#connect#clicked ~callback:(fun _ -> set_disable mogura1; set_enable mogura2; count := !count + 1; text#set_text ("COUNT: "^string_of_int !count)); mogura2#connect#clicked ~callback:(fun _ -> set_disable mogura2; set_enable mogura1; count := !count + 1; text#set_text ("COUNT: "^string_of_int !count)); (* 開始 *) window#show (); Main.main ();; let _ = Printexc.print main ()
マルチスレッドですらない…。
OMakefile
LablGTK を使うときには gtkInit.cmo をリンクしないといけません。普通に FILES[] とかに書いちゃうと、 omake さんは gtkInit.ml から gtkInit.cmo を作ろうと頑張ってしまうので、OCAML_BYTE_LINK_FLAGS に書きます。
# これで正しいのかはわからないのですが、とりあえず動いてます
USE_OCAMLFIND = true OCAMLPACKS[] = unix threads lablgtk2 OCAMLINCLUDES += lablgkt2 NATIVE_ENABLED = $(not $(OCAMLOPT_EXISTS)) BYTE_ENABLED = $(OCAMLC_EXISTS) OCAMLCFLAGS += -thread -w -s -warn-error a OCAML_BYTE_LINK_FLAGS += gtkInit.cmo FILES[] = sampleapp PROGRAM = sampleapp OCAML_OTHER_LIBS += unix threads lablgtk .DEFAULT: $(OCamlProgram $(PROGRAM), $(FILES))
Thread とか Event を使わない場合、 unix とか threads とかはいらないと思われ。
