2002-04-01
λ. Y先生のところに、僕をSAに使ってみないかとアピールしに行こうかと思ってたら、先生からメールが。すっごい偶然。感激。まさかエイプリルフールじゃないよね?
λ. 今日は、エイプリルフール・ネタを一日考えていました。(嘘)
λ. Binary operations and diagonal arguments
対角線論法は diagonal arguments っていうのか。
2005-04-01
λ. 『独島／竹島 韓国の論理』 - 金学俊 著, Hosaka Yuji 訳
何というか、読んでて疲れたよ、パパン。
私が日本人だからかも知れないけど、「独島は韓国領」という結論ありきで、それに沿うよう史料を「〜に違いない」「〜の可能性がある」「〜と解釈できる」といった具合に当てはめているという印象を少し受けた。
λ. 中国外務省「軍事費、日本の方が多い」
日本の防衛費が多いのには人件費が高いという理由もあるし、中国の軍事費*1が少ないように見えるのには人民元が不当に安いという理由もあると思う。額の単純な比較にそれほど意味があるとは思えない。ちなみに、人員は圧倒的に中国の方が多いし、軍事費のGDP比や政府予算比でみても中国の方が高かったはず。それに加えて、中国はここ数年軍事費の伸び率が前年比二桁増を続けてて、現在軍拡まっしぐら…… わたしゃ具体的な戦力については全然知らんけど、客観的に見て日本より中国の方がずっと軍事に重きを置いてるのは間違いないと思うよ。
それにしても「中国はどの国も侵略したことはない」ってのは悪い冗談だとしか思えん。チベット、ウイグル、満州を武力で併合したのも、朝鮮戦争に参加したのも、パラセル諸島(西沙諸島,ホアンサ諸島)を武力で制圧し事実上領土化したのも「侵略」にはあたらないと? それから今現在「反国家分裂法」を制定し武力で台湾を脅しているのは?
(2005-11-04追記) CIA の The World Factbook の Military の項目を日本と中国で比較してみる。……普通に中国の方が多いんですけど。
| Japan | China | |
|---|---|---|
| dollar figure | $45.841 billion | $67.49 billion |
| percent of GDP | 1% | 4.3% |
*1 中国は軍事費の全体を公表しているわけではないという話もあるが……
λ. 『ルビま！』200504号（休刊号）
月刊『ルビま！』は、今月号(2005年4月号)をもって休刊いたします。これまで応援していただいた読者の皆様には深く感謝しております。 大変ありがとうございました。
思いっきし笑いますた。GJ!
2007-04-01
λ. MAD PEOPLE β01: EPISODE 1101 「でかマクロとぷちマクロ」
<URL:http://straws.sakura.ne.jp/madb01/index.cgi?bid=1101> に参加していた。
2008-04-01
λ. 『圏論による論理学—高階論理とトポス』 清水 義夫
貸してもらったので、ざっと読んだ。 トポスに関しては元々あまり知らなかったこともあり勉強になったが、哲学的な話は正直よくわからなかった。
第一章 関数型高階論理
関数型高階論理 λ-h.o.l. の 定義は、プリミティブを少なくするために工夫している部分以外は普通。 λ-h.o.l は、型の一つとして真理値の型 t を持ち、命題はこの型を持つような項(≠型)であるような論理。 この論理だと命題それ自体は型にならないので、型理論からカリーハワード同型対応で得られる高階論理とは流儀が違う感じ(?)。 そういえば、「言語の意味論」の授業でモンタギュー文法とPTQをやったときに使った内包論理ILもこんな感じの高階論理だった(c.f. 言語の意味論(2006))。
と思ったら、簡易モンタギュー文法の話が出てきた。モンタギュー文法についてもう少し詳しい話を知りたい人は前述の「言語の意味論」の講義資料と、中村さんのノート「UG とPTQ の概要」とを読むと良いと思う。
第二章 トポス
圏論の諸概念とトポスを定義して λ-h.o.l. をトポスで解釈する。
トポスで解釈するといっても任意のトポスではなく、集合圏のトポスでの解釈。 なんだ、一般のトポスで解釈するんじゃないのね。 まあ、第一章で λ-h.o.l. は古典論理として定義されているので、任意のトポスで解釈することは出来ないのは当然だけど……λ-h.o.l.はなんでわざわざ古典論理にしたのかな。
ラムダ式に対する解釈の定義は、あまりフォーマルな定義にはなっていないが言いたいことは分かる。 ただ、論理記号 T, F, ¬, ∧ は略記法として導入していたので、それに対して明示的に定義を与えているのは変。 まあ、略記法に基づいて解釈しても同じものになるはずだけど。
それから、第一章で導入していた λ-h.o.l. の拡張には、確定記述(definite description)と自然数があったが、自然数しかトポスで解釈していないのは何故だろう。 (追記: 確定記述(definite description) - ヒビルテ (2008-04-03)で少し書いたが、確定記述の解釈にはコンテキストないしは継続のような概念が必要になるが、トポスにはそれらに直接対応する概念はないので、直接の翻訳は出来なくて当たり前。)
あと、λh.o.l. の集合圏のトポスでの解釈の健全性を証明していながら、完全性については全く触れていないのはちょっと拍子抜け。 トポスが「われわれの知性にとって普遍性かつ基底的な事態に根ざす言語」であることから、λ-h.o.l.が「われわれの知性にとって普遍性かつ基底的な事態」に係わっていることを主張するためには、単に解釈可能というだけでなく、完全性などのより強い性質を示さなくて良いのだろうか。 トポスはリッチな構造を持っている分、λ-h.o.l. に限らずいろんなものを解釈可能なわけで……
それから、トポスの定義で「始対象」「直和」「プッシュアウト」の存在条件が不要であることについては、証明はややこしいとかではぶかれていたが、どうやるんだろう。 トポスはよく知らないので、すぐにはわからなかった。 後でやってみる。
第三章 トポスの基本定理
著者がトポスの基本定理と呼ぶ以下の定理の証明。
E をトポスとし， B を E の任意の対象とする．このとき， E↓B もトポスである。
また A も E の任意の対象とし、f : A→B を E の矢とするとき、 E↓A と E↓B の間には， f* : E↓B → E↓A および ∑f : E↓A → E↓B, ∏f : E↓A → E↓B なる関手 f*, ∑f, ∏f が存在し，∑f ⊣ f* ⊣ ∏f が成立する。
この本では Locally Cartesian Closed Category (LCCC) については言及されていないが、これは E↓B に subobject classifier が存在することと、E が LCCC であることとを示すことと同じ。
第四章 プルバック関手f*の右-随伴関手∏f
前章で一般的に証明していなかった部分のきちんとした証明。 結構面倒くさい。以前にrpfさんから elementary topos は LCCC になっていると聞いていたけど、そのときはこんなに面倒くさいとは思わなかったよ。
partial arrow classifier と singleton の概念をはじめて知った。 面白い。
この章が一番勉強になった。
第五章 リミット、空間性トポス、限量記号
.
結び
「多少比喩的にいえば」と断ってはあったものの、対象でトポスをスライスすることが何故「視座」を設定することになるのか分からなかった。 というか、ここで言っている「視座」が何なのか分からなかった。 LCCCによる型理論の解釈(c.f. On the Interpretation of Type Theory in Locally Cartesian Closed Categories)の場合だと、コンテキストに対応するので理解できないこともないのだけど。
他にも、哲学的なことに関しては、「示された」と書かれていることで、何故言えるのか論理を追うことが出来なかった部分が多い。
関連
- はてなダイアリー - 「圏論による論理学—高階論理とトポス」を含む日記
- lambda high order logic - 白のカピバラの逆極限 S144-3
- nucさんによると結構酷い間違いもあったみたいだけど、すごい勢いで斜め読みしてたので気づかなかった……
ψ kjana [.数学の人かと思ってたらもうちょっと早く出てたら 読んでたんじゃないかという論文読んでてびっくり :-)]
ψ さかい [数学の人だと思われていたのは初めてかも。 数学は好きだけど、SFCにはあまり数学の授業ないからなぁ…… ちなみに、..]