日々の流転

λ. 常識力検定

サイトに載っている三問は当然ながら全問正解したけど、なんだかなぁと思った。

λ. Amaya

Amayaのソースコードを眺める。wchar_t == Unicode を仮定してるし、マルチバイト文字の事なんか全然考えてないし、文字列とバイト列の区別も付いてないところもあるし、他にも色々とダメすぎ。CHAR_Tという型が#defineされていて、この中身は_I18N_が定義されている場合にはwchar_t、そうでない場合にはcharになるんだけど、CHAR_Tを使って宣言されている関数が、charで実装されていたりして嫌になる。こいつを国際化するなんて、ひょっとして僕はとんでもない難題を引き受けてしまったのだろうか…

λ. とりあえず、gdk_font_loadしてる部分をgdk_fontset_loadに置き換えた。次はUnicodeと他のコードとの変換処理にiconv等を使えるようにしよう…

λ. Alan Kayの講演会

Alan Kayの講演会があったんだけど、寝忘したため他の用事が片付かず、行くことが出来なかった。残念。

λ. 嬉しいコメント

学部二年の方から、僕のページについて嬉しいコメントをもらいました。

λ. google://税効果会計 (約20,300件)

いま盛んに耳にする「税効果会計」って、結局どういうものなのか、いまいち良く分からない。

λ. 予算編成論

ゲストスピーカーが決まった。長野県知事の田中康夫氏と財務省の田中秀明氏。田中秀明氏を『構造改革論の誤解』の田中秀臣氏と一瞬勘違いしてしまった。

λ. KNOPPIX

こないだのknoppixのCDを学校の貸し出しlaptopで試してみた。

λ. 萩野服部研

RQL班の進捗状況(?)について説明。スライドの作成にはMing/Slideを試してみた。お手軽なのは良いのだけど、はみ出さないように文章を削ったりとか本質的でない努力をする必要があった。

安達さんがファイルシステムについて発表していた。興味を惹かれたのはファイルシステムが何のために存在するのかという話。僕は、ファイルシステムの体現する思想というのは ものにはすべて名前がある という事に尽きると思うし、ファイルシステムの目的は名前のための空間を提供する事だと思う。ところで、MINIX本を読んでいるみたいだけど、Practical File System Design with the Be File System とかはどうですかね?

λ. From Algebras and Coalgebras to Dialgebras

紹介されたので印刷してみる。

この Erik Poll って、春学期の最後に向井研で簡単に発表した論文 "Subtyping and Inheritance for Categorical Datatypes" の著者と同じ人ですね。

λ. 『あなたは虚人と星に舞う』, 上遠野 浩平 [著], 中澤一登[イラスト]

を読んだ。

λ. 建碑法要など

小雨(?)の中、建碑法要。 ビストロ ラ・シャンソン デリカテッセン デリシューで昼食。 プールで1km泳いでから帰る。

λ. 計算機言語で定理証明 (Proof Party.JP)

計算機言語で定理証明とかいう、なんだか良く分からないし怖そうなイベントに参加してきた。

Agdaについては池上さんやranhaさんが紹介してくれるだろうから、対話型定理証明器をdisって、自動定理証明器の素晴らしさを語ろうと思っていたのだが準備が間に合わず、会場でずっとごにょごにょ作業していた。あんまり他の人の話を聞いてなくて済みません m(_ _)m

しかし、対話型定理証明器をdisろうと思っていたのだけど、私がそんなことをする以前にAgdaはフルボッコだった。 一方、Coqはやっぱり凄いなぁ、と思った。

お題

以下、作ったものとか色々。

さんすう

• 自然数(エンコーディングは問わず)の加算での可換法則、結合法則、分配法則を証明。
• (1 + 2 + ... + n) = n*(n+1) / 2 の証明

自動定理証明器である The E Equational Theorem Prover (eprover)に証明させてみた(nat.tptp)。 帰納法が必要なのだけど、普通の自動定理証明器は公理型(axiom schema)を書けないので、帰納法のインスタンスを個別に書く必要があって面倒くさい。 また、割り算の定義が面倒くさかったので、(1 + 2 + ... + n) = n*(n+1) / 2 の代わりに両辺をニ倍した (1 + 2 + ... + n)*2 = n*(n+1) を扱っている。

おまけに、Jahobでも証明をしてみた(Nat.java)。 実行結果(jahob-nat.txt)。 (1 + 2 + ... + n) = n(n+1) / 2 の証明に関しては、ホーア論理 - ヒビルテ(2003-05-16)も参照。

すうがく

• Bolzano–Weierstrassの定理(収束するとかいうヤツの方)
• 中間値の定理(The Intermediate Value Theorem)
• むしろ実数の構成周辺を埋める?

時間がなくて手を出せず。

kikxさんがCoqで華麗に証明していて痺れた。

アルゴリズムの性質

• concat(l1,concat(l2,l3)) = concat(concat(l1,l2),l3)を証明する。
• reverse (reverse list) = list : リストのリバース　のリバースが元のリストと等しい事を証明する。
• あるソート関数がちゃんとソートする事を証明?(ソート関数が何かはご自由)

concatとreverseに関する証明は「さんすう」と同様にeproverに証明させた(list.tptp)。 この問題は「さんすう」よりも遥かに簡単。

ソートに関しては、バブルソートの部分正当性をJahobで証明した(BubbleSort.java, Node.java)。 実行結果(jahob-bubblesort.txt)。 本当は最初はクイックソートの方の証明を試みていた(Quicksort.java)のだけど、現在公開されているJahobは関数呼び出しを正しく扱えないようなので断念。 あと、論文 An Integrated Proof Language for Imperative Programs に書いてあったカッコいい機能を使いたい場面があったのだけど、現在公開されているバージョンには実装されてなくて、しょぼーんという感じだった。

それから、こないだクイックソート関数をAgdaで定義したので、これがちゃんとソートを行う関数になっていることを証明するというのも、時間があったらやってみたかった。 まあ、これは出来るのは分かりきっていて、面倒くさいだけの話だけど。

数理論理学

• 1階命題論理でresolutionが成り立つ事を示す
• 直観主義論理での二重否定除去と排中律の同値性

resolutionに関しては、自動定理証明器の基づいているものなので、まあ導出できて当然。 resolution.tptp

二重否定除去と排中律の同値性については、普通の自動定理証明器は直観主義論理ではなく古典論理に基づいているので、パス。 ところで、そういえば直観主義論理のための自動定理証明器というのは、あまり聞かないな。何でだろう……

自動定理証明以外なら「二重否定除去⇒排中律」は以前2006-04-29にHaskellで書いた。 逆の「排中律⇒二重否定除去」も一応Haskellで書いておく(こっちはかなり自明だけど)。 命題論理の範囲ならAgdaよりもHaskellの方がお手軽。

{-# LANGUAGE RankNTypes, TypeOperators #-}

type Absurd = forall a. a
type Not a = a -> Absurd
type a `Or` b = Either a b

em2callcc :: (forall x. x `Or` Not x) -> (forall x. (Not (Not x) -> x))
em2callcc em nnx =
    case em of
      Left x -> x
      Right nx -> nnx nx

パズル

• 何か簡単なモノ
• 最もスタンダードなハノイの塔で、最短の手数が(2^n)-1に成る事を示す。

時間がなくて手を出せず。

簡単では無い系

• Church-Rosserの定理(型無しλ計算の合流性証明)
• 古典一階命題論理の完全性証明(ヒルベルト流 Lukasiewiczの公理系)

時間がなくて手を出せず。ただ、これは自動定理証明器では難しそうだ。

Church-Rosssrの定理は以前Agda1で書いて、去年の Haskell Hackathon in 2008 September のときにAgda2向けに書き直した(ただし未公開)のだけど、束縛を nested types で表した関係で素直な再帰にならなくて、停止性検査を通っていない状態なので、この機会になんとかするというのもやってはみたかったんだけど……

その他

• お昼:
• Domino On Acid - Natural Deduction Visualized As A Game Of Dominoes
• カタン
• 焼肉

関連リンク

• #proofparty
• Proof Party の問題をCoqで挑戦 - にわとり小屋でのプログラミング日記 (2009-10-23)
• Haskell Not 98 - Yet Another Ranha (2009-10-23)
• 定理証明の会で実演した中間値の定理の証明 - 菊やんの雑記帳 (2009-10-26)
• 計算機言語で定理証明#1 - Yet Another Ranha (2009-10-27)