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

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

贅沢なグロタンディーク宇宙と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:「半」は「反」と聞き間違われる可能性があるから嫌なんだけど、適切な言葉が思いつかなかった。