0引数関数と定数は同じなのか？：圏的ラムダ計算の立場から考える

引数を持たない純関数と定数って、区別すべきでしょうか。f() と f を別物とみなすか、それとも f() と f は同じものだとしちゃうか、という問題です。（副作用の話とかは考えません。）

別にどうでもいい些細なことのようですが、この問題のせいで微妙な齟齬が生まれたりします。圏的ラムダ計算の立場からこの問題を考えてみます。以下のような、ある種の等式を示すのが目標です。

('a *) ≡ "a

シングルクォート（'）、ダブルクォート（"）、アスタリクス（*）、同値関係≡の意味はこの記事内で説明します。

内容：

定数定義と関数定義
ラムダ式の構文
射のクォーティング
射のフルカリー化
推論規則と意味規則
射を表す定数記号の意味
値定数と関数定数の導入
シングルクォート定数とダブルクォート定数の関係

定数定義と関数定義

整数値2に名前を付けるとして、JavaScriptで書いてみると：

// 方法1
const two = 2;

// 方法2
function two() {return 2}

two でも two() でも値はまったく変わりません。値が同じでも定数と関数を区別することが多いようですが、オブジェクトのメンバーの場合、プロパティ obj.two と引数なしメソッド obj.two() を区別しないケースや、互いに入れ替えることができるケースもありますね。

twoとtwo()を区別するかしないかは、趣味的な問題でどっちでもいいような気がします。ですが、「セマンティック駆動な圏的ラムダ計算とシーケント」で述べたように、デカルト閉圏ありきの立場だと、定数値記号と引数なし関数記号はデリケートな問題で、丁寧に見ていく必要があります。結果を言えば、定数値記号と引数なし関数記号は区別したほうが辻褄があいます。

ちょっと変な記号法ですが、値aに対する定数記号を"a、値aをリターンする0引数関数記号を'aと書くことにすると、const two で定義されたtwoは "2、function two で定義されたtwoは '2 となります。0引数関数呼び出しに使う () を * と書いてもいいとして、≡ は左右が互いに交換可能の意味とするなら：

('2 *) ≡ "2

という奇妙な等式が得られます。「関数としての2の、0引数による呼び出し」と「定数としての2」は「互いに交換可能」という意味ですから、まー当然なんですが。以下では、この等式の一般形を示します。

ラムダ式の構文

まず、ラムダ式の構文を定義しておきます。式（expression）と項（term）は特に区別しないで同義語として使います。

Varは変数（に使う記号）の集合とします。Typeは型定数の集合ですが、「セマンティック駆動な圏的ラムダ計算とシーケント」の方式を採用して、デカルト閉圏Cを準備して、Type = |C| とします。型定数の記号と圏Cの対象そのものを同一視します。Var, Typeをもとに、ラムダ式の構文をBNFで定義します。BNFの構文変数と対応する構文的要素の集合を同じ記号で表します。

Expr ::= Var | 'λ' Var ':' Type '.' Expr | Expr Expr | '(' Expr ')'

ここで、'λ', ':', '.', '(', ')' はリテラルトークンです。この構文でのラムダ式の例は、λx:A.x （x∈Var, A∈Type）とか、(g f)λy:B.λx:A.y （f, g, x, y∈Var, A, B∈Type）など。
上記の構文だと、束縛変数以外の変数は型なしですが、ラムダ式は必ず型コンテキストと共に使うので、自由変数も型コンテキストにより型付け（typing）できることになります。今回は、この単純な構文をベースにします。

さて、問題の定数記号ですが、Constという構文要素の集合があるとして、Constで構文を拡張します。拡張した構文は次のとおりです。

Expr ::= Var | Const | 'λ' Var ':' Type '.' Expr | Expr Expr | '(' Expr ')'

一例として、kとjがConstの要素だとして、(λy:C^B.λx:A. y k)(z j) （x, y, z∈Var, A, B, C∈Type）はラムダ式です。

なお、型宣言、型コンテキスト、型シーケント（型判断）の構文は以下のとおりです。εは空で、*は任意回の繰り返しを表します。

TypeDecl ::= Var ':' Type
TypeContext ::= ε | TypeDecl (',' TypeDecl)*
TypeSequent ::= TypeContext '⇒' Expr ':' Type

射のクォーティング

型定数記号と圏Cの対象は同一視されて、Type = |C| でした。それならば、同様に Const = Mor(C) = (Cの射の集合) と定義するのが漢らしいでしょう。ただし、後で混乱しそうなので、いちおう「ConstとMor(C)は同型だが別な集合」としておきます。f∈Mor(C)に対して、'f という記号を用意して、Q:Mor(C)→Const を、Q(f) = 'f で定義します。Qは同型（可逆、双射）なので、Q^-1('f) = f です。f ←→ 'f により、Mor(C) と Const は1：1に対応します。

f:A→B in C のとき 'f:B^A として定数記号の型付け（typing）をします。A^B は A^B の別表記です（「圏の指数のための中置演算子記号」参照）。'f:B^A という型宣言が仮定されるとは、(⇒ 'f:B^A) という形の型シーケントはすべて公理として追加しておくということです。例えば、(x:A ⇒ ('f x):B) は、追加した公理から次のように証明できます。

     *                     *
 ---------[追加公理]  -----------[公理 恒等]
 ⇒ 'f:B^A            x:A ⇒ x:A
 --------------------------------[適用]
       x:A ⇒ ('f x):B

Q:Mor(C)→Const をクォーティング、Q^-1:Const→Mor(C)→ をアンクォーティングと呼ぶことにします。クォーティング／アンクォーティングは、意味領域と構文領域のあいだの対応です。しかし、アンクォーティングQ^-1が意味写像（セマンティクス）を与えるかどうかは別問題です。クォートした定数の意味は何になるかは次節以降で順次説明します。

射のフルカリー化

Cはデカルト閉圏ですから、対象 A, B, C に対して、C(A×B, C) $\stackrel{\sim}{=}$ C(A, B^C) が成立します。この同型を与える写像はカリー化です。カリー化を Λ_A,B,C:C(A×B, C)→C(A, B^C) とします。

以下、IがCの終対象（直積のモノイド単位でもある）とします。一般的なカリー化 Λ_A,B,Cでは、Λ_A,B,C(f) の域としてAが残りますが、域がIになるまでカリー化することをフルカリー化と呼びましょう。具体的には、C(A, B) $\stackrel{\sim}{=}$ C(I×A, B) $\stackrel{\sim}{=}$ C(I, A^B) を利用します。

φ_A:A→I×A を直積の単位に関する標準的同型射とします。このφは、通常λ^-1と書かれるのですが、ここでギリシャ文字λを使うと混乱するので、φにしました。f∈C(A, B) に対して、C(I×A, B) の射を φ_A;f で与えて、さらに、Λ_I,A,B(φ_A;f) を作ると、それは C(I, A^B) に入ります。

以上の構成を図式的にまとめると：

  φ:I×A→A   f:A→B  
  ---------------------[射の結合]
     (φ;f):I×A→B
  ---------------------[カリー化]
    Λ(φ;f):I→A^B

この構成を行う写像を Λ^full_A,B:C(A, B)→C(I, B^A) とします。つまり、

Λ^full_A,B(f) := Λ_I,A,B(φ_A;f)

このΛ^fullがフルカリー化です。

fが決まればその域・余域A, Bも決まるので、Λ^full_A,B(f) の下付きA, Bは省略して Λ^full(f) とも書きます。Σ_A∈|C|(-) は、Cの対象すべてに渡って足し合わせる総直和だとして、C(I, |C|) = Σ_B∈|C|(C(I, B) と置きましょう。すると、Λ^full: Mor(C)→C(I, |C|) と書けます。Λ^fullは、圏Cのすべての射を、C(I, |C|) のなかに押し込める写像です。C(I, |C|) は、I→X （X∈|C|）の形の射の全体 {f∈Mor(C) | dom(f) = I } です。

推論規則と意味規則

推論規則は、一種の構文生成規則です。推論図を積み重ねた証明図と呼ばれる構文的図形を組み立てる方法を与え、証明図が構文的に正しいかどうかを判断する基準になります。意味規則は、型定数、型シーケント、推論図などの構文的要素に対して、意味的領域であるデカルト閉圏Cの対象、射、オペレーターなどを割り当てる規則です。

今の設定では、型定数記号の集合 = Const = |C| で、型定数と対象を同一しているので、型の意味は自明です（それ自体が意味）。型シーケント（型判断）の意味はCの射となります。そして、推論規則（推論図）の意味は、いくつかの射（オペランド）からひとつの射を作り出す圏的オペレータです。オペランドが0個のオペレーターは公理に対応します。オペランド1個（単項）、オペランド2個（二項）のオペランドが基本推論規則に対応し、それらを構文的に組合せて作った証明図がより複雑なオペレーターに対応します。

推論規則と意味規則がきちんと与えられれば、「証明図 |→ 圏C上のオペレーター」という意味写像が定義できます。別な言い方をすると、証明図は圏C上のオペレーターを記述するプログラムコードであり、そのプログラムの構文と意味を与えようとしているわけです

推論規則と意味規則の定義と整合性はチェックする必要があります。次のような点を確認します。

意図したシーケント／証明図はすべて構文的に生成できる。
余計な（意図せぬ）シーケント／証明図は生成されない。
任意に与えられた、“正しい”シーケント／証明図に、意味を確実に一意的に割り当れられる。

「セマンティック駆動な圏的ラムダ計算とシーケント」に、だいたいの推論規則と意味規則を書いていますが、隅々までチェックしているわけではありません。今回も、必要な推論規則／意味規則を引用するだけで、全体の詳細は述べません。

注意すべきは、型／シーケント／推論規則には意味を定義しますが、ラムダ式の意味は定義しないことです。ラムダ式はシーケントの構成部品でそれ自体では意味を持ちません。もし、「ラムダ式の意味」を定義したいなら、シーケントに埋め込んで定義する必要があります（実際にそうします）。

Cの射 f:A→B in C をクォートした定数記号 'f∈Const に対して、次の2つのシーケントを考えます。

⇒ 'f:B^A
x:A ⇒ ('f x):B

一番目は定数'fに関する追加公理になっていて、二番目は公理から証明可能な（証明図が描ける）シーケントです。

結論を言ってしまうと、2つのシーケントの意味は次のようになります。以下で、ブラケットは意味写像 [-]:シーケント→圏の射です。

[⇒ 'f:B^A] = (Λ^full_A,B(f):I→B^A in C)
[x:A ⇒ ('f x):B] = (f:A→B in C)

問題はこのような定義が整合性を持つか？です。それを次節で確認しましょう。

射を表す定数記号の意味

定数記号を入れる前の公理は、(x:A ⇒ x:A) という形のシーケントだけでした。変数記号xの選び方はどうでもよくて、アルファ変換で同値（アルファ同値）になるので、圏Cの対象と公理シーケントは事実上1：1対応していることになります。「対象←→恒等射←→公理シーケント」と三者が対応してます。

圏Cの射fに対して、(⇒ 'f:B^A) と (x:A ⇒ ('f x):B) のどちらを公理にしてもいいのですが、(⇒ 'f:B^A) を公理に選ぶことにしましょう。意味規則により、[⇒ 'f:B^A] = Λ^full(f) = Λ_I,A,A(φ_A:f) です。つまり、クォートされた記号 'f を Λ(φ;f) = Λ^full(f) として扱うことになります。

追加の公理シーケント (⇒ 'f:B^A) から (x:A ⇒ ('f x):B) を導ける根拠は次の推論です。

 ⇒ 'f:B^A            x:A ⇒ x:A
 --------------------------------[適用]
       x:A ⇒ ('f x):B

この推論に対応する意味計算（圏Cにおける圏的計算）は次のとおり。以下で、φ'はφ^-1のことです。

             *                  *
    ------------------[定数] -------[恒等]
    Λ(φ;f):I→B^A       id:A→A
    --------------------------------[直積]
    Λ(φ;f)×id:I×A→(B^A)×A         apply:(B^A)×A→B
    -------------------------------------------------------[射の結合]
      *                (Λ(φ;f)×id);apply:I×A→B
 -----------[左単位]  -------------------------------[ベータ変換]
 φ':A→I×A            φ;f:I×A→B
 ------------------------------------[射の結合]
              f:A→B

圏C上での計算では、基本的な射とオペレーターを幾つか組み合わせた計算になってますが、次のことは言えます。

シーケント (⇒ 'f:B^A) の意味が Λ(φ;f) ならば、シーケント (x:A ⇒ ('f x):B) の意味は f である。

これは、シーケント (⇒ 'f:B^A) への意味割り当てと推論規則「適用」の意味規則のもとで、[x:A ⇒ ('f x):B] = f という意味割り当てが妥当である（整合性を持つ、矛盾しない）ことを示しています。

(x:A ⇒ ('f x):B) を公理シーケントに選び、[x:A ⇒ ('f x):B] = f を公理の意味に採用しても問題はありません。次の証明図を意味規則に沿って圏C内でたどれば、(⇒ f') の意味（Cの射）が出てきます。

        *
  ------------------[追加の公理]
    x:A ⇒ ('f x):B
  ----------------------[カリー化]
     ⇒ λx:A.('f x):B^A
  ----------------------[イータ変換]
     ⇒ f':B^A

値定数と関数定数の導入

a:I→A in C としましょう。射aをクォートした記号 'a の型は、定義より A^I となります。シーケント (⇒ 'a:A^I) が公理です。この公理は [⇒ 'a:A^I] = (Λ^full(a):I→A^I) という意味を持ちます。AとA^IはC内で同型ですが、同じとは言えません。よって、aとΛ^full(a) も同じだとは断言できません。

射aそのものを再現したいときは、シーケント (x:I ⇒ ('a x):A) という変数を含むシーケントの意味を考える必要があります。別に我慢できないほどの不便だとは思いませんが、変数を添えないで直接aを再現できたほうが便利です。そこで、'a とは別な定数記号を導入します。

今まで、Constという単一の構文領域を使ってきましたが、ConstをValConstとFunConstに2つに分割します。ValConstとFunConstは互いに交わらない集合で、ValConst $\stackrel{\sim}{=}$ C(I, |C|)、FunConst $\stackrel{\sim}{=}$ Mor(C) だとします。

Q:Mor(C)→Const と書いたクォート写像を、改めて Q₁:Mor(C)→FunConst とします。つまり、FunConst = {'f | f∈Mor(C} となります。そして新しく、Q₂:C(I, |C|)→ValCons を Q₂(f) = "a と定義します。この結果 ValConst = {'a | a∈C(I, |C|)} となります。ラムダ式の構文は、Const ::= ValConst | FunConst を追加すれだけで、その他は変更なしです。

さて、型付け規則と意味規則です。ダブルクォートした "a の型は A だとします。つまり、(⇒ "a:A) というシーケントを公理に追加します。その意味は、[⇒ "a:A] = a とします。これで、ダブルクォート定数の型と意味が決まりました。

シングルクォート定数とダブルクォート定数の関係

MとNは同じ型Aを持つ閉じたラムダ式だとします。「閉じた」とは自由変数を持たないことです。自由変数を持たないので、コントキストが空であるシーケント (⇒ M:A), (⇒ N):A を作ることができます。2つのシーケントの意味が等しい [⇒ M:A] = [⇒ N:A] over C とき、M ≡ N と書くことにします。これは、「MとNがCにおいて同じモノを意味する」ということです。

"id_I を * と略記することにします。* は値定数（ValConstの要素）です。ダブルクォート定数の型付け規則と意味規則から [⇒ *:I] = [⇒ "id_I:I] = id_I となります。

代入（カット）の推論規則（「セマンティック駆動な圏的ラムダ計算とシーケント」を参照）から、次の図式は正しい証明図です。

  ⇒ *:I   u:I ⇒ ('a u):A
  -------------------------[代入]
     ⇒ ('a *):A

[⇒ *:I] = id_I, [u:I ⇒ ('a u):A] = a は分かっているので、代入規則の意味（射の結合）から、[⇒ ('a *):A] = a が出ます。

一方で、定義から [⇒ "a:A] = a だったので、[⇒ ('a *):A] = [⇒ "a:A] = a が成立します。このことから：

('a *) ≡ "a

これでやっと、冒頭に示した目標にたどり着きました。