与えられた関数達を素材にして新しい関数を作り出すこと -- これは基本中の基本ですね。でも、整理されてないかも知れません。整理しましょう。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\ot}{\leftarrow}
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Ent}{ \sqsubseteq }
\newcommand{\hinfer}{ \rightrightarrows }% horizontal meta rule (infer)
\newcommand{\vinfer}{ \downdownarrows }% vertical meta rule (infer)
`$
内容：
言葉と記号を整理しよう
関数の構成法〈作り方〉は基本的なことです。内容的には基本的でも、言葉や記号で混乱している可能性はあります。
「シーケントに関する不満と対策」より：
「オーバーロードやコンフリクトは日常茶飯事なのだから、そんなに気にすることないよ」と思う人もいるでしょう。僕もかつてはさほど気にしてませんでした。が、ここ10年くらいの経験で、「オーバーロード／コンフリクトを適切に処理する」ことは、とてもとてもとても難しいことだ、と痛感しました。
言葉と記号を適切に処理するのはとてもとてもとても難しいのです。難しい処理には次があります。
- 同義語・多義語を処理する。
- 名前・記号のオーバーロード／コンフリクトを処理する。
- 記号の乱用〈濫用〉を処理する。
- 省略と暗黙の了解事項を処理する〈補完する〉。
内容もさることながら、上記のような言葉と記号の処理にも注意しながら整理します。目指すところは、「呼び方・書き方・言い回しなんてどうでもいい」と達観することです。「どうでもいい」と達観するには、呼び方・書き方・言い回しに注意を向ける経験が必要です。
同義語
次のイコールは同義語の意味です。
- ソート ＝ 型
- オペレーション ＝ 関数
- 構成法 ＝ 構成子 ＝ コンストラクタ ＝ コンビネータ
微妙な差とか、用語運用の規約とかはありません。同義語なんだからいつでもどこでも*1置き換え可能〈interchangeable〉です。上の用語を組み合わせた「型コンストラクタ」と「ソートコンビネータ」も同義語です。意味は同じですが、趣味・好みによる優先度はあるかも知れません。例えば、「型コンビネータ」より「型コンストラクタ」を優先するとか。
「型」「関数」「コンビネータ」に「コンビネータ」を後置できます。「型コンビネータ」、「関数コンビネータ」、「コンビネータコンビネータ」と。「コンビネータコンビネータ」という繰り返しが気持ち悪いとか、語感〈感情 | 気分〉でゴチャゴチャ言うのはやめましょう。「コンビネータコンビネータ」を組み合わせる演算なら「コンビネータコンビネータコンビネータ」です。「コンストラクタコンビネータコンストラクタ」でも同義です。
「基本」「複合」という形容詞を系統的に使います。
| 基本 | 複合 | |
|---|---|---|
| 型 | 基本型 | 複合型 |
| 関数 | 基本関数 | 複合関数 |
| コンビネータ | 基本コンビネータ | 複合コンビネータ |
「基本」と「複合」は排他的ではありません。例えば、基本関数は複合関数です。複合してないのに複合はオカシイとか、語感〈感情 | 気分〉でゴチャゴチャ言うのはやめましょう。感情・気分は抑え込んでドライに「そういう約束」と割り切ります。
多義語
「ペア」と「リスト」は普通の意味で使います。ペアと長さ2のリストは同一視します。この記事では「リスト」ですが、「タプル」と言っても間違いではありません。
「デカルト・ペアリング」と「デカルト・タプリング」は、後述する関数コンビネータ〈関数構成法〉の名前です。「デカルト・ペアリング」と「デカルト・タプリング」の結果を「デカルト・ペア」と「デカルト・タプル」と呼びます。「デカルト・ペアリング」「デカルト・ペア」を単に「ペア」と呼ぶかも知れません。「デカルト・タプリング」「デカルト・タプル」を単に「タプル」と呼ぶかも知れません。
したがって、「ペア」「タプル」は曖昧多義語となります。関数のペアからペア（操作）によりペア（結果）が得られます。
基本型、基本・型コンストラクタ、基本関数
この記事は Sets-as-Types の立場なので、型〈ソート〉と集合は同じ意味です。次の型〈集合〉は基本型です。
- 空集合 ＝ ネバー型 ： 記号は $`\mbf{0}`$
- 特定された単元集合 ＝ ユニット型 ： 記号は $`\mbf{1}`$
他に、必要に応じて基本型は追加してもかまいません。例えば、自然数型 $`\mbf{N}`$ とか二値ブーリアン型 $`\mbf{B}`$ とか。
基本・型コンストラクタ（基本型・コンストラクタではない）には次があります*2。
- 直積コンストラクタ〈direct product constructor〉 ： 記号は $`\hyp \times \hyp`$
- 直和コンストラクタ〈direct sum constructor〉 ： 記号は $`\hyp + \hyp`$
- 関数集合コンストラクタ〈function-set constructor〉 ： 記号は $`[\hyp\to \hyp]`$ または $`[\hyp \ot \hyp]`$
最初に決めた〈合意した〉基本型から、基本・型コンストラクタを使って複合型を作れます。例えば：
- $`\mbf{1}`$ （基本型も複合型）
- $`\mbf{1} \times \mbf{1}`$
- $`\mbf{1} \times \mbf{N}`$ （$`\mbf{N}`$ が基本型に入っているとして）
- $`\mbf{1} + \mbf{N}`$
- $`[\mbf{N} \to \mbf{N}]`$
- $`[\mbf{N} \ot [\mbf{N} \to \mbf{N}] ]`$
- $`[\mbf{N} \ot [\mbf{N} \to \mbf{N}] ]\times [\mbf{N} \to \mbf{N}]`$
- $`[(\mbf{1} \times \mbf{N})\times \mbf{B} \to \mbf{B}]`$ （$`\mbf{B}`$ が基本型に入っているとして）
$`\bar{n} := \{1, \cdots, n\}`$ として、型〈集合〉のリストを次のように書きます。
$`\quad \vec{A} = (A_1, \cdots, A_n) = (A_i)_{i\in \bar{n}}`$
直積コンストラクタ／直和コンストラクタの拡張として、有限パイ型コンストラクタ〈finite pi type constructor〉と有限シグマ型コンストラクタ〈finite sigma type constructor〉を定義します。
$`\quad \prod \vec{A} = \prod (A_1, \cdots, A_n) = \prod (A_i)_{i\in \bar{n}}
= \prod_{i\in \bar{n}} A_i`$
$`\quad \sum \vec{A} = \sum (A_1, \cdots, A_n) = \sum (A_i)_{i\in \bar{n}}
= \sum_{i\in \bar{n}} A_i`$
有限とは限らない一般のパイ型／シグマ型を導入しても話は大差ないですが、今日は有限の場合に限ります。パイ型／シグマ型の書き方は人により色々です。色々な書き方を列挙するのも鬱陶しいのでやめますが、多少のバリエーションには対応できるようにしましょう。
有限パイ型と有限シグマ型に関して、次の基本関数を導入します。
- 射影〈projection〉 ： $`\pi^{\vec{A}}_k : \prod \vec{A} \to A_k`$
- 入射〈injection〉 ： $`\iota^{\vec{A}}_k : A_k \to \sum \vec{A}`$
$`\pi, \iota`$ に付いた上付きは適宜省略します。
関数を評価する関数も基本関数です。
- 右評価〈right evaluation〉 ： $`\mrm{rev}_{A, B} : [A \to B]\times A \to B`$
- 左評価〈left evaluation〉 ： $`\mrm{lev}_{A, B} : A \times [A \to B] \to B`$
基本・関数コンビネータ
以下の基本・関数コンビネータ〈基本・関数コンストラクタ〉を紹介します。
- 結合〈合成〉
- デカルトペアリング、デカルトタプリング
- デカルトコペアリング、デカルトコタプリング
- カリー化（左右）
- 反カリー化（左右）
- 射影の後結合
- 入射の前結合
- 評価の後結合
関数コンビネータも関数ですが、その仕様を次の形で書きます。
$`\text{仮引数リスト}`$
$`\vinfer \text{関数コンビネータの名前}`$
$`\text{結果の記述}`$
例えば：
$`(f:A \to B, g:B \to C)\\
\vinfer \text{Composition}\\
f;g : A\to C
`$
横書きにしたいなら：
$`\quad \text{Composition} : (f:A \to B, g:B \to C) \hinfer f;g : A\to C
`$
実際、関数コンビネータは次のような関数〈写像〉です。
$`\quad \text{Composition}_{A,B,C} : \mbf{Set}(A, B)\times \mbf{Set}(B, C) \to \mbf{Set}(A, C)
`$
以下の記述では、下付きの $`{A,B,C}`$ のような型パラメータは省略します。
基本・関数コンビネータの記述
結合〈合成〉：
$`(f:A \to B, g:B \to C)\\
\vinfer \text{Composition}\\
f;g : A\to C
`$
デカルトペアリング：
$`(f:X\to A, g:X \to B)\\
\vinfer \text{Cartesian Pairing}\\
\langle f, g\rangle : X \to A\times B
`$
デカルトタプリング：
$`(f_i:X\to A_i)_{i\in \bar{n}}\\
\vinfer \text{Cartesian Tupliing}\\
\langle f_i \rangle : X \to \prod_{i\in \bar{n}} A_i
`$
デカルトコペアリング：
$`(f:A\to Y, g:B\to Y)\\
\vinfer \text{Cartesian Copairing}\\
[f, g ] : (A+B) \to Y
`$
デカルトコタプリング：
$`(f:A_i \to Y)_{i\in \bar{n}}\\
\vinfer \text{Cartesian Cotupling}\\
[f_i]_{i\in \bar{n}} : (\sum_{i\in \bar{n}} A_i) \to Y
`$
カリー化（右のみ）：
$`(f: A\times B \to C)\\
\vinfer \text{Right Currying}\\
f^\cap : A \to [C\ot B]
`$
反カリー化（右のみ）
$`g : A \to [C\ot B]\\
\vinfer \text{Right Uncurrying}\\
g_\cup : A\times B \to C
`$
射影の後結合：
$`(f: X \to \prod_{i\in \bar{n}} A_i)\\
\vinfer \text{Projection Post-Composition}\\
f;\pi_k : X \to A_k
`$
入射の前結合：
$`(f: \sum_{i\in \bar{n}} A_i \to Y)\\
\vinfer \text{Injection Pre-Composition}\\
\iota_k ; f : A_k \to Y
`$
評価（右のみ）の後結合：
$`(g:X \to [B\ot A], a:X \to A) \\
\vinfer \text{Right Evaluation Post-Composition}\\
\langle g, a\rangle ; \mrm{rev} : X \to B
`$
カリー／ハワード／ランベック対応
カリー／ハワード／ランベック対応によれば次の対応があります。
| 型付きラムダ計算 | 論理 |
|---|---|
| 型項 | 論理式 |
| ラムダ項〈計算式〉 | 自然演繹の証明項 |
| 基本・関数コンビネータ | シーケント計算の推論規則 |
| 複合・関数コンビネータ | シーケント計算の証明項 |
論理側がわからなくても、型付きラムダ計算側で考えれば同じことです。定理の証明を書くことと、関数の計算式を書くことは同じことです。
前節の基本・関数コンビネータは、次のような推論規則に対応します。
| 型付きラムダ計算 | 論理 |
|---|---|
| 結合〈合成〉 | カット |
| デカルトペアリング、デカルトタプリング | 連言〈AND〉の（結論側への）導入 |
| デカルトコペアリング、デカルトコタプリング | 選言〈OR〉の（仮説側への）導入 |
| カリー化（左右） | 含意の（結論側への）導入 |
| 反カリー化（左右） | 含意の除去 |
| 射影の後結合 | 連言の除去 |
| 入射の前結合 | 選言の除去 |
| 評価の後結合 | モーダスポネンスの明示的使用による含意の除去 |
歴史的経緯による「呼び方・書き方・言い回しの違い」から、カリー／ハワード／ランベック対応が見えなくなっていることは残念なことです。「呼び方・書き方・言い回しなんてどうでもいい」と達観できれば、型付きラムダ計算と論理が（呼び方・書き方・言い回しは違えども）同じ構造であることが理解できるでしょう。
[追記]
論理と型理論に関するカリー／ハワード／ランベック対応のより詳しいことは、以下の過去記事を参照してください。
[/追記]
