この記事は、「Propositions-as-Types が説明困難な事情： n回目の整理」の続きです。
カリー／ハワード／ランベック対応は、型付きラムダ計算、論理、圏論のあいだの対応を与えます。細部までハッキリとした美しい対応があります。
にもかかわらず、用語法・記法がサッパリまったく対応しておらず、グッチャン・グッチャンにこんがらかりまくりで、せっかくの美しい対応を完膚なきまで台無しにしてしまうという、実に困った悲惨な状況なわけです。
前回記事「Propositions-as-Types が説明困難な事情： n回目の整理」に引き続き、悲惨な状況を、知識グラフ（用語・用法図を含む）により分析・整理します。
最近、知識グラフに変更や追加がありましたが、前回記事からの変更・追加についてはこの記事内で都度説明します。$`\newcommand{\T}[1]{ \text{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\In}{\text{ in } }
\newcommand{\BR}[1]{ \big[\!\big[ {#1} \big]\!\big] } % BRacket
`$
内容：
はじめに
前回記事「Propositions-as-Types が説明困難な事情： n回目の整理」と同様に、圏論には触れず、型付きラムダ計算と論理の対応を考えます。型付きラムダ計算の下部構造としての型理論は集合論的依存型理論です。単純型とは単なる集合で、依存性型（次の段落で説明）はファミリー〈集合族〉だと考えます。対応する論理は、直観主義高階論理ですが、古典一階述語論理だと考えてもさほど不都合はありません。
「依存型〈dependent type〉」という用語の曖昧性からの混乱を軽減するために、「依存性型〈type with dependency〉」という言葉を使います。依存性型はファミリーのことです（集合論ベースなので）。「依存型」は、シグマ型またはパイ型を表すことがあります。
曖昧語「依存型」を使うと、次の文は正しい事実を述べた文です。
- 依存型から依存型を作ると依存型だが、作った依存型は単純型のこともある。
より説明的に言えば：
- ファミリーである依存性型から、シグマ構成またはパイ構成でシグマ型またはパイ型を作ると、作った〈構成した〉パイ型またはシグマ型は単純型のこともある。
「依存和型」「依存積型」という言葉は使用禁止にします。ひどい混乱の原因となるので、僕は金輪際使いません！ 使わなくても何も困らないのでご安心ください。
型付きラムダ計算（下部構造は集合論的依存型理論）と論理の対応をハッキリさせるには、次の作業をする必要があります。
- 集合とファミリーの分類
- 型の分類
- 命題の分類
- 関数の分類
- 証明の分類
- 集合・ファミリー-型の対応をハッキリさせる。
- 型-命題の対応をハッキリさせる。
- 関数-証明の対応をハッキリさせる。
これらを遂行すれば、用語・記法の対応はだいたい出来るでしょう。しかし、語句レベルではなくて文レベルの対応が必要です。逐語訳ではホントにまったく全然ダメで、分野ごとの文化的違いまで考慮して意訳する必要があります。ときに、意訳は（逐語訳とは）まったく違う表現になることもあります。
記事タイトルの Proofs-as-Terms は、Propositions-as-Types と共にカリー／ハワード／ランベック対応のキャッチフレーズですが、Proof も Term も曖昧すぎて何を言いたいのか分かりません。我々の今の設定で強いて解読すれば、「証明項とラムダ項は対応するよ」、「証明項とラムダ項は同じようなものだ」ということです。これはそのとおりです。
関数
関数については比較的にお馴染みでしょう。以下はTypeScriptによる関数定義です。
function norm(x:number, y:number) : number { return Math.sqrt(x^2 + y^2) }
関数定義は関数そのものではありません。関数定義は、関数を定義するための構文的記号形式です。意味的世界に居る概念的事物としての関数を、関数定義と区別したいときは関数実体と呼ぶことにします。
上の関数定義で、波括弧〈ブレイス〉で囲まれた部分は（関数定義の）定義本体〈definition body | body of definition〉と呼びます。定義本体をどう書くかはプログラミング言語ごとに違うでしょうが、我々は現実のプログラミング言語ではなくてラムダ計算のラムダ項を使うことにします。つまり、定義本体はラムダ項になります。
'$`\lambda`$' ではじまるラムダ項はラムダ抽象〈関数抽象〉と呼びます。すべてのラムダ項がラムダ抽象なわけではありません。以下は、上の関数定義に対応する理論的ラムダ抽象です。
$`\quad \lambda(x: \mbf{R}, y:\mbf{R}).( \sqrt{x^2 + y^2})`$
過去記事「宇宙のラムダ計算 7： アノテーション、シンタックスシュガー // 型アノテーション」において、'$`\in`$' や '$`:`$' の3つの用法が区別できないで困ると言いました。3つの用法とは：
- 宣言のなかで使う '$`\in`$', '$`:`$'
- 命題のなかで使う '$`\in`$', '$`:`$'
- アノテーションのなかで使う '$`\in`$', '$`:`$'
過去記事では、宣言のなかでは '$`:`$' を使うと約束しました。この約束はそのまま使います。アノテーションは常に '$`\in`$' と約束したのですが、これは変更します。次のようにします。
| 用途 | 集合論的文脈 | 型理論的文脈 |
|---|---|---|
| 宣言 | $`:`$ | $`:`$ |
| アノテーション | $`\in`$ | $`::`$ |
| 命題 | $`\in`$ | $`::`$ |
型理論的文脈で '$`\in`$' が出てくるとかなり違和感があるからです。
先のラムダ抽象に、戻り値型の型アノテーションを付けると次のようになります。
$`\quad \lambda(x: \mbf{R}, y:\mbf{R}).( \sqrt{x^2 + y^2} \; :: \mbf{R}_{\ge 0})`$
このラムダ抽象（が表す関数実体）の戻り値型が $`\mbf{R}`$ か $`\mbf{R}_{\ge 0}`$ なのかは、関数 $`\sqrt{\hyp}`$ の戻り値型がどう宣言されているかによりますが、ここでは $`\mbf{R}_{\ge 0}`$（非負の実数全体）だとしておきましょう。
戻り値型の型アノテーションを省略しても型推論で計算できることが多いですが、ちゃんと書いておいたほうが分かりやすいです。
「関数」を分析する知識グラフ
「関数」という言葉の曖昧性と、関数に関わる諸概念の相互関係を図解した知識グラフは次のようになります。
$`\T{知識グラフ 1}\\
\quad \xymatrix{
{}
&\T{関数実体}
&{}
\\
{}
&\T{関数定義} \ar@{-->}[u]_{\T{解釈できる}}
&{}
\\
\T{【曖昧】関数} \ar@{|->}[uur]^1 \ar@{|->}[ur]^2 \ar@{|->}[r]^3
\ar@{|->}[dr]_4 \ar@{|->}[ddr]_5
&\T{【役割り名】定義本体} \ar[u]_{\T{part-of}} \ar[d]^{\T{should-be}}
&{}
\\
{}
&\T{ラムダ項}
&\T{ラムダ式} \ar@{=}[l]
\\
{}
&\T{ラムダ抽象} \ar@{^{(}->}[u]
&\T{関数抽象} \ar@{=}[l]
}`$
この図の説明をしていきましょう。
関数定義と関数実体の関係は次（同義の文達）のように言えます
- 関数定義は、関数実体と解釈できる。
- 関数定義は、関数実体を表す。
- 関数定義は、関数実体を意味する。
- 関数定義は、関数実体を定義する。
関数定義と関数実体の関係を詳しく調べるのはプログラム意味論の役目です。
$`\T{part-of}`$ と $`\T{should-be}`$ は次のように読み下せます。
- 定義本体は、関数定義のパート〈構成素 | 部品〉である。
- 定義本体は、ラムダ項〈ラムダ式〉であるべき。
$`\T{part-of}`$ と $`\T{should-be}`$ の組み合わせは、次のような射影関数（「知識グラフ 2： 直感的かつ正確な伝達のために // 射影関数」参照）を定義します。
$`\quad \hat{}\T{定義本体} : \BR{\T{関数定義}} \to \BR{\T{ラムダ項}} \In \mbf{Set}`$
ここで：
- $`\BR{\T{関数定義}}`$ は、「関数定義」と呼ばれるすべてのモノ（構文的対象物）からなる集合
- $`\BR{\T{ラムダ項}}`$ は、「ラムダ項」と呼ばれるすべてのモノ（構文的対象物）からなる集合
- $`\hat{}\T{定義本体}`$ は、関数定義から、「定義本体」と呼ばれるパート〈構成素〉を取り出す関数
パートを取り出す関数が射影関数です。
関数定義のプログラミング言語によらない記述は次の形（具体例）にします。
$`\quad \T{function }\mrm{norm}(x: \mbf{R}, y:\mbf{R}).(\\
\qquad \sqrt{x^2 + y^2} \; :: \mbf{R}_{\ge 0}\\
\quad)`$
ほとんどラムダ抽象と変わりませんが、関数定義とラムダ抽象は別な構文的対象物だとします。
上記関数定義は、関数に $`\mrm{norm}`$ という名前を付けてますが、名前を付けない関数定義（無名関数定義）も許します。
$`\quad \T{function }(x: \mbf{R}, y:\mbf{R}).(\\
\qquad \sqrt{x^2 + y^2} \; :: \mbf{R}_{\ge 0}\\
\quad)`$
こうなると、ほんとにラムダ抽象と区別がつかないし、実際同一視する流儀もあります。が、ここでは、名前を付けない関数定義とラムダ抽象は別な構文的対象物だとします。区別しておいたほうが（後で）便利なことがあります。
名前付き関数定義、無名関数定義（名前を付けない関数定義）、ラムダ抽象はいずれも関数実体を表します。次のような知識グラフが描けます。
$`\T{知識グラフ 2}\\
\quad \xymatrix{
{}
&\T{名前付き関数定義} \ar@{-->}[r]^{\T{解釈できる}}
&{名前付き関数実体} \ar@{-}[d]|{-}
\\
\T{関数定義} \ar@{|->}[ur] \ar@{|->}[r]
&\T{無名関数定義}\ar@{-->}[r]^{\T{解釈できる}}
&\T{関数実体}
\\
{}
&\T{ラムダ抽象} \ar@{-->}[ur]_{\T{解釈できる}}
&{}
}
`$
名前付き関数実体と関数実体を結ぶ線は、これらが互いに排他的であることを表します。名前付き関数実体は、名前という追加情報を持つので、単なる関数実体とは別物です。
関数定義（名前付き関数定義と無名関数定義）とラムダ抽象では、解釈の仕方（関数実体を表すやり方）が違います。この違いはラムダ計算の意味論では重要になります。が、今はこれ以上踏み込みません。
「証明」はどうか？
型付きラムダ計算の「関数」にほぼ対応する論理の用語は「証明」です。前節の“知識グラフ 1”と同じレイアウトで、証明に関わる諸概念の相互関係を図解してみます。
$`\T{知識グラフ 3}\\
\quad \xymatrix{
{}
&\T{?_1}
&{}
\\
{}
&\T{定理記述} \ar@{-->}[u]_{\T{解釈できる}}
&\T{定理} \ar@{=}[l]
\\
\T{【曖昧】証明} \ar@{|->}[uur]^1 \ar@{}[ur]^2 \ar@{|->}[r]^3
\ar@{|->}[dr]_4 \ar@{|->}[ddr]_5
&\T{【役割り名】証明} \ar[u]_{\T{part-of}} \ar[d]^{\T{should-be}}
&{}
\\
{}
&\T{証明項}
&{}
\\
{}
&\T{?_2} \ar@{^{(}->}[u]
&{}
}`$
番号 2 のところに矢印がないのはミスではありません。論理では、定理記述（単に定理とも言う）を証明と呼ぶことはないのです。
$`\T{part-of}`$ と $`\T{should-be}`$ から射影関数は定義できます。
$`\quad \hat{}\T{証明} : \BR{\T{定理記述}} \to \BR{\T{証明項}} \In \mbf{Set}`$
ここで：
- $`\BR{\T{定理記述}}`$ は、「定理記述」と呼ばれるすべてのモノ（構文的対象物）からなる集合
- $`\BR{\T{証明項}}`$ は、「証明項」と呼ばれるすべてのモノ（構文的対象物）からなる集合
- $`\hat{}\T{証明}`$ は、定理記述から、「証明」と呼ばれるパート〈構成素〉を取り出す関数
構成素役割り名〈パート役割り名〉としての「証明」は、（定理記述の）「証明パート」とかにしたほうが紛れがないでしょう。あるいは、（定理記述の）「記述本体」とか呼ぶのがよいでしょう。
名前が欠損している「?_1」は、構文的対象物である定理記述に対する意味的対象物、いわば証明実体です。通常の論理では、実体に注目しないので名前さえ付いてません。もう一箇所の欠損「?_2」はラムダ抽象の対応物です。これもきちんと取り上げないでお茶を濁しているので名前がありません。
このままでは、カリー／ハワード／ランベック対応を語れないので、欠損部分に名前を与えて“知識グラフ 3”を書き換えます。
$`\T{知識グラフ 4}\\
\quad \xymatrix{
{}
&\T{証拠}
&{}
\\
{}
&\T{定理記述} \ar@{-->}[u]_{\T{解釈できる}}
&\T{定理} \ar@{=}[l]
\\
\T{【曖昧】証明} \ar@{|->}[uur]^1 \ar@{}[ur]^2 \ar@{|->}[r]^3
\ar@{|->}[dr]_4 \ar@{|->}[ddr]_5
&\T{【役割り名】証明パート} \ar[u]_{\T{part-of}} \ar[d]^{\T{should-be}}
&\T{記述本体} \ar@{=}[l]
\\
{}
&\T{証明項}
&{}
\\
{}
&\T{証明抽象} \ar@{^{(}->}[u]
&{}
}`$
定理記述の実体は証拠〈witness〉、ラムダ抽象の論理版は証明抽象〈proof abstraction〉です。これが適切な名前かどうかは分かりませんが、とにかく名前がないと話にならないので、こう名付けます。
“知識グラフ 2”の論理版も描いておきます。
$`\T{知識グラフ 5}\\
\quad \xymatrix{
{}
&\T{名前付き定理記述} \ar@{-->}[r]^{\T{解釈できる}}
&{名前付き証拠} \ar@{-}[d]|{-}
\\
\T{定理記述} \ar@{|->}[ur] \ar@{|->}[r]
&\T{無名定理記述}\ar@{-->}[r]^{\T{解釈できる}}
&\T{証拠}
\\
{}
&\T{証明抽象} \ar@{-->}[ur]_{\T{解釈できる}}
&{}
}
`$
関数-証明の対応
ここまでの準備によって、やっと関数-証明の対応を描けるようになりました。以下のように対応します。
$`\T{知識グラフ 6}\\
\quad \xymatrix{
{}
&\T{関数実体}
&\T{証拠} \ar@{<->}[l]
&{}
\\
{}
&\T{関数定義} \ar@{-->}[u]^{\T{解釈できる}}
&\T{定理記述} \ar@{<->}[l] \ar@{-->}[u]_{\T{解釈できる}}
&\T{定理} \ar@{=}[l]
\\
\T{}
&\T{定義本体} \ar[u]^{\T{part-of}} \ar[d]_{\T{should-be} }
&\T{証明パート} \ar@{<->}[l] \ar[u]_{\T{part-of}} \ar[d]^{\T{should-be} }
&\T{記述本体} \ar@{=}[l]
\\
\T{ラムダ式} \ar@{=}[r]
&\T{ラムダ項}
&\T{証明項} \ar@{<->}[l]
&{}
\\
\T{関数抽象} \ar@{=}[r]
&\T{ラムダ抽象} \ar@{_{(}->}[u]
&{証明抽象} \ar@{<->}[l] \ar@{^{(}->}[u]
&{}
}`$
そしてそれから
「はじめに」に挙げた8個の作業項目のうち、8番目しか終わっていません。まだ作業は残っています。続きは近いタイミングで書くと思います。
