日々の流転

λ. 英語の notion と concept

今日の疑問。 英語の「notion」と「concept」には違いがあるのは分かるが、その違いは具体的には何で、どう使い分けたら良い?　あと、日本語に訳すときに訳し分ける必要はあるだろうか?

追記

sumiiの日記 - 英語の類語 で「こういうときには Longman Activator」と教えてもらった。これまで知らなかったけど、便利そうだ。

λ. Structural Subtyping

• soutaroにっき - OCamlのStructural Polymorphism
• 晩ごはんの履歴 - 多相レコード

この辺りの話は良く知らないので勉強になるなぁ。

λ. 生活保護費 : 65歳以上・持ち家に暮らし、貸し付け方式に

これをきっかけにリバースモーゲージがもっと普及するといいなぁ、と思った。

λ. ニセ科学フォーラム

という楽しげなイベントが東京であったそうな。 聴きにいってみたかったかも。

• 配布資料

λ. IOモナドの実行順序を規定するのは何か?

• sshi.Continual - ふつける勉強会 10回目
• lethevert is a programmer - Haskell : モナドの実行順序は何によって規定されているのだろうか？
• haskellのある暮らし - モナドの実行順序はいかにして既定されるか
• lethevert is a programmer - Haskell : モナドの実行順序

あたりの話だけど……

(>>)が非可換なモナド*1では a >> b と b >> a は異なる値であることがあり、必然的に順序の概念が生まれる。そして、IOモナドは(>>)が非可換になるように定義されたモナドであり、Haskellの処理系はmainという名前のIOモナドの値を、その順序に従った一連のIOアクションに変換する。

ただこれだけの話。 つまり、IOモナドの実行順序を規定しているのは、IOモナドが持っている非可換性である。 評価順だとか正格性とかみたいなややこしい話は全く本質的ではない。

IOモナドの具体的定義

で、これらの要求を満たすようにIOモナドを具体的にどう定義するかだけど……そんなのはまあどうとでもなる。例えばこんな感じの単純なものでも構わない*2。

data IO' a
    = Return a
    | forall b. Bind (IO' b) (b -> IO' a)
    | PutChar Char

instance Monad IO' where
  (>>=)  = Bind
  return = Return

putChar :: Char -> IO' ()
putChar = PutChar

というか、こういう単純な表現にしてやると、IOモナドの値はIOアクションを表す単なる値に過ぎないというのが良くわかるのではないかと思う。

もちろん、実際の処理系で使われている定義はもっと巧妙……というか普通は処理系固有の黒魔術になってるけど。

λ. 熱力学とガベージコレクション

かねてから、計算機科学者は熱・温度・エネルギーといった熱力学の概念を知っているべきと思っていたので、丁度それらの紹介があった"Thermodynamics and Garbage Collection"(.html, .ps.gz)*1を、「熱力学とガベージコレクション」でこっそり翻訳中。まあ、GCへの適用についてはかなり眉に唾を付けた方が良いと思うが。

そういえば、熱力学は20041220#p01ごろには武藤先生のブームだったけど、これはもう終わってしまったかな。

追記 (2006-09-09)

resolutionは分解能だという指摘をtakotとまつもとさんから受けたので、そのように修正。お二人に感謝。

λ. ボルツマン没後100年

昨日熱力学のことを書いたが、実は今日はボルツマンの没後100年目の日だったそうだ。そして、このことは偶然見たex-constさんの雑記帳(2006-09-05)で知った。小さな偶然が二つ。

• Ludwig Boltzmann - Wikipedia, the free encyclopedia

λ. 今日の英語: represent

The Japanese government is represented at the conference.

「日本政府は会議に代表を送っている」という意味だそうな。 representってこういう使い方もするのね。 知らなかった(バカ)。

λ. Xiph QuickTime Components (XiphQT)

RubyKaigi2006の音声ファイルが Ogg Vorbis だったので、iTunesで聴くためにインストールしてみた。

λ. 外延性と参照透明性

自然言語に関する議論では「外延性」と「参照透明性」はしばしば同じような意味で使われるが、コンピュータサイエンスではこれらはだいぶ区別されているように思える。これはなんでなんだろうなぁ、とふと思った。

λ. (->) の種

Haskellには種(kind)の多相はないことになっているが、GHCでは「(->)」は「*」と「#」という複数の種の型に適用可能だったりする。では「->」の種はどうなるかと思って試してみたら、こんなの出てきた。

Prelude> :k (->)
(->) :: ?? -> ? -> *

λ. 親王誕生

なんとも目出度いです。 もっともこれで皇統の問題が根本的に解決するわけではないですが……

Bottom Note (2006-09-06)で紹介されていた、アルジャジーラ(الجزيرة)の記事の「The boy will be third in line to the Chrysanthemum throne after his uncle and his father.」という表現には「へー」と思った。「Chrysanthemum」って何かと思ったら菊のことなんですね……

それから、テレビで言っていた「『おぎゃー』とおっしゃった」という表現が、なんだか可笑しかった。

λ. The Daikon invariant detector

<URL:http://lambda-the-ultimate.org/node/1700> より。 機械学習で不変量をというアイディアが面白い。

λ. Haskellに正格性注釈が無いのは何故か?

lethevert is a programmer - Haskell : モナドはややこしい のコメント欄での議論で、「何故HaskellにはCleanの正格性注釈にあたるものはないのだろうか?」と思い少し考えた。

GHC等の処理系では内部で正格性解析を行い、正格性の情報を利用して最適化などを行ってはいる。では、もし正格性の情報をユーザーから見えない内部情報ではなく、型として扱うことにしたらどうなるだろうか。とりあえず、一般の関数型の型構築子 (->) とは別に、正格な関数のための型構築子 (!->) を導入することにする。そして、(!->) a b のシンタックスシュガーとして !a -> b と書けることにもする。

関数 a -> b が必要とされる文脈では正格な関数 !a -> b も使えて欲しいから、!a -> b は a -> b のサブタイプになるのが望ましい。しかし、現在のHaskellにはサブタイプ関係は存在しないため、これを実現するには型システムにそれなりの変更を加える必要がある。障壁その1。

これが仮に解決したとして、次に「f x = 0」のような非正格な関数に対して、正格な関数の型を宣言したときにどうなるかを考えてみる。例えばこんな感じ。

f :: !Int -> Int
f x = 0

このとき処理系はどのように振舞うべきか。

1. 明らかな選択肢は「型エラー」とすることだろう。しかし、正格性解析は通常は型検査後に行われるので、型エラーにしようとするとややこしいことになる。また、正格性解析は型検査と違ってそもそも完全ではなく、正格な関数を解析機が正格と認識できない場合がある。そのような場合にエラーとなるのは(よほど分かり易い基準でも無い限り)どうかとも思う。
2. それとは別の選択肢として、エラーにはせず正格な関数としてコンパイル/実行するという選択肢がある。ただ、これは同じ式が型によって違った意味を持つということを意味するので、一種のアドホック多相である。型クラス以外のアドホック多相をさらに導入するというのは、やはり躊躇われるものがある。

これらの問題に勝る正格性注釈のメリットがあるかと言えば……私には無いように思われる。*1

ただ、Haskellも正格なプログラムを書きやすくする方向へは進化していて、「f x = x `seq` 0」と書く代わりに「f !x = 0」と書くことの出来るBangパターンというものが GHC 6.5 には実装されている。*2 正格なプログラムが書きにくいという単純な問題はこのBangパターンでまず解決するだろう。それでもしも型レベルでしか解決できない問題が残ったとしたら、その時点で正格性注釈について議論すれば良いのではないかと思う。

2006-09-14 追記

lethervertさんが Clean の正格性注釈について、<URL:http://d.hatena.ne.jp/lethevert/20060911/p1> で解説してくれた。一見して型に見えるけど、実際は型ではないとのこと。これでCleanへの疑問が一つ解けた。

λ. 「デスノート」作者、小畑健容疑者逮捕

正直、車のコンソールボックス内に刃渡り8.6センチのアーミーナイフ(折りたたみ式)を持っていたくらいで……と思わなくもない。みせしめ感がひしひしと。ところで、産経の「ライトのせいで…「デスノート」作者、小畑健容疑者逮捕」という表題は狙っているのかな。

λ. MapReduce: Simplified Data Processing on Large Clusters. Jeffrey Dean and Sanjay Ghemawat

いまさらだけど読んだ。大規模データセットをクラスタ内で処理するためのプログラミングモデル MapReduce の提案・構築・評価。この論文からは特別優れたアイディアや技術は読み取れないが、これだけスケールするものを実際に作って使っているということが一番すごいと思った。

λ. M2ミーティング

wikimania報告会20060902でのtakotのスライドの紹介など。

λ. 今日の名言: 「高度な技術的理由は政治的理由と区別がつかない」

確かにそうかも。

λ. Parsing expression grammar (PEG)

Matzにっき(2006-09-08) - Parsing expression grammar より。なかなか便利で扱いやすそうな形式化だと思った。

• 曖昧性が無い。
• 無制限の先読みが可能なのでレキサとパーサを分ける必要はない。
• Packrat Parser として実装することで、文字列長に対して線形の計算量に。

しかし、 {aⁿ bⁿ cⁿ | n≧1} のPEGはだいぶトリッキーだと思った。 こんなの普通書けないって。

S ← &(A !b) a+ B !c
A ← a A? b
B ← b B? c

それから、以下の部分がよくわからなかった。

It is also possible to build LL parsers and LR parsers from parsing expression grammars, but the unlimited lookahead capability of the grammar formalism is lost in this case.

PEGはCFGでない言語を表現可能なのにLLやLRで扱えるのか?　LLやLRってCFGじゃない言語を扱えたっけ?　それから、「the unlimited lookahead capability of the grammar formalism is lost in this case.」というのは、必要な先読みの上限を変換時に静的に決定可能だから LL(k) や LR(k) になるということか?　いや、上の例を考えてみても先読みの上限は静的に決定することは出来ないか。

Haskell用のパーサジェネレータもあるみたいだし、今度試してみるか。

追記

そういえば、言語の差分やintersectionをとることが可能なパーサコンビネータについて、暖めていたアイディアが一つあったのだけど、PEG + Packrat Parser があれば不要だということに気づいた。しょぼーん。

λ. 『τになるまで待って』 森 博嗣

を読んだ。 Amazonの書評では散々だけど、それなりに楽しめた。 トリックを強引と思う人もいるだろうけど、犯人の行動としてそこまで変だとは思わないしね。だいたい、犯人がミステリー受けするような行動を取らなくてはいけないという理屈はないわけで。

Quotation (p.209)

「そういった、何故そうしたのか、という理由に立ち入ると、最初から数々の可能性が否定されてしまうことになるんじゃないかな」山吹が言う。「そうじゃなくて、物理的にどんな方法が現実にありうるのか、をまず問うべきだよ。理由というのは人間の気持ちの問題であって、そんな心理まで考慮していたら、結局は論理に曖昧性を持ち込むだけで、目標が霞んじゃうと思う」

λ. Comonadic Functional Attribute Evaluation. Tarmo Uustalu and Varmo Vene.

<URL:http://lambda-the-ultimate.org/node/1666> より。あー、そっか。属性文法も一種の contextual effect で、comonadで扱えるのか。気づかなかった。面白い。

λ. [ ruby-Bugs-5711 ] REXML fails to parse UTF-16 XML.

UTF-16なXMLをパース出来ないことがある。 多分、二回デコードしようとしてるんだろう。

λ. [ruby-list:42792] KconvはBMP外の文字を扱えない?

標準ライブラリに、きちんと動作する UTF-8 ⇔ UTF-16 の変換が存在しないのは問題ではないかと思った。

λ. 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 もあるしね。

λ. PPL Summer School 2006

今日は PPL Summer School に行ってくる。 色々な人に会えるであろうから楽しみ。

行ってきた。昨日のSLACSはほとんど宇宙語の世界だったが、今日はこころある人間の言語のようで、気楽に聴いていられた。色々な人にお会いできたが、あまり話すことが出来ず残念だった。

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

• 他の方の感想など

λ. 圏論の諸相

講師

木下 佳樹 先生（産業技術総合研究所）

概要

圏論は、圏の構造についての理論ではあるが、その利用者にとっては、ものの見方を与え、いい定義を探すための道具であるという面がある。定理の証明よりいい定義を見つけるのが難しい、というのは、圏論や型理論に共通の特徴で、同じ数学でも整数論などとちがうところである。圏論特有の普遍性を用いた議論のすすめかたを紹介する。時間があれば、函数プログラマが興味を持たれると思われる単子(monad)と代数系の関係について説明して、単子の公理の種明かしの助けとしたいが、二時間ではあまり内容に深入りできそうにない。むしろ、圏論の学び方について、いくつか提案してみたい。

同型の記号「≅」を「∝」だか「∽」だかで代用していたが、同型の記号「≅」は Unicode には含まれる(U+2245)し、JIS X 0213 にも含まれる(1-2-77)。なので、UnicodeベースのPowerPointでは普通に使えますよ。そうコメントしようかと思ったが機会を逃してしまった。

「証明が自明だとして論文がrejectされる。証明が自明になるよう工夫して理論を構成しているのに、それをわかってくれない」という Michael Barr の嘆きの話が面白かった。Barrほどの人でもそんなことがあるのね。

最後の方で、ちょこっと Lawvere theory や Sketch の話をしていて、「equational horn clause は lawvere theory をはみだすが sketch では扱える」とか「formal theory を対象化しているので、theoryに対する操作を扱える」とか言っていたが、このあたりの話をもっと聞きたかったなぁ。

動かしてみたい人にはAgdaやCoq等の定理証明系がお勧めと言っていたが、個人的には結構微妙だと思う。これらの上で圏論を形式化しようとすると、等号の扱いとか圏論にとって非本質的な部分で落とし穴にはまりがちだと思うので(というか、私ははまった)。それから、個人的には、動く例が欲しいのであれば他にも CPL や Computational Category Theory も試すことも出来ると思う。CPLは、今回扱ったものの中では equalizer や coequalizer は扱えないが、inductive/coinductiveなデータ型は扱えるしね。

それから、時間がないため講演では触れていなかったが、配布資料のMonoid(単)の説明が間違ってる。正しい図は以下の通り。

対応する等式は以下のようになる。

• m∘(id_M×m) = m∘(m×id_M)∘α
• m∘(e×id_M) = λ
• m∘(id_M×e) = ϱ

λ. お昼

中央食堂(?)で定食。

宇宙語は沢山ある ⇒ 宇宙は広い

圏論や数学での「極限」という言葉の使われ方は非常にまぎらわしい。20030704#p01を参照。

λ. 2時間で真似(まね)ぶ関数型言語のコンパイラ

講師

住井 英二郎 先生 (東北大学)

概要

関数型言語MLの極めて小さなサブセットのコンパイラについて解説する。表面言語からアセンブリまで、すべてのパスを理解することにより、「関数型言語も命令型言語と同様に効率のよいコードへ（しかもより簡単に）コンパイルできる」ことを納得し、「関数型言語は難しい」「関数型言語は遅い」「関数型言語は命令型言語とまったく異なる」といった迷信を打破する。

<URL:http://d.hatena.ne.jp/sumii/20060912/1158058050>

色々なマニアックな話や裏話(?)が聴けて楽しかった。

僕はA正規形(A-Normal Form; The Essence of Compiling with Continuationsを参照)とK正規形(K-Normal Form)の違いがずっと気になっていたのだけど、その違いを教えてもらったのは収穫だった。A正規系ではletの右辺のletは許されず、また末尾以外のifも許されない。それに対してK正規形はそこまで厳しくはない。例えば、「... (if ...) ...」のような式は、CPSやA正規形だとまわりの部分を全部複製するか関数にするかする必要があり、これが嫌だったためMinCamlでK正規系を選んだとのこと。というか、このことは <URL:http://d.hatena.ne.jp/sumii/20051207/1133967246#c> に既に書いてあったのに見落としてた。

質疑で「Closure変換はラムダ・リフティング(lambda lifting)ではダメなのか?」という話がU野氏からあった。部分適用が存在するならば、ラムダリフティングで super combinator に変換し、部分適用すればローカルな関数が得られる。ただ、MinCamlには部分適用がないからクロージャ変換をラムダリフティングに置き換えることは出来ない。結局、「部分適用」か「クロージャ変換」のいずれかを実装すれば他方も実現できるということだと思う。なお、部分適用の実装については Making a fast curry: push/enter vs. eval/apply for higher-order languages を参照せよ。

以下雑多なメモ。

• Schemeはset!でいきなり変数に代入できるので、コンパイラが面倒くさい。
  • 【2007-01-17 追記】 黎明日記(電撃戦) (2007-01-02)で「自分の記憶が正しければ Common Lisp や Emacs Lisp の setf/setq なら可能だけど Scheme の set! は無理だったと思う」ツッコミが。もう記憶が怪しいのだけど、「いきなり」というのは「MLでは参照型の値を使うのに対して、Schemeでは一般の変数に対していきなり代入することが出来てしまう」ということについての話だったと思う。
• アセンブリ生成が長いのは、書かなくてはならない文字列が長いからであって、中身が長いわけではない
• コンパイラ作っていて一番難しかったのはif文。
• K正規系への変換では
  • Sparcでは定数(特に大きな定数)は則値で使えないので、定数も一時変数におく。
  • 変数を一時変数におかないのは、デバッグのときに見やすいように。
• インライン展開のヒューリステッィクは「シンタックスツリーのノードの数」と「千回やって止まらなかったら止める」程度の簡単なものでも十分。
• Lispのダイナミックバインディングは最初はバグだったらしい。
• フロー解析のかわりに、関数の定義があったらスコープの中だけで「自由変数がない」ことを認識。
• OCamlで末尾呼び出しを判定するには、生成されたバイトコードをみるのが、事実上一番手軽。
• ocamloptは多相性をサポートするため浮動小数点数をボックス化してアロケートするから、一部のベンチマークで遅くなる。
• raytraceでmincamlがgccと比べて遅いのは、浮動小数点演算のスケジューリングの最適化が大きい。
• ocamloptは let rec と書かれているだけでインライン展開を諦めるので注意。
• コンパイル時間。レジスタ割り当ての先読みに O(n²) とかあるはずだけど、gccもO(n²)くらいのアルゴリズムは結構使っていたりする。レジスタ割り当てでバックトラックしないようにしたのでそんなに問題にはならないのでは。

λ. 述語抽象化によるアルゴリズムの検証 〜 シェープ解析を例として

講師

田辺 良則 先生 (産業技術総合研究所)

概要

設計したアルゴリズムが正しいことを検証したいとき，それを表現したソースコードまたは擬似コードの検証に帰着できれば嬉しい．「検証」への様々なアプローチのなかに，モデル検査と呼ばれる「力ずくで全部の可能性を数え上げてチェックしてしまおう」という手法があるが，対象がソースコードの場合，素朴に扱うと可能な組合せが多すぎて，この手法は破綻してしまう．しかし，抽象化という，本質的でない違いを無視することで組合せを減らす方法の進歩により，ソースコードの検証も可能になってきている．このチュートリアルでは，抽象化，特に，このような検証の枠組みとしてよく用いられる述語抽象化を紹介する．基本となる考え方から始めて，いくつかのトピックと，研究レベルの検証ツールについて述べ，応用として，シェープ解析と呼ばれる分野でのアルゴリズム検証例を示す．

「圏論の諸相」はほとんど既知の内容だったし、「2時間で真似(まね)ぶ関数型言語のコンパイラ」もある程度前提知識を持っている話だったのに対して、この話は色々と新鮮だった。

述語抽象化の話が面白い。私は、具体状態の上に同値関係を定義して、抽象状態と遷移関係を定義するのだと思い込んでいたが、そうではないのだな。その代わり、述語抽象化によって抽象状態を定義し、最弱事前条件を使って遷移関係を定義する。その上で Existential Abstraction を示し、simulationの関係になっていることを確かめる。

「述語抽象化による安全性検証: 全体像」のスライドのループの終了が保障されているわけではないという話で、質問してループが終了しない例を教えてもらったのだけど、具体例を忘れてしまった。もし知っている人がいたら、教えていただけるとありがたいです。

情報の不等号、この不等号の向きは逆にして1/2を⊥とした半順序集合と考えた方がよいのではないかと思った。けど、開集合のようなものと考えれば、1/2がこの不等号で最大なのも納得できるか。

それはそうと、例の『四日で学ぶモデル検査』(読書記録) の続編が読みたくなった。

λ. 今日のSLACS

今日は、学術的興味よりも楽しさを優先して、SLACSではなく、PPL Summer School に来てしまったわけだけど、今日のSLACSがどんな感じだったのか気になる。昨日は様相論理関係が多かったが、今日はもう少し自分の興味に近い話が多かったしね。それから、それらの中で「Prologによるmakeの実装 〜Mipl〜」という題目だけが浮いていたのでﾜｸﾜｸﾃｶﾃｶしてたのに……*1

発表資料とかって公開されないのかなぁ……

【追記】 「PrologによるMakeの実装」のプロシンでの発表についての言及をメモ。

ささださん

「Makefileの実装，という言葉が面白かった．」

とおるさん

「じつは一番興味があるタイトルだったんだけど、いまは実装はぜんぜんできてないらしい。」

λ. カクレカラクリ

期待してたけど、つまらなかった。 栗山千明は結構似合っていたと思うが。

• TBS「カクレカラクリ」
• karakuri120.jp
• mixi:カクレカラクリプロジェクト

λ. Pangoで縦書テキストが表示可能に

射撃しつつ前転 (2006-09-13)より。素晴らしい。

以前に「starts at bottom of page」というエントリでは「縦書きの日本語の中にアラビア文字を埋め込む時には、改行方向を合わせるために下から上へ書く気がする」と書いたけど、リンク先のスクリーンショットではアラビア文字を上から下へと書いているな。実際の例を見たことがないので、どちらが正しいかは知らんけど……

【追記】……とか書いていたら、小熊さんから「左縦書きのモンゴル語（蒙古文字）にローマンアルファベットが混じる場合」の事例が。 ありがとうございます。

λ. Haskellのリストとはそもそも何者かという問題

Haskellの代数的データ型の解釈は、OCamlのような正格な言語での解釈よりも確かに複雑だけど、使っていて悩んだ経験はあまり無い。そもそも、Haskellのデータ型にどんな値が存在するかを考えるときに、いちいち領域理論を使って考えたりしないし。……複雑に感じるかどうかには慣れの問題も大きいのではないかと思います。

OCamlでのリスト型の領域は⊥を除けば、全ての有限リストのみからなる集合、すなわち帰納的に定義される集合になっている。一方、Haskellでのリスト型の領域は「⊥を含む値」を除けば、全ての有限および無限のリストからなる集合、すなわち余帰納的に定義される集合になっている。したがって、始代数になっているかはさて置き、帰納的というよりは余帰納的なものとして理解したほうが良いと思います。

ところで、<URL:http://d.hatena.ne.jp/taisuke_h/20060827#1156687935> によると、OCamlでも無限リストがリスト型に属するようです。ということは、きちんと意味論を考えるのならOCamlの場合にもHaskellと同様の領域を考えなくてはいけないような……。それとも「lazy」はHaskellでの「unsafe〜」のように意味論を無視したバックドアなのでしょうか……

【追記】 <URL:http://d.hatena.ne.jp/yoriyuki/20060915/p1> で、Lazyモジュールは型が変わるので問題ないとの指摘。うわー、恥ずかしいことを書いてしまったー orz

【さらに追記】 いや、lazyについては間違いだったけど、「let rec a = 1 :: 2 :: a」は結局無限リストになるのだから、無限リストを含む領域を考えなくてはならないというのは変らないはず。

【追記】 sumiiさんの人から借りてきた２セントも参照のこと。

λ. CleanとHaskellの宣言スタイルの違い

Concurrent Clean : カリー化と効率 の「Cleanではエクスポートする関数は定義モジュールファイルに関数の型宣言だけを記述するというスタイル」という部分を読んで、HaskellとCleanの宣言のスタイルの違いが少し理解できた気がする。

Clean入門(22)：モジュールによれば、Cleanではモジュールを使うのに必要な情報は*.dclファイルとしてユーザによって記述される。そのため、効率的なコンパイルのために、アリティや正格性も宣言の一部として記述することになっているのだろう。 それに対して、Haskellの代表的処理系であるGHCでは、モジュールをコンパイルすると*.hiファイルが生成され、この中にモジュールを使うのに必要な型情報・アリティ・正格性等の情報が格納される*1。そして、そのモジュールを使うコードをコンパイルする際にはそこから情報が参照される。そのため、正格性やアリティをユーザが宣言で明示せずとも、それらを利用した効率的なコード生成が可能になっている。 そのあたりの違いが、HaskellとCleanの宣言のスタイルの違いの一つの理由ではないだろうか。

ところで、どうしてこのような違いが生まれたか考えていて感じたのだけど、Haskellは出来る限り言語や意味論を拡張せず処理系で対処するのに対して、Cleanは言語や意味論を拡張して対処する方にわりと寄っているように思える。モナドvs一意型や、ラムダ計算vsグラフ書き換え系といった対比からもそれはうかがえる。以前はCleanのことを「Haskellに似てるけど何だか奇妙な言語」だと思っていたけど、そう考えるとCleanのデザインディシジョンもなんだか理解できそうだ。

λ. 今日の英語: kind of

If you don't know Arcueid, you're really kind of a failure as an otaku.

「a kind of」と言わなくて良いのだろうか。もし「kind of」を副詞的に使っているのならその後にくるのは形容詞か動詞のような気がするし。

λ. [ruby-ext:02317] Procをブロックとして渡すには

RubyKaigiの後に聞いてみようと思っていたのに、すっかり忘れていた質問。拡張ライブラリで少しメタなことをやろうとすると、結構必要になると思うんだけどな。

λ. M2ミーティング

非生産的すぎ。

λ. Mule-UCS は JIS X 0213 の文字を UTF-8 で保存できない?

Meadow2.xでMule-UCSを使っているのだけど、バッファ中に JIS X 0213 の文字(例えば⊗とか≅とか)が含まれていると、UTF-8で保存できなくて困ってしまう。UTF-8のファイルを読み込むときには JIS X 0213 の文字として読み込むくせに、保存できないというのは微妙すぎ。ひょっとして、Meadow3.x(Emacs22)では直ってたりするのかな……

【2006-09-26追記】 Meadow 3.x にしたけど解決しなかった。Mule-UCS を外してしまって、JIS X 0213 系のエンコーディングは jisx0213 without Mule-UCS で読み書きするようにすれば良い?

【2006-10-01追記】 <URL:http://www.m17n.org/mlarchive/mule-ja/200208/msg00014.html> によると、un-define-safe-charsets-for-coding-systemsにjisx0213がないためで、unicode-basic-translation-charset-order-listを設定すれば良かったらしい。 そのようにしたら解決した。

λ. 『ふつうのHaskellプログラミング』読書会

今日読み終わるかと思っていたけど、まだ続く。

λ. 『ハッカーズ』

PDFで半分公開されているので読んでみた。 結構引き込まれるものがある。

• スラッシュドット ジャパン | ケビン・ミトニックの「ハッカーズ」、PDF で半分公開:
• 発売前先行公開（PDF版）＋この話題書を「あなたのブログでオススメしてみませんか」コンテスト

λ. 第二一回圏論勉強会

今日は圏論勉強会だった。写真。グラフA={・→・}の冪 A^A の計算が面倒だった。

λ. 単語力(タンゴリキ)

単語力は英語の語彙力を判定するサイトです。１０題の３択問題に答えると、あなたの語彙力が０から９９９までのスコアとなって出てきます。スコアは単語の難易度と解答時間と正答率から計算されます。単語力には４０００人が参加するランキングがあり、そこで他の利用者と順位を競うことができます。

Joker小言集:単語力 で知った。結構はまりそう。現在の単語力461。

λ. 𠮷野家の牛丼が限定で復活

ニュースで「いと、おいしい」と聞こえたと思ったら「いとおしい」だった。牛丼がいとおしいって……

λ. 国歌斉唱強制は違憲・東京地裁判決

なんか納得のいかん判決だなぁ。すっきりしない。 まあ、たぶん高裁でひっくりかえるんじゃないかとは思うが。

まず、式典を適正に行うことは教師の職務の一環であり、そのために教育委員会が通達や指導を行うのも通常のことのはずです。そして、学習指導要領を前提とすれば、「入学式や卒業式などにおいては、その意義を踏まえ、国旗を掲揚するとともに、国歌を斉唱するよう指導するものとする」とある以上、国旗掲揚と国歌斉唱が適正であることも明らかです。で、もし教師が自らは起立や斉唱を行わないとしたら、その教師の「指導」が説得力を持つとは思えませんから、そのために都教育委が通達や指導を行うのは裁量の範囲でしょう。

一方、地方公務員法第32条には「職員は、その職務を遂行するに当つて、法令、条例、地方公共団体の規則及び地方公共団体の機関の定める規程に従い、且つ、上司の職務上の命令に忠実に従わなければならない」と規定されているわけで、規定や通達に反し職務を放棄するのであれば、処罰の対象になっても仕方がないでしょう。もちろん、犯罪を行わされるとかなら話は別だけど、そういう話ではないしね。

現在の学習指導要領を否定するならともかく、単に大綱的な基準であるからといって、そこから思想良心の自由を職務放棄の免罪符にするのは個人的にはちと無理があるように思えます。実際、通達以前の同種の訴訟の多くでは教諭側が敗訴していると聞いていますし。

それはそうと、国旗・国歌は国家の象徴なわけで、それらに最低限の敬意を払うことの出来ないような人が、何故公僕として公教育に従事することを選んでいるのかがそもそも不思議です(本人にとってそれは矛盾ではないの?)。日本には職業選択の自由があり、自らの思想・良心を絶対に曲げたくないのであれば、信念に矛盾しない職業を選ぶべきでしょう。例えば、暴力を無条件に悪とする信念を持つ人は自衛官にはなるべきではないでしょうし。

ところで、判決はこの通達及びそれに基づく指導を教育基本法第10条の「教育は、不当な支配に服することなく、国民全体に対し直接に責任を負って行われるべきものである」における「不当な支配」にあたるとしているわけですが、同じ条文中の「国民全体に対する直接の責任」についてはどう考えるべきなのでしょうか。第九二回帝国議会衆議院教育基本法案委員会議第一回(1947-03-14)の中で、永井勝次郎委員の質問に対する辻田力文部事務官の答弁には以下のようにあるそうです。

次の「国民全体に対して直接に責任を負って行われるべきものでる」と申しますのは、さればとて、教育者が単なる独善に陥って、勝手なことをしていいということではないのでありまして、教育者自身が国民全体に対して直接に責任を負っておるという自覚のもとに、教育は実施されなければならぬということを徹底いたしますために、まず、教育行政上において教育自体のあるべき姿をうたったわけであります。

で、えーっと、件の方々の行動は正直「国民全体に対する責任」を負っているようにはあまり見えないわけですが……

……と、釣られてみたクマ──！！

しかしまあ、20050331#p03でも書いたが、こんな事で揉めてるのは本当に阿呆らしいよな。

参考

• 問題となった通達
• 国旗及び国歌に関する法律

λ. let rec と循環的定義と有理数と

ふと、OCaml で let rec を使って定義される値というのは有理数に似てるなと思った。リスト型を例にとると、任意の無限リストではなく途中で循環が現れる無限リストだけが表現可能で、これは循環小数(=有理数)に似ている。それから、自然数がinductiveで実数がcoinductiveなので、その中間は有理数だろうという安直な思いつき。

といって、そのような不動点を特徴付ける原理が思い浮かぶわけでもないけど。

【2006-09-26追記】 そのものずばり rational type という概念があることを知った。 そういや、rational tree というのもあったなぁ。 これらが圏論の言葉で定義できるかが気になる。

【2006-09-29追記】 キャリアが有限集合であるF余代数とそれらの準同型からなる圏を CoAlg(F)_fin とする。忘却関手 U_F: CoAlg(F)_fin→Set の余極限を考えるのはどうか?　……いや、このアプローチはイマイチな気がする。むしろ Adámek らの方法の特別な場合と考えることが出来ないかどうかを考えたほうが良いか?

λ. 『アンチ・ハウス』 森博嗣, 阿竹克人

を読んだ。

λ. 『ガセネッタ＆(と)シモネッタ』 米原 万里

を読んだ。

λ. 正格な言語での不動点演算子

正格な言語、例えばOCamlでは、以下のようにして不動点演算子を定義することが出来る*1。これは常識ですね。

# let rec fix f x = f (fix f) x ;;
val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = <fun>
# let fib' f x = if x <= 1 then 1 else f (x - 1) + f (x - 2) ;;
val fib' : (int -> int) -> int -> int = <fun>
# let fib = fix fib' ;;
val fib : int -> int = <fun>
# fib 10 ;;
- : int = 89

で、ここでクイズなのだけど、f に対して fix f というのは一体何者でしょうか?　「そんなの f の最小不動点に決まってるじゃん」と思うかも知れないけど、ここでは正格な言語を考えているので「f ⊥ = ⊥」で、最小不動点は⊥なのでした。

λ. 自転車パンク

自転車の後輪の空気がすぐ抜けてしまうので、パンクしたかなと思い自転車屋へ。 やはりパンクしていて、チューブにパッチを当ててもらった。 手際よく作業しているのを見ていると楽しい。

λ. プログラミング言語処理系に関するコロキウム

今日はプログラミング言語処理系に関するコロキウムというのがあったのだけど、筑波まで2時間以上かかることを知って、諦めてしまった。

soutaroさんの「大堀先生の偉大さについて」というエントリが非常に楽しげ。

λ. Rubyist Magazine 0016 号

を読んだ。

λ. 誕生日

今日は誕生日。

最近時間が過ぎ去るのがずいぶん速い気がする。 こんな調子だと人生なんかあっという間に終わってしまうに違いない。 けど、それは流石に困るので、もう少し気合入れて色々頑張らねば。

λ. Build, Augment and Destroy, Universally. Neil Ghani, Tarmo Uustalu, and Varmo Vene

<URL:http://lambda-the-ultimate.org/node/1717>で知って何気なく読んだのだが、「うわっ、やられたっ」と思った。何故これを自分で思いつけなかったのかと思うと悔しい。

帰納的なデータ型を関手Fの始代数としてではなく、忘却関手 U_F: F-Alg → C の極限錐(limiting cone) として特徴付ける。U_Fの錐(C,Θ)から極限錐(μF,fold_F)への一意な射への対応を与えるのがbuild。この特徴づけと始代数による特徴づけは等しい。

ここで、(C,Θ)が錐になっているために必要な条件は ∀h:(X,φ)→(Y,ψ). U_F(h)∘Θ_(X,φ) = Θ_(Y,ψ) で、ちょっと書き換えると ∀h:X→Y. (∀φ:FX→X, ψ:FY→Y. h∘φ = ψ∘Fh ⇒ h∘Θ_(X,φ) = Θ_(Y,ψ)) となり、実はΘを hom(F-,-)→hom(C,-) と考えたときの strong dinaturality になっていたりする。

もちろん、fold/build だけでなく unfold/destroy についても同様のことが言える。また、buildのさらなる一般化であるaugmentもモナドを使って同様に扱うことが出来る(が、こっちは結構ややこしい)。

【2006-11-15追記】augment周りのコードをHaskellで書いてみる

maoさんが<URL:http://d.hatena.ne.jp/m-a-o/20061107#p2>で「augmentを書こうとして挫折した。Monadに持ち上げるとこの(>>=)が定義できねー」と書いていたので、試しにHaskellで書いてみた。Control.RecursionモジュールはCategory Extrasのもの。 型クラスのインスタンスを定義するためにnewtypeでラップしているために、元の定義よりだいぶ複雑になってしまっている。あと、Category Extras でのFixpointクラスにあたるようなクラスを定義できれば、もっと扱いやすい定義が可能かも知れない。

import Control.Recursion
import Control.Monad

data T' h a x
    = Eta' a
    | Tau' (h x)

t' :: (a -> b) -> (h x -> b) -> (T' h a x -> b)
t' f g (Eta' a)  = f a
t' f g (Tau' hx) = g hx

instance Functor h => Functor (T' h a) where
    fmap f = t' Eta' (Tau' . fmap f)

newtype T h a = T{ unT :: Fix (T' h a) }

eta :: Functor h => a -> T h a
eta = T . In . Eta'

tau :: Functor h => h (T h a) -> T h a
tau = T . In . Tau' . fmap unT

ext :: forall h a b. Functor h => (a -> T h b) -> (T h a -> T h b)
ext f = fold (t' f tau) . unT

instance Functor h => Monad (T h) where
    return  = eta
    m >>= f = ext f m
instance Functor h => Functor (T h) where
    fmap = liftM
instance Functor h => Fixpoint (T' h a) (T h a) where
    inF  = T . inF . fmap unT
    outF = fmap T . outF . unT

augment :: Functor h =>
           (a -> T h b) ->
           (forall x. (T' h a x -> x) -> (c -> x)) ->
           c -> T h b
augment f theta = theta (t' f tau)

λ. 植芝理一のマンガみたいな人

MORILOG ACADEMY - 【図工】　特別講義２の記述を読んで、最上の日々(2006-09-25)と同じく「植芝理一のマンガみたい」という感想を持った。いやー、世の中には面白い人がいるものだ。

λ. 小泉首相退任

小泉政権が発足したのが2001-04-26だったから、それから大体5年半がたったことになる。その間には色々なことがあった。

• 派閥推薦を受け入れない組閣
• 経済財政諮問会議主導の予算編成と歳出削減
• 「改革無くして成長なし」という言葉に代表される構造改革路線。不良債権処理の加速。景気の低迷と失業率の増加。
• 産業再生機構の発足。ペイオフ解禁の延期。金融機関の保有株買い入れ。
• 911の同時多発テロと、その後成立したテロ対策特別措置法に基づいた後方支援
• 外務省改革と、田中真紀子と鈴木宗男の対立
• クリントン政権下で冷え込んだ日米関係の改善
• 電撃的な訪朝と平壌宣言。拉致被害者5名およびその家族の帰国。その後の日朝関係の行き詰まり。
• 米国のイラク攻撃に際しての率先した支持
• イラク特別措置法の成立と、それに基づくイラク復興支援
• 靖国神社参拝をきっかけとした中韓二カ国との関係の冷え込み
• 有事法制の成立
• 東シナ海の天然ガス田開発に関する日中の対立
• 道路公団民営化をはじめとする特殊法人改革
• 年金改革
• スマトラ沖地震と津波災害に対する支援
• 郵政民営化と郵政解散
• 狂牛病騒動
• 北朝鮮によるミサイル発射実験
• ……

評価は人それぞれだけど、振り返るとそれなりに感慨深いものもある。 個人的には「改革無くして成長なし」の誤りを認めずに退任してしまうことは残念だし、個別の政策には批判したい部分が多々あるが、同時に小泉政権は概ねよくやっていたのではないかとも思う。 ともあれ、5年半お疲れ様でした。

λ. Alloy Analyzer

The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

MISE EN PAGES | alloy - the model analyzer より。面白そう。

λ. 生協でバスカードを買う

残念。生協ではバスカードはEdyで買うことが出来ない。 Edyに少しチャージしすぎてしまったのでEdyを消費したかったのだけど、Edyが使えないのならいつものように金券ショップで買っていれば良かった。しょぼーん。

λ. 革命機械

銀茄子園の「革命機械（その２）」という絵を見て感動した。発想が凄い。

• 革命機械（その２） (18禁; 残酷描写注意)

λ. 今日の向井研

今期はHaskellをやるらしいので久しぶりに顔を出してみる。さかいくん(≠私)を目撃できるかと思ったが、残念ながら目撃できなかった。向井先生は圏論の効用を語るのに例のオートマトンと余代数の話をしていた。 Aczelがhypersetという名前をあまり好きでなかった一方、Barwiseはそのような存在に対する信念があったらしいとか。 それからコルメラワー(Alain Colmerauer)の無限木の理論との対応(?)とか。

Lambek計算に関して「Language & Grammar : Studies in Mathematical Linguistics and Natural Language」という本を紹介してもらった。

λ. 現実逃避

領域理論や圏論の難しい話に疲れて、プログラミングに現実逃避。 楽しい。まあ、これも思うように行かないことが多いんだけど。

λ. 『日本の国境』 山田 吉彦

を読んだ。