曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

おすすめの記事

 当ブログは論理学を中心とした哲学・数学・計算機科学の勉強記録と、アニメの批評・感想を中心に書いております。おすすめの記事は以下です。

 

 

cut-elimination.hatenablog.com

 アニメにもジェンダーフェミニズムを考えるうえで示唆に富んだ作品はたくさんありますよ、という記事です。いろいろな作品を紹介しています。本当の目的はアニメ一般に対する「前時代的」という批判への反論です。私の調べが進むにつれてアップデートされていきます。

 

 

cut-elimination.hatenablog.com

 アニメーションおよびアニメの技術面や、アニメを見るという経験にフォーカスを当て、「アニメとは何か?」というテーマを哲学的に考えます。アニメが好きな方、哲学に興味がある方におすすめです。

 

 

cut-elimination.hatenablog.com

 藤井聡太先生の脳内には将棋盤がないという説を、様々なインタビューや棋士の証言をもとに検証しています。

 

 

cut-elimination.hatenablog.com

 マンガ『チェンソーマン』第43話に出てくるロシア語の歌を翻訳しています。元ネタはなんなのかもちょいと考察しています。

 

あとはカテゴリーから見てみてください。

【しゃあっコヒーレンス・スペース!】整合空間(coherence space)をじっくりとその2 安定関数(stable function)

 ↓これの続きです。

cut-elimination.hatenablog.com

今回は安定関数が出てくるはずです。

用語の整理

 いろいろ用語、記法が出てきている。

用語・記法:整合空間 {\mathcal A} の要素を {\mathcal A}点(point)という。|{\mathcal A}| のクリークを整合部分集合(coherence subset)とも言う。点とは即ち整合部分集合である。また、{\mathcal A} の点のうち有限集合であるものの集合を {\mathcal A}_{fin} と書く。

 もうちょっと定義っぽい定義も出てくる。

定義:a \in {\mathcal A}近似(approximant)とは、任意の a の部分集合 a' である。有限近似とは近似のうち有限集合であるもの。

整合空間の定義1)より、近似も {\mathcal A} の要素である。

有限近似の性質

 近似は有限のものさえあれば良さそうだということが徐々に示されていく。まずは以下の命題。

命題1:任意の a \in {\mathcal A} はその有限近似の集合の和である。即ち

 a = \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}

証明:\alpha \in a とすると、\alpha \in \{\alpha\} \subset a となり、勿論 \{\alpha\} は有限集合なので \alpha \in \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}。よって a \subset \bigcup \{a_\circ \mid a_\circ \subset a & a_\circ \; {\rm finite} \}。また \alpha \in \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \} とすると、ある a の有限部分集合 a' が存在して \alpha \in a'。よって \alpha \in a なので \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \} \subset a。以上より a = \bigcup \{a_\circ \mid a_\circ \subset a, \; a_\circ \; {\rm finite} \}

また、以下も成立つ。

命題2:a \in {\mathcal A} の有限近似の集合 I は有向である。即ち、I は空でなく、任意の二つの要素 a_1, a_2 \in I に対して a_1, a_2 \subset a' となる a' \in I が存在する。

証明:どんな集合でも空集合を部分集合として持つため、常に \emptyset \in I。よって I は空でない。また、a_1, a_2 \in I の時、a' = a_1 \cup a_2 とすればこれも a の有限部分集合なので  a_1, a_2 \subset a' かつ a' \in I。以上から I は有向集合である。

 近似の導入は、再帰理論において全関数ではない部分関数を考えるように、様々なデータに全的な(真な)ものと部分的なものとの区別を与えることになる。これが近似の発想だとジラール先生は述べている。ただし {\mathcal Bool}{\mathcal Int} は、全的なものはブール値や自然数のシングルトンで部分的なものは空集合という単純な分れ方をする。

 その後いろいろ書いてあるのは難しげなので割愛。安定関数に移る。

安定関数の定義と性質

定義:二つの整合空間 {\mathcal A}, {\mathcal B} が与えられた時、{\mathcal A} から {\mathcal B} への関数 F が安定であるのは、以下の条件を満す時である。

1) a' \subset a \Rightarrow F(a') \subset F(a) 単調性

2) F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i))\{a_i\}_{i \in I} は有向集合族)連続性

3) a_1 \cup a_2 \in {\mathcal A} \Rightarrow F(a_1 \cap a_2) = F(a_1) \cap F(a_2) 安定性

実は連続性は単調性を含意している

命題3:F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i)) \Rightarrow [a' \subset a \Rightarrow F(a') \subset F(a)]

証明:F\bigl(\bigcup^\uparrow_{i \in I}a_i\bigr) = \bigcup_{i \in I}(F(a_i)) を仮定する。a' \subset a とすると \{a', a\} は有向集合になる。よって仮定より F\bigl(\bigcup \{a', a\}\bigr) = F(a) = \bigcup \{F(a'), F(a)\}F(a') \subset \bigcup \{F(a'), F(a)\} なので F(a') \subset F(a)

 連続性について重要な性質がある。

命題4:F は連続 \Leftrightarrow F(a) = \bigcup \{F(a_\circ) \mid a_\circ \subset a, \; a_\circ \; {\rm finite}\} & F は単調

証明:(\Rightarrow) F が連続と仮定する。命題1より、a = \bigcup \{a_\circ \subset a, \; a_\circ \; {\rm finite}\}。これと命題3より。

(\Leftarrow) F(a) = \bigcup \{F(a_\circ) \mid a_\circ \subset a, \; a_\circ \; {\rm finite}\} & F は単調を仮定する。単調性より、任意の有向集合族 \{a_i\}_{i \in I} について F(a_i) \subset F(\bigcup^\uparrow_{i \in I} a_i) なので、\bigcup F(a_i) \subset F(\bigcup^\uparrow_{i \in I} a_i)。また、\beta \in \bigcup^\uparrow_{i \in I} a_i とする。仮定より F(\bigcup^\uparrow_{i \in I} a_i) = \bigcup \{F(a_\circ) \mid a_\circ \subset \bigcup^\uparrow_{i \in I} a_i, \; a_\circ \; {\rm finite}\} なので、ある \bigcup^\uparrow_{i \in I} a_i の 有限部分集合 a'_\circ が存在して \beta \in F(a'_\circ)a'_\circ\bigcup^\uparrow_{i \in I} a_i の有限部分集合なので、ある有限個の a_1, a_2, ..., a_k の和の部分集合となる。これらは有向なので、和集合 a_l(l \in I) は存在する。a'_\circ \subset a_l なので単調性より F(a'_\circ) \subset F(a_l)F(a_l) \subset \bigcup^\uparrow_{i \in I} F(a_i) なので F(a'_\circ) \subset \bigcup^\uparrow_{i \in I} F(a_i)。よって F(\bigcup^\uparrow_{i \in I} a_i) \subset \bigcup^\uparrow_{i \in I} F(a_i)。以上より F(\bigcup^\uparrow_{i \in I} a_i) = \bigcup^\uparrow_{i \in I} F(a_i)

"Proof and Types"ではあまり詳しく書いていなくて、単調性なしで連続性と同値になるように読み取れるようなことが書いてあるのだが、単調性なしで良いのかどうかは分らなかった。まあまあまあ。「線形論理の誕生」では「有限呼び出し性」という同じような性質+単調性と連続性との同値性を証明していたので、それに倣った。とにかく、定義域のデータの有限近似さえ得られていれば安定関数は復元できるということが分る。

 続いて安定性について。これは圏論的に解釈すると自然だと書いてある。整合空間を \subset を射とする圏と見ると、単調性は関手であることを表し、連続性はフィルター付き余極限というやつを表す。そして安定性は a \subset a \cup b \supset bプルバックの保存と同じことになる。まあ証明せずとも図を書いてみれば明らかでしょう。

 ドメインが整合空間であるという条件の有効性を表す例が挙げられている。我々は {\mathcal Int} から {\mathcal Int} へのどんな関数も安定関数で表現できるのであって欲しい。{\mathbb N} から {\mathbb N} への関数 ff(0) = f(1) = 0, \; f(n+2) = 1 と定義する。これに対応する安定関数 FF(\{0\}) = F(\{1\}) = \{0\}, \; F(\{n + 2\}) = \{1\} となる筈である。また、単調性より F(\emptyset) = \emptyset とならなければならない。この時、F(\{0\} \cap \{1\}) = F(\emptyset) = \emptyset \neq F(\{0\}) \cap F(\{1\}) = \{0\} であるが、01 が整合でないこと、つまり \{0\} \cup \{1\} = \{0, 1\} \in {\mathcal Int} から、安定性は侵されていないことになる。

 どんな関数も安定関数で表現できることは証明できるっぽい。

命題5:任意の {\mathbb N} から {\mathbb N} への関数  f に対して、\{n\} \mapsto \{f(n)\} であるような安定関数 F : {\mathcal Int} \to {\mathcal Int} が存在する。

証明:F(\emptyset) = \emptyset, F(\{n\}) = \{f(n)\} としてこれが安定関数であることを確認すれば良い。

単調性:{\mathcal Int} の要素 a, a'a \subset a' となるのは a = \emptyset の時だけだが、F(\emptyset) = \emptyset なので F が単調性を満たすことは明らか。

連続性:{\mathcal Int} の部分集合で有向集合となるのは \{\emptyset, \{m\}\} という形のものだけであるが、この時 \bigcup \{\emptyset, \{m\}\} = \{m\}F(\emptyset) = \emptyset なので、F(\bigcup \{\emptyset, \{m\}\}) = F(\{m\}) = \{f(m)\} = \bigcup \{\emptyset, \{f(m)\}\} = \bigcup \{F(\emptyset), F(\{m\}) となり、連続性も満す。

安定性:a \cup a' となるのは a = \emptyset または a' = \emptyset の時のみである。このとき a \cap a' = \emptyset なので、F(a \cap a') = F(\emptyset) = \emptyset となる。F(a)F(a') もどちらかが \emptyset になるので、F(a) \cap F(a') = \emptyset でもある。よって F(a \cap a') = F(a) \cap F(a') で安定性も満す。

 また、安定性の条件は最小近似の存在を保証するということが匂わされているが、これはまたそのうち。

 また次回。

安倍晋三銃撃事件から見る日本のマンガやアニメ、そして北野映画(あまり真面目な記事ではないです)

 安倍晋三が銃撃された際の映像を見ると、明らかに警備がミスっている。その原因は色々考えられるだろうが、まあ日本では銃を使った襲撃は珍しいのできちんと想定されていなかったのだろう。そんな中、5ちゃんねるで以下のような証言がよく拡散されていた。

要人警護に詳しい警察関係者 
「あそこまで接近されているのは一つ厳しいところ、止められなくても誰かがとめにいっていてもよかった。銃で撃たれる想定の訓練はもちろんしている。 
ただ、今回のようにいきなり銃を取り出して撃つのは今までない。多くの訓練は思想をもった人間などが『安倍!』などと叫んで撃つといった想定が多い。 
今まで日本にいなかったタイプの襲い方だろうし、やはり、いきなりこういう形は厳しい」 

ソースはテレビ朝日のニュース記事のようだが、リンクが消えていた。しかしその後の訓練映像なんかを見ていても、どうも武器を持っているのに声で威嚇してくる犯人を想定しているケースが多いようだ。

 さて、日本のバトル・マンガなんかでは、叫びながら技を繰り出すシーンが多い。「うおおおおおお!」と言いながら剣を振りまくったり、技の名前を叫んだり。私はそういうのは緊張感やリアリティがないので良くないと思っている。マンガならばまだ文字なのでまあまだ良いが、映像化すると変に悠長になる。日本のテロ対策もこういう類の緊張感の無さがあったのではないかと思う。

 で、この種のことをブログで書くとついでに述べるのが中国アニメ「羅小黒戦記」の素晴しさである*1。このアニメでは「うおおおおおお!」や技名叫びがない。バトル・シーンは緻密に演出・作画され緊張感がある。

 押井守監督が『押井守の映画50年50本』という本で北野武監督の「その男、凶暴につき」について語っていたのだが、押井氏曰くたけしは既存の映画に対する疑問をそのまま映画にしているという。普段映画を観ていて「あそこはなんでこうしないんだ」と思うようなことを積み重ねた作品だというのだ。北野映画は銃撃する前に大袈裟な威嚇などしない。そんな事をする暇があったらもう撃っている。北野映画の独特の緊張感の源泉の一つはこれであろう。そして羅小黒戦記のMTJJ監督も、たけしと似たような疑問を日本のマンガやアニメに対して持っていたのではないか。

 今度『チェンソーマン』のアニメをやるが、同作は技の名前がほぼない。大袈裟なバトル演出もあまりないように思う。作者の藤本タツキ先生は北野映画のファンらしいから影響があるのかもしれない*2。リアリティのある映像化ができそうで期待してるます。

*1:今度テレビでやるよ!

*2:チェンソーマン』でただの民間人がヒットマンだったりする展開があってあれは「ソナチネ」っぽさを感じた。

【しゃあっコヒーレンス・スペース!】整合空間(coherence space)をじっくりとその1

 ↓これの続きっちゃあ続きである。

cut-elimination.hatenablog.com

"Proofs and Types"を読んでいくシリーズだったが、第7章のSystem Tの導入をちょっと飛ばして第8章の整合空間(coherence space)を詳細に読みたいのよ。

 整合空間から線形論理を解説している照井先生の「線形論理の誕生」という論文も勉強になるので適宜参照する。

https://www.kurims.kyoto-u.ac.jp/~terui/birth.pdf

動機

 整合空間はプログラムの表示的意味論を構築するための数学的道具である。まず表示的意味論の発想というものがちゃんと解説されている。「誕生」でも似たような議論がある。表示的意味論では、型を集合、関数としてのプログラムを数学的な関数と対応させる。しかしこの時、どのような数学的関数を取ってこれば良いかが問題となる。「あらゆる関数」としてしまうと意味がない*1。スコット流の表示的意味論(領域理論)では、型を位相空間(領域、ドメイン)と対応させ、関数をそれらの間の連続写像に限定する。こうすることでデータやプログラムに近似を導入し、逆に言うと近似が可能な集合や関数に表示的意味論を限定できたのである。ちょっと先走ると、整合空間による意味論は、型を整合空間とし、連続写像に更なる性質を加えた安定写像というものに関数を限定する訳だ*2

 ジラール先生はスコット流の表示的意味論にいくつか不満を述べている。一つは関数空間の収束を上手く扱えないとか書いてあるのだが私にはよく分らなかった。もう一つは、トポロジーという幾何学的な道具立てがあまり意味を成していないという点である。スコット意味論が位相空間になったのは単なる偶然ではないかと指摘している。「よってトポロジー的直観自体が誤りではないかと考え、もっと別なのを探そうとするのは自然なことである」(54ページ)。

 この批判がどれくらい刺さっているのかは分らないが、そういうわけなので整合空間理論はトポロジーに拘らない。スコット意味論を更に単純化して再構成する。

定義、例

 整合空間の定義は以下の通り。

定義:整合空間とは、以下の条件を満す(集合の)集合 {\mathcal A} である。

1) a \in {\mathcal A} かつ a' \subset a ならば a' \in {\mathcal A}

2) M \subset {\mathcal A} として (\forall a_1, a_2 \in M)[a_1 \cup a_2 \in {\mathcal A}] ならば \bigcup M \in {\mathcal A}

すぐに分るのは、\emptyset \in {\mathcal A} である。何故なら何かしらの a \in {\mathcal A} について \emptyset \subset a なので条件1)より。個々の整合空間はデータの領域を表す。※整合空間全体の集合というのが存在するのかどうか分らないので、以下ちょっとボカします。

 例が挙げられている。まず {\mathcal Bool}\{\emptyset, \{{\bf t}\}, \{{\bf f}\}\} というもの。そして {\mathcal Int}\{\emptyset, \{0\}, \{1\}, \{2\}, ...\} という感じ。どちらも定義を満たしている。部分集合や和集合が簡単なものしかないので確かめるのは容易である。整合空間ではないものの例としては \{\emptyset, \{0\}, \{1\}, \{2\}, \{1, 2\}, \{0, 2\}, \{0, 1\}\} というのが挙げられている。部分集合 \{\{0\}, \{1\}, \{2\}\} はどの二つの要素の和集合ももとの集合に属すが、\bigcup \{\{0\}, \{1\}, \{2\}\} = \{0, 1, 2\} はそうではない(\{0, 1, 2\} を要素として付け加えれば整合空間になる)。

 続いて網の定義

|{\mathcal A}| := \bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}

とする。|{\mathcal A}| の要素をトークと呼ぶ。トークン間の {\mathcal A} を法とした整合関係を以下のように定義する。

 \alpha \ddagger \alpha' \; ({\rm mod} \; {\mathcal A})*3 iff \{\alpha, \alpha'\} \in {\mathcal A}

これは反射的で対称的な関係である。よって |{\mathcal A}|\ddagger を付与したものは(反射的な)無向グラフとなり、これを {\mathcal A}網(web)と呼ぶ。

整合空間の性質と諸々の証明、そして考察

 整合空間 {\mathcal A} について \bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\} となることを証明しておく。

命題1:整合空間 {\mathcal A} について \bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}

証明:\alpha' \in \bigcup {\mathcal A} とすると、ある a \in {\mathcal A} が存在して \alpha' \in a。この a について \{\alpha'\} \subset a が言える。整合空間の定義1)より \{\alpha'\} \in {\mathcal A}。よって \alpha' \in \{\alpha \mid \{\alpha\} \in {\mathcal A}\}。故に \bigcup {\mathcal A} \subset \{\alpha \mid \{\alpha\} \in {\mathcal A}\}

 また、\alpha' \in \{\alpha \mid \{\alpha\} \in {\mathcal A}\} ならば \{\alpha'\} \in {\mathcal A} であるが、\alpha' \in \{\alpha'\} なので \alpha' \in \bigcup {\mathcal A}。よって \{\alpha \mid \{\alpha\} \in {\mathcal A}\} \subset \bigcup {\mathcal A}

 以上より  \bigcup {\mathcal A} = \{\alpha \mid \{\alpha\} \in {\mathcal A}\}

この命題から、整合空間からその網への対応付け |\cdot|単射だということも見て取れる。全ての網には当然対応する整合空間が存在するので、整合空間(たち)と網(たち)の間には全単射が存在する。しかしこれだけにとどまらない。

 網からもとの整合空間を得る具体的な操作がある。まずは以下の命題を示す。

命題2:整合空間 {\mathcal A} について以下が成立つ。

 a \in {\mathcal A} \Leftrightarrow a \subset |{\mathcal A}| & (\forall \alpha_1, \alpha_2 \in a)[\alpha_1 \ddagger \alpha_2\; ({\rm mod} \; {\mathcal A})]

証明:(\Rightarrow) a \in {\mathcal A} と仮定する。\alpha \in a ならば \{\alpha\} \subset a が言えるので、整合空間の定義1)より \{\alpha\} \in {\mathcal A}。よって網の定義より \alpha \in |{\mathcal A}| なので a \subset |{\mathcal A}|。また、任意の \alpha_1, \alpha_2 \in a について \{\alpha_1, \alpha_2\} \subset a が言えるが、これも同様に \{\alpha_1, \alpha_2\} \in {\mathcal A}。よって \alpha_1 \ddagger \alpha_2\; ({\rm mod} \; {\mathcal A})

(\Leftarrow) a \subset |{\mathcal A}|(\forall \alpha_1, \alpha_2 \in a)[\alpha_1 \ddagger \alpha_2 \; ({\rm mod} \; {\mathcal A})] すなわち (\forall \alpha_1, \alpha_2 \in a)[\{\alpha_1, \alpha_2\} \in {\mathcal A}] を仮定する。 \{\{\alpha\} \mid \alpha \in a\} という集合を考える。\{\alpha'\} \in \{\{\alpha\} \mid \alpha \in a\} ならば \alpha' \in a であり、仮定より \alpha' \in |{\mathcal A}|。よって網の定義より \{\alpha'\} \in {\mathcal A} となるから、\{\{\alpha\} \mid \alpha \in a\} \subset {\mathcal A} である。また任意の \{\alpha_1\}, \{\alpha_2\} \in \{\{\alpha\} \mid \alpha \in a\} について \alpha_1, \alpha_2 \in a なので、仮定より \{\alpha_1, \alpha_2\} = \{\alpha_1\} \cup \{\alpha_2\} \in {\mathcal A}。以上と整合空間の定義2)から \bigcup \{\{\alpha\} \mid \alpha \in a\} \in {\mathcal A}。しかし \bigcup \{\{\alpha\} \mid \alpha \in a\} = a であるので a \in {\mathcal A}

全てのノード間に辺があるグラフを完全グラフという。あるグラフの完全グラフであるような部分グラフをグラフ理論ではクリークという。この命題が主張するのは、整合空間から網を作った時、網のクリークの集合がもとの整合空間になっているという事である。

 もっと言うと実は整合空間はグラフとクリークから定義できる。まず、任意の反射的無向グラフのクリークの集合は整合空間になる。

命題3:反射的無向グラフのクリークの集合は整合空間である。

証明:反射的無向グラフ {\mathcal G} = (G, \ddagger) のクリークの集合 C({\mathcal G})(より厳密にはクリークのノードの集合の集合)が整合空間の定義の二つの条件を満している事を示す。

1) g \in C({\mathcal G}) かつ g' \subset g と仮定する。任意の \gamma_1, \gamma_2 \in g' について \gamma_1, \gamma_2 \in g \in C({\mathcal G}) なので、\gamma_1 \ddagger \gamma_2。よって g' もクリークなので g' \in C({\mathcal G})

2) M \subset C({\mathcal G}) とし、(\forall g_1, g_2 \in M)[g_1 \cup g_2 \in C({\mathcal G})] とする。任意の \gamma_1, \gamma_2 \in \bigcup M についてある g'_1, g'_2 \in M が存在し \gamma_1 \in g'_1 かつ \gamma_2 \in g'_2、よって \gamma_1, \gamma_2 \in g'_1 \cup g'_2。仮定より、g'_1 \cup g'_2 \in C({\mathcal G}) なので \gamma_1 \ddagger \gamma_2。したがって \bigcup M もクリークなので \bigcup M \in C({\mathcal G})

命題2より、任意の整合空間は整合関係で作った反射的無向グラフのクリークの集合だった。そして命題3より、任意の反射的無向グラフのクリークの集合は整合空間である。よって以下が言える。

定理:整合関係と反射的無向グラフのクリークの集合は同じである(クラスとして一致する)。

 反射的無向グラフからクリークの集合を得る操作は、反射的無向グラフたちから整合空間たちへの写像となる。しかも命題2を見れば分る通り、この操作は整合空間から網を得る操作(これは命題1より単射だった)の逆写像になっている(よって整合空間(反射的無向グラフのクリークの集合)と網との間には全単射がある)。反射的無向グラフから整合空間を作り、その網を定義するともとの反射的無向グラフに戻るのである。よって反射的無向グラフは常に何らかの整合空間の網となる。なので整合空間を定義する際は、反射的無向グラフを網と呼んでそのクリークの集合を整合空間としても良い。「線形論理の誕生」ではこの方法で定義しているのだが、反射的無向グラフ(網)の方を整合空間と呼んでる。この定義でも良い訳だが、適宜読み替える必要がある。

 反射的無向グラフから整合空間を作った時、その網を定義通りに作ったらそれがちゃんともとのグラフになっているかどうかは気になる所である。反射的無向グラフから網を作る操作が全単射であるということがもう分っているからこれは既に示されている筈だが、もうちょい考えてみる。命題3の証明中の定義を再利用する。\gamma_1, \gamma_2 \in |C({\mathcal G})|\gamma_1 \ddagger \gamma_2 \; ({\rm mod} \; C({\mathcal G})) とは、\{\gamma_1, \gamma_2\} \in C({\mathcal G}) ということ、すなわち \{\gamma_1, \gamma_2\}{\mathcal G} のクリークという事である。これは \gamma_1 \ddagger \gamma_2 と同値である。つまり \gamma_1 \ddagger \gamma_2 \; ({\rm mod} \; C({\mathcal G}))\gamma_1 \ddagger \gamma_2 は同値な訳で、万事オッケーである。

まとめ

 なんだか初等的集合論の練習問題みたいなことを延々とやってきたが、何故かと言うとジラール先生と照井先生で整合空間の定義が違ったのがずっと気になっていたからである。細かい計算を色々やってようやく御二方の定義が大体同じものであることが示せたっぽい。でめたしでめたし。

 整合空間で終って安定写像に行けなかったけれどもまあそのうち続きを書きます。

*1:非可算無限になってしまって非効率である(照井)し、「計算論的に興味深いオブジェクトが集合論的関数の海に溺れてしまう」(ジラール)。

*2:安定写像とは何で何が凄いのかとかまでは本記事では扱えず。

*3:記号がもとのやつと違うけど許してちょんまげ。

【お気持ち表明】反出生主義の押し付けは良くない

 密かにトゥイッターで「反出生」と検索して世の反出生主義の受容を調べている。するとよく目にするのが「押し付けは良くない」論である。ヴィーガンに対してもよく言われるが、子供を産まないとか肉を食べないとか勝手にやってくれ、他人に価値観を押し付けるな、という訳である。まあ確かに押し付けがましい人もいる。

 こういうことを言い出すと倫理を考えるということが無意味になってしまう恐れがある。例えば「人を殺してはいけないという考えを押し付けるな、お前は勝手に殺さないようにしておけ、私は殺す」というような主張は普通はおかしい。道徳的な主張というのは自分で勝手に実践するためにあるだけのものでなく、一般性を持っている。他人にまで効果の対象を拡げなければ意味がない。

 ただし、人を殺してはいけないという道徳は、それを開発した人が周りに押し付けた訳ではあるまい。奴隷は良くないとかなんでもそうだが、徐々にそういう倫理観が広まっていって法律が作られるに至ったのだろう*1。そうでないと全体主義国家みたいに無理が生ずるのではなかろうか。反出生主義にしても、それが正しいと思う人が粘り強く主張し続けて常識になるまでしなければなるまい。とすると押し付けは逆効果になるのではないか。

 私は反出生主義は「今のところ」「けっこう」正しいと思っているのだが、それほど他人に熱弁したい気持ちはない。ただ、産んでしまったがためにいろいろ苦悩を背負っている感じの人を見ると、もうちょっと考えたら良かったのにな〜とかは思う。あと自分の産みたい気持ちだけでなく生れてくる子供が将来「生れてこない方が良かった」と思わないかどうかを考えることは是非やっていただきたい。こういう人生の決断の際の指針として反出生主義は広まるべきと思う。しかしこういうことをちゃんと考えられる理性があるような人に対しては、反出生主義の押し付けはやはり逆効果だろう。

 反出生主義を正しいと思っている人からすると大した考えもなく子を作っている人がイラつくのも分るが、しかし人類の滅亡など一朝一夕で達成されるものでもなし。まあ私にできることはブログでお気持ちを表明することくらいである。

*1:とか思うのは私が自然主義者だからでしょうか…

札幌の味噌ラーメンについて

 マンガワンで『ラーメン発見伝』を読んでいる。札幌の味噌ラーメンをディスる回は結構有名らしい。第3巻に載っているっぽい。

 藤本曰く「味噌という調味料はうますぎる」。よってスープが味噌の味に塗り固められてしまう。というわけなのでそこそこちゃんとした札幌ラーメン屋は味噌に負けないような濃いスープを開発するらしい。しかしそうするとマニア向けになってしまう。漫画では特殊な味噌を使うことで濃すぎず味噌の味を活かしたラーメンを作って解決している。

 この回が描かれたのは20年以上前だけど現在はどうなのだろう。私は先日「すみれ」という有名な札幌ラーメン屋に行ってきた。味噌に負けない濃い味系だと思う。「すみれの歴史」というページを見てみると、『ラーメン発見伝』のこの回の当時には既に有名だったっぽい。

www.sumireya.com

ということは藤本のディスの範疇に入っているだろう。美味しかったけどね。とか言ってる私は「情報を食べている」だけなのかも。

ジラール先生の"Proofs and Types"の5,6章を(ちょっと真剣に)読む(シーケント計算、強正規化定理)

 ↓これの続きでこざる。
cut-elimination.hatenablog.com

シーケント計算

 シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなんだ。私はPROLOGの仕組みを知らないので調べねばね。タブローがシーケント計算の一部だというのは分りそうで分らない。。。
 続いてシーケント計算が定義される。構造規則が思いの外重要であるとある。確かに構造規則が重要だからこそ構造規則を制限した線形論理が生れた訳だ。
 前回までであまりピンときていなかった対称性が分ってきた。シーケント計算は左と右で対称性がある。ここでいう対称性とはカットが除去できるということで、論理が満すべき条件である。
 今回はちゃんと図を描いたぞ!

 Γ,A|-Δ     Γ,B|-Δ
--------(∧左1) --------(∧左2)---(1)
Γ,A∧B|-Δ    Γ,A∧B|-Δ

Γ|-A,Δ Γ'|-B,Δ'
---------------(∧右)---(2)
 Γ,Γ'|-A∧B,Δ,Δ'

 Γ|-A,Δ
--------(∧右1?)---(3)
Γ|-A∧B,Δ

 A|-A      B|-B
------(∧右1?) ------(∧左2)
A|-A∧B     A∧B|-B    ---(4)
---------------------Cut
     A|-B

 ∧の規則は(1)と(2)のように定義される。線形論理の知識を先取りすると、左規則は加法的連言の規則で右規則は乗法的連言の規則になっている。これはありなのかなと思ったが、弱化を使えばカットが除去できるので別に良いのだろう。
 対称性について自分なりに考えてみた。∧右規則が(3)のようだったら、場合によってはカットが除去できない。これは(4)を見ればわかる。よって(1)と(3)で定義される結合子は対称性を持たない。証明論的意味論ではトンクというダメな結合子の例がよく出てくる。これはそこから着想を得た。トンクは正規化定理を満さない。後で述べられている通り、正規な証明はカットの無い証明と対応する。ジラール先生が言っている対称性は証明論的意味論の結合子の正当化と近いんじゃないかと思う。しかしジラール先生は証明論的意味論に言及しているイメージがないのであまり評価していなさそう。
 しかしこの後で非対称な解釈というのが出てきていて、これはよく分らなかった。"Basic Proof Theory"にこんな話が出てきた気がするがサボっているので分らない。
 自然演繹との対応も述べられているのだが、ちょっと抽象的で分りにくかったなあ。もうちょっと考えてみたい。シーケント計算から自然演繹への翻訳は一意だが逆はそうではないとのこと。

強正規化定理

 強正規化定理の詳しい証明。帰着可能性の概念を用いて証明しており、それを詳細に解説してあるのがありがたい。全ての項は帰着可能であり、帰着可能性は強正規化可能性を含意している、という証明である。これは後で述べるシステムFの強正規化定理の証明にも応用できるので詳しく述べているらしい。
 型無ラムダ計算と違って型の構造帰納法が使えるから型付ラムダ計算は強正規化可能なのだということがよく分った気がする。
 CR1〜4の条件と6.3.1と6.3.2からどのように帰着可能性定理が導かれているのかちゃんと説明されていない気がしてならない。私の考えでは項の複雑さとnステップの変換で帰着可能というnとの二重帰納法が使われているのではないかと思う。どうでしょう。

まとめ

けっこう難しくて先行き不安である。

ジラール先生の"Proofs and Types"の3,4章を(ちょっと真剣に)読む(カリー=ハワード同型、正規化定理)

 ↓これの続きでっせ。

cut-elimination.hatenablog.com

3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。

Chapter 3 カリー=ハワード同型

 命題を型と対応させる。型付項のシステムにおいても sense と denotation の二項対立が現れる。denotation はプログラムの denotational semantics(表示的意味論)の背景にある。もちろん。それは denotation の等式を与える静的なものである。対して sense の方は操作的意味論をもたらす。こちらは書換えを与える動的なものである。

 スコット意味論など表示的意味論は栄えているが、操作的意味論はまだ十分ではないとジラール先生は考えている。「アルゴリズムの真に操作的な意味論を確立することがコンピュータ科学における最も重要な問題かもしれない」とすら述べている(14ページ)。

 続いて型付ラムダ計算が定義される *1。複合型は U \times VU \to V の二つなので、命題論理の (\land, \Rightarrow) 断片と対応する。

 3.3の "Operational significance" という節で型についての哲学的考察が展開されている。項はプログラムを表し、プログラムは denotation を計算する。そしてプログラムの型はプログラムの仕様だという。とすると型はプログラムの情報をどれくらい詳細に含むべきかということになる。本書ではかなり原始的なものでしかないが、もっと情報量豊富な型のシステムを作ることもできるらしい。

 更に、型はプログラムのモジュールをプラグする(plugging)ための取り決めであると考えることができる。これはナルホドである。型のマッチはモジュールの挿入が失敗しないためのものと考えると分りやすい。またこう考えるとインプットとアウトプットも対称的なものと見做せるという。この考え方は萌芽的だというが、(see appendix B)とあり、このappendix B は線形論理の解説である。線形論理は相互作用的な計算を表現するといわれる(照井一成先生)が、それがここに現れているようだ。

 変換の定義をした後、自然変換との同型が示される。これが単なる全単射でなく同型であるというのは、構造まで同じということだ。Chapter 2 で証明間の"equal"とされていたものがここでは"rewriting"と言い直される。これは変換に対応するからである。

 関数と証明はそれぞれ別に生れたものであるから異なる点があるはずだが、同型性によって相手側にその対応物を考えられるということが重要であるという。関数は操作的なものである。ということは良い (構成的)論理は操作的であるべきだ。逆に論理は暗に対称性を持つのであるから、型付計算体系もそれを意識すべきだ、とのこと。関数→論理の方向は私もよく考えるが、論理→関数はあんまり考えたことがなかったなあ。

 この同型性は、論理と計算が同じ物を別の仕方で表現したものであることを示している!

Chapter 4 正規化定理

 チャーチ=ロッサー定理の簡単な解説と正規化定理のやや詳しい証明が書かれている。

 私は型無ラムダ計算の正規化定理と型付ラムダ計算の強正規化定理の証明は見たことがあるが、本章のような型付ラムダ計算の(弱)正規化定理の証明は初めて見たかもしれない。

 正規化定理の証明では degree というのを定義している。正規化定理を証明するには、必ず正規形を導ける変換戦略を発見すれば十分である。ここの証明では「最も degree が大きくしかもそこに含まれているリデックスはどれも degree がより小さい」ようなリデックスから変換していくとしている。しかしこのようなリデックスが存在することもちゃんと証明しなければならないような気がしてならない! だがそれが存在しない項が存在すると仮定するとそれは長さが無限になってしまうからいいのか(背理法)。ちょっと自信無し。そしてこの変換をすると最大の degree を持つリデックスが減ることがレンマで示されたので最大の degree とその数で二重帰納法にすれば正規化定理が証明できる。

 という感じ。

 ジラール先生はこれが「弱」正規化定理であることをやや強調気味な感じがする。

感想

 ジラール先生はカット除去を論理の「対称性」と表現しているが、それがまだあまりピンときていない。

*1:カリー流とチャーチ流とあるがジラール先生のはどっちだっけ。