この記事は、「宇宙のラムダ計算」「宇宙のラムダ計算 2： 構文」の続きです。ラムダ抽象の仮引数リストを独立させた、“依存性を持つ（かも知れない）型リスト”について述べます。$`%\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{\PR}[1]{ \langle{#1}\rangle } % PRoposition
`$
内容：
ハブ記事：
名前と型の分離
ラムダ抽象の一般的な形は次のようでした。
$`\quad \lambda\,\msc{P}.\msc{B}`$
$`\msc{P}`$ は仮引数リスト〈formal parameter list〉です。仮引数リストの一般的な形は：
$`\quad (x_1:T_1, x_2:T_2, \cdots, x_n:T_n)`$
ここで、$`x_1, x_2, \cdots, x_n`$ は変数名です。$`T_1, T_2, \cdots , T_n`$ は各変数の型になります。
仮引数リストを、名前（変数名）のリストと型のリストに分離するとは、次の2つのリストを作ることです。
- 名前のリスト $`(x_1, x_2, \cdots, x_n)`$
- 型のリスト $`(T_1, T_2, \cdots, T_n)`$
仮引数リストを名前のリストと型のリストに分離できれば、ラムダ抽象を次の形に書けます。
$`\quad \lambda\,(x_1, x_2, \cdots, x_n)::(T_1, T_2, \cdots, T_n).\msc{B}`$
さらに、$`\vec{x} := (x_1, x_2, \cdots, x_n)`$ 、$`\vec{T} := (T_1, T_2, \cdots, T_n)`$ と置くことにより、ラムダ抽象は次のように書けます。
$`\quad \lambda\,\vec{x} :: \vec{T}.\msc{B}`$
この形は理論的取り扱いに便利です。
簡単な例を見てみましょう。まず、通常の書き方：
$`\quad \lambda\,(x:\mbf{R}, y:\mbf{R}, n : \mbf{N}).(x^n + y^n :\mbf{R})`$
仮引数リストを次のように分離できます。
$`\quad \lambda\,(x, y, n):: (\mbf{R}, \mbf{R}, \mbf{N}).(x^n + y^n :\mbf{R})`$
仮引数リストを名前のリストと型のリストに分離するのは簡単に思えます。が、リストが依存リストだとそれほど簡単でもありません。
依存性がある場合
集合 $`X`$ の要素を $`n`$ 個並べたリスト（タプルと言っても同じ）の最後の項目〈成分〉を取り出す関数を $`\mrm{last}`$ としましょう。関数 $`\mrm{last}`$ は次のように定義できます。
$`\mrm{last} := \lambda\,(X : \mbf{U}, n :\mbf{N}, x : X^n).(x_n : X)`$
通常は暗黙に固定して考える $`X, n`$ も引数としています。
関数 $`\mrm{last}`$ の仮引数リストは：
$`\quad (X : \mbf{U}, n :\mbf{N}, x : X^n)`$
名前のリストは簡単です。
$`\quad (X , n, x)`$
では、型のリストは？
$`\quad (\mbf{U}, \mbf{N}, X^n)`$
これではダメです。3番目の型では、変数 $`X, n`$ が使われていますが、名前は取り去ってしまった（名前のリストに移してしまった）ので、$`X^n`$ が意味不明になってしまいます。
これを解決するには、仮引数リストから名前を削除する操作が必要です。名前の削除については、幾つかの過去記事があります。この記事で再度最初から説明しますが。
名前の削除
前節で出てきたリスト $`(X : \mbf{U}, n :\mbf{N}, x : X^n)`$ は名前（変数名）を持っています。このリストから名前を削除するとは、名前の代わりに番号を使うことです。名前と番号の対応は次のようです（当たり前の対応です）。
| 名前 | 番号 |
|---|---|
| $`X`$ | $`1`$ |
| $`n`$ | $`2`$ |
| $`x`$ | $`3`$ |
この対応表に基づいて、名前を番号に単純置き換えしてみましょう。
$`\quad (1 : \mbf{U}, 2 :\mbf{N}, 3 : 1^2)`$
$`1^2`$ はオカシイですね。番号を参照するときは、生の自然数値を使っては駄目です。名前ではなくて番号で識別する変数を $1, $2 などと書くスクリプト言語があります。これに倣って、番号を参照するときはドル記号を前置することにします。
$`\quad (1 : \mbf{U}, 2 :\mbf{N}, 3 : $1^{$2})`$
位置番号としての $`1, 2, 3`$ は無くても大丈夫なので取り除くと：
$`\quad (\mbf{U}, \mbf{N}, $1^{$2})`$
これが名前を削除した依存性を持つリストです。名前（変数名、ラベル）が無いということは、リネームの必要がなく、名前から自由になっている、ということです。名前から自由なので、どんな名前リストとでも組み合わせることができます。例えば：
$`\quad \lambda\,(A, k, v)::(\mbf{U}, \mbf{N}, $1^{$2}).(v_k : A)`$
名前リストと型リストを混ぜた形なら：
$`\quad \lambda\,(A : \mbf{U}, k: \mbf{N}, v : A^k).(v_k : A)`$
変数名リストとボディはリネームの作用（アルファ変換）を受けますが、型リストはリネームの作用は受けません。名前が無いので、そもそもリネームが起きないのです。
「宇宙のラムダ計算 2： 構文」に出てきた3つの仮引数リスト（以下）から、名前を持たない型リストを作ってみましょう。
- $`(x:\mbf{R}, y: \mbf{R}, p: \PR{ y \ne 0 \lor x \lt 0})`$
- $`(S: |\mbf{Semigrp}|, h: \PR{\mrm{HasUniqueUnit}(S)} )`$
- $`(U : \mbf{Universe}, X : U, Y : U, f: \mrm{Map}(X, Y), A : \mrm{Pow}(X), B : \mrm{Pow}(Y), c: \langle f(A) \subseteq B \rangle)`$
まず、位置番号は残した形：
- $`(1:\mbf{R}, 2: \mbf{R}, 3: \PR{ $2 \ne 0 \lor $1 \lt 0})`$
- $`(1: |\mbf{Semigrp}|, 2: \PR{\mrm{HasUniqueUnit}($1)} )`$
- $`(1 : \mbf{Universe}, 2 : $1, 3 : $1, 4: \mrm{Map}($2, $3), 5 : \mrm{Pow}($2), 6 : \mrm{Pow}($3), 7: \langle $4($5) \subseteq $6 \rangle)`$
位置番号を消してしまえば：
- $`(\mbf{R}, \mbf{R}, \PR{ $2 \ne 0 \lor $1 \lt 0})`$
- $`(|\mbf{Semigrp}|, \PR{\mrm{HasUniqueUnit}($1)} )`$
- $`(\mbf{Universe}, $1, $1, \mrm{Map}($2, $3), \mrm{Pow}($2),\mrm{Pow}($3), \langle $4($5) \subseteq $6 \rangle)`$
ご覧の通り、非常に可読性が悪くなっています。対策を考えましょう。
依存性を持つ型リスト
依存性を持つ（かも知れない）型リストは、ラムダ抽象の一部として使いたいだけでなくて、それ自身で独立した構文的対象物としても扱いたいのです。例えば、前節の2番目の型リストに $`\mrm{UnitalSemigrp}`$ という名前を付けて使いたいのです。
$`\mrm{UnitalSemigrp} := (|\mbf{Semigrp}|, \PR{\mrm{HasUniqueUnit}($1)} )`$
$`:=`$ の右は名前〈ラベル〉を持たない依存性を持つ型リストです。名前を持たないので非常に読みにくい。可読性を高めるために名前〈変数名 | ラベル〉を復活させると、その名前は大域的に公開されて（漏れ出て）しまいます。しかし、束縛変数にすれば名前を閉じ込めることができます。
変数名〈ラベル〉として出現する名前を束縛する束縛子〈binder〉を導入しましょう。その束縛子を $`\tau`$ とします。ギリシャ文字 $`\tau`$ に特に深い意味はありません（浅い意味は後述）。使い方は：
$`\mrm{UnitalSemigrp} := \tau(S, h).(S:|\mbf{Semigrp}|, h: \PR{\mrm{HasUniqueUnit}(S)} )`$
これで、$`S, h`$ は束縛変数となり、名前が外部に漏れることはなくなります。$`\tau`$ は $`\lambda`$ や $`\varepsilon`$ と同じく束縛子〈バインダー〉なので、束縛変数のリネーム（アルファ変換）は作用します。例えば、$`S\mapsto A, h \mapsto C`$ とリネームすれば：
$`\mrm{UnitalSemigrp} := \tau(A, C).(A:|\mbf{Semigrp}|, C: \PR{\mrm{HasUniqueUnit}(A)} )`$
丸括弧リストの代わりに波括弧形式（「宇宙のラムダ計算 2： 構文 // ボディリストの波括弧形式」参照）でもいいとします。
$`\mrm{UnitalSemigrp} := \tau(A, C).\{\\
\quad A:|\mbf{Semigrp}|\\
\quad C: \PR{\mrm{HasUniqueUnit}(A)} \\
\}
`$
この形を見るとわかるように、依存性を持つ（かも知れない）型リストは、型理論のコンテキスト、インスティチューション理論の指標の類似物です。類似物というより、コンテキスト／指標の別表現と言ったほうがいいかも知れません。
ところで、束縛子 $`\tau`$ の直後の束縛変数リストは、型リストに出現する名前〈ラベル〉と同じで冗長です。次の書き方を許すとします。
$`\mrm{UnitalSemigrp} := \tau(*).\{\\
\quad A:|\mbf{Semigrp}|\\
\quad C: \PR{\mrm{HasUniqueUnit}(A)} \\
\}
`$
依存性を持つ型リストを別に定義しておくと、ラムダ抽象を簡潔に書けます。
$`\mrm{unitAndCarrier} := \lambda\,(S, h)::\mrm{UnitalSemigrp}\; \{\\
\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)}\\
\}
`$
宇宙規模の関数 $`\mrm{unitAndCarrier}`$ は、仮引数名リスト〈formal parameter name list〉$`(S, h)`$ を持ちます。仮引数型リスト〈formal parameter type list〉は $`\mrm{UnitalSemigrp}`$ です。そして、依存性を持つ（かも知れない）型リスト $`\mrm{UnitalSemigrp}`$ は別に定義されています。
関数 $`\mrm{unitAndCarrier}`$ の戻り値型リスト〈return-value type list〉も事前に定義しておくことができます。
$`\mrm{PointedSet} := \tau(*).\{\\
\quad X : \mbf{U}\\
\quad a : X\\
\}
`$
すると、$`\mrm{unitAndCarrier}`$ は次のように書けます。
$`\mrm{unitAndCarrier} := \lambda\,(S, h)::\mrm{UnitalSemigrp}\; \{\\
\quad (X, \T{@private } u, a) :: \mrm{PointedSet} ::= (\\
\quad\quad \u{S}, \\
\quad\quad \varepsilon\langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle : \langle \exists! e\in \u{S}. \mrm{IsUnitOf(e, S)}\rangle, \\
\quad\quad \varepsilon!\, e\in \u{S}.\mrm{IsUnitOf(e, S)}\\
\quad)\\
\}
`$
この書き方のいい点は、関数 $`\mrm{unitAndCarrier}`$ が、単位元を持つ半群（$`\mrm{UnitalSemigrp}`$）を引数として受け取って、付点集合（$`\mrm{PointedSet}`$）を戻り値として返すことが一目瞭然なことです。プライベートな項目が入っていることで、少しややこしくなってはいますが。
タウ束縛子とタウ抽象
前節で導入した束縛子 $`\tau`$ をタウ束縛子〈tau binder〉と呼ぶことにします。
単独の裸の型リスト、例えば $`(S:|\mbf{Semigrp}|, h: \PR{\mrm{HasUniqueUnit}(S)} )`$ に出現する変数名〈ラベル名〉 $`S, h`$ は、自由変数であり大域的な名前だと考えましょう。タウ束縛子 $`\tau(S, h)`$ は、これらの名前をスコープ内に閉じ込める働きを持ちます。変数〈ラベル〉は束縛変数となるので、名前が外部に公開・漏出することはありません。アルファ変換（リネーム）で移りあえる型リストは同一視されます。
「アルファ変換で移りあえるなら同値」とした同値類を、直接的・一意的に表現する方法が名前を削除した型リストです。名前があるからアルファ変換による自由度が生まれますが、名前を奪えば自由度が殺されて一意的な表示となります。
依存性を持つ（かも知れない）型リストを、タウ束縛子で束縛した型を、ラムダ抽象に倣ってタウ抽象〈tau abstraction〉と呼ぶことにします。ラムダ抽象が、自由変数を持つラムダ式〈ラムダ項〉を束縛して作った関数を表す式〈項〉であるのと同様に、タウ抽象は、自由変数〈自由ラベル〉を持つ型リストを束縛して作った式〈項〉です。
タウ抽象は何を表す式〈項〉でしょうか？ これはある種の型だと思っていいでしょう。ラムダ抽象が定義する関数の域や余域の指定にタウ抽象が使えるのが状況証拠です。しかし、「型」という言葉は人により場合により違うので、安易に「タウ抽象は型を表す」と言うのはリスキーです。「型」概念は色々あるだろうが、タウ抽象が「型」を表すと考える立場もあり得る、ということです。
タウ（τ）について
$`\tau`$ は type の最初の文字 t に対応するギリシャ文字です。前節で述べたように、タウ抽象が表すモノを型〈type〉と呼ぶ立場もあり得るので $`\tau`$ としたのです。
しかし、依存型理論の「型」がタウ抽象と一致しているとは言えません。むしろ、依存型理論の「コンテキスト」がタウ抽象に近いでしょう。余計な混乱／余計な軋轢を避けたいので、正面から「型〈type〉」とは言わないで「タウ〈$`\tau`$〉」と呼ぶことにします。
ちょっと気になるのは、束縛子としての $`\tau`$ が別な意味で既に使われていることです。ブルバキが、ヒルベルトのイプシロン記号にタウを使っています。Wikipedia の Epsilon calculus ページの Bourbaki notation の節（Epsilon_calculus#Bourbaki_notation）に載っています。しかし、現時点ではイプシロンの代わりにタウを使うことはほとんどないので、まーいいとします。
まとめ
タウ抽象を（構文的対象物とみて）$`{\msc{A}}, {\msc{B}}`$ で表すと、タウ抽象を使ったラムダ抽象の形式は次のようになります。
- 丸括弧形式 $`\lambda\, {\msc{X}}::{\msc{A}}.( {\msc{F}} :: {\msc{B}} )`$
- 波括弧形式 $`\lambda\, {\msc{X}}::{\msc{A}}.\{{\msc{Y}}:: {\msc{B}} ::= {\msc{F}} \}`$
ここで：
- $`\msc{X}, \msc{Y}`$ は、変数名〈ラベル〉のリスト
- $`\msc{F}`$ は、式〈項〉のリスト
通常は、変数名のリストとタウ抽象（型のリスト）を混ぜてひとつのリストに書くほうが便利ですが、分離すると理論的取り扱いが楽になります。例えば、ラムダ抽象が表す関数のプロファイル（域・余域の仕様）は $`\msc{A} \to \msc{B}`$ だと即座に分かります。
タウ抽象で（ある種の）型を表し、ラムダ抽象で関数を表すことにすると、中学校で習う平方根や二次関数から、宇宙規模の巨大な構成〈construction〉まで、一律に記述できます。実際の記述例をまた次の機会に紹介するかも知れません。
