日々の流転

λ. 数学基礎論の考え方・学び方

講師

田中 一之 （東北大学大学院理学研究科数学専攻教授）

題目

数学基礎論の考え方・学び方

内容

ゲーデル以降，数学基礎論は何をしてきたか？ この講演では，論理，ゲーム，超限帰納法，不完全性などの基本概念を軸にして，数学基礎論の深化発展を振り返り，さらに最近の研究動向の例として私と仲間たちの研究も紹介する．

ポスター

これを聞きに行ってきた。

メモ

書きかけ。

• 数学基礎論とは何か?
  • 欧米ではロジックという呼び方が普及している。そのなかで数学の基礎を研究している人がいる。
• 現代論理学の始まりは不完全性定理を発見したとき。
  • 1930年9月5日 精密科学認識論会議 初日 各1時間の講演
    • カルナップ 論理主義
    • ハイティング 直観主義
    • フォンノイマン 形式主義
  • 翌日ゲーデルが完全性定理に関して20分の講演をし、(第一)不完全性定理についても簡単に触れた。
• 中世の普遍論争と比較すると
  • クワイン「何が存在するかについて」
  • 論理主義 = 実在論(realism) … プラトニズム
    • 普遍者は心の外に存在し、発見される
  • 直観主義 = 概念論(cenceptualism)
    • 普遍者は心の構成物として発明される
  • 形式主義 = 唯名論(nominalism) … オッカム
    • 普遍者は個物を抽象化した名前に過ぎない
  • ウンベルト・エーコ「薔薇の名前」
• 数学の思想対立の流れ
  • いろんな直観主義がある
  • カントル集合論 vs. クロネッカー算術化
  • ラッセル論理主義 vs. ポアンカレ直観主義
    • ポアンカレは数学的帰納法の論理的明証性を主張、非可述的定義を禁止
  • ヒルベルト形式主義 vs. ブラウワー直観主義
• 不完全性定理とヒルベルトのプログラム
  • イデアルな数学 … 無限とかを含む
  • リアルな数学 … 写実的な数学。有限記号列を有限に扱う
  • 記号化還元 : イデアルな数学→リアルな数学
  • コード化/算術化 : リアルな数学→イデアルな数学
  • HP1 : イデアルな数学からリアルな数学への還元
  • HP2a : リアルな数学の無矛盾性 x ← 第二不完全性定理
  • HP2b : リアルな数学の決定可能性 x ← 第一不完全性定理
• 不完全性定理
  • 第一不完全性定理から導かれる重要な結論は、再帰的でない集合の存在。たとえば、PAの定理のゲーデル数の集合 { ⌜A⌝ : PA ⊢ A } は再帰的でない。
• 再帰理論の点からの発展
  • Church
    • Kleene
      • Addison
    • Rosser
      • Sacks
        • Friedman
        • Simpson
        • Harrington
    • Turing
      • Gandy
        • Paris
  • KleeneとAddisonによるeffective記述集合論
  • Kreisel, Kripke, Sacks らによる admissible集合論
  • Friedmanが2階算術と逆数学について研究
  • ParisとHarringtonが新しい独立命題を発見
• 再帰理論はなぜロジックか?
  • ホップス … 唯名論、唯物論
    • 「あらゆる推論は、加算と減算に還元される」
  • ライプニッツ
    • 「ペンを持ち、机に向かい、計算しよう」
  • ブール
    • 「論理の計算」
  • ド・モルガン
    • 「形式論理学あるいは必然と可能の推論計算」
  • ヒルベルト
    • 「決定問題が数学論理学の中心問題である」
• 余談・集合論の誕生
  • 三角級数の一意性の問題
  • 加算順序数であれば実数に埋め込める
  • カントル・ベンディクソンの定理
• 公理的集合論のモデル
  • 1930 ツェルメロは集合論の累積階層モデルVを提唱
  • 1938 ゲーデルは集合論の構成可能モデルLを発明
• ゲーデルの重要コメント集
  • 「構成可能」という語は、非可述的方法を遮断する直観主義的意味に理解されたい。
  • 構成可能集合とは、ラッセルの分岐型理論を超限順序を含むように拡張して得られる集合である
  • 集合論は、それ自体で閉じた公理系をなしているのではなく、新しい公理によって拡張を行うように促している。そうした公理は、非常におおきな基数の存在を示す公理として形式化できる
• 余談. 連続体仮説の独立性
• 2階算術 = Hilbert-Bernays算術
  • 実連続関数は、可算個の有理数上の値で決定されているので、自然数の集合で表せる
  • RCA₀ は計算機の扱える数学
  • WKL₀ は RCA₀ に弱Königの補題を追加したもの
  • Π¹₁式で定義される集合の存在を要請する公理をRCA₀に加えたものがΠ¹₁-CA₀である。無限ゲームの決定性はこれをすぐ超える。
• ゲームの理論について
• ヒンティッカ・ゲーム 197?
• メタ・ヒンティッカ・ゲーム (T 1986)
  • Player I: 論理式φを選ぶ
  • Player II: 真か偽を選ぶ
  • 補題. I は必勝法を持たない
  • 補題. II が必勝法をもてば真偽が定義できる
  • 系. Δ⁰₁ゲームの決定性はPAでは証明できない
• 無限ゲーム
  • 注: Δ¹₁の決定性はZFC集合論で証明可能であり、その必勝法はΔ¹₂集合で見つけられる
• 二階算術と無限ゲーム
  • Δ¹₁の決定性は Z₂ でも証明できない
  • Δ⁰₂の決定性は Δ¹₂内包公理から証明できない
  • アプローチ (注: メモしそこなってそう)
    • Δ⁰₂ 決定性を証明するために、Π¹₁超限再帰公理を導入 (Weak axioms of determinacy and subsystems of second order arithmetic の話?)
    • Σ⁰₂ 決定性を証明するために、Σ¹₁ 単調帰納的定義を導入 (〃 の話?)
    • Δ⁰₃ 決定性を証明するために、Σ¹₁ ……を導入 (Weak determinacy and iterations of inductive definitionsの話?)
  • 二階算術の命題として簡単に書けるのに、二階算術の普通の公理からはなかなか出てこないのが面白い
• 超限帰納的定義
• 参考文献
  • 数の体系と超準モデル
  • 確かさを求めて
  • 数学の基礎をめぐる論争
  • 逆数学と二階算術
  • ゲーデルと20世紀の論理学
• 逆数学
  • 定理の方が自明であって、公理の方を探す
  • 数学基礎論というと基礎付けるということに重点が置かれてしまうが、それが中心的テーマだったのはデーデル以前。ゲーデル以降はむしろ考え方を反対にしている。
  • 基礎付けられないものをもってきて、それに還元するよりも、複雑なものをもってきてそれがどれくらい複雑化をみている(⇒ 逆数学)。
  • 代数と幾何のように、どっちが基礎かというのは今はもう意味はない。両方から見れるのが面白い。

関連

• 非専門家向け数学基礎論の考え方・学び方 - かがみさんの日記(2009-06-06)

λ. スコーレムの有限主義 by 出口 康夫

を読んだ。

λ. iPhoneのSMSのバックアップ

iTunesがバックアップしているファイルが、Windowsならば c:/Users/ユーザ名/AppData/Roaming/Apple Computer/MobileSync/Backup/iPhoneのID?/3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata とかにあるので、このファイルをバックアップしておけばよい。

このファイルはSQLiteのファイルなので、sqlite3 -csv -separator ',' 3d0d7e5fb2ce288813306e4d4636395e047a3d28.mddata "select * from message;" > output.csv でCSVに変換できる。

λ. “Data types á la carte” by Wouter Swierstra

• <URL:http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf>
• 10.1017/S0956796808006758

を読んだ。これは以下を使って、いわゆる Expression Problem を解決する話。

• 明示的な不動点の構成
  • data Expr f = In (f (Expr f))
• シグニチャ関手の埋め込みを表す型クラス
  • class (Functor sub, Functor sup) ⇒ sub :<: sup where inj :: sub a → sup a
• 定義したい関数毎の型クラス

例えば、式の型に乗算を追加して、それを扱えるように評価関数を拡張するには、以下のようなものを書くだけで良い。

data Mul x = Mul x x

instance Functor Mul where
  fmap f (Mul x y) = Mul (f x) (f y)

-- スマートコンストラクタ
infix 7 ⊗
(⊗) :: (Mul :<: f) ⇒ Expr f → Expr f → Expr f
x ⊗ y = inject (Mul x y)

instance Eval Mul where
  evalAlgebra (Mul x y) = x*y

ちょっと、「へぇ」と思ったのは、data Term f a = Pure a | Impure (f (Term f)) で定義されるモナド Term f は自由モナドだけど、Term自身もモナドの圏から関手の圏への忘却関手の左随伴になっているという意味で自由、という話。

あと、オーバーラップするインスタンスを使うから Haskell 98 じゃないと言っているけど、そもそも f :<: g という多引数の型クラスを使っている時点で Haskell 98 ではないだろと思った。

関連

• Data Types a la Carte | Lambda the Ultimate
• Wadler's Blog: Data Types a la Carte

λ. tDiaryを2.3.2にアップデート

この日記で使っているtDiaryを2.3.2にした。 一番の理由は、いい加減UTF-8化したくなっていたこと。 EUC-JPだと人名・数学記号・ソースコード(Agda2とか)を書くのが非常に面倒くさいことになってたので。 あと、iPhone判定ルーチンがデフォルトで入ってるという理由もあった。

アップデートして、disp_referrerの置換結果が文字化けするというの以外は特に問題なし。 ただ、category.rbのカテゴリはこれまでのEUC-JPなURIでは正常に表示されなくなっていたので、それはまずいだろうと思って、パッチを当てた(チケット #163)。

【2009-08-02追記】 変換結果が存在する実際に存在するカテゴリ名なのかを検査するようにパッチを更新した。category-to-native2.patch

【2009-08-22追記】 [Hiki-dev:01293]によると、「EUC-JPやISO-8859-1でvalidなバイトストリングはUTF-8としてvalidにはならない」らしいので、UTF-8としてvalidでないときだけ変換を行う簡易版パッチ category-to-native3.patch を作成。 ただ、Big5についても同様なのかはわからない……

λ. 『ツレがうつになりまして。』 細川貂々

読了。

λ. 数学基礎論を巡るつぶやき

週末にtwitter上で行われていたやりとりが非常に面白く、散逸してしまうのが勿体無かったので、まとめてみた。 しかし、twitter上のやり取りを後から追いかけるのは想像以上に大変だった……

• salmonsnare (#1 #2 #3 #4 #5 #6): 基礎の公理の成り立たない集合論 (non well-founded set theory) について, これって、AFA集合論のことか。引用「いずれにしても， 数学としては，基礎の公理の成り立たない集合の理論 （つまりその理論ですでに確立している結果や将来確立されるであろう結果の総体）が数学理論として 「美しい」，あるいは，「面白い」（ものになる）かどうかが， この理論の（数学理論としての）存在意義の評価を左右することになるのだろうと思います．」　この辺の議論の流れをつかみたい。昔、こういう資料を見つけて読んでいたことがある。超集合論—circularityの論理の現在—
• h_kagami (#1 #2): Axiom of Foundation を否定した「集合論」って集合論の本質的に重要な議論が全然できなくなると思います。「超」がついてるのであれなのですが、はたして「集合論」と呼べるのかどうかは疑問に思っています。もちろん AF を否定した「集合論」の研究を否定しているわけではありません。
  • kururu_goedel (#1 #2 #3): 基礎の公理が成り立たないモデルでの集合論は、有効な局面もある(とi-landさんが言っていた)のですが、その研究には基礎の公理が成り立っているモデルからの視点が不可欠になるだろうということです。 選択公理と決定性の公理の話と同様、どちらが正しいというレベルではなくて、どちらが与えられた状況下で有効かで見ていくべきものだと思います。そして、基礎の公理はとても強力かつ害が少ないので普段は仮定するほうが自然。 渕野先生が書いていらした文章も、結局はそういう切り口だったと思います。
  • ytb_at_twt (#1): すみません、基礎の公理の件ですが「基礎の公理はとても強力かつ害が少ないので普段は仮定するほうが自然。」というのは、standardな集合論者の偏見が混じっていませんか。
  • kururu_goedel (#1 #2): 確かに言葉の選び方が良くなかったです。ごめんなさい。偏見はもちろん入っていますし、それは込みで読んでいただきたいところなのですが(たかだかtwitterだし) 私が良くないと考えているのは、「基礎の公理は不自然なので仮定するべきでない」という見方であって、「不可欠｣は勇み足ですね。要は、ZFCとZF+ADの関係みたいになればいいなと思っているだけでして。
  • ytb_at_twt (#1 #2): ついでに、「その研究には基礎の公理が成り立っているモデルからの視点が不可欠になるだろうということです。」について、極論すれば「ZFの証明は自然数論の枠組みで形式化できるから集合論には自然数論の視点が不可欠」とか言えるような気もするのですが。 F先生が「数学の基礎」という言葉で何を意図されておられるのか、私には理解できません。
  • kururu_goedel (#1 #2 #3 #4): 私自身は『数学を展開するための基礎としての集合論』みたいな言い方からは微妙に距離をおいているつもりでいます。一般向けの文章でもプロポーザルでも立ち入り過ぎないようにしています。 そういうのを云々できるほど、哲学の知識も数学全体の知識もありません。謙遜でも逃げでもなく事実として。 でも、数学の多くがZFC上で展開できて、かつZFCに特有のテクニックを使って強力な議論を展開できるから、有効な見方のひとつであることは確かだと思うのですが。私にはそれで十分です。 つーか楽しいじゃんよーZFC。ZFC抜きでgeneral topologyできないじゃん。PCF使ってDowker space作ったり、minimal walk使ってL-space作ったり出来ないじゃん。つーか、俺の飯の種なくなるじゃん。
  • ytb_at_twt (#1): ZFC楽しいよねー。便利なツールも揃ってるし、ツール自体いじって楽しいし。ついでに、「基礎の公理はADなみに面白い」ってのにも賛成。それだけだったら、何の文句もありません。楽しい学会をお過ごしください。
• masahiro_sakai (#1): 外延性の成り立たない集合論を考えることすらあるのだから、それに比べれば、基礎の公理が成り立たない集合論なんてかわいいものだと思うけどなぁ。
  • h_kagami (#1): 道具としてではなく集合論そのものを研究対象とする場合、基礎の公理を否定したものを「集合論」とは呼びにくい気がします。
• masahiro_sakai (#1 #2): 渕野先生の 基礎の公理の成り立たない集合論 (non well-founded set theory) について には概ね異論はないけど、基礎の公理の成り立たない集合論を持ち出すことが、「大砲で雀を撃つ」ようなものという感覚は私には良くわからない。 基礎の公理の成り立たない集合論を使えば話が簡単になるところで、基礎の公理の成り立つ集合論の内部で作ったモデルを使って間接的に議論するのは、むしろ回りくどくはないのだろうか。

  • ytb_at_twt (#1 #2 #3): 渕野先生は

    1. ZFCは全ての数学の基礎である
    2. 解析学など、他の理論は全てZFCの中でコーディングされ展開される
    3. ZFCで直接は扱えないストリームなどを扱うZFAも、ZFCの中で展開される
    4. ZFAは、あくまでZFCの中で展開されるサブ理論であり、「数学の基礎ではない」
    5. ZFAを「ZFCと同等に重要」というためには、ZFAを「数学の基礎」と見なす必要がある
    6. しかし、そうすると、超限帰納法による既存の集合論の証明技術がoverkillされてしまう
    7. 「大砲(ZFAの基礎理論化)で雀（ストリームetc）を撃つ」のは、益少なく、無駄である。

    という感じだと思うのですが、いかがでしょうか。

    • masahiro_sakai (#1): 「意識のモデル，ないし概念認識のモデルを考察するときに」という前提で、基礎の公理と反基礎の公理のトレードオフを考えてましたが、「ZFAの基礎理論化」が前提なら納得です。
    • ytb_at_twt (#1 #2 #3): 渕野先生の論法の問題点は、彼の議論で重要な役割を果たす「数学の基礎としての集合論」と言う言葉の意味がよく分からないと言うことです。ZFAを研究している人は「数学の基礎」を目指している訳じゃない。 単に数学の論理的分析をするための枠組みならたくさんある。各種集合論、各種型理論、逆数学、etc. 異なる理論間の数学的内容の比較の共通プラットフォームとしては圏論があり、「その意味において圏論こそ数学の基礎だ」とAwodeyが絶叫していた。 渕野先生は「数学の基礎としての集合論」って言葉で何を意図しているのか理解不能だし、ZFAのような「数学の基礎としての集合論」を目指していない理論を、そうとなり得ないという理由で攻撃するのはお門違いではないかと思います。だから私は渕野先生に反対です。
    • masahiro_sakai (#1): 『ZFAのような「数学の基礎としての集合論」を目指していない理論を、そうとなり得ないという理由で攻撃するのはお門違い』というのも同意。これを読んで、渕野先生の文章に対してどこかひっかかっていたのが、すっきりしました。
  • kururu_goedel (#1 #2 #3): そういうのは私も同意するところなんですが、元々ZFCはその中で他の理論をモデル化するのが普通の利用法なわけで、考えているZFAのモデルがZFCの中で構成されているとイメージまたは仮定しても何の害もないような。 私のようなZFCの外にはほとんど出れないような人間でも、簡単な群論の問題を解くのにそれがZFCの中にあるものかなんて考えないわけですから。 あー、ZFCの中でモデル化したZFAのモデルには何らかの制限が加わるとかいうのなら、話は別なのですが。そのあたりよく知らないので。
    • masahiro_sakai (#1): それはその通りだと思います。ただ、モデルを使って考えることは、議論の単純さとかの点で、モデル化される理論を直接使って考えることの、完全なオルタナティヴにはならないのではないかと思って、あのように書きました。
    • h_kagami (#1: 「G を群とする」と言った途端群論のモデルを考えていることになると思いますが、そんなに不便でしょうか。
      • h_kagami (#1 #2): ちょっと真面目に考えたのですが。例えば V ≠ L の場合 L を「外側から」眺める観点は非常に有用です。 例えば AFA を理論として通常の集合論をモデルと考えた場合、その逆の場合、「外側から見る」という観点でどちらが面白いかという判断は有用かも知れません。
      • h_kagami (#1): どっちが理論でどっちがその内部で作れるモデルなのかの主導権争いみたいな感じもしないではない。あ。また余計なことを。
      • ytb_at_twt (#1): 主導権を主張しているのはF先生だということをお忘れ無く。
      • h_kagami (#1 #2 #3): 主導権と書いたのは余計なことでした。ただ集合論を道具としてではなく、その内部を研究されている方が、AF の否定という言明について「そんなばかな」と思われる気持ちはよく分かります。もちろん AFA について「そんなばかな」なんて言ってません。そもそも基礎の公理がないと清楚清純萌え萌え美少女ねたが使いにくくなるではないか。
    • masahiro_sakai (#1): うーん。念頭にあったのは、例えば自然数の乗算の可換性はペアノ算術だけで証明出来るのに、ペアノ算術のモデルを持ち出して議論するといったものです。
    • h_kagami (#1): 了解しました。たしかに範疇的な公理系を考える場合と非範疇的な公理系の場合ちょっと雰囲気が違うかも知れません。さらに集合論系は独特なので。
    • masahiro_sakai (#1): 私は範疇性について全然わかってないのですが、ここでは集合論が範疇的ということでしょうか? (そういえば、ZF2ではquasi-categoricityが成り立つとかなんとか昔聞いたような……)
    • h_kagami (#1 #2 #3 #4 #5 #6): 範疇性は例えば実数論のように公理と基数が与えれたときその基数であるモデルが唯一存在する理論だったと思います。すみませんいまいち自信なしです。 なんというかある種の対象を規定するための公理という感じだと思います。数論とか実数論とか実体があるという感じで。 群論みたいなのは「群」を規定するというよりも議論の仮定というニュアンスが強いかなと。 なので群論の場合理論で考えてもモデルで考えても特に違いはなくて、逆に範疇的な理論とそのモデルというのは扱いに違いがでるのではと。 集合論に関しては難しすぎて良く分からないです。ちょっといいかげんなこと書いたかも知れません。ごめんなさい。 例えば実数の可算モデルと言われると驚きますが、群論のなんとか基数モデルと言っても別に驚かないという感じでしょうか。
• h_kagami (#1 #2): 色々な批判を受けながらも数学の基礎としての集合論もすいぶん寿命が長いと思います。 数学の基礎という点ではいずれ新しい理論に道をゆずる日が来るかも知れません。そうなったとしても集合論内部の構造研究はまだまだ続くと思います。
• h_kagami (#1): ZFC が、色々批判もあるかと思いますが、いまのところ伝統的な数学的構造とそれなり相性が良い理由はよく分かりません。
• patho_logic: (#1 #2 #3): twitter 上の「数学基礎論を巡るつぶやき」残しておけないだろうか。このまま消えてしまうのがもったいない。断片的な発言を引いて「やっぱ基礎論怪しいね」みたいなことになると困る。

その後の話。

• yoriyuki (#1 #2 #3 #4 #5 #6): http://bit.ly/KIKuL だけど　そもそも *The* Foundation とは何か、という問いを立てているみたいだけど、あまり共感しないなあ。数学というのは、「雑多な技法の寄せ集め」だと思う。集合論の公理についていえば、http://dx.doi.org/10.1016/j.apal.2008.09.010 みたいに公理の強さを精密に測定していくというのが生産的だ。ちなみに基礎の公理はあまり強くなくて、外延性公理の方が強いらしい。

λ. iPhone OS 3.0 にアップデート

昨夜、寝る前は「更新ファイルを確認」を押しても今使っている2.2.1が最新だといわれてしまって、「もう更新できてる人いいなぁ」と思っていたら、朝になって更新来てた。 で、早速更新したら、更新自体はすぐ終わったのだけど、その後のアクティベーションが

申し訳ありませんが、SIMカードを読み取ることができません。iPhoneを接続し直してください。または電話会社にご来店いただき、SIMカードを交換してください。

というメッセージで失敗する。 で、この状態だと電話ネットワークだけじゃなくて、緊急電話を除く一切の機能が使えないのね……

それは困るので、再起動したり繋ぎなおしたり色々試したが、結局うまく行かなかった。 一応、PCの問題も疑って、別のPCで試してみたら、下のようなダイアログボックスが出てきた。

しかし、iPhone本体の画面はアクティベーション待ちのままで、パスコードも何も入力できず……

結局、夜帰ってきてから何度か試していたら、ようやくアクティベーションに成功した。が、もう何十回試したかわからんし、うんざり。 ようやく 3.0 の新機能を試せる……けど、なんかもうどうでもよくなってしまった。

「流石Apple、相変わらずのすばらしいクオリティだな」と思う素敵な体験をした一日だった。はぁ……

λ. TeXユーザの集い 2009

この夏、「TeXユーザの集い 2009」というイベントが開催されるそうです。 TeXに関わっている人は参加を検討してみてはいかがでしょうか。 発表も募集しています(締め切りは6月末日)。

日時

2009年8月29日（土）*1 9:30〜17:30（終了後に懇親会を開催します）

場所

東京大学生産技術研究所

招待講演

中野 賢 氏

目的

TeXに関する開発・活用例について発表すること、ユーザの立場から問題点や要望を発信すること、専門家のもつ組版技術の知識・理解を共有すること、交友を深めることなど

λ. 飲み会

某研修で同じクラスだった人たちで久しぶりに飲み会。 2年も経つと色々あるもんだなぁ。

λ. 『ドコモとau』 塚本 潔

読了。携帯電話業界にはこれまで全然興味なかったけど、なかなか色々あったんだねぇ。

λ. “Parsing Expression Grammars: A Recognition-Based Syntactic Foundation” by Bryan Ford

•  <URL:http://portal.acm.org/citation.cfm?id=964011>
•  <URL:http://pdos.csail.mit.edu/~baford/packrat/popl04/>
•  スライド

PEGのオリジナル論文だが、今頃になって読んだ。

PEGって理論的な性質とか全然証明されていないものだと思い込んでいたけど、結構色々証明されてるのね。 そんなことも知らずに、「CFG⊆PEGならO(n²)より小さな計算量のBMMが作れて矛盾、とか言えないんだろうか。」*1とか言ってたのかよ、という感じだけど。

面白かったのは、やはりPEGで表現できる空列εを含まない言語は、述語(predicate)を含まないPEGで表現できるという話。 述語を除去する変形がとても巧妙。

関連

• Parsing expression grammar (PEG) - ヒビルテ(2006-09-09)
• Packrat Parsing: Simple, Powerful, Lazy, Linear Time. Bryan Ford - ヒビルテ(2006-01-09)

λ. Σモノイド—メタ変数と明示的環境を持つ高階構文 by 浜名誠

を読んだ。後で書く。

λ. 鞄のベルトが壊れた

長年使っていたWWW2005鞄のベルトが壊れた。 流石にこれだけ長く使ってると色々ボロが出てくるなぁ。 ベルトだけ買ってきて交換すればいいかな……

λ. Bluetooth ヘッドフォンを購入

iPhoneがBluetoothヘッドフォンに対応したので、どうせだからBluetoothヘッドフォンを何か買ってみることに。どれにするかは結構悩んだんだけど、結局 SONY ワイヤレスステレオヘッドセット BT140QP ブラック DR-BT140QP/B にした。

注文した直後にmzpさんの「iphoneとsonyの組み合わせでブチブチ切れる」という話をきいて不安だったが、特に問題なかった。自宅だと二階と一階でも平気だった。

ただ、耳かけ型にしたのは失敗だったかも。これまでカナル型を使っていたんだけど、それに比べてこれは遮音性がまるで無いな。電車の中とかだと結構辛いかも。 それから、走ると落ちそうだし、ケーブルの触れている首が気になって仕方ないので、思ったほど開放感はない。

あと、遅延は割とある。GeekBreafTVをみてたら、動画と音が結構ずれてしまった。

λ. WAKE UP キャンペーン

住信SBIネット銀行の WAKE UP キャンペーン というのに当選。 さわやこおふぃというのを貰った。 わーい。

λ. ソフトバンクの2009Springキャンペーン

ソフトバンクオンラインショップ 2009Springキャンペーン でJCBギフト券1000円と microSD 2GB をもらった。 が、ギフト券はともかく microSD は iPhone だから使途がない……

λ. ICFP Programming Contest 2009

今年も Team Sampou というチーム名で ICFP Programming Contest に参加してた。 今年のメンバーは、私、nobsun、[1..100]>>=penさん、cut-seaさんという感じ。 オンラインでのやり取りにはChatonのhaskell-jpルームを使っていた。

• haskell-ja > Archives > 2009/06/26
• haskell-ja > Archives > 2009/06/27
• haskell-ja > Archives > 2009/06/28
• haskell-ja > Archives > 2009/06/29

今年は、しょうもないバグで時間を使いすぎて出遅れて、2002が誤差のせいでホーマン遷移一回ではクリア出来ないのをどうしようかと考えているうちに時間切れになってしまった、という感じ。 途中では300xの Eccentric Meet and Greet まではギリギリなんとかなるんじゃないかと思ってたけど、見込みが甘かったなぁ。 結局、2002はギリギリで解けたけど、最終的なスコアは Weighted Total Score 1002.1329 (8 problems solved) 。 とても楽しかった72時間だけど、今年も結果を出せなかったのは少し残念。

• 提出物 icfp09-0.20090630.250.tar.gz
• ちょっと修正版 ICFPC09-sakai-0.20090705.tar.gz

振り返り

Keep

可視化ツールを作ったこと

昨年のshinhさんとかを見て可視化重要と思ってたので、作ってみて、確かにそうだと思った。

Problem

分業が出来なかった。

分業すべきところで、分業出来てなかった。私が土曜日の午前中別の用事があって集まれなかったのが一因。まあ、みんな土台から自分で書きたがるしね。

しょうもないバグに悩みすぎ。

Input命令がSqrt命令にデコードされているとか、0xCAFEBABEが0xCAFABABEになってるとか、しょうもないバグで半日以上つぶれた。

過剰な抽象化レイヤ

昨年、あまりにアドホックなコードを書いてしまい収集がつかなくなってしまったことの反省から、今年はArrowベースのFRP(Functional Reactive Programming)とその上のタスク記述用のMonadを作ったんだけど、これは今回の問題には抽象化レイヤが過剰だった。結果として、それを作るために時間を使いすぎたし、また他の人がいじりにくくしてしまったと思う。

デバッグ用の口

上で書いた抽象化レイヤにはログ出力用の口を用意していなかったので、実行の様子の観察がtrace関数頼りになってしまっていた。ちゃんとログ出力用の口を用意しておくべき。

寝不足

興奮してあまり寝れていなかった。あまり眠気は感じなかったけど、やっぱり疲れてはいて効率は低下している。コードを書いていると気づきにくいけど、数学的な事を考えると、寝不足なのが直ぐにわかる。

Try

コードカバレッジツール

命令デコードミスについては、コードカバレッジツールを使えば、VMのコードの特定の部分が実行されないことから気づけたはず。GHC にも Haskell Program Coverage (HPC) が付属しているし、カバレッジツールは使えるようにはなっておこう。

ちゃんと寝る

ちゃんと寝よう。どうやったらいいのかわかんないけど。

関連

• ICFP Programming Contest 2007 - ヒビルテ(2007-07-20)
• ICFP Programming Contest 2008 終了 - ヒビルテ(2008-07-15)
• ICFPC 2009感想エントリとかリンク集 - hogeなlog(2009-07-01)