日々の流転

λ. 「型の型」問題

LL Future のスタッフ&発表者の打ち上げ*1で「型の型」についての話が出たらしい。 あろはさんのTwitterの<URL:http://twitter.com/alohakun/statuses/904102768>や、東京行ってきた - 黎明日記とそのコメント欄で、その辺りの話が出ていたので、ちょっと簡単な説明を書いてみる。

HaskellとかCCの場合

まず、Haskellの場合。 Haskellでは型の型は「種(kind)」と呼ばれていて普通の型とはレベルの異なるものになっている。つまり、型の型は普通の型ではない。

種について簡単に説明する。 例えば、Bool や Maybe Bool などの型は * という種に属する。 また、Maybeという型構築子は * に属する型を受け取って * に属する型を返す関数なので、*→* という種に属する。また、一般化薔薇木のデータ型 data GRose f a = GBranch (f (GRose f a)) で定義される型構築子 GRose は (*→*)→*→* という種に属する。 種の存在意義は型をパラメータとして受け取るような何かを型付けすることだ。 Haskellの場合にはその「何か」には、Maybe :: *→* や GRose :: (*→*)→*→* のような型構築子と、[] :: ∀a::*. [a] や map :: ∀a::*. [a]→[a] のような多相的な式との二つがある。

このようなHaskellの型システムの背景にはFωやλωと呼ばれる型理論が存在していて、Fωにさらに依存型を追加するとCC(Calculus of Construction)やλCと呼ばれる型理論になる。

ところで、型の型が種なら、種の型はなんだということになるが、CCではそれは考えないし、λCでは便宜的に定数記号 □ に属するということにしている。 何故かというと、これらの型理論では種を受け取る「何か」を扱わないから、種の型を考える意味があまりないため。

AgdaとかCoqの場合

CCのような型理論とは毛色の違う型理論もある。

例えば、Agdaの型理論では通常の型はSetに属するがSet自身はSetには属さない。その代わりSet1という型があり、これがSet1を要素かつ部分として含む。さらに、Set2はSet1を要素かつ部分として含み、Set∈Set1∈Set2∈… という風に型の宇宙が累積的階層をなしている。 ある階層に属する型を集めた全体(型の型)は、その階層自身には属さずに一つ上の階層に属するものになる。 つまり、「型の型」は同じレベルの型ではない。

一方、Coqの型理論では通常の型はSetに属してSetはTypeに属している。そして、Typeは構文的にはType自身に属する、すなわち Type∈Type なのだけど、これは文字通りの「Typeの型はType」という意味ではない。 CoqのTypeは実のところ単一の型ではなく、Type と書いたものは実際には適当な自然数αをおいて(Agdaでいうところの) Setα として解釈されている。そして、Type∈Type は実際には Setα∈Setβ と α<β という制約とを表しているのである*2。 なので、意味的にはAgdaの場合と同じで、「型の型」は同じレベルの型でない。

何故「型の型」を型にしないのか?

CCの場合にしても、AgdaやCoqの場合にしても、なんでこんなにややこしい仕組みにしているかというと、素朴に型全体の型SetもSet自身に属すると考えると、ジラールのパラドックス(Girard's paradox)*3が成り立ってしまうため。 ジラールのパラドックスが成り立ってしまうと、論理体系としては矛盾してしまうし、計算的にも強正規化性が成り立たなくなってしまって、まああんまりよろしくない。

2008-09-10追記

ytbさんが Martin-Lofの V∈V 理論とそのパラドックス - あいまいな本日の私 というエントリでジラールのパラドックスについて面白そうなことを書いているのを発見。

λ. 飲み会

• AdS/CFT対応
  • Anti de Sitter space
    • Black hole
    • 5次元の超重力理論
  • Conformed Field Theory
    • 四次元の場の理論 guage theory
  • Juan Maldacena
• 量子色力学 (Quantum Chromodynamics, QCD)
• 大栗博司 (Hirosi Ooguri)
• Atiyah-Singer の K-theory
• Mr. guage 理論 Gerard t'Hooft

ホログラフィー原理の話を知っていたら、ちょっと感動されてしまった。もっとも、私は エレガントな宇宙 や Decoding Universe でちょっと読んだくらいの知識しか知らないのだけど。

λ. “Models of LCF” by Robin Milner

PCF and LCF | Lambda the Ultimate より。そういえば、PCFとかLCFってちゃんと勉強したことないなぁ、と思って読んでみた。typoが結構多い上、このPDFはページ順も変なので注意。内容は、不動点演算子を持つ型付きラムダ計算を古典領域理論で解釈し、半順序関係 a≦b を原子命題とする論理LCFの推論規則がこの解釈に対して健全であることを示したもの。

λ. 「君の身体を変換してみよ」展

ICC ONLINE | ICCキッズ・プログラム 2008 「君の身体を変換してみよ」展、そのうち見に行こうと思っていたらもう終わっていた。 <URL:http://www.youtube.com/watch?v=ZeSZsBwnp8c> の紹介を観ると非常に面白そうで、見に行けば良かったと後悔。

λ. “Lightweight Monadic Regions” by Oleg Kiselyov and Chung-chieh Shan

Lightweight Monadic Regions | Lambda the Ultimate より。

リージョンを使ったリソース管理を行うモナドをHaskellで実装する話。 ランク2多相を用いてリソースがエスケープしないことを保障するのは誰でも思いつくけど、リージョンの入れ子とリージョン多相性を工夫して実現していて凄かった。 インターフェースだけ見ると非常に単純なんだけど、実装を見るとお馴染みの TypeCast を使ってて「やっぱしw」という感じ。 あと、typestate*1を型にエンコードすることでリソースが(手動で)解放されることを保証する方法も実装*2して、比較をしている。

どうでもいいけど、型エラーのメッセージが分かりにくいかもという話に対して、「Such error messages are also emitted when ..., so they should be familiar to haskell programmers.」とか書いてあって、うけた。

λ. ALC 10 のビデオ

The 10th Asian Logic Conference (ALC 10) のビデオが公開されている。 面白そう。

λ. うみねこのなく頃に Episode 3

読了。 夜更かししてやっていたので、眠い。 面白かったけど、戦闘シーンとかの文章のノリは見てられなかった。

λ. 帰りに泳いできた

帰りに近くのプールで泳いできた。例によって1kmを30分くらいで。 泳いでいたら、すごく肩がこっていたことに気づく。 それがほぐれて(?)気持ちいい。 いい運動したし、今日はよく眠れそうだ。

λ. ソフトウェア仕様の差分について by 石井忠夫

ソフトウェアの発展問題というのを型理論で扱おうという話。 ソフトウェア発展問題というのは以下のような問題。

今、考えている発展問題に現れうる全ての仕様の集合をS、全てのプログラムの集合をPとし、ある仕様 S∈S からプログラム P∈P が導かれることを S⊢P と表す。 また、仕様とプログラムの集合にある順序関係 ⊑ を導入し、仕様 S が S' に発展することを S⊑S' と表す。 この時、ソフトウェア発展問題は仮定 S⊢P 及び S⊑S' の下で、条件 P⊑P' 及び S'⊢P' を満すプログラム P' を見出すことと定式化される。 ここで、仕様の発展 S⊑S' が任意であれば、両者に共通部分が無くプログラム P' は新規に実現する必要がある。 他方、両者に共通部分が多く含まれ、両仕様の差分を活用して P から P' が効果的に実現される時には発展問題を考えることができる。

でもって、型理論での型=仕様, 項=プログラムという枠組みで、型と項にそれぞれ順序 ⊑ と、合併⊕、差分⊖、共通部分⊗を定義して、このソフトウェア発展問題を形式化しようとしている。 ただ、導入した順序がソフトウェアの発展をどの程度表現できているのかはちょっと疑問。

• <URL:http://ci.nii.ac.jp/naid/110006390496/>
• <URL:http://www.citeulike.org/user/msakai/article/3188477>

λ. MS-IMEがお馬鹿になってしまった

以前に、/.Jの「MS IMEの変換効率悪化は開発が中国にシフトしたのが原因?」という記事で紹介されていた古川享氏の「MS IMEさらに...お馬鹿になっていく」。 他人事だと思っていたら、うちのPCでも最近これになってしまったっぽい。「かまくらし」が「釜暮らし」になったり「しらないひと」が「白ない人」になったりして、しかも正しい候補が出てこない……(涙

仕方がないので、「コントロールパネル」「地域と言語のオプション」「キーボードと言語」「キーボードの変更」「Microsoft IME」からユーザー辞書を修復して直った。

λ. 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み

手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み, 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹, 信学技報 SS2006-41 (KBSE2006-17), 電子情報通信学会 (2006年-10月).

項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．2つの異なる関数が任意の入力に対して同様の出力を返すことは帰納的定理として捉えられるので,帰納的定理の証明法は関数型プログラムの等価性の検証に利用できる．本研究では,項書換えにおける帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には,手続き型プログラムから書換え系への変換を与え,その変換により手続き型プログラムの等価性を項書換え系の関数の等価性に帰着できることを示す．

項書き換え系はこんな使い方も出来るのかと驚いた論文。 項書き換え系について詳しくないので、細かい議論はあまり追えてないのだけど、アイディアがとても面白かった。

手続き型のプログラムから、プログラムカウンタと変数の値とを項で表した、(決定可能)条件付き項書き換え系へと変換する。例えば、

int sum1(int x){
  int i=0; int z=0;
  while(i<x){
    i=i+1; z=z+i;
  }
  return z;
}

という関数は

sum1(x) → U1(x, 0)
U1(x, i) → U2(x, i, 0)
U2(x, i, z) → U3(x, i, z) <== i < x
U3(x, i, z) → U4(x, Add(i, S(0)), z)
U4(x, i, z) → U5(x, i, Add(z, i))
U5(x, i, z) → U2(x, i, z)
U2(x, i, z) → U6(x, i, z) <== i >= x
U6(x, i, z) → U7(z)
U7(y) → y

という項書き換え系になる。

さらに、項書き換え系で書いた仕様

sum0(0) → 0
sum0(S(x)) → Add(sum0(x), S(x))

を用意して、sum0(x) = sum1(x) が帰納的定理であることを、潜在帰納法を使って証明する。

項書き換え系に変換して何が嬉しいかというと、普通なら帰納法が必要な定理の証明を、直接帰納法を用いずに出来る潜在帰納法等の方法があって、自動化がしやすいところ。ただ、この論文の時点ではまだ自動化は出来ていないけど。

ちなみに、こないだの第68回情報処理学会・プログラミング研究会で、同じ著者らの「潜在帰納法を利用した手続き型プログラム検証の試み」という題の発表があった。

λ. 第四十四回圏論勉強会

今日は圏論勉強会。板書の写真

Abramskyの"Temperley-Lieb algebra: From knot theory to logic and computation via quantum mechanics"を読む4回目で、今回は 5 Categorical Quantum Mechanics の後半、5.2 Quantum non-logic vs. quantum hyper-logic と 5.3 Remarks を読んだ。 前回が中途半端なところで終わったせいで、量子テレポーテーションについてそれぞれに調べたり考えたりしてたけど、今回はそれぞれの調べたことや理解を確認するという感じだった。

Abramskyらのここでの量子テレポーテーションの説明だと、bonotakeさんが 「Abramsky & Coecke の量子テレポーテーションがちょっとわかりかけてきた - たけをの日記＠天竺から帰ってきたよ」で貼っていた以下の図のように、観測の効果と古典情報の通信が添え字の選択として暗黙的に扱われてしまっていて、圏の中できちんと扱われていない(それらが射として扱われていない)。

もっとも、観測の効果については(密度行列に対する)superoperatorを射とする圏にすればちゃんと圏の中で扱えるはず*1だし、檜山さんの「量子テレポーテーションの楽屋裏 - 檜山正幸のキマイラ飼育記」によると Bob Coecke, Duško Pavlović "Quantum measurements without sums" では古典チャンネルもちゃんと扱えているようなので、原理的な問題ではなくこの時点での説明の単純化のためだとは思うけど。 ただまあ、いろいろとズルい説明なのは確かで、どんな読者層が想定されているのかはちょっと気になるところ。

あと、密度行列と純粋状態・混合状態に関しては、通俗な理解を晒してしまい、ちと恥ずかしかった。 純粋状態と混合状態についてはhiroki_fさんが「純粋状態 混合状態について - hiroki_fの日記」で書いている。

それから、こないだ「飲み会」で書いたことに関係して、日下部さんに暗黒通信団の「K-theory入門」という本を紹介してもらった。 index theory についてhiroki_fさんに訊くのは忘れてしまった。

関連

• 今日は圏論勉強会でした - たけをの日記＠天竺から帰ってきたよ

λ. 観測の扱いと閉じた系・開いた系

昨日の圏論勉強会でもちょっと話した話で、数学的・物理的な根拠は全く無いただの思いつきなんだけど、観測の扱いが複雑なのは、ひょっとして観測者が系の外部として扱われているから、つまり開いた系を考えているからではないのかと思った。 観測者自身も系の一部として含めた閉じた系を考えれば、全部ユニタリ変換だけになったりしないのか?

そう思ったきっかけは、Decoding the Universe の p.208 で以下のように、デコヒーレンスが環境とのエンタグルメントとして説明されていたこと*1。

The process of an object's gradual and increasing entanglement with its environment — the flow of information about an object into its surroundings — is known as decoherence.

あと、これはちょっと違う話だけど、宇宙全体を閉じた系として考えるとして、The principle of deferred measurement が一般に成り立つのなら、すべての観察は宇宙の終わり*2まで先延ばししてしまって、宇宙の終わりまでは全部ユニタリ変換だけで考えたりしてはいけないのだろうか。 もちろん、それは我々の視点での現象を説明しなさそうだけど。

λ. 『ウルトラダラー』 手嶋 龍一

ウルトラ・ダラー(手嶋 龍一) を読んだ。だいぶ前に「伊藤洋一の Round Up World Now」で紹介されていて、読もうと思っていた本。人物描写は微妙だと思ったが、内容はとても面白かった。そういえば、ライトノベルとかでないちゃんとした小説を読むのはずいぶん久しぶりだ。

λ. Agda2 on Meadow

darcsレポジトリからとってきたAgda2のスナップショットをMeadow3の上で動かそうとした。

README の記述は NTEmacs22 を想定したものになっていて、ucs-fonts と mule-fonts をインストールして設定する方法が書いてあったけど、それらのフォントは基本的にはMeadowのパッケージで入っているはずなのでその辺りは無視。 そうしたら、「File mode specification error: (error "No fonts match `-misc-fixed-medium-r-normal--18-120-100-100-c-90-iso8859-1'")」と言われてしまった。

仕方ないので、READMEの記述に従おうとしたが、Meadowだとフォント周りはNTEmacsと若干異なっている部分があるみたいで、どうもうまくいかない。 結局、.emacsに「(setq agda2-fontset-name nil)」と書き、agda-mode.elの以下の部分をコメントアウトしたら、解決した。

(if window-system
    (create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t))

λ. 帰りに泳いできた

先週に続いて今週も、帰りに1km・30分くらい泳いできた。 体力無いので、やっぱりこれくらいでバテる。

λ. Analyzing Websites for User-Visible Security Design Flaws

Analyzing Websites for User-Visible Security Design Flaws by Laura Falk, Atul Prakash and Kevin Borders.

In this paper, we examine the prevalence of user-visible security design flaws by looking at sites from 214 U.S. financial institutions. We specifically chose financial websites because of their high security requirements. We found a number of flaws that may lead users to make bad security decisions, even if they are knowledgeable about security and exhibit proper browser use consistent with the site’s security policies.

To our surprise, these design flaws were widespread. We found that 76% of the sites in our survey suffered from at least one design flaw. This indicates that these flaws are not widely understood, even by experts who are responsible for web security. Finally, we present our methodology for testing websites and discuss how it can help systematically discover user-visible security design flaws.

ちょっと前に、/.Jの「銀行ウェブサイトの大半はセキュアではない?」という記事で取り上げられていた論文。2006年に米国の金融関連の214のWebサイトに対して、以下の5つの設計上の問題について調査したところ、76%の金融機関になんらかの問題があったという話。

1. Break in the chain of trust: 安全なページでのユーザーへの通知なしでの、違うドメインへのリダイレクト
2. Presenting secure login options on insecure pages: 安全でないページにログインフォームがある
3. Contact information/security advice on insecure pages: 連絡先や安全に関わる情報が安全でないページにある
4. Inadequate policies for user ids and passwords: e-mailアドレスや社会保障番号のような推測しやすいIDを使わせていたり、短いパスワードを許しているか
5. E-Mailing security sensitive information insecurely: 安全に関わるような情報をe-mailで送っているか

これらの項目はアカウントを作ったりログインしたりせずに調査できるもののなかで、良く見られた問題を選択している。

λ. ダークナイト

ダークナイト見てきた。ヒース・レジャーの演じるジョーカーがかっこ良かった(＞＜)

λ. SPINによるモデル検査 (1) by 野中さん

メモ。 野中さんによるSPINチュートリアル。 非常によくまとまっている。

λ. The Transactional Memory / Garbage Collection Analogy

The Transactional Memory / Garbage Collection Analogy by Dan Grossman

Transactional memory (TM) is to
shared-memory concurrency
as
garbage collection (GC) is to
memory management.

The Transactional Memory / Garbage Collection Analogy | Lambda the Ultimate より。

A unified theory of garbage collection のようなものを期待していたら、本当にただのアナロジーだった。 もっとも、著者がCycloneの作者の一人であることもあって、非常に説得力のあるアナロジーではあるのだけど。

あと、X10, Fortress, Chapel といった次世代の言語ではトランザクショナルメモリが言語の一部になっているそうな。X10とFortressは知ってたけど、Chapelってのもあるのね。

λ. 量子誤り訂正符号

decoherenceによる問題は量子誤り訂正符号で常に回避可能なものなのだろうか?　回避可能だとして、それはGCのように普段はその存在を意識しないで構わないものになるのだろうか?　それともトランザクショナルメモリーのように抽象的にではあっても存在を意識する必要があるものになるのだろうか?　知人と量子計算について話していてちょっとそんなことを思った。まだ量子誤り訂正符号がどんなものなのか私は全然理解してないけど。

λ. シュシュ

シュシュって何かと思ったら、ヘアアクセサリなのね。 シュッ・シュッとは関係ないと。

• シュッ・シュッ
  • ネットピープル分類学 その傾向と対策 (Shibuya.pm Technical Talk #4)
  • Web日記の魅力は粗暴性なのか？ - 「高木浩光＠茨城県つくば市の日記」跡地 (2003-10-12)

λ. Church-Rosser Theorem in Agda2

Haskell Hackathon in 2008 September に参加。やるネタは幾つか考えていたのだけど、結局、昔Agda1で書いたチャーチロッサーの定理の証明をAgda2で書き直すということをやっていた。

(詳しくは後で)

λ. Mの型付け

Mコンビネータ*1 λx. x x は多相型を適当に使うと型付け出来る。 例えばHaskell(GHC)ならば以下の通り。

m :: (forall a. a->a) -> (forall a. a->a)
m x = (x :: (forall a. a->a) -> (forall a. a->a)) x

これが出来るのは 型 forall a. a->a に属する真っ当な要素は id だけだから。

では、同様にすると、Yコンビネータ*2 λf. (λx. f (x x)) (λx. f (x x)) も型付け出来るだろうか?

λ. Sets in types, types in sets

Sets in types, types in sets by Benjamin Werner, in Proceedings of TACS'97

We present two mutual encodings, respectively of the Calculus of Inductive Constructions in Zermelo-Fraenkel set theory and the opposite way. More precisely, we actually construct two families of encodings, relating the number of universes in the type theory with the number of inaccessible cardinals in the set theory. The main result is that both hierarchies of logical formalisms interleave w.r.t. expressive power and thus are essentially equivalent. Both encodings are quite elementary: type theory is interpreted in set theory through a generalization of Coquand 's simple proof-irrelevance interpretation. Set theory is encoded in type theory using a variant of Aczel's encoding; we have formally checked this last part using the Coq proof assistant.

ytbさんの 2008-06-14 - あいまいな本日の私 より。

概要

集合論ZFCと型理論CICの間の埋め込みの話。 ZFC_i を ZFC に i 個の到達不能基数を加えたもの、CIC_i を型の宇宙を Type_i までに制限した CIC として、その間の以下の図のような相対無矛盾性の関係があることを示している(矢印の逆向きに埋め込みが可能)。

少し詳しい話

ただし、この論文で扱っている CIC (Calculus of Inductive Construction) は、Coquand らの CC (Calculus of Construction) の変種である Luo の ECC(Extended Calculus of Constructions, c.f. 20060503#p02) に、帰納的データ型を追加したもの。なので、現在のCoqとは違ってPropが非可述的(impredicative)な宇宙になっている。(2018-03-06追記: CoqのPropはimpredicativeか。当時は何を勘違いしてたんだろう……)

また、CICそのものではなくCICに以下のようなものを加えたものを考えている。

排中律

EM := ΠP : Prop. P∨¬P

Type-theoretical Description Axiom on level i:

TTDA_i := ΠA,B : Type_i. ΠP : A → B → Prop. (Πa : A. ∃b : B. (P a b)) → ∃f : A→B. (Πa : A. P a (f a))

Type-theoretical Choice Axiom on level i:

TTCA_i := ΠA : Type_i. ΠR : A→A→Prop. (equiv A R) → ∃f: A→A. Πx,y : A. (R x y) → (f x = f y)

ただし、ここでの存在記号は通常の依存直和(Σ-types)ではなく ∃a : A. P a := ΠX : Prop. (Πa : A. P a → X) → X で定義されるものなので注意。

で、CICからZFCへの埋め込みは、Propに関してはproof-irrelevantな解釈を用い、他に関しては通常の集合論的な解釈をしている。 それによって、ZFC_{i-1} が無矛盾ならば、CIC_i + EM + TTDA_1 + … + TTDA_n + TTCA_1 + … + TTCA_n が無矛盾であることを示している。

一方、ZFCのCICへの埋め込みに関しては、まず集合と等号と要素関係を以下のように帰納的に定義して埋め込みをしている。

Inductive Set : Type_{i+1} :=
  | sup : ΠA : Type_i. (A → Set) → Set.

Fixpoint Eq : Set → Set → Prop :=
  fun (sup A f : Set) (sup B g : Set) ⇒
    (Πa : A. ∃b : B. Eq (f a) (g b)) ∧
    (Πb : B. ∃a : A. Eq (f a) (g b)).

Definition In : Set → Set → Prop :=
  fun (E : Set) (sup A f : Set) ⇒
    ∃a : A. Eq E (f a).

その上で以下のようなことを示している

• Z は CIC_2 + EM にエンコードできる
• ZF は CIC_2 + EM + TTDA_3 にエンコードできる
• ZFC は CIC_3 + EM + TTDA_3 + TTCA_3 にエンコードできる
• ZFC_n は CIC_{n+2} + EM + TTDA_{n+1} にエンコードできる

余談

以前にOCaml-Nagoyaの飲み会に参加したときに、普通の数学をそのままCoq上に持ってくるには集合論をエンコードする必要があるのではないかという話をして、そのときに念頭にあったのはここでやっているようなものだったので、具体的なエンコードとその性質が分かってすっきりした。

ただ、排中律に関してはEMを追加すれば良いし、集合論と型理論の違いについてはこのような埋め込みを考えれば良いとしても、一階述語論理と高階述語論理の違いが問題になることはないのか、その辺りはまだよく分からない。

λ. QMLでの観測のSuperoperatorによる解釈

以下のような二つの関数を考える。

• Qid (b,qb) |- b :: qb
• Meas (b,qb) |- if b then qtrue else qfalse :: qb

前者は観測を伴わない恒等関数で、後者は観測を伴う関数。 この二つの関数を superoperator で解釈してみる。

QML> runS "test2.qml" "Qid"
OK 
Super-op input = 1,
Super-op output = 1,
([True,True],[True,True],1.0 :+ 0.0)
([True,False],[True,False],1.0 :+ 0.0)
([False,True],[False,True],1.0 :+ 0.0)
([False,False],[False,False],1.0 :+ 0.0)
QML> runS "test2.qml" "Meas"
OK 
Super-op input = 1,
Super-op output = 1,
([True,True],[True,True],1.0 :+ 0.0)
([False,False],[False,False],1.0 :+ 0.0)
QML> 

ちゃんと違う結果になっている。

ついでに、例として、|φ〉 = (1/√2)(|0〉 + |1〉) に対応する密度行列 |φ〉〈φ| = (1/2)(|0〉〈0| + |0〉〈1| + |1〉〈0| + |1〉〈1|) にこれらの関数を適用してみると、Qidを適用した結果はこのままである一方、Measを適用した結果は Meas(|φ〉〈φ|) = (1/2)(|0〉〈0| + |1〉〈1|) になる。

というわけで、第四十四回圏論勉強会 - ヒビルテ (2008-09-14) で「観測の効果については(密度行列に対する)superoperatorを射とする圏にすればちゃんと圏の中で扱えるはず」と書いたが、たしかに観測による効果(の少なくとも一部)については圏の内部で扱えているようだ。

λ. 帰りに泳いで来た

毎週水曜に泳ぎに行くことにしようかと思ったいたのだけど、昨日は泳ぎに行く時間が無かったので、今週は今日泳いできた。30分弱で1km。泳いでたら途中で横腹が痛くなってきた。運動して腹が痛くなるのは久しぶりで、なんだか懐かしい。

λ. ICFP Programming Contest 2008 結果

結局、我々の Team Sampou は Trial 9 で脱落し、shinhさんによる unofficial ranking の Results of Team Sampou によると298チーム中63位だったとか。 すぐ脱落したものと勘違いしてたけど、一応は Trial 9 まで残ってたんだね。 来年こそはもう少し上位に入りたいものだ。

参考

• ICFPCのfinal roundのマップ - Onion開発再開しつつある日記(2008-08-15) (Trial 1〜7までのマップ)
• ICFP Programming Contest 2008 終了 - ヒビルテ(2008-07-15)

λ. 誕生日

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

第22章「黒帯のためのLISP」と第23章「実践：スパムフィルタ」。

λ. A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments

A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments by Joseph A. Goguen and R. M. Burstall

To ease constructing institutions, and to clarify various notions, this paper introduces two further concepts. A charter consists of an adjunction, a “base” functor, and a “ground” object; we show that “chartering” is a convenient way to “found” institutions. Parchments provide a notion of sentential syntax, and a simple way to “write” charters and thus get institutions. Parchments capture the insight that the syntax of logic is an initial algebra. Everything is illustrated with the many-sorted equational institution. Parchments also explicate the sense of finitude that is appropriate for specifications. Finally, we introduce generalized institutions, which generalize both institutions and Mayoh's “galleries”, and we introduce corresponding generalized charters and parchments.

昔、向井先生にハードコピーを貰ったまま積読になっていた論文。 institutionの幾つかの定義と、典型的な場合についてinstitutionを作るためのcharterとparchmentという枠組みについての紹介。

institutionの定義に関しては通常の定義に加えて、以下の三つ組みによる定義があって、これ何で自分でこれ気づけなかったのかと思った。そして、この定義から一般化することで generalized institution が得られる。

• 関手 Mod : Sign^op → Cat
• 関手 Sen : Sign → Cat
• 対角自然変換 ⊧ : |Mod(_)|×Sen(_) → 2

charter は随伴から insitution を定義するためのもので、図で書くとこんな感じのもの。

ここで Syn は syntactic system で、「文」だけでなく他の構文的な要素も含むような圏で、Bはそのなかから「文」の成分だけを取り出してくるような関手。こうしておいて Sen を BF で定義する。G は syntactic system の全ての解釈を集めてきたようなもの。 ただ、equational charter での G の定義はサイズの問題が無いのかちょっと不安。

parchment は、自由代数を使うことにして随伴になることを自動的に保障するもの。 関手 Lang : Sign → SigAlg を用意しておいて、Syn は Lang(Σ)代数の圏をΣに関してつぶして作る。

あと、個人的には「The original motivation for developing institutions was to do the “Clear tricks” once and for all, over any (suitable) logical system」と書いてあって、institutionのそもそもの動機が分かってスッキリした。ここで言っている“Clear tricks”というのは代数的仕様記述言語Clearで使われている以下のような手法のこと。

• use colimits to put theories together
• use diagrams as environments to keep track of shared subtheories
• use data constraints to define particular structures (i.e., abstract data types)
• use pushouts to apply generic theories to their “actual” arguments, and
• use theory morphisms to describe the bindings of actuals at interface theories (also called “requirement” theories).

λ. 日本のスイッチ最終回

日本のスイッチ、今年に入ってからはほぼ毎週やっていたんだけど、終わっちゃうのね……

λ. 宴会