「宇宙のラムダ計算」の続きです。
宇宙のラムダ計算にはどんな構文がいいでしょうか？ 構文の決定には、心理的・感情的エルゴノミクスも考慮する必要があります。違和感がないか、気持ちよく書けるか？ といった問題です。可読性とタイピング量の節約も考慮すべき点です。しばしば、可読性とタイピング量の節約は相反する条件になります。
別な考慮点として、既存の構文との互換性や類似性があります。あまりに見慣れない／目新しい構文は抵抗があるだろうし、学習負担を増やします。
様々な（ときに相反する）要求のバランスをとるのは難しいのですが、とりあえず、たたき台を考えてみましょう。記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\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}
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] }
`$
内容：
ハブ記事：
はじめに
この記事では、ラムダ計算の構文は、構文論と意味論を厳密に区別しないスタイルで述べます。通常のインフォーマルなラムダ計算を説明するスタイルです。もし、構文論と意味論をハッキリ分けるのならば、なにかしらの構文的対象物〈syntactic object〉$`\msc{X}`$ に対して、その意味を $`\BR{\msc{X}}`$ と書きます。今回は、$`\msc{X}`$ と $`\BR{\msc{X}}`$ をあまり区別しない／同一視することが多い、ということです。
しかし、構文的対象物（式／項）であることを強調したいときはスクリプト体の文字（$`\msc{X}`$ や $`\msc{A}`$）で書くことにします。また、構文と意味の区別を意識すべきときには「構文的には ～」「意味的には ～」といった言い方で説明します。
意味論〈セマンティクス〉の基盤となる集合論はZFC集合論に宇宙公理〈Axiom of Universes〉を追加したものです。宇宙公理を使って、$`\mbf{N}`$ を含むグロタンディーク宇宙 $`\mbf{U} = \mbf{U}_0`$ をとり、より上位の宇宙を順番に選んでいくことにより、宇宙の系列（タワー）を作れます。
$`\quad \mbf{U}_0 \in \mbf{U}_1 \in \mbf{U}_2 \in \cdots`$
可算無限個の宇宙達のタワーを固定した上で、タルスキー／グロタンディーク集合論を作業用の集合論として使います。タルスキー／グロタンディーク集合論の“集合”とは、どれかの宇宙の要素です。タルスキー／グロタンディーク集合論の“クラス”とは、ZFC集合論の集合のことです（「宇宙のラムダ計算 // 集合、クラス、関数、クラス関数」参照）。
どれかひとつの宇宙を特定して、その宇宙に相対的な真クラス〈proper class〉とは、その宇宙の要素にはならないクラスのことです。ある宇宙の真クラスは、別の宇宙では集合かも知れません。どの宇宙から見ても真クラスとなるクラスもあります。我々は、宇宙内に居る集合だけでなくクラス（ZFC集合論の任意の集合）も自由に使います。
定数記号
次の記号は、宇宙のラムダ計算の定数です。
- $`\msf{V}`$ ： フォン・ノイマン宇宙（ZFC集合論の宇宙）を表す記号
- $`\mbf{U}_0, \mbf{U}_1, \mbf{U}_2, \cdots`$ ： 可算無限個の宇宙定数
- $`\mbf{Universe}`$ ： すべての宇宙からなる集合を表す定数
前節で述べたように、“記号”と“記号が表す実体”を同一視することがあります。例えば、$`\BR{\mbf{U_0}} = \mbf{U}_0`$ のように考えます。
$`\mbf{Universe}`$ は可算無限集合で、宇宙のあいだの所属関係で全順序集合になります。順序も込めて $`\mbf{N} \cong \mbf{Universe}`$ です。この同型は次の対応で与えられます。
$`\quad \mbf{N} \ni k \longleftrightarrow \mbf{U}_k \in \mbf{Universe}`$
最初の宇宙 $`\mbf{U}_0`$ は単に $`\mbf{U}`$ とも書きます。プライム〈ダッシュ〉を付けると“次の宇宙”を表すことにします。
$`\quad \mbf{U} = \mbf{U}_0, \mbf{U'} = \mbf{U}_1, \mbf{U''} = \mbf{U}_2, \cdots`$
各宇宙に対応する集合圏（を表す記号）も、宇宙のラムダ計算の定数です。一般的には $`\mbf{Set}_{\mbf{U}_k}`$ と表しますが、最初のほうは文字種・フォントを変えて表します。
$`\quad \mbf{Set} := \mbf{Set}_{\mbf{U}}`$
$`\quad \mbf{SET} := \mbf{Set}_{\mbf{U'}}`$
$`\quad \mbb{SET} := \mbf{Set}_{\mbf{U''}}`$
フォン・ノイマン宇宙 $`\msf{V}`$ から作る集合圏は $`\msf{SET}`$（サンセリフ体）と書きます。
よく知られた集合の固有名 $`\mbf{N}, \mbf{Z}, \mbf{R}`$ なども最初から入っているとします。$`\mbf{N}`$ の要素は（オフィシャルには）フォン・ノイマンの自然数だとします。例えば
$`\quad 3 = \{\,\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\} \,\}`$
です（「根本的誤解： 集合論、圏論、型理論 // アトム信仰」参照）。
オフィシャルには、順序ペア〈順序付きペア〉もクラトフスキー・ペアだとします（「ペアの形式的な定義 // 順序ペア」参照）。もちろん、通常はクラトフスキー・ペアを意識する必要はありません。
我々は贅沢主義（「贅沢なタルスキー／グロタンディーク集合論」参照）を採用しているので、宇宙にはたくさんの集合論的演算が最初から備わっているとします（「宇宙のラムダ計算 // 集合論的演算」参照）。自然数の順序・算術演算や実数の順序・算術演算なども最初から関係記号・関数記号として入っています。必要なモノ（に対する定数記号）は何でも入っている前提です。
また、上で述べた各種の集合圏も最初から備わっているとします。圏に付随する演算、域〈domain〉・余域〈codomain〉・恒等〈identity〉・結合〈composition〉なども自由に使えます。必要に応じて、集合圏以外の圏、例えばモノイドの圏 $`\mbf{Mon}`$ や実数係数のベクトル空間の圏 $`\mbf{Vect}_{\mbf{R}}`$ なども追加して使います。
実用的にラムダ式を書くためには、オーバーロード解決のための型クラスやコアージョン（に類似）のメカニズムが必要ですが、これらについては必要になったときに都度言及します。
ラムダ抽象のパーツ
ここでは、ラムダ計算やラムダ式はすべて型付きで考えます。
ラムダ抽象は、ラムダ式〈ラムダ項〉のなかでも特に関数を表す式です。多くの人が、ラムダ式の典型例としてラムダ抽象を思い浮かべるでしょう*1。ラムダ抽象は次の形です。
$`\quad \lambda\,\msc{P}.\msc{B}`$
$`\msc{P}, \msc{B}`$ は構文的なパーツを表していて、$`\msc{P}`$ は仮引数リスト〈formal parameter list〉、$`\msc{B}`$ はボディ〈body〉と呼びます。例を見てみましょう。
$`\quad \lambda\,(x\in \mbf{R}, y\in \mbf{R}).(\sqrt{x^2 + y^2} \in \mbf{R})`$
この例では、$`(x\in \mbf{R}, y\in \mbf{R})`$ が仮引数リスト、$`(\sqrt{x^2 + y^2} \in \mbf{R})`$ がボディです。一般的にはボディもリストです。この例では、成分がひとつのリストです。
引数や戻り値の型宣言に所属記号 '$`\in`$' を使いましたが、プログラミング言語や型理論の習慣ではコロンです。コロンのほうが落ち着きがいいので、コロンを採用することにします。
$`\quad \lambda\,(x : \mbf{R}, y : \mbf{R}).(\sqrt{x^2 + y^2} : \mbf{R})`$
引数に条件が付くとき（部分関数になるとき）の書き方が悩みのタネです。「宇宙のラムダ計算」で使った記法は分かりやすく自然なのですが、「記法は変更するだろう」で述べた問題があります。
例えば、$`(x: \mbf{R}, y:\mbf{R})`$ の $`x,y`$ に $`y \ne 0 \lor x \lt 0`$ という条件を付けるとします。Propositions-as-Types の立場では、命題も型なので、次のように書いてもいいはずです。
$`\quad (x: \mbf{R}, y:\mbf{R}, p: y \ne 0 \lor x \lt 0)`$
理屈ではOKです。が、多くの人が違和感をおぼえるでしょう（見にくいし）。違和感と難読性を軽減するために、命題（構文的には論理式）は山形括弧で囲むことにします。
$`\quad (x: \mbf{R}, y:\mbf{R}, p: \langle y \ne 0 \lor x \lt 0\rangle)`$
こう書いても、「$`p`$ は何なんだ？」となるでしょう。$`p`$ は命題のインスタンスを表す変数ですが、そう言っても「命題のインスタンスとは何なんだ？」ですよね。命題のインスタンスは証明なんですが、$`y \ne 0 \lor x \lt 0`$ の証明と言ってもやっぱりピンとこないでしょう。
暫定的な説明ですが、$`p`$ は、$`y \ne 0 \lor x \lt 0`$ が成立することを保証するデータなのだ、と思ってください。そのデータを命題に対する証拠〈witness〉と呼びます。変数 $`p`$ は、命題 $`y \ne 0 \lor x \lt 0`$ の証拠を表す変数です。
なんらかの関数 $`G`$ に $`G(x, y)`$ と引数を渡すと、$`G`$ は $`x, y`$ を任意の2つの実数と解釈します。が、$`G(x, y, p)`$ と $`p`$ も渡すと $`y \ne 0 \lor x \lt 0`$ という条件も $`G`$ に伝わることになります。通常は、命題の証拠が明示的な引数にはされないことが多いですが、それは次のような理由でしょう。
- 関数 $`G`$ を呼ぶ側が、条件を満たさない $`x,y`$ を渡さないように気をつけるから大丈夫。
- なぜか関数 $`G`$ も、以心伝心で条件を知っているから大丈夫。
- 条件を満たさない $`x,y`$ を渡したら、$`G`$ が例外・エラーで報告するはずだから大丈夫。
ここでは、条件（が成立すること）をエンコードしたデータ（それが証拠）を $`G`$ に渡す、という流儀で考えます。この流儀が珍しいので違和感があるかも知れませんが、原則的にはこうします*2。
命題も含まれる仮引数リストを持つラムダ抽象の例を挙げます。
$`\quad \lambda\,(x: \mbf{R}, y:\mbf{R}, p: \langle y \ne 0 \lor x \lt 0\rangle).(\sqrt{x^2+y^2} : \mbf{R}, \arctan \frac{y}{x} : \mbf{R})
`$
これは、直交座標から極座標への変換なので、余域が $`\mbf{R}\times \mbf{R} = \mbf{R}^2`$ になるのは奇妙ですが、その点はまた後で触れます。
すぐ上の例では、ボディもリストでした。リストであることを強調するときはボディリスト〈body list〉ということにします。
ボディリストの波括弧形式
前節の関数の逆で、極座標を直交座標に変換する関数を考えましょう。仮引数リストはどうなるでしょうか？ $`(r: \mbf{R}, \theta :\mbf{R})`$ ですか？ $`r`$ は正の実数で、$`\theta`$ は $`0\lt \theta \lt 2\pi`$ が自然ですよね。この条件も仮引数リストに書くと次のようになります。
$`\quad \lambda\,(r : \mbf{R}, u: \langle 0 \lt r \rangle, \theta : \mbf{R},
v : \langle 0\lt \theta \lt 2\pi \rangle).(
r \cos \theta : \mbf{R}, r \sin \theta : \mbf{R}
)
`$
この関数も余域が $`\mbf{R}\times\mbf{R} = \mbf{R}^2`$ です。余域にも条件を付けるためには、書き方を少し変えたほうが便利です。
今まで、ボディリストは丸括弧で囲んだリストで、リストの成分〈項目〉は、「式 : 型」という形でした。それを次のように変えます。
- リストは波括弧で囲む。
- リストの成分〈項目〉は、「変数名 : 型 := 式」の形とする。
- 区切り記号のカンマは、改行に置き換えてもよい。（改行区切りも可能）
まったく同じ関数（ラムダ抽象）を、波括弧形式〈brace form〉で書いてみます。
$`\quad \lambda\,(r : \mbf{R}, u: \langle 0 \lt r \rangle, \theta : \mbf{R},
v : \langle 0\lt \theta \lt 2\pi \rangle).\{ \\
\qquad x : \mbf{R} := r \cos \theta\\
\qquad y : \mbf{R} := r \sin \theta\\
\quad \}
`$
この書き方なら、長いボディリストも見やすく書けます。戻り値が2つの実数 $`x, y`$ だけでなくて、条件となる命題の証拠も戻り値であるなら次のようです。
$`\quad \lambda\,(r : \mbf{R}, u: \langle 0 \lt r \rangle, \theta : \mbf{R},
v : \langle 0\lt \theta \lt 2\pi \rangle).\{ \\
\qquad x : \mbf{R} := r \cos \theta\\
\qquad y : \mbf{R} := r \sin \theta\\
\qquad p : \langle y \ne 0 \lor x \lt 0 \rangle := \,??? \\
\quad \}
`$
'$`???`$' の部分には何が入るのでしょうか？ 実は、ここには命題 $`y \ne 0 \lor x \lt 0 `$ の証明が入ります。通常、証明は自然言語ベースの文章で書くので、ラムダ式の一部に証明が入ると言われてもイメージがわかないかも知れません。
証明も形式化〈formalize〉すれば、なんらかの式（構文的対象物）として書けます。その式を証明項〈proof term〉とか証明オブジェクト〈proof object〉と呼びます。'$`???`$' の部分には証明項が入るわけです。
証明項をちゃんと定義するのは手間がかかるので、ここでは割愛します。が、「通常の証明なら書けそうだ」とは思えるでしょう。念の為に、証明の仮定を '$`\in`$' を使った命題として列挙すると：
- $`r \in \mbf{R}`$
- $`0 \lt r`$
- $`\theta \in \mbf{R}`$
- $`0 \lt \theta \lt 2\pi`$
- $`x \in \mbf{R}`$
- $`x = r \cos \theta`$
- $`y \in \mbf{R}`$
- $`y = r \sin \theta`$
証明すべき結論の命題は：
- $`y \ne 0 \lor x \lt 0 `$
証明は書けそうでしょ。
さて、実際の証明を書く代わりに、「この命題には証明がちゃんとあって、その証明が ～」という意味を表す記法としてヒルベルトのイプシロン記号を使いましょう。命題 $`P`$ の証明を（それが在るとして）$`\varepsilon \langle P\rangle`$ と書きます。例えば：
$`\quad \varepsilon \langle y \ne 0 \lor x \lt 0 \rangle`$
これは略記であって、証明には（たいていは）仮定が必要ですから、（上に列挙した）仮定の集まりを $`\Gamma`$ として：
$`\quad \varepsilon \langle \Gamma \vdash y \ne 0 \lor x \lt 0 \rangle`$
この記法のココロは； $`\langle \Gamma \vdash P \rangle`$ は、$`\Gamma`$ を仮定して命題 $`P`$ を導く証明（＝証拠）の集合だと解釈します。証明が在る前提なら、証明（＝証拠）の集合は空ではありません。イプシロン記号は集合から要素を取り出します。よって、$`\varepsilon \langle \Gamma \vdash P \rangle`$ は $`P`$ の証明（＝証拠）のひとつです。
ヒルベルトのイプシロン記号を使った書き方は便宜的なもので、ズルしていることには注意してください。イプシロンで証拠の集合から要素をひとつ取り出す段階で、証拠の集合が空でないと仮定しています。この仮定はあきらかにズルです。
宇宙規模のラムダ抽象
前節の直交座標と極座標の変換は、日常的な計算でした。宇宙規模の計算として、「宇宙のラムダ計算 // ラムダ式で書く」の例を波括弧形式で書いてみます。
$`\quad \lambda\,(S : |\mbf{Semigrp}|, h : \langle \mrm{HasUniqueUnit}(S)\rangle ).\{ \\
\qquad X : \mbf{U} := \u{S}\\
\qquad a : X := \varepsilon!\, e\in \u{S}.\mrm{IsUnitOf(e, S)}\\
\quad\}
`$
$`h`$ は、半群 $`S`$ が一意的な単位元を持つことを表す証拠です。$`h`$ はボディのどこで使われているのでしょうか？ 一意的な要素を取り出す $`\varepsilon!`$ の使用を正当化〈justify〉するために $`h`$ が必要です。正当化命題〈justification〉は次の命題です。
$`\quad \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}`$
イプシロン記号使用の正当化命題もボディに書き込んでみます。が、結果〈出力〉には影響しないので、プログラミング言語の習慣に倣ってプライベート修飾子（$`\T{@private}`$ とする）を付けます。
$`\quad \lambda\,(S : |\mbf{Semigrp}|, h : \langle \mrm{HasUniqueUnit}(S)\rangle ).\{ \\
\qquad X : \mbf{U} := \u{S}\\
\qquad \T{@private } u : \langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle := \varepsilon\langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle \\
\qquad a : X := \varepsilon!\, e\in \u{S}.\mrm{IsUnitOf(e, S)}\\
\quad\}
`$
$`u`$ に対する証明項はズルしています。しかも証明の仮定を省略しています。
上のラムダ抽象で定義される関数に名前を付けたいなら、名前にラムダ抽象を束縛すればいいのです。名前への値の束縛も '$`:=`$' で書くなら：
$`\mrm{unitAndCarrier} := \lambda\,(S : |\mbf{Semigrp}|, h : \langle \mrm{HasUniqueUnit}(S)\rangle ).\{ \\
\qquad X : \mbf{U} := \u{S}\\
\qquad \T{@private } u : \langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle := \varepsilon\langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle \\
\qquad a : X := \varepsilon!\, e\in \u{S}.\mrm{IsUnitOf(e, S)}\\
\quad\}
`$
次のように書くと、よりプログラミング言語っぽい雰囲気になります。
$`\T{fun }\mrm{unitAndCarrier} \;(S : |\mbf{Semigrp}|, h : \langle \mrm{HasUniqueUnit}(S)\rangle )\:\{ \\
\quad X : \mbf{U} := \u{S}\\
\quad \T{@private } u : \langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle := \varepsilon\langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle \\
\quad a : X := \varepsilon!\, e\in \u{S}.\mrm{IsUnitOf(e, S)}\\
\}
`$
あまりプログラミング言語っぽくしようとすると、「オラがプログラミング言語に寄せろ」的な不毛な議論を呼び起こす*3ので、この程度にしておきます。
もうひとつの例： 関数の域・余域の制限
関数〈写像〉 $`f:X \to Y\In \mbf{Set}`$ があるとき、$`f`$ の域と余域を制限することを考えます。$`A\subseteq X`$ と $`B\subseteq Y`$ をとって、域と余域を制限した関数 $`g:A \to B \In \mbf{Set}`$ を作れます。ただし、$`f(A) \subseteq B`$ という条件は必要です。
関数の域・余域を制限する関数（宇宙規模の関数）を $`\mrm{Restr}`$ とします。通常は、$`\mrm{Restr}`$ を縦棒で書くことが多いです。
$`\quad f|_A^B := \mrm{Restr}(f, A, B)`$
宇宙規模の関数 $`\mrm{Restr}`$ には、どの宇宙で考えているかも明示的な引数〈パラメータ〉とすることにします。次のようなラムダ抽象で書けます。
$`\mrm{Restr} := \lambda\,(U : \mbf{Universe}, X : U, Y : U, f: \mrm{Map}(X, Y),\\
\quad A : \mrm{Pow}(X), B : \mrm{Pow}(Y),
c: \langle f(A) \subseteq B \rangle
).\{ \\
\qquad U : \mbf{Universe} := U\\
\qquad A : U := A\\
\qquad B : U := B\\
\qquad \T{@private } u : \langle \forall x\in A. f(x) \in B\rangle := \varepsilon\langle \forall x\in A. f(x) \in B\rangle\\
\qquad g : \mrm{Map}(A, B) := \lambda\, (x:A).(f(x) : B)\\
\quad\}
`$
この関数の結果〈出力 | 戻り値〉は、次の形の依存リスト〈依存タプル〉です。
$`\quad (U, A, B, g)\\
\quad \T{where }U\in \mbf{Universe}, A\in U, B\in U, g\in \mrm{Map}(A, B)
`$
プライベートな $`u`$（命題の証拠・証明）は、$`\lambda\, (x:A).(f(x) : B)`$ というラムダ抽象を正当化する正当化命題の証拠です。ここでもズルしてますが、引数にある $`c`$ から $`u`$ は自明（事実上同じ命題の証拠）です。
$`\mrm{Restr}`$ には引数がイッパイありますが、宇宙 $`U`$ は通常暗黙に仮定され、$`X, Y`$ は $`f`$ から推論〈infer〉できて、条件 $`c`$ も省略する習慣があるので、$`\mrm{Restr}(f, A, B)`$ のような書き方が許されます（大目に見ていい、ということ）。
そしてそれから
この記事で定義したラムダ抽象の構文はたたき台です。変更や追加があるかも知れません。そのときはまた続きの記事を書くことにします。
ラムダ式、特にラムダ抽象が、日常的な計算・関数だけでなくて、宇宙規模の関数も同じように記述できることは分かったと思います。この強力な記述能力の応用についても、また続きを書くかも知れません。
