■

[HoTT]HoTTをこっそり学ぶ　その2

　さて、まずはMartin-L\scriptsize{\ddot{o}}f依存型理論というのを勉強せんといかんわけだが、調べれば調べるほどなんだかとっ散らかっている感がある。標準的な定式化というのがあるようなないような、バリエーションも多く、表記の違いなのか何か本質的な違いがあるのかさえよくわからない。Martin-L\scriptsize{\ddot{o}}fその人でさえ、いくつかバリエーションを発表している。まー、いろいろ調べている内に分かったことがいくつか。

　Martin-L\scriptsize{\ddot{o}}f依存型理論は大別して２つある。extensionalなものとintensionalなものである。この２つの違いは、後述するように、＝（等号）の構造の違いである。その違いの結果として、extensionalなMartin-L\scriptsize{\ddot{o}}f依存型理論のモデルは、局所デカルト閉圏（locally cartesian closed category）になる一方で、intensionalなもののモデルとして(∞,1)-category(こっちでもlocally cartesian closedらしい)が必要になるという。HoTTと関連しているのは、当然後者である。前者については高階論理とトポスに関連する成書がすでにあり、それは Lambek & Scottである。（有名な本らしく、なぜかすでに持っていたが、もちろん本棚の肥やし）

Introduction to Higher-Order Categorical Logic (Cambridge Studies in Advanced Mathematics) by J. Lambek P. J. Scott(1988-03-25)

Introduction to Higher-Order Categorical Logic (Cambridge Studies in Advanced Mathematics) by J. Lambek P. J. Scott(1988-03-25)

　もう一つ、歴史的な変遷があるのは型理論の基礎付けに使うuniverse \mathcal{U}の構造の違いである。最初にMartin-L\scriptsize{\ddot{o}}fが1971年に発表したバージョンでは、\mathcal{U}:\mathcal{U}（型全体の集まりは型になる）という公理があり、直ちにGirardがそこから矛盾を導いたために破棄され、最終的には階層状の構造を持ったuniverseに落ち着いている。Girardの論文は学位論文らしく、さすがにネットに落ちていなかったが、個人的にも興味があるところなので引き続き追及しているところである。ただ、どう細工するのかは不明だが、計算機に応用した際には\mathcal{U}:\mathcal{U}でも大丈夫という文献もあり、混迷を深めている気がする。


　さて、intensionalとextensionalの違いについて。
これは2つのobjectがどういう条件を満たしていると等しいと定義されているかに関連している。例えば集合A,Bが等しいのはその要素が等しいとき（そしてその時に限る）である。

A=B \stackrel{\mathrm{def}}{\equiv} \forall x (x \in A \Leftrightarrow x \in B)

これは代表的なextensionalな定義である。集合A,Bがどのように構成されたかはまったく問わず、その結果のみが比較される。もう一つ例をあげてみよう。関数f,gが等しいのはその定義域が等しくかつその値が等しい時である。

f=g \stackrel{\mathrm{def}}{\equiv} (dom(f)=dom(g)) \land \forall x \in dom(f)( f(x) = g(x) )

これもf,gがもともとどのように定義されたのかは問われていない。

　一方、intensionalな等しさの一例をあげよう。整数を与えると何らかの計算を行って整数を返すような２つの計算機プログラムP(n),Q(n)を考えてみる。一つの等しさの定義は関数として等しい結果を与えるプログラムは等しいとするextensionalな定義である。別の定義としてプログラムコードが完全に等しい時のみ等しいとする定義で、これがintensionalな定義の一例である。objectがどのように構成されたかに立ち入って等しいの条件を定めたとき intensionalと呼ばれると言ってよい（と思う）。ただし、プログラムの例でもコードそのものでなく、使っている計算アルゴリズムが同じならば同じとするように様々な定義もありえるだろう（正確に定義するのは面倒だろうが）。

　ただ、思うにextensionalとintensionalの区別はさほど明確なものではない。私が悩ましいと思うのは次のような例である。自然数 \mathbb{N}から自然数 \mathbb{N}への関数を考える。一つは恒等写像 1_\mathbb{N} 、もう一つは f(n)\stackrel{\mathrm{def}}{\equiv} succ^{n}(0)である。ここにsuccは自然数論における後者オペレータである。無論 extensionalな定義では、 1_\mathbb{N}=fであるが、intensionalに等しいかどうか？　そもそも恒等写像がどうやって構成されたか？なんてどうやって考えればよいのだろうか。こうなると記号論理学的なベースからきっちりスタートしないとintensionalかどうかの定義ははっきりしないことがわかる。いずれにせよ、あるelementが等しいということの定義が問題となっている。具体的にMartin-L\scriptsize{\ddot{o}}f依存型理論でそこらあたりがどう表現されているかをみてみる（以下はHoTTのAppendixにある表記を採用する）。

　そこで問題になるのはあるtypeをもつelement間の等しさである。どうやらtypeどうしが等しいかどうかはあまり問題ではないようだ。Martin-L\scriptsize{\ddot{o}}f理論の思想では、あるtypeは証明されるべき命題（proposition)であり、そのtypeを持つelementはその証明(proof)と解釈されるので、

a:A, b:Aのとき a=_{A}b （type Aをもつaとbが等しいかどうかというpropositionに相当する）というtypeが定義される。表記がまぎらわしいので、文献によってはId_{A}(a,b)とかc_{=}(a,b)とか書かれたりもするようだ。さて、extensionalとintensionalの違いはこの a=_{A}bの構造をどう仮定するかの違いとなる。結論を述べると p,q \in a=_{A}bという2つのproof p,qがあったとき、必ず（何らかのelementが等しいという定義のもとに）p=qとなっているとき、extensionalと呼ばれ、そうでないとき、つまり a=_{A}bが何らかの意味で異なったproofを持つときintensionalと呼ばれる。 a=_{A}bの証明が本質的に一つしかないというextensionalな理論はかなり制限が強いと感じられるだろう。

特に a=_{A}aを考えてみよう。Martin-L\scriptsize{\ddot{o}}f依存型理論では、この時に refl_a \in a=_{A}aという公理があり、つまりrefl_aというproofにより、反射律a=aが証明されているという解釈となる。このときintensionalな理論ではrefl_a\neq pであるような反射律a=aの別のproof pが存在している可能性を認めるというのである。今度は逆にどういうこっちゃだが、もちろんMartin-L\scriptsize{\ddot{o}}f理論はある種のフレームワークなので、具体的にどうなっているのかはそのモデルの構造に拠っている。ここでホモトピー理論との関連がうっすらと見えてくる。非常に雑に言うと a=_{A}bを点 a,bを結ぶパスのホモトピー同値類と解釈するのである。 a=_{A}aとは、点aからでて点aに戻るパスのホモトピー同値類、つまり基本群に相当するようなものとなる。HoTTがintensionalな理論を要求するのはこういう事情である。