日々の流転

λ. AOTS TA

大したことは何も出来なかったのに、人形を貰ってしまった。

λ. 多重疑惑

以前に同じ村に参加したことのある人に多重*1疑惑がかかってて、どうも黒っぽい……悲しい。

• 人狼BBS まとめサイト - C国多重荒らし検証ページ
• <URL:http://ex9.2ch.net/test/read.cgi/net/1140840402/435->

λ. instance Bounded Double

そういやDoubleとFloatってBoundedのインスタンスになっていないんだな。 知らなかった。

<URL:http://www.haskell.org/pipermail/haskell/2005-March/015490.html>

λ. Workshop on Linear Logic, Proof Theory and Computer Science (with Lecture Series by Jean-Yves Girard)

に行ってきた。 syd_sydさんやいろんな人にお会いできた。

疲れた。

Jean-Yves Girard (Marseille, IML), “Evolutions of Proof Theory Part I”

生の Jean-Yves Girald にワクワクドキドキ。

• internal と external がなんか良くわからなかった。
• Quantum coherent space とか Hilbert space とか色々わけわからん

昼食

初(UBU)

Naoki Kobayashi (Tohoku University), “Linearity and Order in Type Systems for Programming Languages”

わかりやすい。

f: File(R)

read once

f: File(C)

close once

f: !File(R)

read arbitary times

f: !File(R); File(C)

任意の回数読まれた後に閉じられる

XMLの処理の話を以前にちょっと聞いたときには、Lazyな関数型言語でパースも木の変換も全部lazyにやればいいじゃんと思ったものだが、あるマナーに沿ってトラバースしていることを保障する型システムは非常に面白いと感じた。

• Ordered linear channel types
• Orderdd linear resouce types
• Ordered lineer tree types

Martin Berger (Queen Mary, Univ of London), “Process Calculi and Interaction Types”

Aliasing があると、古典的なホーア論理の syntactic substitution に基づいた規則はうまくいかない。事前条件を詳細化する。例えば「 {(x≠y ∧ !x=7) ∨ (x=y ∧ !y=6)} y := !y + 1 {!x = 7}」。

Sylvain Salvati (NII), “Type systems for syntax”

Montague の話とか出てきてちょっと嬉しかった(ぉぃ

λ. Typed Logical Variables in Haskell. Koen Claessen, Peter Ljunglöf

• <URL:http://jp.citeulike.org/article/310660>

を読んだ。

論理型言語をHaskellに埋め込む話。そのために必要なのは論理変数とバックトラッキングで、型のある論理変数を実現するのにSTRefを使っている。バックトラキングはバックトラックを実装するモナドトランスフォーマーをSTの上に重ねて実現。STRefに書き込む部分では、バックトラックするときに元の値に戻すようにしておく。まあ、当たり前の方法を当たり前に実装したという印象。

バックトラッキングを実装するモナドトランスフォーマーは簡単な実装が示されているだけで、効率的な実装については Ralf Hinze の論文を参照とのこと。その辺りは Backtracking, Interleaving, and Terminating Monad Transformers とも比較してみるべきか。

λ. The dual of substitution is redecoration. Tarmo Uustalu, Varmo Vene

• <URL:http://jp.citeulike.org/article/355413>

確かに、変数を含む無限木に対しても substitution は考えるよなぁ。モナドはfreeなconstructionを扱うのに使うのに使うと思い込んでいたので、cofreeなconstructionに対してモナドを使うことは考えたことがなかった。

iterative monad の概念がいまいちピンとこないな……

Computational Category Theoryでは、substitutionをKleisli圏の射としてmguをcoequalizerとして扱っていた。双対的にredecorationをcoKleisli圏の射とするとequalizerには何か直観的な意味はあるか?

λ. 群の公理の問題

群の公理

• ∀x. 1 x = x
• ∀x. x^-1 x = 1
• ∀x,y,z. (x y) z = x (y z)

から

• ∀x. x 1 = x

を証明せよ。

以前にやったことあるし、とりあえず証明はすぐに出来た。

この群の公理の話はKnuth-Bendixの完備化手続きの例として良く出てくる*1のだが、実際に手で完備化をしようとしたら、規則がオーバーラップする場合を全て列挙する方法が良くわからなくて困ってしまった。俺駄目すぎ。また、列挙する順序によっては本来不要な規則を追加することになってしまうような……

λ. 萩野服部研納会＠聘珍樓

.

λ. unboxed 1-tuple makes sense

<URL:http://article.gmane.org/gmane.comp.lang.haskell.prime/1022> で、こんなことが書かれてあるのを見かけて驚いた。

　

Mmm, not quite. Unboxed tuples are boxed tuples restricted such that they never have to be stored on the heap, but this has no effect on semantics at all. A function returning (# Double,Double #) may still return two thunks.

Yes, this is why the unboxed 1-tuple makes sense :-)

indexArray# :: Array# a -> Int# -> (# a #)

最初、どういう意味があるのかサッパリわからなかったが、<URL:http://www.haskell.org/ghc/docs/5.00/set/primitives.html> の説明を見て、なんとなく理解できた。

Something a bit more interesting goes on when indexing arrays of boxed objects, because the result is simply the boxed object. So presumably it should be entered—we never usually return an unevaluated object! This is a pain: primitive ops aren't supposed to do complicated things like enter objects. The current solution is to return a single element unboxed tuple (see Section 7.2.2).

indexArray#       :: Array# elt -> Int# -> (# elt #)

λ. Unboxed types have kind #.

GHC では unboxed type は # という種(kind)に属していることを偶然知った。<URL:http://www.haskell.org/haskellwiki/Unboxed_type> には表題の「Unboxed types have kind #.」と書いてある。普通の型と扱いを変えるには種を変えてしまうのが確かに一番自然か。

Prelude> :set -fglasgow-exts
Prelude> :kind (# Int, Int #)
(# Int, Int #) :: (#)
Prelude> :module +GHC.Base
Prelude GHC.Base> :kind Int#
Int# :: #
Prelude GHC.Base> :kind Double#
Double# :: #

もっとも、ソースコードに「forall (a:: #). a -> a」みたいな型を書こうとするとパースエラーになってしまう。unboxed type は多相的なものではないのでエラーになるのは当然だが、パースエラーとは酷いwww

Prelude> :kind (forall (a :: *). a -> a)
(forall (a :: *). a -> a) :: *
Prelude> :kind (forall (a :: #). a -> a)
<interactive>:1:14: parse error on input `#)'
Prelude> :kind (forall (a :: # ). a -> a)
<interactive>:1:14: parse error on input `#'

λ. 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」
月（パチ）
照「後手、３五角」

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

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

λ. 素敵な定理 ∀x∀y∃R (x R y)

<URL:http://d.hatena.ne.jp/nuc/20050504/p3> より。

集合論で証明出来るのはもちろんだが、ここでは集合論はあまり本質的ではないように思う。一階述語論理では関係を量化出来ないので、関係を集合にエンコードして量化する必要があった。しかし、高階述語論理*1ならば関係を量化出来るので集合論に頼る必要はなく、あとは単に R = λa.λb. T とおけばこの定理は直ちに言える。また、R = λa.λb. (a=x)∧(b=y) とおけば最初の集合論での構成に対応したものになる。

λ. Audrey Tang 氏

<URL:http://en.wikipedia.org/wiki/Audrey_Tang>

Audrey Tang 氏って1981年生まれだったんだ。 知らなかった。

λ. Transactional Memory with data invariants. Tim Harris, Simon Peyton Jones

• <URL:http://lambda-the-ultimate.org/node/1388>
• <URL:http://research.microsoft.com/~tharris/drafts/2006-invariants-draft.pdf>

面白そう。