日々の流転

λ. アラン・グリーンスパンの名前をど忘れして困った。えっと、スパン・グリーンアランだっけ?、アラン・グリーンスパンだっけ?　それとも、グリーン・アランスパン?

λ. 読んだ本

「ペンデュラム」 1巻

たつねこ[著]

女検視官 江夏冬子 「京都殺人地図」

山村美紗[著]　徳間書店　TOKMA NOVELS　書籍コード: 0293-152064-5229

「ジャングルはいつもハレのちグゥ」 2巻

金田一蓮十郎[著]

λ. ヒアドキュメントで正規表現?

ヒアドキュメントで正規表現が書けない事に気がつく。こんな書き方が出来たらいいのに。

hoge = <</END/
正規表現
END

λ. 学業成績表

とやらが来た。経済理論演習がCだったのがショキングで、泣きたい。そんなに酷かったのかなぁ。しゅん。

λ. テロ

世界貿易センタービルとペンタゴンに旅客機が突っ込んだらしい。ビックリした。パレスチナ開放戦線が犯行声明を出したという噂があるけど、ホントかしら?　エネルギー政権といわれるだけあって、今のブッシュ政権は明らかにパレスチナ寄りだし、パレスチナがアメリカに喧嘩売るなんて、僕にはちょっと信じられない。

λ. CHARITY

Charity is based on the theory of strong categorical datatypes. These are divided into two subclasses: the inductive datatypes (built up by constructors in the familiar way) and the coinductive datatypes (broken down by destructors). Programs over these datatypes are expressed by folds (catamorphisms) and by unfolds (anamorphisms), respectively.

萩野先生が言ってたCPLを発展させたシステムってこれの事かな。

λ. linc-0.5.3 on cygwin

lincがunix domain socketに対してうまく動作しないので少し追いかけてみた。getsockname()で書きこまれるパスの最後が1文字欠けているようだ。調べてみると、予想通り最後のNULL文字分がバッファ長に含まれていない。linc-protocols.cのlinc_protocol_get_sockaddr_unix()を修正したら直った。linc-0.5.3-cygwin-20020911.patch

しかし、test-linc.exeで、クライアント側のlinc_main_loop_run()でブロックしてしまってるみたい。 サーバ側は破棄されているのに、クライアント側でbrokenシグナルが発生していないっぽい。良くわかんないや。ははは。

λ. SLACS 2003

に行ってきた。池上さんにも久しぶりに会えたし、興味深い話も沢山聴けて、とても楽しかった。だけど、ついていけない話も多くて結構悔しい。懇親会にも参加してきた。

λ. Modal logics for coalgebras -- A Survey, 蓮尾 一郎 (東工大)

そういえば、これまで bisimilarity と behavioral equivalence は同じだと思い込んでいて少し恥ずかしかった。本当は、bisimilarity の方が一般には強い条件で、関手Tがweak pullback を保存するならば同値になるのか。

• Technical Report

λ. Regular category の中の非決定性オートマトン, 池上 大介 (産総研/CREST)

最初は割と簡単かなと思っていたら、いつの間にか付いていけなくなっていた。気になっていた話の一つだったので悔しい。Adámek らのアプローチ(cf Automata and Algebras in Categories)の特殊な場合になってるらしい。

λ. 抽象解釈にみられる圏論的構成について, 西澤 弘毅 (東大/産総研)

抽象解釈(abstract interpretation)って名前はよく聞くけどどういうものか知らなかったので、その辺りが良くわかって嬉しかった。今回聴いた発表のなかでちゃんと理解できたのはこれだけかも。

λ. 明示的代入計算の強正規化性の証明について, 桜井貴文 (千葉大)

.

λ. 様相μ計算の完全性について, 鹿島 亮 (東工大)

様相μ計算というのは、様相命題論理の体系に不動点演算子を加えたもの……なのかな。そういう事は全然考えたことが無かったので新鮮に感じた。よくは分からなかったけど。

λ. Announcement of Typed Lambda Calculus and Applications, 長谷川真人 (京大)

国際学会 "Typed Lambda Calculus and Applications" のアナウンス。2005年奈良。typed lambda calculus というタイトルだけど、untypedでも、λ以外でも実は良いらしい。来年の10月くらいが論文の締め切りで、長さ的には15ページ程度らしい。

それから、

Fourth ACM-SIGPLAN Continuation Workshop (CW'04)

deadlineは10/1。

Category Theory in Computer Science (CTCS 2004)

コペンハーゲン。カテゴリの「カ」の字でも入ってればOKらしい (笑)

なんてのもあるそう。

それから、線形論理では「A = (A -o ⊥) -o ⊥」「!A = (A → ⊥) -o ⊥」「?A = (A -o ⊥) → ⊥」が成り立っていて、前者の二つに関しては「A = ∀X. (A -o X) -o X」「!A = ∀X. (A → X) -o X」も言えるのに、最後のだけは「?A = ∀X. (A -o X) → X」ではなく「A = ∀X. (A -o X) → X」になるのは何故か、といった話もしていた。

λ. Flow Analytic Type System for Compiler Optimizations , 松野裕(東大)

.

λ. NP完全問題を解く決定性アルゴリズムについて, 久馬栄道 (愛知学院大)

.

λ. On Sufficient Conditions And Partial Analysis for Secure Cryptographic Protocols, Masao Mori (九大)

.

λ. 『日本再生に「痛み」はいらない』, 岩田 規久男, 八田 達夫

読了。著者達の主張には概ね同意できるし、こういった政策パッケージを提案する政党があったら、先の参院選でも投票を考えたのになぁ……

λ. How to read and write .NS1 files

This document describes the NetStumbler file format. It is primarily intended for people wanting to read NS1 files (for example, to be able to import them into mapping software), however there may be others that want to write their own NS1 files.

メモ。chiko にっき (2004-09-11) より。

λ. 【ジョジョ】プロ市民の奇妙な冒険【ジョジョ】 (2ch)

……

λ. 制限された関数だけクラスのインスタンスにする

GHCなら-fglasgow-extsを指定すれば、インスタンス宣言での型構築子の引数は型変数でなくても大丈夫です。でも、 理由はよく知らないんですけどね。マニュアルの 7.4.4. Instance declarations でもあまり触れられてないけど、型の同義名(type synonym)をインスタンス宣言に使えるようにしたことの自然な帰結なのかな……

λ. Eastern Dawn　東方の夜明け

弾幕STG・東方プロジェクトの生みの親である上海アリス幻樂団神主ＺＵＮ氏をお呼びしてなにかれとトークをしてもらおうというイベントです。ただいまは告知期間で、申し込みは9月15日よりとなっております。尚、定員は150名となっておりますのでご了承ください。

メモ。楽しそうなイベントがあるじゃないですか。

λ. 風邪

風邪ひいたっぽい。喉が痛い。

λ. 衆院選

投票に行ってきた。

小泉政権の経済政策には不満が多かったし、郵政民営化も別に積極的に賛成しているわけではないのだけど、他の政党もその点では五十歩百歩だから比べられないし、他の政党は安全保障等の点で不安だったので、結局消去法で自民へ。もし、民主党にそういった不安点がなくて、かつリフレ政策でも公約にしてれば、民主党に投票することも真剣に検討したんだけどね……

最高裁判所裁判官国民審査は、今回の六人は特に×印を付けるべき理由も見当たらなかったので、そのまま投票。

それにしても、自民党ﾃﾗﾂﾖｽw　自民党単独で290議席以上って、おい……　それはそれで何か不安だ。

λ. LDAPのuserPassword

間違えてuserPasswordを空にしてしまったら、変更しようとしても「ldap_bind: Server is unwilling to perform (53)」「additional info: unauthenticated bind (DN with no password) disallowed」と言われるようになってしまって困った。結局adminになって設定しなおした。

λ. SLACS 2006

に参加。 しかし、みんな頭いいしちゃんと研究してるよなぁ。 いつものように凹んできた。

以下色々書くが、これらは講演内容をまとめたわけではなく、私の単なるメモであり、偏っており間違いを含む可能性も高いのでご注意を。まあ、真に受ける人はいないと思うが。

λ. A subsystem of sequent calculus isomorphic to natural deduction

発表者

中澤巧爾 (京都大学)

概要

シーケント計算のカット除去と自然演繹の正規化との関連について。

自然演繹とシーケント計算はしっかり対応しているものだと思い込んでいたけど、そうでもないのだな。それが一番驚きだった。 NJ_g は β と π (permutative conversion) を持つ自然演繹の体系。シーケント計算のカットには principal cut (p-cut) とそれ以外 (n-cut) があり、p-cutのみを持つ体系が LJ_p 。

• LJ_p ≅ NJ_g
• LJ ≅ NJ_g + ?(explicit substitution)

興味深い話だっただけに、あまり覚えていないのが残念。

• β-protocol ≅ β-reduction
• π-protocol ≅ π-reduction
• n-cut elim ≅ propagation of explicit subst

λ. Kleese's slash interpretationの統一的記述について

発表者

小島健介 (京都大学)

概要

Kleene's slash interpretationは直観主義論理におけるdisjunctionとexistenceの性質を調べるために導入された解釈の一つである。その定式化は対象となる体系ごとに別々に行われていたが、これを統一的に記述することができないかを一階の体系に限定して考察する。

slash interpretation は Kleene がDisjunctionやExistenceの直観主義論理での振る舞いを調べるために、Disjunction and Existence Under Implication in Elementary Intuitionistic Formalisms. Journal of Symbolic Logic, Vol. 27, No. 1 (Mar., 1962), pp. 11-18 で導入したもの(らしい)。

直観主義命題論理(IPL) の slash interpretation では、二項関係 Γ | A を次のように定義。

• Γ | p ⇔ Γ ⊢ p
• Γ | A∧B ⇔ Γ | A and Γ | B
• Γ | A∨B ⇔ (Γ ⊢ A and Γ | A) or (Γ ⊢ B and Γ | B)
• Γ | A→B ⇔ if (Γ ⊢ A and Γ | A) then Γ | B
• Γ | ¬A ⇔ if (Γ ⊢ A and Γ | A) then Γ ⊢ ⊥

これを使うことで、健全性と disjunction property について言うことが出来る(具体的なstatementは忘れた)。

一階述語論理に拡張するには以下のようにする。

• Γ | ∀x.A[x] ⇔ ∀t. Γ | A[t]
• Γ | ∃x.A[x] ⇔ ∃t. Γ ⊢ A[t] and Γ | A[t]

これを使うことで「If - ⊢ A then - | A」が言える。

HA(Heyting Arithmetics)に拡張するには以下のようにする。

• Γ | s=t ⇔ Γ ⊢ s=t
• Γ | ∀x.A[x] ⇔ ∀n∈ω. Γ | A[n]
• Γ | ∃x.A[x] ⇔ ∃n∈ω. Γ ⊢ A[n] and Γ | A[n]

この場合には「If A is closed and - ⊢ A then - | A.」が言える。ただし、- ⊢ A であっても一般には - | A とは限らないので注意(e.g. x=0∨x≠0)。

一般化の方針として、普通のモデルと slash を混ぜてみることを考えた。 first-order structure A と 二項関係 ⊢ が与えられたときに、ρ | A を以下のように定義。

• ρ | P ⇔ ρ ⊨ P and P : atomic
• …
• ρ | ∀x.A[x] ⇔ ∀a∈|A|. ρ(x := a) | A[a]
• ρ | ∃x.A[x] ⇔ ∀a∈|A|. ρ(x := a) ⊢ A and ρ(x := a) | A[a]

これを使って健全性のための十分条件を与える(具体的なstatementは忘れた)。

既存の slash interpretation との対応。

• FOLのslashにはterm model のようなものを考えることで対応
• HAのslashとは閉じた論理式について一致

まとめ

• 普通のstructureを考えてtruthをslashのように定義してみた
• 適切な条件を満たすと健全性が成り立つ
• 定義した枠内でslashの定式化を試みた
  • 一階述語論理では成功
  • 算術では完全には一致しない

質疑応答で「q-realizability interpretation を使わないのは何故か?」というツッコミを龍田先生から言われていた。 それから、休憩時間中の雑談で「帰納的定義」に対して q-realizability interpretation を与える話が出ていた。私は realizability の話は全然知らないけど、気になるなぁ。

λ. The upper part of the lattice NExt(KTB)

発表者

宮崎裕 (北海道大学)

概要

We will describe the structure of the upper part of the lattice of normal modal logics containing KTB, and discuss some related problems.

normal-extension

tra_n = □ⁿ p → □ⁿ⁺¹ p

このクラスの cardinality は 非可算個

量子論理のlatticeであるortholatticeをKTBに埋め込める(?)。それから、KTBやNExt(KTB) についての研究は意外と行われていない、というのもこの研究を始めた理由。

λ. お昼

佐々木克巳先生とご一緒した。TRATTORIA Alioli というところで、ポルチーニ茸のクリームスパゲティ。おいしかった。

λ. A Hybridization of Irreflexive Modal Logics

発表者

佐野勝彦 (京都大学)

概要

Unlike ordinary modal language, hybrid language makes it possible to refer to states (possible worlds) in formulas. This is achieved by a class of formulas called nominals. This talk discusses hybrid language with a sub-modality (called the irreflexive modality) associated with the intersection of the accessibility relation R and the inequality. First, we provide the Hilbert-style axiomatizations (with and without the Gabbay-style rule) for logics of our language, and prove the Kripke completeness. Second, with respect to the frame expressive power, we compare the effect of the irreflexive modality with that of nominals. Finally, we establish the Goldblatt-Thomason-style characterization for our language.

Hybrid Logic については存在すら知らなかったが、結構面白そう。

• Hybrid Logics' Home Page
• Stanford Encyclopedia of Philosophy - Hybrid Logic

非反射的な様相論理をハイブリッド化したらどうなるか?

Modest ◆ gives MORE expressive power to HLs!

Two topological interpretation of ◇:

• ◇ as closure: w ∈ V(◇φ) ⇔ w ∈ ~(V(φ))
• ◇ as derivative: w ∈ V(◇φ) ⇔ w ∈ ~(V(φ)＼w)

<R∩S)i ⇔ <R>i ∧ <S>i

Ultrafilter Extension

λ. 様相定数loopを含む様相論理について

発表者

鈴木徹 (東京工業大学)

ここで言う様相定数はp,q,rといった変数と、⊥,Tといった定数の中間のイメージ。モデルの付値には依存しないが、モデルの形状に依存する。ここで導入するloopはxRxである可能世界xでのみ真になるような様相定数。 loopを導入した体系に関する基本的な性質色々 (配布資料があったので、後でゆっくり読む)。 「■」を加えてもこのloopは表現できない。何故なら、以下の二つを区別できないため。

質疑応答では、このモデルの作り方だとK4(違ったかも?)とかには使えないといった話があった。

【追記】 2006年度 MLG 数理論理学研究集会(第40回)の発表資料。<URL:http://matu.cc.kyushu-u.ac.jp/mlg/pdf/TouluSuzuki.pdf>

λ. 知識論理による匿名性検証のための関数部分知識モデル

発表者

川本裕輔 (東京大学)

知識論理(modal logic of knowledge?)とマルチエージェントシステムを用いた匿名性検証の話。

Fagin, R., J. Y. Halpern, Y. Moses, and M. Y. Vardi (1995). Reasoning about Knowledge. Cambridge, Mass.: MIT Press.

Halpern, J. Y., and O'Neill, K. Anonymity and information hiding in multiagent systems. In Proc. of the 16th IEEE Computer Security Foundations Workshop (2003), pp. 75–88. <URL:http://citeseer.ist.psu.edu/halpern03anonymity.html> で知識論理による匿名性の定式化が行われている(?)。

λ. CM: TLCA 2007

International Conference on Typed Lambda Calculi and Applications.

Important dates:

Dec 22

Title and abstract due

Jan 2

Deadline for submission

Mar 25

Notification of acceptance-rejection

λ. Some classes of relevant modal logics

発表者

関隆宏 (九州大学)

概要

メタ完全な適切論理は構文論的な面から2種類に分類できることが知られている。適切様相論理に対してこのような分類が可能であるか、あるいは別の側面から分類できるかどうかについて考えていく。

Relevant logic (適切論理)は、古典論理のパラドックスを除くために考えられた。

1. paradox of relevance: A→(B→A), A→(B→B)
2. paradox of consistency: (A∧¬A)→B, A→(B∨¬B)

命題適切論理の一つの特徴は「A→B が定理ならばA,Bが共通の命題変数を含む」という点。適切論理にも色々なものがある(最も基本的なのがB)。様相論理は通常古典論理の上で議論されるが、非古典論理上の様相論理が最近(?)注目されてる。ここでは適切論理をベースとした様相論理。

A logic is metacomplete if exactly the sentences true on a certain perferred interpretation of that logic in its metalogic are theorems. メタ完全な適切論理は Reductio 「A ⇒ ~(A→~A)」を認めるかどうかで二つに分類できる(M1-logic, M2-logic)。

適切論理に基づく様相論理で最も基本的なものが B.C_□◇ 。これはnormalではないがregularな様相論理。T-axioms「□A→A」「A→◇A」を認めるか否かで二つに分類できる(ように見える)。Reductioによる分類とあわせて四つに分類。

Metavaluations に関する Slaney's method 。

• The primeness is often called the disjunction property
• Two kind of the primeness
  1. Intuitionistic primeness (IP): if ⊢A∨B, then ⊢A ∨ ⊢B.
  2. Modal primeness (MP): if ⊢□A∨□B, then ⊢A ∨ ⊢B

λ. 帰り

寝不足でしんどいので懇親会には出ずに帰ることに。 明日は PPL Summer School もあるしね。

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

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

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

λ. iteratee I/O勉強会

に参加。詳しくはmaoeさんのブログなどを参照。

• Tweetvite :: iteratee I/O勉強会
• Lazy I/O must go! - Iteratee: 列挙ベースのI/O - 純粋関数型雑記帳
• maoeのブログ
  • HIMA' #1: iteratee I/O勉強会 - maoeのブログ
  • iteratee I/O勉強会 - maoeのブログ

iteratee law とかないのなと思う。 IterVがMonadであることを含意するのが最低限の条件。

それと、以下の iteratee-0.4 での定義をCPSスタイルと言っていたけど、感じとしてはIterVMのモナディックなチャーチエンコーディング(?)を考えているような雰囲気だと思った。もう少しちゃんと考えたいところだけど。

iteratee-0.2 での定義:

data IterVM el m a = DoneM a (StreamG el) 
                   | ContM (Iteratee el m a) 

newtype Iteratee el m a = 
  Iteratee { runIter :: StreamG el -> m (IterVM el m a) } 

iteratee-0.4 での定義:

newtype Iteratee el m a = 
  Iteratee { 
    runIter :: forall r. 
      (a -> Stream el -> m r) -> 
      ((Stream el -> Iteratee el m a) -> Maybe ErrMsg -> m r) -> 
      m r 
   }

あと、全然脱線して、pirapirapiraさんに Epigram, OTT(observational type theory), Pola: a language for PTIME programming とかについて盛り上がる。

• Extensional Equality in Intensional Type Theory - ヒビルテ(2005-05-29)
• Towards Observational Type Theory - ヒビルテ(2006-05-16)
• Observational equality, now! - ヒビルテ(2009-07-15)

その後は例によってシャヒ・ダワットで懇親会。 ビリヤニというのが日本ではここでしか食べられないらしい*1。 それから、アダムの呪い、イブの7人の娘達 とかの話面白かった。 あと、「やっぱりgitは使える様にならないとなぁ」と思った。