日々の流転

λ. Calculational Proof っぽい書き方

等式の証明は大抵は A=B=C=D といった等式の連鎖で表されるが、これはAgdaでは書きにくい。Agdaでは普通は以下のような感じで書くことになるが、式が複雑になることを考えるとBやCの式が複数回出現するのが嫌。また、lem1等と名前を付けずに直接tranIdの引数として書いてしまうことも出来るが、そうすると今度は読みにくくなってしまう。

let lem1 :: Id A B
       = ?
    lem2 :: Id B C
       = ?
    lem3 :: Id C D
       = ?
in lem1 `tranId` lem2 `tranId` lem3

そこで、通常の calculational proof 風の書き方をDSLとして実現できないかと考え、次のようなものを用意してみた。

calc (|X::Set) (x::X) :: Id x x
  = refId x

(:=) (|X::Set) (|x,|y,|z::X) (id1::Id x y) (id2::Id y z)
  :: Id x z
  = tranId id1 id2

by (|X::Set) (|x::X) (y::X) (id::Id x y) :: Id x y
  = id

triv (|X::Set) (|x::X) :: Id x x
  = refId x

これを使うと例えば以下のような書き方が出来る。 演算子の優先順位やらの関係でちょっと不恰好だが、結構便利だ。 「型理論での形式的証明記述の技法について」(20050917#p01)で紹介されていた Chain を使う方法よりもずっと便利なのではないかと思う。

add_assoc (a,b,c::Nat) :: Id (a+(b+c)) ((a+b)+c)
  = ?

distl (a,b,c::Nat) :: Id ((a+b)*c) (a*c + b*c)
  = case a of 
    (zer   )-> refId (b*c)
    (suc a')->
      calc ((a+b)*c)
       :=( (((succ a')+b)*c)    `by`  triv )
       :=( ((succ (a'+b))*c)    `by`  triv )
       :=( (c + (a'+b)*c)       `by`  triv )
       :=( (c + (a'*c + b*c))   `by`  mapId (\x-> c+x) (distl a' b c) )
       :=( ((c + a'*c) + b*c)   `by`  add_assoc c (a'*c) (b*c) )
       :=( ((succ a')*c + b*c)  `by`  triv )
       :=( (a*c + b*c)          `by`  triv )

λ. デスノートネタ

<URL:http://etc4.2ch.net/test/read.cgi/wcomic/1143480199/213> のネタがツボだった。

page.103「宣伝」

照「…37」
月「…」
照「…38」
月「…」
照「…39」
月（パチ）
照「後手、３五角」

照「…じゅーびょ〜」
ニア「…」

照「…にじゅーびょ〜」
ニア「…」