このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

曖昧表現の非曖昧化と解決

とある微分幾何の教科書のなかで使われている関手の表現が曖昧でタメ息が出ました。が、曖昧表現の使用はこの教科書に限らないわけで、いたる所で使われています。一般的な(特定の予備知識を仮定しない)事例で、関数/関手の曖昧表現とその解釈方法を説明します*1
\newcommand{\dand}{\mathop{\&}} % dependent and
\newcommand{\In}{\text{ in }} %
\newcommand{\hyp}{\text{-}} %
\newcommand{\id}{\mathrm{id}} %
\newcommand{\Iff}{\Leftrightarrow } %
\newcommand{\plus}{\mathrm{plus} } %
\newcommand{\C}{\mathrm{C} } %
\newcommand{\LA}{\langle } %
\newcommand{\RA}{\rangle } %
%
\require{color}
\newcommand{\Keyword}[1]{\textcolor{green}{#1} }%
\newcommand{\Where}{ \Keyword{\text{Where } } }%
\newcommand{\For}{\Keyword{ \text{For } } }%
\newcommand{\Define}{\Keyword{ \text{Define } } }%

この説明から、証明支援系などがエラボレーション(「多様体とバンドルのボキャブラリ (1) 基本記法 // 構造と台構造、エラボレーション」参照)機能を持たなくてはならない理由も分かると思います。

内容:

タプル/シーケンスと引数渡し

関数/関手への引数〈argument | 入力〉が複数あるときに、ここでは、タプル引数とシーケンス引数を区別します。タプルは直積の要素を表すとして、(a, b, c) のように、カンマ区切り・丸括弧囲みの構文にします。シーケンスは a\: b\: c のように、空白区切り・囲み記号なしにします。囲み記号なしにすると困るのが、空シーケンスの表現です。この記事では、省略可能な(むしろほとんどの場合省略する)シーケンス囲み記号として '\ulcorner' と ' \urcorner' があるとして、空シーケンスは \ulcorner \urcorner で表します。必要があれば、シーケンスを \ulcorner a\: b\: c \urcorner と囲み付きで書いてもいいです。

関数/関手は、プログラミング言語Haskellのように、カリー化されているとして、引数としてシーケンスを渡します。f\: a\: b\: c のようです。カリー化された関数/関手には部分適用(引数シーケンスの一部を渡すこと)が可能なので、次の表現も意味を持ちます。

  1.  f または  f\: \ulcorner\urcorner
  2. f \: a または f\: \ulcorner a\urcorner
  3. f \: a\: b または f\:\ulcorner a\: b\urcorner

a,\, b,\, c それぞれの型が A,\, B,\, C で、f\: a\: b\: c の型が X になるとき、f のプロファイル(引数型=域 と 戻り値型=余域 の仕様)を次の形で書きます。

\quad f: A\dand B\dand C \to X

アンド記号を使う理由は後で説明します。

多引数〈多変数 | 多項〉の関数/関手は、原則的にはカリー化した形で扱います。つまり、f が適用〈引数渡し〉された形は f(a, b, c) ではなく f\: a\: b\: c または f(a)(b)(c) と書きます。しかし、一緒に渡さないと意味がない引数達はタプルにまとめます。例えば、f\:(a, b)\:c = f( (a, b))(c) 。タプル引数を含む関数/関手のプロファイルは、例えば次のようになります。

\quad  f: (A\times B) \dand C \to X

恒等写像の例

プログラミングで多相関数(ここで定義はしませんが)と呼ばれるもので、おそらく一番簡単な事例は恒等写像 \id でしょう。'\id' とだけ書いても、どの集合の恒等写像か分からないので \id_A \text{ where } A\in |{\bf Set}| のように下付き添字で集合を明示します。今出てきた {\bf Set} は集合(と写像の)圏です。添字の情報から次が分かります。


\quad \id_A : A \to A \In {\bf Set}\\
\Iff\\
\quad \id_A \in {\bf Set}(A, A)

\id_Aa\in A を渡した形は \id_A (a) です。ここで、下付き添字を第一引数と考えて \id\: A\: a と書きます。これは、関数 \id にシーケンス A\: a = \ulcorner A\: a \urcorner を渡した形です。この形の \id のプロファイルは次のようになります。

\quad \id: |{\bf Set}| \dand (\coprod_{X\in |{\bf Set}|} X) \to (\coprod_{X\in |{\bf Set}|} X)

プロファイルがこんな形をしているので、\id は通常の関数とは違うものです。なので多相関数と呼ばれています。プロファイルがイカツイ形をしてますが、これでも引数〈入力〉と戻り値〈出力 | 結果〉の状況を十分には表現できていません。次のような補足説明が必要です。

  1. |{\bf Set}| は、すべての集合からなる“集合”(集合論では集合とは認めてないが)。
  2. \coprod_{X\in |{\bf Set}|} X は、すべての集合のすべての要素を寄せ集めた“集合”(集合論では集合とは認めてないが)。ただし、異なる集合(例えば {\bf Z}{\bf R})に属する要素は別物として区別できるとする。
  3. \id の第一引数は自由に選べる。
  4. \id の第ニ引数は、第一引数で指定した集合の要素でなくてはならない。第二引数は自由ではなくて、第一引数に依存した制約がある。
  5. \id の戻り値は、第一引数で指定した集合の要素になる。これも、第一引数に依存した制約。

プロファイルを次の形にする(依存型の意味でカリー化する)と、制約が少し分かりやすくなります。

\quad \id: |{\bf Set}| \to \coprod_{X\in |{\bf Set}|} Map(X, X)

次なら、もっと分かりやすいでしょう。

\quad \id \in \coprod_{X\in |{\bf Set}|} Map(X, Map(X, X))

依存型理論のシグマ型を使って書けば*2

\quad \id \in \Sigma\big( X\in |{\bf Set}| \mid  Map(X, Map(X, X) ) \big)

依存型理論に基づくプログラミング言語や証明支援系では、引数間の依存関係や引数と戻り値の依存関係を表現する手段がありますが、非形式的コミュニケーションでは、最初に出したような曖昧なプロファイルが想定されるだけで、依存関係は暗黙になります。この記事では、暗黙の依存関係による曖昧な表現が主題なので、\id のプロファイルは最初の形(下に再掲)で考えます。

\quad \id: |{\bf Set}| \dand (\coprod_{X\in |{\bf Set}|} X) \to (\coprod_{X\in |{\bf Set}|} X)

A \dand B はシーケンスの集合ですが、依存シーケンス〈dependent sequence〉を許すとします。\ulcorner a\: b\urcorner \in A\dand B のとき、a\in A は自由に選べますが、b\in B は第一成分に選んだ a に依存する(制約される)かも知れません。依存性・制約がまったくない場合は A\times B (通常の直積)と書きます。

 A \dand B \dand C のような場合は、後(右)に出現する成分が前(左)に出現する成分に依存する可能性を示しています。\dand を使った書き方だけでは、依存性の詳細は分かりません。別に依存性の明示的記述や依存性の推論ルールが必要です。が、実際には暗黙に済まされる場合が多いのです。

暗黙の依存性があるだけならまだしも、引数の省略が絡むと事情はさらに複雑化します。

引数の省略: 暗黙引数と引数デフォルト値

ハイフン、マイナス、アンダースコア(\hyp, -, \_)は、引数の出現位置・場所を指定するプレースホルダに使われます。この記事では、目立つという理由でマイナス記号をプレースホルダに使います*3。例えば、添字と丸括弧を使った \id の引数構文は \id_{-}(-) と書けます。カリー化した引数構文は \id\: - \: - となります。

通常の引数はマイナス記号で表すとして、省略可能引数は疑問符 '?' またはピリオド '.' で示します。疑問符とピリオドでは意味が違います。まずは疑問符から。\id\:?\: - と書いた場合は、第一引数が省略可能なことを意味します。第一引数が省略された場合、指定された他の引数から自動的に推論〈infer〉するとします。プログラミング言語/証明支援系では、推論で埋める省略可能引数は暗黙引数〈implicit argument〉と呼びます。

例えば、引数省略仕様が \id\:?\: - の状況で \id\: 3 と書いたら、第一引数は自動的に推論されて \id\ {\bf Z}\: 3 のように補完〈解決〉されます。ただし、3 から {\bf Z} が自動推論できるためには前提が必要です。リテラル〈定数記号〉 '3' が整数の集合 {\bf Z} の要素を表すと前もって確定しているとします。3\in {\bf R}3\in {\bf N} の可能性はない、ということです。プログラミング言語/証明支援系では、こういう前提を人為的に作り出していますが、一般的には(非形式的コミュニケーションでは)通用しないですね。

リテラルから型を推論するのは無理だとしても、文脈内で文字の型を約束している場合はあります。例えば、n \in {\bf Z},\, x\in {\bf R} とかです。この約束のもとで \id\: n \id\: {\bf Z}\: n と補完〈解決〉することはできます。

疑問符で表す暗黙引数は上述のような方法で補完〈解決〉しますが、ピリオドはデフォルト値〈default value〉が決まっている省略可能引数を表します。例えば、引数省略仕様が \id\:.\: - ならば、第一引数の省略時値〈デフォルト値〉はひとつに決まっています。例えば、デフォルト値が {\bf Z} だとすると、\id = \id\: {\bf Z} ということになります。\id\: 3 は問題なく解釈できますが  \id\: \frac{1}{2} はエラーになります。明示的指定はデフォルト値より優先されるので  \id\: {\bf R}\: \frac{1}{2} はOKです。

省略された引数を可能なら推論で補い、無理ならデフォルト値を使うことを ?. で表すとしましょう。引数省略仕様が \id\:?.\: - の状況で、第一引数デフォルト値が {\bf Z} なら次のような補完〈解決〉がされます。

  1. \id\: 3 \rightsquigarrow \id\: {\bf Z}\: 3
  2. \id\: 3.0 \rightsquigarrow \id\: {\bf R}\: 3.0
  3. \id \rightsquigarrow \id\: {\bf Z}
  4. \id\:{\bf Z}\: 3.0 \rightsquigarrow \text{Error}

型の持ち上げ〈リフト〉

足し算を a + b のように中置演算子記号プラスで書きます。これを関数記号〈関数名〉\plus を使って \plus\: a\: b と書くことにします。様々な足し算があるので、単に \plus\: a\: b では曖昧です。いま、足し算は可換モノイド〈commutative monoid〉の二項演算の意味で使うと約束したとします。そうすると、\plus の第一暗黙引数には可換モノイドが入ることになります。

可換モノイドの圏を {\bf CMon} として、関数 \plus のプロファイルは次のようです。

\quad \plus : |{\bf CMon}| \dand (\coprod_{X\in |{\bf CMon}|} U(X)) \dand (\coprod_{X\in |{\bf CMon}|} U(X)) \to (\coprod_{X\in |{\bf CMon}|} U(X))

これも補足説明が必要ですね。

  1. |{\bf CMon}| は、すべての可換モノイドからなる“集合”(集合論では集合とは認めてないが)。
  2. \coprod_{X\in |{\bf CMon}|} U(X) は、すべての可換モノイドの台集合〈underlying set〉のすべての要素を寄せ集めた“集合”(集合論では集合とは認めてないが)。ただし、異なる可換モノイドの台集合に属する要素は別物として区別できるとする。
  3. \plus の第一引数は自由に選べる。
  4. \plus の第ニ引数・第三引数は、第一引数で指定した可換モノイドの台集合の要素でなくてはならない。第二引数・第三引数は自由ではなくて、第一引数に依存した制約がある。
  5. \plus の戻り値は、第一引数で指定した可換モノイドの台集合の要素になる。これも、第一引数に依存した制約。

さらに、\plus の引数省略仕様は \plus\: ? \: - \: - だとします。第一引数は暗黙引数で、省略されれば第二引数から推論されます。

以上の話は、引数の個数が増えた以外は前節と同じことです。プログラミング言語/証明支援系、そして非形式的コミュニケーションでは、別なエラボレーション(「多様体とバンドルのボキャブラリ (1) 基本記法 // 構造と台構造、エラボレーション」参照)メカニズムがあります。「型クラス」「標準構造/標準インスタンス」などと呼ばれるメカニズムです。これは、\plus の第一引数に「可換モノイドではなくて(足し算を持たない)集合を入れれば良い」とする方式です。

集合として {\bf N}{\bf B}(ブール値の集合 {\bf B} = \{\mathrm{true}, \mathrm{false}\})を考えましょう。集合 {\bf N},\, {\bf B} に載っている可換モノイド構造はひとつには決まりません。例えば、{\bf N} 上では、足し算、掛け算、max(大きいほう)は可換モノイド演算です。しかし、我々の常識から言えば、{\bf N},\, {\bf B} 上の“足し算”は一意に決まります。その一意対応を次の関数としてハッキリと定義します。


Lift: {\bf Addable} = \{{\bf N}, {\bf B}\} \to |{\bf CMon}| \\
\:\\
\quad Lift({\bf N}) := ({\bf N}, +, 0) \in |{\bf CMon}|\\
\quad Lift({\bf B}) := ({\bf B}, \lor, \mathrm{false}) \in |{\bf CMon}|

ここ出てきた記号 '+' は、みんなが知っているアノ“自然数の足し算”です。'\land' もみんなが知っているアノ“論理オア”です。

今定義した Lift:{\bf Addable} \to |{\bf CMon}| を前提にして、例えば \plus \: \mathrm{false} を次のように補完〈解決〉します。

  1. 見た目上の第一引数が型ではないので、実際は第二引数だと判断する。
  2. 第二引数 \mathrm{false} の型が {\bf B} なので、暗黙の第一引数は {\bf B} だと判断。
  3. \plus\: {\bf B}\: \mathrm{false} の第一引数に Lift を適用して \plus\: ({\bf B}, \lor, \mathrm{false})\: \mathrm{false} と再解釈。
  4. 関数記号 \plus の意味は論理オア \lor と解釈。
  5. 実際の表現 (\lor) \: \mathrm{false}: {\bf B} \to {\bf B} が得られる。

最終的に得られた関数は、
(\lor) \: \mathrm{false} := \lambda\, x\in {\bf B}.( false \lor x \,\in {\bf B})
です。

上記の手順では、暗黙引数の推論だけではなくて、Lift も使っています。Lift は集合圏の対象〈集合型インスタンス〉を可換モノイド圏の対象〈可換モノイド型インスタンス〉へと“持ち上げ”ています。持ち上げ〈lift〉は忘却関手 U:{\bf CMon} \to {\bf Set} の部分的逆であり、次が成立しています。

\quad \forall X\in {\bf Addable}.\, U(Lift(X)) = X

持ち上げも多くの場合暗黙に使われます。持ち上げの逆方向である忘却はもっと暗黙に多用されます。忘却については「多様体とバンドルのボキャブラリ (1) 基本記法 // 構造と台構造、エラボレーション」を参照してください。

関手の例

{\bf Top}位相空間の圏、{\bf Rng} を(可換な)環の圏として、反変関手 \C:{\bf Top}^{op} \to {\bf Rng}\In {\bf CAT} を次のように定義します。


\For X\in |{\bf Top}|\\
\Define \C(X) := (X\, 上の実数値連続関数の環)\\
\:\\
\For \varphi:X \to Y \In {\bf Top}\\
\Define \C(\varphi):\C(Y) \to C(X) \In {\bf Rng} := \\
\quad \lambda\, g\in \C(Y).( g\circ \varphi \,\in\C(X) )

g\in \C(Y) はホントは g\in U(\C(Y)) だし、\C(f) が環の準同型写像になることを示す必要があるとか、不備はありますがだいたいはこれでいいでしょう。

次に第一引数を固定して、反変関手 \C(X, -):Open(X)^{op} \to {\bf Rng}\In {\bf CAT} を次のように定義します。以下で、 Open(X) は開集合の集合を包含順序により圏とみなしたものです。g|_U は関数の制限です。


\For U\in |Open(X)|\\
\Define \C(X, U) := (U\, 上の実数値連続関数の環)\\
\:\\
\For U \subseteq V \In Open(X)\\
\Define \C(X, (U \subseteq V)):\C(V) \to C(U) \In {\bf Rng} := \\
\quad \lambda\, g\in \C(V).( g|_U \,\in\C(U) )

これは、位相空間 X 上の連続関数環の前層(層にもなる)の定義なので、人為的な例ではありません。

\C(-)\C(-, -) の両方をまとめて、シーケンス引数の関手 \C\:- \:- を考えましょう。とりあえず対象パートだけを考えれば、そのプロファイルは次のようです。


\quad \C : |{\bf Top}| \dand \coprod_{X\in |{\bf Top}|} |Open(X)| \to |{\bf Rng}|

引数省略仕様は \C\: ? \: . とします。この引数省略仕様は分かりにくいので、節を改めて説明します。

関手における引数省略仕様

残念ながら \C\: ? \: . という引数省略仕様だけでは情報が不足しています。実際には次のような状況だとします。

  1. 暗黙引数である第一引数を推論するには、第二引数が指定されている必要がある。
  2. 第二引数のデフォルト値は、第一引数に依存する。

つまり、第一引数も第二引数も省略すると、エラボレーションのメカニズムは働きません。具体的な推論とデフォルト値は次のようです。

  1. 位相空間 X の開集合 U\subseteq X が第二引数に指定されたら、第一引数は X だと推論する。
  2. 第二引数のデフォルト値は、第一引数である位相空間 X の開集合としての X

これで、引数がひとつだけ指定されたときの解釈はできます。しかし、問題があります。“とある開集合 U”が引数に指定された \C \: U をどう解決すべきでしょう。もし、 U\subseteq X なら、暗黙引数の推論のルールから
\quad \C \: U \rightsquigarrow \C \: X \: U
と補完されます。しかし、開集合はそれ自体を位相空間だとみなすことができます。そうなるとデフォルト値のルールから
\quad \C \: U \rightsquigarrow \C \: U \: U
となります。

この場合は、環としてみた場合  \C \: X \: U  = \C \: U \: U \In {\bf Rng} なので、「どっちでもいい」ということになります。が、たまたま結果オーライなだけでスッキリしません。

この問題は、「親の位相空間 X を持つ開集合 U」と「それ自体で位相空間とみた開集合 U」の区別ができない限り解決できそうにありません。なにかしらの目印が必要なので、「親の位相空間 X を持つ開集合 U」を例えば \LA U \RA と書くことにします。すると:


\quad \C \: \LA U\RA \rightsquigarrow \C \: X \: \LA U \RA \\
\quad \C \: U \rightsquigarrow \C \: U \: \LA U \RA

\C のプロファイルの域〈入力〉の部分が  |{\bf Top}| \dand \coprod_{X\in |{\bf Top}|} |Open(X)| なので、U\in |{\bf Top}|\LA U \RA \in Open(X) かの(排他的)区別ができないと、本来の引数位置(第一引数か第二引数か)の判断もできません。

非曖昧化と解決

関数/関手に引数の一部が指定された曖昧表現があったとき、次の操作を非曖昧化〈disambiguation〉と呼びましょう。

  1. 指定された引数が本来何番目の位置のものかを判断する。
  2. 指定されてない引数が暗黙引数かデフォルト値を持つ引数か、それとも通常の引数(明示的指定を要求する)かを判断する。

非曖昧化により次のような書き換えができます。


\quad \id\: 3 \rightsquigarrow \id\: ? \: 3 \\
\quad \C\: X \rightsquigarrow \C\: X \: .

この後で、疑問符やピリオドの部分を推論値/デフォルト値で埋める作業は解決〈resolution〉と呼びましょう。解決には、先に述べた持ち上げ〈リフト〉の適用が必要かも知れません。

曖昧表現があっても、非曖昧化と解決の手順がハッキリしていれば、それは解消可能な曖昧さです。手順がハッキリしてないときはホントの曖昧さで、どうにもなりません。過度に暗黙の前提に頼ると、どうにもならない曖昧さが生じます -- 非形式的コミュニケーションでは気をつけるべき点です。

*1:微分幾何の事例は別記事にするかも知れません。

*2:実際の依存型理論では、少し違った記法を使うかも知れません。

*3:ハイフン、マイナス、アンダースコアは、無名ラムダ変数としても使うので、引数構文の記述に使うのはこの記事だけの話です。