日々の流転

λ. 六法全書と朝鮮語の辞書を間違えて持ってきてしまった。欝だ。

λ. 人間と法

法的に問題がある事を「瑕疵(かし)」と呼び、その対処には「無効」と「取消」という2通りがある。「無効」は絶対に無効なのだけど、「取消」は一応の有効性を認めたうえでの対処。

λ. 自然言語論

強化文脈自由文法(augmented context free grammar)というのがあるそうだ。

λ. section, retraction, monomorphism, epimorphism

今日は section, retraction, monomorphism, epimorphism の辺りについて説明した。今回は準備不足で思うようにいかなかった。板書ミスをしまくるし、どうもコワレ気味。でも、正直この辺りの話はあまりやる気がしないんだよなぁ。早く発表したい部分に辿りつけるように、次回は頑張ろう。(発表資料)

石原君の発表で、自然演繹の紹介があったのだけど、「∧」と「⇒」の除去規則が知らない形で定義されていたのが面白かった。

 A∧B
─── (E∧)
  A

 A∧B
─── (E∧)
  B

 A⇒B  A
───── (E⇒)
     B

        [A,B]
          :
          :
  A∧B    C
─────── (E∧)
       C

          [B]
           :
           :
  A⇒B  A  C
─────── (E⇒)
       C

λ. カテゴリカルロジック

ロジックを、自然演繹やシーケント計算の代わりに、カテゴリ論的に扱ってやることが出来るらしいという話を聞いた。なるほどと思った。直感的には、命題をオブジェクト、命題間の導出を射とするようなカテゴリを考えれば良いのかな。Terminal Object を恒真、Initial Object を恒偽、Productを「∧」、Coproductを「∨」、Mapping Object を「⇒」と考えて……、あれ? 「¬」は?

[2005-05-29追記] もちろん「0^A」を「¬A」と考えればよい。

λ. 夕食

家族で「さぼてん」へ。

λ. ハムナプトラ / 失われた砂漠の都

を見た。蟲が怖かった。虫の映像が全く素晴らしい。これは夢に見そうだ。でも、スカラべ(糞転がし)って肉食だっけ?

ついでに、イムホテップという名前は、"這い寄る混沌" ナイアルラトホテップ を連想する。

λ. X・Files / ファイト・ザ・フューチャー

3月に撮っておいたのを見た。主立ったキャラクタはすべて登場してるし、スモーキングマンの回想のような形でストーリーが語られるのも良かった。日曜洋画劇場でやったなかでは一番面白かったと思う。

角田さんの日記が詳しい。

λ. Ruby 程式語言 (中国語繁体字)

紅眠の愛の秘密日記より。

λ. 『産直あづまマガジン 3』, 吾妻 ひでお

を読んだ。

λ. バグ?

以下のゴールをrefineしようとすると、「Id |(Wrap A) (In a1) (In a2) = ?197 is unsolvable since Expression a1 is not equal to a」等と言われてしまう。この文脈ではa,a1,a2の間には definitional equality が成り立っていないといけないと思うので、これはバグっぽい気がする。

--#include "Hedberg/SET.alfa"
open SET use Id, refId, Zero

data Wrap (A::Set) = In (a::A)

Bug (A::Set) (x,y::Wrap A) (p::Id x y) :: Set
Bug = case x of
        (In a1)->
            case y of
              (In a2)->
                  let f (q::Id a1 a2) :: Set
                      f = case q of
                            (ref a)->
                                {! Id p (refId (In a)) !}
                  in Zero

λ. モデル検査法のソフトウェア検証への応用. 中島震

コンピュータソフトウェア, Vol.23, No.2 (2006), pp.72-86.

を読んだ。 チュートリアルというよりはサーベイのような気がしないでもない。

今日は他の人たちと別府に行こうと思っていたのだけど、朝起きたら気持悪くて仕方なかったのでパス。午前中は寝たり、『カンディード』を読んだりしていた。古典は味わい深いなぁ。

午後になったら体調が良くなってきたので、またプールで1km泳いできた。今日は30分くらいで泳げた。 それから、フィットネスルームのオリエンテーションを受けて会員カードを作ってもらった。ちなみに、オリエンテーションをしてくれたインストラクタのお姉さんが綺麗だった。しかし、体力テストでのエアロバイクのスコア(?)が最低ランクで、予想通りとはいえ残念。明日からは昼勤で多分プールが開いている時間には行けそうにないので、フィットネスルームの方を活用したい。

λ. RHG読書会::東京 Practical Common Lisp

echo-stream 面白い。

λ. A,O,B,ABの比率が4:3:2:1として、任意に4人集めたときにその全員の血液型が異なる確率

A,O,B,ABの比率が4:3:2:1として、任意に4人集めたときにその全員の血液型が異なる確率

finalfusionさんの問題が面白そうだったので、素朴な確率モナドを使って、Haskellで簡単に解いてみた。

import Data.List (nub)
import qualified Data.Map as M
import Control.Monad

newtype Fractional w => P w a = P{ runP :: [(a, w)] }

instance Fractional w => Monad (P w) where
    return a = P [(a, 1)]
    m >>= f = P $ do
      (a,p) <- runP m
      (b,q) <- runP (f a)
      return (b, p*q)

random :: Fractional w => [(a,Integer)] -> P w a
random xs = P [(a, fromInteger w / s) | (a,w) <- xs ]
  where s = fromInteger $ sum (map snd xs)

data BloodType = A | O | B | AB deriving (Show, Eq)

bloodtype :: Fractional w => P w BloodType
bloodtype = random [(A,4),(O,3),(B,2),(AB,1)]

problem :: Fractional w => P w Bool
problem = do
  xs <- replicateM 4 bloodtype
  return $ length (nub xs) == 4

ans :: Double
ans = M.fromListWith (+) (runP problem) M.! True