日々の流転

λ. 信頼や期待を裏切ることは心苦しい。信頼/期待されない事は心が楽だろうか?

λ. Channel Theory

竹内さんの「学習の経過」。情報射はInfomorphismの訳なのか。

λ. Classificationと情報射の圏

2日の定義は間違いで、⊨_A は「タイプとトークンの関係」ではなく「トークンとタイプの関係」だった。なので、修正。

λ. UMP

まずは、Terminal object, Initial object, Product, Coproduct について考えた。ちゃんと証明したわけではないけど、多分あってると思う。関係は直積の部分集合であることの注意。

Terminal object

• typ(T) = {x} (ie: singleton set)
• tok(T) = φ
• ⊨_T = φ

Initial object

• typ(I) = φ
• tok(I) = {x} (ie: singleton set)
• ⊨_I = φ

Product

projection map を p: A×B→A, q: A×B→B とすると、

• typ(A×B) = typ(A)×typ(B)
• tok(A×B) = tok(A)+tok(B)
• ⊨_A×B = {(x,y) | x = p_tok(a), a ⊨_A p_typ(y)} ∪ {(x,y) | x = q_tok(b), b ⊨_B q_typ(y)}

Coproduct

injection map を i: A→A+B, j: B→A+B とすると、

• typ(A+B) = typ(A)+typ(B)
• tok(A+B) = tok(A)×tok(B)
• ⊨_A+B = {(x,y) | y = i_typ(α), i_tok(x) ⊨_A α} ∪ {(x,y) | y = j_typ(β), j_tok(x) ⊨_B β}

λ. Agda

Agda をインストールした。AgdaはCoqやIsabelle/HOLなんかと同様の定理証明系(証明支援系)。特徴は証明を関数型言語のプログラムとして書く点だろうか。文法はHaskellに似ているが、dependent type も扱える。証明を独自の言語で書くのではなく、関数型言語の一般的な notation で書けるのは、私のようなプログラマには嬉しそうだ。

使ってみてまず驚いたのは再帰的な定義が好き勝手に出来る点。例えば、bottom (P :: Set) :: P = bottom P なんて定義も出来てしまう。Isabelle/HOL なんかでは「再帰呼び出しのときに、引数がある意味で必ず小さくなることを示すことが必要」だったけど、Agdaはこれで問題ないのだろうか!?

[2005-05-19 追記] Why Dependent Types Matter. Thorsten Altenkirch Conor McBride James McKinna には次のように書いてあった。

It's reasonable to allow arbitrary recursion in type-level programs, provided you have some sort of cut-off mechanism which interrupts loops when they happen in practice. This is the approach taken by the Agda proof system, Cayenne and by Haskell with `undecidable instances' —Haskell's overloading resolution amounts to executing a kind of `compile-time Prolog'. Agda restores logical soundness by a separate termination check, performed after typechecking. The basic point is that you include recursive programs in types at your own risk: mostly they're benign and typechecking behaves sensibly.

[2006-03-25 追記] 上記の bottom のような定義は、C-c C-x C-t で agda-check-termination にかけると "The call: bottom\n might lead to non-termination" と判定してくれる。停止性の保障に使ってるアルゴリズムは何なんだろう? Size Change Termination (SCT)?

もっとも、以下のように定義すると停止性チェックは通ってしまう。 このような場合をちゃんと扱うにはどうすればよいか?　また、これは GHCのinlinerの問題と似ているように思うがどうなのか?

data T (P::Set) = PsiInv (x :: T P -> P)
 
psi (|P::Set) (x::T P) :: T P -> P
  = case x of
    (PsiInv y) -> y
 
fix (|P::Set) (f::P -> P) :: P
  = let g (x::T P) :: P = f (psi x x)
    in g (PsiInv g)
 
id (|P::Set) (x::P) :: P = x
 
bottom (P::Set) :: P = fix id

[2006-03-25 追記] いや、以下のアッカーマン関数の停止性を認識できないので、SCTではないか。ソースを見ると、src/Termination.hs には「Based on "foetus" type checker of Andreas Abel and Thorsten Altenkirch (Ludwigs-Maximilians-University, 1997-1999).」と書いてあるので、Andreas Abel. foetus Termination Checker for Simple Functional Programs が元になっているのかな。まあ、どうでもいいけど。

data Nat = Zero | Succ (m::Nat)
 
ack (m::Nat) (n::Nat) :: Nat
  = case m of 
    (Zero   )-> Succ n
    (Succ m')->
      case n of 
      (Zero   )-> ack m' (Succ Zero)
      (Succ n')-> ack m' (ack m n')

λ. ホーンティング

安直で分かりやすい構図。ホラーという感じはあまりしないな。

λ. 五月病!?

どうもやる気が出ない。やらなくちゃいけないことは幾つかあるのだけど、取り掛かる気が億劫で仕方ない。困った。——困っていたら、これがひょっとしていわゆる五月病って奴なのではないかと思った。なるほど。そう考えたら、なんだか少し気が楽になった。気が楽になっただけで、問題は一切解決してないけど。

λ. 『ファイブスター物語 12巻』

を読んだ。個人的に見所だったのは、ダイ・グの苦悩とクリスティンの決意。それから、KOGがガクガクブルブルしてるのにウケた。いや、ストーリーよくわかってないんだけどね。

Quotation

もう泣かぬ……
もう恐れぬ

戦と血しか知らずに死んでゆくことを
恐れることはもうない

たとえ花壇に花は咲かずとも
私はもう一生に足りる恋をした！

陛下に赤子を千人殺せと言わるれば殺そう！
一国を滅ぼせと言わるればこの手で灰にしよう！

これ以上何を望むか！
生きる証はここにある！

λ. 知識発見法と古川研勉強会

• <URL:http://bruch.sfc.keio.ac.jp:5130/dsweb/View/Collection-1867>
• <URL:http://bruch.sfc.keio.ac.jp:5130/dsweb/Get/Document-13375/11-54-13-23-1.ppt>
• 窃盗犯にさせられるソクラテスwww
• 発想推論 + イベント計算 = Plannning
• ATMS = assumption-based truth maintenance system
• Prologメタインタプリタによるアブダクション。Prolog楽しい。<URL:http://web.sfc.keio.ac.jp/~mukai/2006-LP/04/practice/meta.html>
• 古川研:Abduction勉強会

λ. 大分二日目

憂鬱になったり、前向きになったり、気分が不安定な自分が嫌になる。

最寄のジャスコで必要なものを色々買ってきた。 帰りは暗くなっていたのだが、街灯がなく怖かった。 帰ってきてから、買ったヨーグルトを食べよう思ったのだが、そこでスプーンを買ってきていないことに気付く。ヨーグルトはああずけ。

Air-Edgeの64Kbpsは、テキスト情報だけをやり取りするだけならともかく、メディア系のデータを扱おうとすると辛い。たった6MBのポッドキャスト(読売ニュースポッドキャスト)をダウンロードするのに10分以上かかる。あと、Google Maps なんかも結構重い。ただ、SFC-GCのビデオはそれなりに観れた!

Ruby会議のチケット追加販売の情報が出てるな。 5/12は夜勤なので、朝ならチケットを買いに行ける。 今度こそ忘れないようにしないと。

λ. Chapter 9 の練習問題1

半順序集合PのAlexandrov位相と、Idl(P)のスコット位相が、フレームとして同型であることを示す問題。

準備

Idl(P)のスコット開集合aが与えられたとする。 各 x∈a は、Idl(P) の代数性より x = ⨆^↑{↓y | y∈P, ↓y⊑x } と表せる。 スコット開集合はdirected-joinによって到達不可能なので、ある ↓y∈{↓y | y∈P, ↓y⊑x } がaに含まれ、x∈↑↓y となる。 よって、{↑↓y | y∈P} はIdl(P)のスコット位相の開基。

証明

• Idl(P)のスコット開集合aに対して、Pのupper-closedな集合 φ(a) = {x∈P | ↓x∈a} を対応させ、
• Pのupper-closedな集合bに対して、Idl(P)のスコット位相 ψ(b) = ⋃{↑↓x | x∈b} を対応させる。

この対応がフレーム準同型になっていることは明らか。

同型になっていることを示す。

• φ(ψ(b)) = {x∈P | ↓x∈⋃{↑↓x | x∈b}} = {x∈P | ∃y∈b. y⊑x} = b
• ψ(φ(a)) = ⋃{↑↓x | x∈{x∈P | ↓x∈a}} = ⋃{↑↓x | x∈P, ↓x∈a} = a
  ここで開基であることを利用している。

解釈

algebraic dcpo 上のスコット開集合は、それに含まれるコンパクトな要素が決まれば決まるということ。

λ. ディスプレイ壊れた

急にデスクトップマシンのディスプレイが壊れた。 電源を入れると映るのだが数秒でフェードアウトして映らなくなる。 落ち込んでるときに嫌なことが重なるものだな……orz

ちなみに、使っていたのは、20030220#p01に買ったSotecのPC STATION SX6130Cとセットだったディスプレイで、MAG Innovision の Product No. MAG565 の Model No. 568 とかいうやつ。

λ. 虹

帰りに虹が見えた。 虹は綺麗だったけど、ちょっと不気味だなと思う。

λ. Google Code Jam 2010 Qualification Round

問題はそんなに難しい問題ではなかったのだけど、思いの他苦戦してしまった。 次のラウンドには一応進めたけれど、感覚が鈍ってるなぁ……

• Participant Details: sakai ― Code Jam 2010 Statistic

A. Snapper Chain

3問のうち一番苦戦したのがこの問題。 最初に書いたのは以下のようなプログラムで、Smallは簡単に解けるのだけど、Largeの上限のデータとかを生成して食わせると、とても終了しない。

{-# LANGUAGE Rank2Types, ScopedTypeVariables #-}
import Data.Array.ST
import Control.Monad
import Control.Monad.ST
import Text.Printf

f :: forall st. Int -> Int -> ST st Bool
f n k = do
  (power :: STUArray st Int Bool) <- newArray (1,n+1) False
  (state :: STUArray st Int Bool) <- newArray (1,n) False
  let updatePower = do
        writeArray power 1 True
        forM_ [2..n+1] $ \pos -> do
          b1 <- readArray power (pos - 1)
          b2 <- readArray state (pos - 1)
          writeArray power pos (b1 && b2)
      updateState = do
        forM_ [1..n] $ \pos -> do
          isPowered <- readArray power pos 
          when isPowered $ do
            isON <- readArray state pos
            writeArray state pos (not isON)
  updatePower
  forM_ [1..k] $ \_ -> updateState >> updatePower
  readArray power (n+1)

main :: IO ()
main = do
  t <- readLn
  forM_ [(1::Int)..t] $ \i -> do
    [n,k] <- liftM (map read . words) $ getLine
    printf "Case #%d: %s\n" i (if runST (f n k) then "ON" else "OFF")

Largeサイズの入力を扱えるようにと数回プログラムを書き直したが、その途中でトレースを表示して、初めて二進数のインクリメントになっている事に気づいた。 問題文の文章にちょっと騙された。

import Control.Monad
import Text.Printf
import Data.Bits

f :: Int -> Int -> Bool
f n k = and [testBit k i | i<-[0..n-1]]

main :: IO ()
main = do
  t <- readLn
  forM_ [(1::Int)..t] $ \i -> do
    [n,k] <- liftM (map read . words) $ getLine
    printf "Case #%d: %s\n" i (if f n k then "ON" else "OFF")

B. Fair Warning

Bは個人的には3問の中で一番簡単で、特に工夫は必要なかった。

import Control.Monad
import Text.Printf

f :: [Integer] -> Integer
f ts = (t - ((ts !! 0) `mod` t)) `mod` t
  where t = g ts

g :: [Integer] -> Integer
g ts = foldl1 gcd [ti - tj | ti <- ts, tj <- ts, ti > tj]

main :: IO ()
main = do
  c <- readLn
  forM_ [(1::Int)..c] $ \i -> do
    (n:ts) <- liftM (map read . words) $ getLine
    printf "Case #%d: %d\n" i (f ts)

【2010-05-27追記】 Google Code Jam 2010 Qualification Round — Scratch Leaf — MAYAH.JP によれば、上のソースのgは以下のようにすれば十分で、より少ない計算量で出来たらしい。そりゃそうだ。

g :: [Integer] -> Integer
g ts = foldl1 gcd [ti - t0 | ti <- ts', ti /= t0]
  where (t0:ts') = sort ts

C. Theme Park

最初に書いたのはC.hs。 Smallは当然解けるのだけど、甘い見積もりでLargeをダウンロードしてしまったら、時間内に解けなくて撃墜。 ちょっと工夫して、テーブル化して高速なべき乗法を使うようにしたら解けた(C2.hs)。 Largeはちゃんと性能的にも解けると確信してからダウンロードしないと駄目だなぁ。勿体無いことをした。 これは実際に参加してみて初めて感じた点。

【追記】 誰かがこの問題についてTwitterで「鳩ノ巣原理の良い例題」と書いていて*1、そのときは意味が分からなかったけど、後でku-ma-meさんに説明していて、そういう方法もあったと気づいた。