次の2つの記事の続きです。
Propositions-As-Typesというよく知られたキャッチフレーズを、グロタンディーク宇宙の観点からなるべく明確にします。$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\Imp}{\Rightarrow}
\newcommand{\hyp}{\text{-} }
%\newcommand{\dtimes}{\mathop{!\!{\times}} }
%\newcommand{\dto}{\mathrel{!\!{\to}} }
\newcommand{\code}[1]{ \ulcorner{#1}\urcorner}
\newcommand{\decode}[1]{ \urcorner{#1}\ulcorner}
`$
内容:
グロタンディーク宇宙と集合論・圏論・型理論
グロタンディーク宇宙 $`U`$ の条件〈公理〉として、節約主義〈ミニマリズム | 最小限主義〉でも贅沢主義でも、次の2つは共通です(「贅沢主義者のグロタンディーク宇宙」参照)。
- 所属関係に関して推移的: $`\forall x, y.\; x\in U \land y\in x \Imp y\in U`$
- 自然数全体の集合を要素として含む: $`\mbf{N}\in U`$
二番目は、「無限を扱いたい」という要求を満たすためです。有限だけで事が済むなら不要な公理です。
オリジナルの節約主義に基づくグロタンディーク宇宙が備えている集合論的操作は次の3つです。
- 順序なしペア〈unordered pair〉: $`x, y\mapsto \{x, y\}`$
- ベキ集合: $`x\mapsto \mrm{Pow}(x)`$
- ファミリーの合併: $`(f:x \to U)\mapsto \bigcup(x\mid f)`$
贅沢主義では、出来る操作はもっと増えます。贅沢主義の眼目は、道具・手段を自作する手間を省いて、最初から十分な道具・手段を揃えておこう、ということです。贅沢主義では、次の操作も“出来ること”に入れます。
- 順序ペア〈ordered pair〉: $`x, y\mapsto (x, y)`$
- 単元集合: $`x\mapsto \{x\}`$
- シグマ型: $`(f:x \to U)\mapsto \Sigma(x\mid f)`$
- パイ型: $`(f:x \to U)\mapsto \Pi(x\mid f)`$
- オメガ型: $`(f:x \to U)\mapsto \Omega(x\mid f)`$
直和集合、直積集合、関数集合も最初から入れてもいいですが、これらは極めて簡単に定義できます。
- 直和集合: $`x + y := \Sigma(\{1,2\} \mid \{ 1\mapsto x, 2\mapsto y\} )`$
- 直積集合: $`x\times y := \Pi(\{1,2\} \mid \{ 1\mapsto x, 2\mapsto y\} )`$
- 関数集合: $`\mrm{Map}(x, y) := \Pi(x \mid \lambda\, t\in x. y )`$
直和集合、直積集合、関数集合は、最初から入っている〈ビルトインな〉操作と思っても、上記のようにして後から作ったと思っても、どっちでもいいです。
贅沢主義の観点からのグロタンディーク宇宙は、必要があれば、“ZFC集合論から”も“圏論から”も“型理論から”も道具・手段を借用してよい対象物です。
- グロタンディーク宇宙 $`U`$ は、ZFC集合論内の集合である。したがって、ZFC集合論における集合として取り扱ってよい。
- グロタンディーク宇宙 $`U`$ は、$`U`$ 上の集合圏 $`\mbf{Set}_U`$ の対象達のクラス〈大きな集合〉である; $`U = |\mbf{Set}_U|`$ 。したがって、集合圏 $`\mbf{Set}_U`$ に関する概念・手法は自由に使ってよい。
- グロタンディーク宇宙 $`U`$ と集合圏 $`\mbf{Set}_U`$ は、単純型理論の意味論的モデルだとみなしてよい。「型は $`\mbf{Set}_U`$ の対象($`U`$ の要素)、インスタンスは $`\mbf{Set}_U`$ の射、型宇宙は $`|\mbf{Set}_U|`$」である。「型・インスタンス・宇宙とタルスキ宇宙系列」参照。
- グロタンディーク宇宙 $`U`$ と集合圏 $`\mbf{Set}_U`$ とバンドルの圏 $`\mbf{Bun}_U := \mrm{Bun}(\mbf{Set}_U)`$ は、依存型理論の意味論的モデルだとみなしてよい。「型は $`\mbf{Set}_U`$ のバンドル($`\mbf{Bun}_U`$ の対象)、インスタンスは $`\mbf{Set}_U`$ のバンドルのセクション、型宇宙は $`|\mbf{Bun}_U|`$」である。「型・インスタンス・宇宙とタルスキ宇宙系列」参照。
依存型理論の型はバンドルに対応しますが、バンドル-ファミリー対応により「型はファミリーである」ともみなせます。バンドル-ファミリー対応をシッカリ理解してないと混乱するところです。バンドル-ファミリー対応についいては:
半タルスキ方式の宇宙系列
単一のグロタンディーク宇宙 $`U`$ だけでなく、ひとつ上位の宇宙 $`U'`$ も考えましょう。「型・インスタンス・宇宙とタルスキ宇宙系列」で述べたように、タルスキ方式の宇宙系列では、$`U \in U'`$ とは考えません。宇宙 $`U`$ の“コード”が $`U'`$ の要素(上位の型)として存在します。
宇宙 $`U`$ のコードを、ゲーデルコードに倣って $`\code{U}`$ と書くことにします。次は成立します。
$`\quad \code{U} \in U'`$
タルスキ方式では、$`U`$ の要素を $`U'`$ の要素とみなすには、持ち上げ演算 $`t`$ を作用させる必要があります。これは煩雑です。ここでは、$`U\subset U'`$ であるかのようにみなします。言い方を変えると、$`t`$ による埋め込み $`t(a) \in U'`$ を $`a\in U`$ と同一視するってことです。
$`U`$ と $`U'`$ から作った集合圏をそれぞれ次のように書くことにします。
$`\quad \mbf{Set} := \mbf{Set}_{U}\\
\quad \mbf{SET} := \mbf{Set}_{U'}
`$
すると、宇宙 $`U`$ におけるファミリーは次のように書けます。
$`\quad f: x \to \code{U} \In \mbf{SET}`$
$`U`$ の要素は型(単純な型)とみなせますが、小さい型〈small type〉と呼ぶことにします。$`U'`$ の要素は大きい型〈large type〉です。
上に述べた方式は次のようにまとめられます。
- 小さい型は、小さい型達の宇宙 $`U`$ に居住している。
- 小さい型達の宇宙 $`U`$ を、そのまま大きい型とみなすことはできない。
- 小さい型達の宇宙 $`U`$ のコード $`\code{U}`$ は、大きい型である。
- 大きい型は、大きい型達の宇宙 $`U'`$ に居住している。
- 小さい型は、そのまま大きい型とみなすことができる。
型の居住関係〈type inhabitation relation〉をコロンで表すとして:
- $`U : U'`$ は成立しない。
- $`\code{U} : U'`$ は成立する。
- $`a:U \Imp a:U'`$ は成立する。
「宇宙は型をホストする場所であり、場所である宇宙が住むべき場所はない」ということです。しかし、宇宙の代理であるコードは、大きな型になります。コードには住むべき場所が定まります(「住む」に関しては「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照)。
ここまでに述べた方式は、タルスキ方式を簡略化しています。が、ラッセル方式ではありません。半タルスキ方式〈semi-Tarski-style〉と呼ぶことにします*1。半タルスキ方式は、「型の型の型」や「型の型の型の型」を安直・野放図に考えてハマルことを予防する効果はあると思います。
しかしながら、記号の乱用で(あるいは、略記の約束で)「$`\code{U}`$ を $`U`$ と書く」とすると、事実上ラッセル方式になってしまいます。記号の乱用をどこまで許すか? を決めるのは難しい判断です。
「命題は型だ」とは?
Propositions-As-Types〈PAT〉は定着したキャッチフレーズなので、僕もよく使いますが、このなかに出てくる"proposition"〈「命題」〉の解釈が問題になります。「命題」の意味は曖昧で、少なくとも次の3つの用法があります。
- 真偽値
- 述語
- 論理式
「命題は型だ」の解釈も少なくとも3つはあります。
- 真偽値は型だ。
- 述語は型だ。
- 論理式は型だ。
これらの曖昧な主張を、明確にしましょう。
まず、グロタンディーク宇宙 $`U`$ をひとつに固定して、次のような別名を付けます。
$`\quad \mbf{Type} := U\\
\quad \mbf{Logic} := U
`$
$`\mbf{Type}`$ と $`\mbf{Logic}`$ は呼び名が違うだけで実体は同じグロタンディーク宇宙です。呼び名が2つあるのは、次の理由です。
- 宇宙 $`\mbf{Type}`$ に住む型はデータの型として使う。このことを強調するために、$`\mbf{Type}`$ はデータ型宇宙〈data-type universe〉とも呼ぶ。
- 宇宙 $`\mbf{Logic}`$ に住む型は論理のための型として使う。このことを強調するために、$`\mbf{Logic}`$ は論理型宇宙〈logic-type universe〉とも呼ぶ。
「論理型プログラミング言語」なんてのがありますが、それとは何の関係もありません。"logic"はそのまま形容詞的にも使います。logical〈ロジカル〉を使って、「論理的な人」とか「論理的に考える」とかを連想されるとチョット困るからです。言葉の印象による誤解・曲解は非常に多いので、気を使ってます。
最初の取り決めは、宇宙 $`\mbf{Logic}`$(それが指す実体は $`\mbf{Type}`$ と同じ)に住む型を“真偽値として使う”ということです。$`\mbf{Logic}`$ の居住者〈inhabitant〉は型ですから、次の主張はそのまま受け入れられます。
- 真偽値は型(宇宙 $`\mbf{Logic}`$ の居住者)だ。
通常、述語とは次のような関数だと定義されるでしょう。
$`\quad p:X \to \mbf{B} \In \mbf{Set}`$
ここで、$`\mbf{B} = \{0, 1\}`$ はブール値の二元集合です。今我々は、真偽値は $`\mbf{Logic}`$ の居住者(つまり、論理型)だと約束しているので、述語の定義は次のように変わります。
$`\quad p:X \to \mbf{Loigc} \In \mbf{SET}\\
\quad \text{where }X \in \mbf{Type}
`$
真偽値をブール値(集合 $`\mbf{B}`$ の居住者)から論理型(宇宙 $`\mbf{Logic}`$ の居住者)に変えるのは、「そのほうが便利だから」という理由です。そうしても大丈夫であることは、以下の過去記事を参照してください。
述語は論理型を値とする型ファミリーなので、「述語は型だ」は不正確です。次ならいいでしょう。
- 述語はパラメータを持つ型だ。
パラメータを持つ型は型ファミリーなので、次でも同じです。
- 述語は型ファミリーだ。
さて、論理式〈formula〉ですが、これは構文的概念です。なにかを表す構文的対象物〈syntactic object〉を項〈term〉と呼びます。論理式は、論理で使う項です。「論理式は型だ」をより正確に言えば:
- 真偽値を表す項は、型項〈type term〉だ。
- 述語を表す項は、パラメータ付きの型項だ。
例えば論理式 $`x \ge 0 \land y \ge 0`$ は、構文的には、パラメータ $`x, y`$ を持つ型項とみなされます。パラメータ $`x, y`$ が確定したとき、それは真偽値、つまり論理型(宇宙 $`\mbf{Logic}`$ の居住者)となります。
どこが便利なのか?
nLab項目 propositions as types の最初の一文を引用すると:
In type theory, the paradigm of propositions as types says that propositions and types are essentially the same.
型理論における propositions as types パラダイムでは、命題と型は本質的に同じだと考えます。
命題〈真偽値〉を型(宇宙 $`\mbf{Logic}`$ の居住者)だとする理由は、「そのほうが便利だから」だと言いました。便利、あるいは話が簡単になることのひとつは、データ型と論理型を区別する必要がなくなることです。そもそも、$`\mbf{Type}`$ と $`\mbf{Logic}`$ は同じグロタンディーク宇宙を指す別名なので、最初から、データ型と論理型の区別なんてないのですけどね。
カリー/ハワード/ランベック対応によれば、依存型理論と論理の概念・記法は次のように対応します。
$`\text{依存型理論}`$ | $`\text{論理}`$ |
---|---|
$`\mbf{0}`$ | $`0`$ |
$`\mbf{1}`$ | $`1`$ |
$`\times`$ | $`\land`$ |
$`+`$ | $`\lor`$ |
$`\mrm{Map}(\hyp, \hyp)`$ | $`\Imp`$ |
$`\mrm{Map}(\hyp, \mbf{0})`$ | $`\lnot`$ |
$`\Sigma`$ | $`\exists`$ |
$`\Pi`$ | $`\forall`$ |
これらは“対応する”というより、同じモノの別名になります。記号の使い分けは気分的なものであり、例えば、論理アンドに '$`\times`$'(集合の直積)を使っても別にかまいません。
多くの人は、論理アンドと集合の直積は別物だ(間違いではないです)と教わっているでしょうから「気持ち悪い」という感情はあるでしょう。二種類の記号法を準備しているのは、気持ち悪さを緩和するためだとも言えます。
*1:「半」は「反」と聞き間違われる可能性があるから嫌なんだけど、適切な言葉が思いつかなかった。