宇宙のラムダ計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)

グロタンディーク宇宙は、フォン・ノイマン宇宙（ZFC集合論の宇宙）のなかの“ある種の代数系（演算を備えた集合）”だと考えられます。代数系としてのグロタンディーク宇宙での計算には、通常のラムダ計算が使えます。なぜなら、外側のフォン・ノイマン宇宙から作られた集合圏も、グロタンディーク宇宙から作られた集合圏も、デカルト閉圏なので型付きラムダ計算は普通に出来るからです。

記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\u}[1]{\underline{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
\newcommand{\T}[1]{ \text{#1} }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\Imp}{\Rightarrow }
%\newcommand{\twoto}{\Rightarrow}
\newcommand{\parto}{\supset\!\to}
`$

内容：

基本的な設定
集合、クラス、関数、クラス関数
集合論的演算
宇宙のラムダ式
簡単な例
例題：モノイドと半群
ラムダ式で書く
記法は変更するだろう

シリーズ記事：

基本的な設定

$`\msf{V}`$（サンセリフ体の V）はフォン・ノイマン宇宙（ZFC集合論の宇宙）、$`\msf{SET}`$ は $`\msf{V}`$ から作られた集合圏だとします。ZFCに宇宙公理〈Axiom of Universes〉を追加しておくことにします。

宇宙公理から、自然数の集合 $`\mbf{N}`$ を含むグロタンディーク宇宙は存在するので、そのようなグロタンディーク宇宙をひとつ選んで $`\mbf{U}`$ とします。$`\mbf{U}`$ より上位の（$`\mbf{U}`$ を要素として含む）グロタンディーク宇宙を $`\mbf{U'}`$ 、さらに上位のグロタンディーク宇宙を $`\mbf{U''}`$ とします。$`\mbf{U}, \mbf{U'}, \mbf{U''}`$ から作られた集合圏を次のように書きます。

$`\mbf{Set} := \mbf{Set}_{\mbf{U}}`$
$`\mbf{SET} := \mbf{Set}_{\mbf{U'}}`$
$`\mbb{SET} := \mbf{Set}_{\mbf{U''}}`$

グロタンディーク宇宙は $`\msf{SET}`$ 内の代数系だとみなします。これについては、以下の過去記事を参照してください。

グロタンディーク宇宙 $`\mbf{U}`$ の“台集合”と“備わってる関係と演算達”をちゃんと書くと：

$`\mbf{U} = (\u{\mbf{U}}, \mrm{Mem}_{\mbf{U}}, \mrm{UnordPair}_{\mbf{U}}, \mrm{Pow}_{\mbf{U}}, \mrm{Union}_{\mbf{U}}, \cdots)`$

「$`\cdots`$」の部分には、その他の演算をたくさん並べてかまいません。贅沢なグロタンディーク宇宙を考えます。贅沢なグロタンディーク宇宙に関しては以下の過去記事を参照してください。

贅沢なタルスキー／グロタンディーク集合論 // 贅沢であること（概略）
贅沢主義者のグロタンディーク宇宙（より詳しく）

混乱の心配がなければ、グロタンディーク宇宙を単に宇宙〈universe〉とも呼びます。記号の乱用と略記で次のように書きます。

$`\quad \mbf{U} = (\mbf{U}, \mrm{Mem}, \mrm{UnordPair}, \mrm{Pow}, \mrm{Union}, \cdots)`$

フォン・ノイマン宇宙やグロタンディーク宇宙から作られた集合圏は、直積・単元集合と指数集合〈関数集合 | 関数空間〉によりデカルト閉圏になります。各集合圏のデカルト閉構造を、宇宙（フォン・ノイマン宇宙含む）でインデックスして書くなら：

$`(\mbf{Set}_{\msf{V}}, \times_{\msf{V}}, \mbf{1}_{\msf{V}}, [\hyp, \hyp]_{\msf{V}})`$
$`(\mbf{Set}_{\mbf{U}}, \times_{\mbf{U}}, \mbf{1}_{\mbf{U}}, [\hyp, \hyp]_{\mbf{U}})`$
$`(\mbf{Set}_{\mbf{U'}}, \times_{\mbf{U'}}, \mbf{1}_{\mbf{U'}}, [\hyp, \hyp]_{\mbf{U'}})`$
$`(\mbf{Set}_{\mbf{U''}}, \times_{\mbf{U''}}, \mbf{1}_{\mbf{U''}}, [\hyp, \hyp]_\mbf{U''}{})`$

しかし、これは煩雑なので、以下のような記号の乱用と略記を使います。

$`\quad \mbf{SET} = (\mbf{SET}, \times, \mbf{1}, [\hyp, \hyp])`$

つまり、$`\times, \mbf{1}, [\hyp, \hyp]`$ などは宇宙多相〈universe polymorphic〉な演算記号として使います。

集合、クラス、関数、クラス関数

ZFC集合論には、オフィシャルなクラス概念はありません（潜在的にクラス概念を使ってますが）。フォン・ノイマン／ベルナイス／ゲーデル集合論〈NBG集合論 | von Neumann–Bernays–Gödel set theory〉では正式にクラスを扱います。ZFC集合論ベースであっても、宇宙〈グロタンディーク宇宙〉に相対的なクラス概念は導入できます。

以下、「贅沢なタルスキー／グロタンディーク集合論補遺」に書いた内容ですが、ここで再度述べます。

宇宙 $`\mbf{U}`$ の要素は $`\mbf{U}`$ の集合〈set in $`\mbf{U}`$〉と呼びます。フォン・ノイマン宇宙 $`\msf{V}`$ の要素（ZFC集合論の集合）はクラス〈class〉と呼びます。$`\mbf{U}`$ の集合はクラスですが、クラスが $`\mbf{U}`$ の集合になるとは限りません。$`\mbf{U}`$ の集合であるクラスは$`\mbf{U}`$-小クラス〈$`\mbf{U}`$-small class〉と呼びます。$`\mbf{U}`$-小クラスではないクラスは$`\mbf{U}`$-真クラス〈$`\mbf{U}`$-proper class〉です。

$`\mbf{U}`$-真クラスであって、$`\mrm{Pow}(\mbf{U})`$ の要素となるクラスは、控えめな$`\mbf{U}`$-真クラス〈modest $`\mbf{U}`$-proper class〉と呼びます。控えめな$`\mbf{U}`$-真クラスは、$`\mbf{U'}`$ の集合になります。真クラス（小さくないクラス）であっても、控えめな真クラスなら、ひとつ上の宇宙内では普通の集合として扱えます。実際に出てくる真クラスは、ほとんど控えめな真クラスです。

$`\mbf{U}`$ の関数〈function in $`\mbf{U}`$〉は、$`\mbf{U}`$ の集合のあいだの関数です。これは、圏 $`\mbf{Set}`$ の射のことです。クラス関数〈class function〉は、クラスのあいだの関数のことです。クラス関数は、$`\mbf{U}`$ の関数とは限りませんが、$`\mbf{U}`$ の関数となる場合もあります。

$`\mbf{U}`$ の関数となっているクラス関数を$`\mbf{U}`$-小クラス関数〈$`\mbf{U}`$-small class function〉、$`\mbf{U}`$ の関数とはなってないクラス関数は$`\mbf{U}`$-真クラス関数〈$`\mbf{U}`$-proper class function〉と呼ぶことにします。$`\mbf{U}`$-小クラス関数は、$`\mbf{U}`$ の関数です。

集合論的演算

宇宙〈グロタンディーク宇宙〉に備わっている様々な演算を集合論的演算〈set-theoretic operator〉と呼ぶことにします。我々は贅沢主義の立場なので、基本演算以外の集合論的演算をたくさん考えます。集合論的演算を幾つか挙げると：

$`\mrm{UnordPair} : \mbf{U}\times\mbf{U} \to \mbf{U} \In\mbf{SET}`$
$`\mrm{Pair} : \mbf{U}\times\mbf{U} \to \mbf{U} \In\mbf{SET}`$ （順序付きペア）
$`n\mrm{Tuple} : \mbf{U}^n \to \mbf{U} \In\mbf{SET}`$ （n-タプル）
$`\mrm{Map} : \mbf{U}\times\mbf{U} \to \mbf{U} \In\mbf{SET}`$ （関数集合〈写像集合〉）
$`\mrm{Singl} : \mbf{U} \to \mbf{U} \In\mbf{SET}`$ （単元集合）
$`\mrm{Prod} : \mbf{U}\times \mbf{U} \to \mbf{U} \In\mbf{SET}`$ （直積集合）

集合論的演算のなかには部分演算〈partial operator〉もあります。部分演算は $`\parto`$ で書きます。例えば：

$`\mrm{TheElement} : \mbf{U} \parto \mbf{U} \In \mbf{SET}`$ （唯一の要素、下に説明あり）
$`\mrm{SecondOfPair} : \mbf{U} \parto \mbf{U} \In \mbf{SET}`$ （ペアの第二成分）
$`\mrm{Complement} : \mbf{U}\times \mbf{U} \parto \mbf{U} \In \mbf{SET}`$ （補集合）

$`\mrm{TheElement}`$ は単元集合に対して、その唯一の要素を取り出す演算です。部分演算の定義域を $`\mrm{def}(\hyp)`$ で書くとして：

$`\quad \mrm{def}(\mrm{TheElement}) = \{x\in \mbf{U}\mid x \T{ は単元集合}\}`$

ペアの第二成分と補集合の定義域は：

$`\quad \mrm{def}(\mrm{SecondOfPair}) = \{x\in \mbf{U}\mid x \T{ はペア}\}`$
$`\quad \mrm{def}(\mrm{Complement}) = \{(x, y)\in \mbf{U}\times \mbf{U} \mid x \subseteq y\}`$

日本語で書いた「$`\cdots \T{ は単元集合}`$」や「$`\cdots \T{ はペア}`$」は、頑張れば集合論の論理式で書けます。

ここから先、集合論的演算には部分演算も許します。つまり、集合論的演算が全域とは限らないことになります。

$`\mbf{U}`$ の集合論的演算は、$`\mbf{SET}`$ では部分関数になります。$`f:A \parto B \In \mbf{SET}`$ は、次のような図式だと解釈します。

$`\quad \xymatrix{
{}
&{\mrm{def}(f)} \ar@{_{(}->}[dl] \ar[dr]^{\u{f}}
&{}
\\
{A}
&{}
&{B}
}\\
\quad \In \mbf{SET}
`$

$`\u{f}`$ は、部分関数 $`f`$ から作った全域関数（普通の関数）です。図からわかるように、部分関数は、集合圏内のスパンで、左脚が包含写像であるものです。

宇宙のラムダ式

集合圏 $`\mbf{SET}`$ はデカルト閉圏で、特定の対象 $`\mbf{U}`$ （正確にはグロタンディーク宇宙の台集合 $`\u{\mbf{U}}`$）を持ちます。また、対象 $`\mbf{U}`$（宇宙）に関わるたくさんの集合論的演算を部分関数として含みます。部分関数は $`\mbf{SET}`$ の射ではありませんが、$`\mbf{SET}`$ 内の簡単な図式ですから「含む」と言ってもいいでしょう。

$`\mbf{SET}`$ がデカルト閉圏であることから、型付きラムダ計算は普通に行えます。ただし、部分関数も扱いたいので、少し工夫が要ります。部分関数 $`f:A\parto B`$ の定義域 $`\mrm{def}(f)`$ が、命題（意味的には述語、構文的には論理式） $`P`$ で特定できるとします。つまり：

$`\quad \xymatrix{
{}
&{ \{x\in A\mid P\}} \ar@{_{(}->}[dl] \ar[dr]^{\u{f}}
&{}
\\
{A}
&{}
&{B}
}\\
\quad \In \mbf{SET}
`$

このとき、部分関数 $`f`$ を次の形のラムダ式〈ラムダ項〉で書き表すことにします。

$`\quad f := \lambda( x\in A\mid P).(\msc{F} \in B)`$

$`\msc{F}`$ は関数 $`\u{f}`$ を表す式です。この形式には次の情報が含まれます。

$`\mrm{dom}(f) = A`$
$`\mrm{def}(f) = \{x\in A\mid P\}`$
$`\mrm{cod}(f) = B`$

部分関数の結合〈composition〉の計算はちょっと面倒になります。もうひとつの部分関数を次だとします。

$`\quad g := \lambda( y\in B\mid Q).(\msc{G} \in C)`$

$`f; g = g\circ f`$ を表すラムダ式は次の形になります。

$`\quad g\circ f := \lambda(x\in A\mid P\land \u{f}^* Q).(\msc{G}[\msc{F}] \in C)`$

ここで、$`\u{f}^* Q`$ は、$`B`$ 上の述語 $`Q`$ を関数 $`\u{f}`$ で引き戻した $`A`$ 上の述語です。構文的には、論理式 $`Q`$ に式 $`\msc{F}`$ を代入した $`Q[\msc{F}]`$ になります。$`\msc{G}[\msc{F}]`$ は、式 $`\msc{G}`$ に式 $`\msc{F}`$ を代入した式です。代入の手順をちゃんと説明すると面倒ですが、皆さんご存知の常識的な手順です。

多変数関数は
$`\quad \lambda(x_1\in A_1, \cdots ,x_n\in A_n\mid P).(\cdots)`$
と書きますが、これは
$`\quad \lambda( (x_1, \cdots ,x_n)\in A_1\times \cdots \times A_n\mid P).(\cdots)`$
と同じだと考えます。

全域関数のときは、定義域を指定する命題（述語、論理式）$`P`$ を省略します。

宇宙 $`\mbf{U}`$ に関するラムダ計算の場合、次のルールを適用します。

変数の型、戻り値の型が省略された場合は、型は $`\mbf{U}`$ だと解釈する。

例えば、
$`\quad \lambda(x_1, x_2, x_3).(x_2)`$
は、
$`\quad \lambda(x_1\in \mbf{U}, x_2\in \mbf{U}, x_3\in \mbf{U}).(x_2 \in \mbf{U})`$
のことです。

$`\mbf{U}`$ 内の関数や、$`\mbf{U}`$ のファミリー〈集合族〉もラムダ式で表します。そのとき、必要があれば次の書き方を使います。

$`\quad f := \lambda(x\in A \in \mbf{U}).(\msc{F} \in B\in \mbf{U})
`$
$`\quad G := \lambda(x\in A \in \mbf{U}).(\msc{G} \in \mbf{U})
`$

$`f`$ は、$`\mbf{U}`$ 内の関数 $`f:A \to B\In \mbf{Set}`$ です。$`G`$ は、$`\mbf{U}`$ のファミリー〈集合族〉 $`G:A \to \mbf{U} \In \mbf{SET}`$ です。

簡単な例

$`\quad \mrm{T}_X := \lambda(x\in X \in \mbf{U}).( \mrm{Singl}(x) )`$

戻り値型が省略されているので、$`\in \mbf{U}`$ を補完して考えると、$`\mrm{T}_X`$ は次のような関数です。

$`\quad \mrm{T}_X : X \to \mbf{U} \In \mbf{SET}`$

$`X\in \mbf{U}`$ だったので、これは $`\mbf{U}`$ のファミリーです。$`\mrm{Singl}`$ は単元集合（を作る関数）だったので、$`T_X`$ の対応は：

$`\quad X \ni x \mapsto \{x\} \in \mbf{U}`$

$`\mrm{T}_X`$ の下付きの $`{}_X`$ を引数だと思って、$`X`$ を引数に取る関数も明示的に書けば：

$`\quad \mrm{T} := \lambda(X\in \mbf{U}).(
\lambda(x\in X \in \mbf{U}).( \mrm{Singl}(x) )
\;\in \mrm{Map}(X, \mbf{U})
)
`$

集合（単に「集合」といえば、$`\mbf{U}`$ の集合）$`X`$ に、常に $`C\in \mbf{U}`$ を対応付ける定数関数を $`\mrm{K}_X^C`$ とします。その定義は：

$`\quad \mrm{K}_X^C := \lambda(x\in X \in \mbf{U}).( C )`$

$`(C \in \mbf{U})`$ の $`\in \mbf{U}`$ は省略していいルールだったので省略しています。

$`\mrm{K}_X^C`$ の下付き・上付きの $`{}_X^C`$ を2つの引数だと思って、$`X, C`$ を引数に取る関数も明示的に書けば：

$`\quad \mrm{K} := \lambda(X, C).(
\lambda(x\in X).( C )
\;\in \mrm{Map}(X, \mbf{U})
)
`$

$`(X\in \mbf{U}, C\in \mbf{U})`$ の引数型 $`\mbf{U}`$ は省略しました。

三番目の例として、特定の宇宙 $`\mbf{U}`$ ではなくて、“任意の宇宙” $`U`$ 上のシグマ型の定義をラムダ式で書き下しましょう。$`\sum_{U, X}F`$ を $`\mrm{Sigma}(U, X, F)`$ という3変数〈3引数〉の関数だとみなします。

$`\quad \mrm{Sigma} := \lambda(U\in\mbf{Universe}, X\in U, F\in \mrm{Map}(X, U)).(\\
\qquad \bigcup_{x\in X} (\{x\}\times F(x) )
\;\in U \\
\quad )
`$

関数（ラムダ抽象）の本体をより正確に書けば：

$`\quad \mrm{Union}\left(\,
\lambda(x\in X).(\mrm{Prod}(\mrm{Singl}(x), F(x) ) )
\,\right)
`$

$`\mrm{Union}, \mrm{Prod}, \mrm{Singl}`$ は、宇宙（フォン・ノイマン宇宙でもグロタンディーク宇宙でも）に備え付け・組み込みの関数でした。

この関数〈ラムダ抽象〉の引数リスト〈ラムダリスト〉を見ると、
$`\quad (U\in\mbf{Universe}, X\in U, F\in \mrm{Map}(X, U))`$
これは依存リスト〈依存タプル〉です。実は、宇宙のラムダ計算は依存ラムダ計算です。今回は依存性についてこれ以上踏み込みませんが。

例題：モノイドと半群

$`\mbf{Semigrp}`$ は半群達の圏〈category of semigroups〉、$`\mbf{Mon}`$ はモノイド達の圏〈category of monoids〉とします。半群もモノイドも宇宙 $`\mbf{U}`$ で考えているとします。そのとき、次のようにみなせます。

$`\quad |\mbf{Semigrp}| \subseteq \mbf{U}`$
$`\quad |\mbf{Mon}| \subseteq \mbf{U}`$

これには納得いかない人がいるかもしれません。「根本的誤解：集合論、圏論、型理論」から引用します。

集合を表す有向グラフは、無条件ではありませんが、それでも極めて複雑な構造を持ち得ます。我々は、どんな複雑な情報でも集合のなかにエンコードする（書き込む）ことが出来ます。つまり集合は、概念的なメディアリソース〈media resource〉、あるいは情報担体〈information-bearing object〉なのです。
情報隠蔽としてのフラット集合はよいのですが、すべての集合をフラット集合と捉えてしまうと、集合がとてつもなく複雑な構造を持てるという大事な事実を忘れてしまいがちです。
集合に対するメンタルイメージとして、アトムのフラットな集まりではなくて、とてつもなく複雑でとてつもなく深い入れ子構造を持つかも知れない有向グラフを思い浮かべましょう。

半群でもモノイドでも、“単一の $`\mbf{U}`$ の集合”にエンコードできます。ある集合が半群（をエンコードした集合）かどうかは、次のような述語（構文的には論理式）で判定できます。$`\mbf{B}`$ は真偽値の二元集合〈ブーリアン型〉です。

$`\quad \mrm{IsSemigrp} : \mbf{U} \to \mbf{B}\In \mbf{SET}`$

したがって、$`|\mbf{Semigrp}|`$ は $`\mbf{U}`$ の部分集合として（原理的には）確定できます。

$`\quad |\mbf{Semigrp}| = \{X\in \mbf{U} \mid \mrm{IsSemigrp}(X) \}`$

モノイドの場合も同じです。

$`|\mbf{Semigrp}| \subseteq \mbf{U}`$ がどうしても気持ち悪い（僕も気持ち悪いです）なら、$`|\mbf{Semigrp}|`$ から $`\mbf{U}`$ への埋め込みがあり、その埋め込み像と $`|\mbf{Semigrp}|`$ を同一視している、と考えるといいでしょう。

圏 $`\mbf{Mon}`$ からの、2つの忘却関手を考えます。モノイドの単位元と単位法則を忘れて半群だとみなす関手 $`U_1`$ と、モノイドの台集合と単位元だけを取り出して付点集合〈pointed set〉だとみなす関手 $`U_2`$ です。これらの関手の対象パートだけ考えます。つまり忘却写像を考えます。2つの忘却写像を関手と同じ記号 $`U_1, U_2`$ で表すと以下の図式になります。

$`\quad \xymatrix{
{}
&{|\mbf{Mon}| } \ar[dl]_{U_1} \ar[dr]^{U_2}
&{}
\\
{|\mbf{Semigrp}| }
&{}
&{|\mbf{PtSet}| }
}\\
\quad \In \mbf{SET}
`$

さて問題です。以下の図式を可換にする部分関数で、定義域ができるだけ大きなものを見つけて、具体的に書き下してください。「具体的」には程度があります -- ほんとに全部書き出すと大変なので、適当に端折ってもいいです。

$`\quad \xymatrix{
{}
&{|\mbf{Mon}| } \ar[dl]_{U_1} \ar[dr]^{U_2}
&{}
\\
{|\mbf{Semigrp}| } \ar@{)->}[rr]_{?}
&{}
&{|\mbf{PtSet}| }
}\\
\quad \In \mbf{SET}
`$

ラムダ式で書く

一般論として、この種の問題では、以下のパターンの述語があると便利です。

$`\mrm{IsXxxOf}(x, A)`$ ： $`x`$ は $`A`$ の Xxx である。
$`\mrm{HasXxx}(A)`$ ： $`A`$ は Xxx を持っている。
$`\mrm{XxxIsUniqueFor}(A)`$ ： $`A`$ の Xxx は（存在すれば）一意的である。
$`\mrm{HasUniqueXxx}(A)`$ ： $`A`$ は一意的な（ひとつだけの）Xxx を持っている。

簡単な例として、$`x`$ も $`A`$ も実数だとして、Xxx は正の平方根（sqrt = square root）だとすると：

$`\mrm{IsSqrtOf}(r, a)`$ ： $`r`$ は $`a`$ の正平方根である。
$`\mrm{HasSqrt}(a)`$ ： $`a`$ は正平方根を持っている。
$`\mrm{SqrtIsUniqueFor}(a)`$ ： $`a`$ の正平方根は（存在すれば）一意的である。
$`\mrm{HasUniqueSqrt}(a)`$ ： $`a`$ は一意的な（ひとつだけの）正平方根を持っている。

これらは独立な述語ではなくて、$`\mrm{IsXxxOf}`$ があれば他は定義可能です。

$`\mrm{HasXxx}(A) :\equiv \exists x. \mrm{IsXxxOf}(x, A)`$
$`\mrm{XxxIsUniqueFor}(A) :\equiv \forall x, y.( \mrm{IsXxxOf}(x, A)\land \mrm{IsXxxOf}(y, A) \Imp x = y )`$
$`\mrm{HasUniqueXxx}(A) :\equiv \mrm{HasXxx}(A) \land \mrm{XxxIsUniqueFor}(A)`$

$`\mrm{HasUniqueXxx}(A)`$ が成立している前提で、$`A`$ から Xxx である $`x`$ を取り出す関数を書けます。その関数の式は：

$`\quad \lambda(A \in Y \mid \mrm{HasUniqueXxx}(A)).(
\varepsilon!\, x \in X. \mrm{IsXxxOf}(x, A)
\;\in Z
)
`$

ここで、$`X, Y, Z`$ は適当な集合〈型〉で、$`\varepsilon!`$ は一意性が保証されている前提で使うヒルベルトのイプシロン記号だとします。$`\varepsilon!\, x\in X. P(x)`$ は次と同じです。

$`\quad \mrm{TheElement}(\{x\in X\mid P(x) \})`$

実数の正平方根の場合ならば、この方法で平方根関数を定義できます。

$`\quad \mrm{sqrt} :=
\lambda(a \in \mbf{R} \mid \mrm{HasUniqueSqrt}(a)).(\\
\qquad \varepsilon!\, r \in \mbf{R}. \mrm{IsSqrtOf}(r, a)
\;\in \mbf{R}\\
\quad)
`$

さて、前節の問題に対しては、次の述語を考えます。

$`\mrm{IsUnitOf}(e, S)`$ ： $`e`$ は半群 $`S`$ の単位元である。
$`\mrm{HasUnit}(S)`$ ：半群 $`S`$ は単位元を持っている。
$`\mrm{UnitIsUniqueFor}(S)`$ ：半群 $`S`$ の単位元は（存在すれば）一意的である。
$`\mrm{HasUniqueUnit}(S)`$ ：半群 $`S`$ は一意的な（ひとつだけの）単位元を持っている。

$`\mrm{IsUnitOf}`$ は、半群 $`S`$ の台集合 $`\u{S}`$ と演算 $`*`$ を使って次のように書けます。

$`\quad \mrm{IsUnitOf}(e, S) :\equiv
\forall x\in \u{S}.( e*x = x*e = x )
`$

$`\mrm{IsUnitOf}`$ により $`\mrm{HasUnit}`$ は定義できます。$`\mrm{UnitIsUniqueFor}`$ は証明可能な命題（任意の $`S`$ で成立）です。したがって、$`\mrm{HasUnit}(S)`$ が言えれば $`\mrm{HasUniqueUnit}(S)`$ も言えます。

前節の問題の解となる部分関数は、平方根の場合と同じように書けます。

$`\quad \mrm{unitAndCarrier} :=
\lambda(S \in |\mbf{Semigrp}| \mid \mrm{HasUniqueUnit}(S)).(\\
\qquad (\u{S} , \varepsilon!\, e \in \u{S}. \mrm{IsUnitOf}(e, S) )
\;\in |\mbf{PtSet}|\\
\quad)
`$

記法は変更するだろう

この記事にはたぶん続きがあります。この記事で使った記法は変更することになるでしょう。$`\lambda( x\in A\mid P).(\msc{F} \in B)`$ という書き方は読みやすくて“なかなかいい”と思うのですが、次の問題があります。

型と命題を完全に分離して（縦棒の左と右に）書いているが、Propositions-as-Types の立場からは、型と命題は同じように扱いたい。
命題 $`P`$ の後に、さらに変数の型宣言を続けて書きたいことがある。この記法ではそれができない。

依存性を本格的に導入して、Propositions-as-Types の立場を採用するなら、型宣言も命題も同じ書き方が望ましいので、$`( x\in A\mid P)`$ は $`(x\in A, p\in P)`$ となりますが、これは奇妙な感じです。$`(x : A, p : P)`$ とか $`(x\in A, p\in \langle P \rangle)`$ とかだと違和感は薄まるでしょう。いずれにしても、ラムダ計算を一般化すると $`(x : A\mid P)`$ は使えなくなりそうです。

今回説明した概念で、あまり使ってないもの（例えばクラス関数）がありますが、それは次の記事の準備だと思ってください。今日はここまで（「今日はここまで」参照）。

続きの記事：宇宙のラムダ計算 2：構文