このブログの更新は X（旧Twitter）アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

［参照用 記事］

贅沢なグロタンディーク宇宙とPropositions-As-Types

雑記／備忘

次の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つは共通です（「贅沢主義者のグロタンディーク宇宙」参照）。

  1. 所属関係に関して推移的： $`\forall x, y.\; x\in U \land y\in x \Imp y\in U`$
  2. 自然数全体の集合を要素として含む： $`\mbf{N}\in U`$

二番目は、「無限を扱いたい」という要求を満たすためです。有限だけで事が済むなら不要な公理です。

オリジナルの節約主義に基づくグロタンディーク宇宙が備えている集合論的操作は次の3つです。

  1. 順序なしペア〈unordered pair〉： $`x, y\mapsto \{x, y\}`$
  2. ベキ集合： $`x\mapsto \mrm{Pow}(x)`$
  3. ファミリーの合併： $`(f:x \to U)\mapsto \bigcup(x\mid f)`$

贅沢主義では、出来る操作はもっと増えます。贅沢主義の眼目は、道具・手段を自作する手間を省いて、最初から十分な道具・手段を揃えておこう、ということです。贅沢主義では、次の操作も“出来ること”に入れます。

  1. 順序ペア〈ordered pair〉： $`x, y\mapsto (x, y)`$
  2. 単元集合： $`x\mapsto \{x\}`$
  3. シグマ型： $`(f:x \to U)\mapsto \Sigma(x\mid f)`$
  4. パイ型： $`(f:x \to U)\mapsto \Pi(x\mid f)`$
  5. オメガ型： $`(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〉です。

上に述べた方式は次のようにまとめられます。

  1. 小さい型は、小さい型達の宇宙 $`U`$ に居住している。
  2. 小さい型達の宇宙 $`U`$ を、そのまま大きい型とみなすことはできない。
  3. 小さい型達の宇宙 $`U`$ のコード $`\code{U}`$ は、大きい型である。
  4. 大きい型は、大きい型達の宇宙 $`U'`$ に居住している。
  5. 小さい型は、そのまま大きい型とみなすことができる。

型の居住関係〈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つの用法があります。

  1. 真偽値
  2. 述語
  3. 論理式

「命題は型だ」の解釈も少なくとも3つはあります。

  1. 真偽値は型だ。
  2. 述語は型だ。
  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:「半」は「反」と聞き間違われる可能性があるから嫌なんだけど、適切な言葉が思いつかなかった。