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

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

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

［参照用 記事］

再帰的関数定義と不動点

ここ何回か不動点の話を書きました。

解析学や幾何学でも不動点定理を使いますが、我々の興味は別なところにあります。再帰や帰納と呼ばれる手法や現象を不動点により説明したいのです。よく知られた例（人によっては「またそれか」）ですが、階乗関数〈factorial function〉の定義とセマンティクスについて紹介します。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\DNat}{\overline{{\bf N}} }
\newcommand{\DBool}{\overline{{\bf B}} }
\newcommand{\FN}{ {\bf FN} }
\newcommand{\In}{\text{ in } }
\newcommand{\On}{\text{ on } }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Condition}{\Keyword{Condition } }%
\newcommand{\Where}{\Keyword{Where } }%
\newcommand{\Define}{\Keyword{Define } }%
%\newcommand{\Let}{\Keyword{Let } }%
\newcommand{\Declare}{\Keyword{Declare } }%
`$

内容：

関数の再帰的定義

自然数 $`n`$ を変数とする階乗関数 $`\mrm{fact}`$ は次のように定義します。

  1. $`n = 0`$ のとき、$`\mrm{fact}(0) = 1`$
  2. その他のとき、$`\mrm{fact}(n) = n \times \mrm{fact}(n - 1)`$

これは十分に明確な定義だし、上の定義をプログラムコードとして書き写すこともできます。そして、そのプログラムはちゃんと動きます。

我々は、再帰的に定義された階乗関数が一意的に存在することを信じています。が、一般的な再帰的定義は、実在する関数をいつでもチャンと参照しているのでしょうか？ 参照対象〈デノテーション〉である関数を特に想定しないで適当に再帰的定義を書いたときでも、参照対象の関数は実在しているのでしょうか？

例えば次は、とある関数 $`f`$ の再帰的な定義です。

  1. $`n = 0, 1`$ のとき、$`f(0) = f(1) = 1`$
  2. その他のとき、
    1. $`n`$ が偶数のとき、$`f(n) = f(n/2)`$
    2. $`n`$ が奇数のとき、$`f(n) = f(3n + 1)`$

この $`f`$ はコラッツ予想に出てくる関数ですが、その挙動はよくわかってない謎の関数です。

比較的簡単な再帰的定義で謎の関数を生み出してしまうとなると、そもそも、再帰的な定義という手法がいつでも確実に関数を定義してるのか？ と疑問がわきます。

これらの疑問に答えるには、「再帰的に定義された関数」ではなくて、「再帰的に関数を定義する手法」のほうを定式化して議論の対象にする必要があります。

以下では、階乗関数を事例にしますが、「再帰的に階乗関数を定義する手法」のほうに注目してください。

部分関数と情報順序

「再帰的定義は関数を定義するのか？」という問〈とい〉を考えるなら、まず関数とは何かをハッキリさせる必要があります。今の文脈では、関数として“プログラムにより計算できる関数”を想定しています。プログラムが無限走行してしまったり、例外を投げてしまう現象を経験した方なら、プログラムにより計算できる関数が全域的〈total〉とは限らないことは身に沁みてご存知でしょう。

というわけで、部分関数の概念をサポートするために各集合〈データ型 | データ領域〉にボトム（記号 $`\bot`$ で表す）を追加します。$`f(x) = \bot`$ なら関数 $`f`$ の $`x`$ での値は未定義です。つまり、ボトム導入により部分関数（ときに未定義かも知れない関数）を表現できます。

通常値として自然数と真偽値を使うので、ボトムを追加したデータ領域を次のように定義します。

$`\quad \DNat := {\bf N} + \{\bot_{\bf N} \}`$
$`\quad \DBool := {\bf B} + \{\bot_{\bf B} \} = \{\mrm{True}, \mrm{False}, \bot_{\bf B} \}`$

以下、$`\bot_{\bf N}, \bot_{\bf B}`$ は両方とも単に $`\bot`$ と書きます。通常値を $`x, y`$ として情報順序〈information order〉（記号 $`\sqsubseteq`$ で表す）を次のように定義します。

  • $`\bot \sqsubset x`$
  • 異なる通常値どうしは比較できない。$`x \sqsubseteq y \Imp x = y`$

記号の乱用で、$`\DNat = (\DNat, \sqsubseteq)`$ のように書きます。つまり、順序集合としての $`\DNat`$ とその台集合〈underlying set〉を同じ記号で表します。

データ領域としては、基本的なデータ領域である $`\DNat, \DBool`$ から直積と指数〈関数集合〉により構成される順序集合を考えます（後で再論）。関数は、順序集合のあいだの単調関数を考えます。単調関数がボトムを保存することは要求しません。

単調関数 $`f,g :\DNat \to \DNat`$ のあだいに次の順序を入れます。

$`\quad f \sqsubseteq g :\Iff \forall x\in \DNat. f(x)\sqsubseteq g(x)
%`$

単調関数のあいだの順序も情報順序と呼び、同じ記号 $`\sqsubseteq`$ で表します。$`n \mapsto \bot`$ という定数関数は、情報順序に関して最小元になります。

[補足]

ボトムと共に、矛盾した値であるトップ（記号 $`\top`$ で表す）を入れることもあります。ボトムは情報の不足（なんだかワカラナイ）を表しますが、トップは情報の過剰（そんなはずナイダロ）を表します。情報が不足（$`\bot`$）、適切（通常値）、過剰（$`\top`$）により、情報順序が生じます。

自然数を表すはずの変数 $`x`$ に関する“情報の程度”を次のように考えられます。

  • $`x = \bot`$ ： $`x`$ に関して何の情報もない。なんだかワカラナイ。
  • $`x = 3`$ ： $`x`$ は $`3`$ であるとの情報がある。
  • $`x = 4`$ ： $`x`$ は $`4`$ であるとの情報がある。
  • $`x = \top`$ ： 例えば、$`x`$ は $`3`$ 、同時に $`x`$ は $`4`$ でもあるとの情報がある。そんなはずナイダロ、矛盾してる。

ボトムとトップの意味を逆にするときもあるし、情報順序の“解釈”には他の解釈（例：近似解釈）もあるので、これは一例です。特定の解釈にあまり拘らないほうがいいですよ。

真偽値のボトムとトップを追加した場合の情報順序関係を図示すると次のようです。

　　　Ｔ
　　／　＼
　／　　　＼
True　　　False
　＼　　　／
　　＼　／
　　　⊥

今回は、トップは不要なのでボトムだけを追加しました。

[/補足]

自然数上の関数の集合

前節で述べたように、部分関数もサポートするためにボトムを導入しました。注意すべきは、ボトムを導入することにより部分関数を考える必要がなくなっていることです。皆さんを戸惑わせるような物言いになりますが、「部分関数を考える必要があるが、部分関数を考える必要はない」のです。

このことをハッキリさせるために、次の記法を使います。

  • $`{\bf Ord}(\DNat, \DNat)`$ ： 順序集合としての $`\DNat`$ のあいだの、すべての単調関数からなる集合。
  • $`{\bf Ord}(\DNat, \DNat)_{\bot\text{-presv}}`$ ： 順序集合としての $`\DNat`$ のあいだの、ボトムを保存〈preserve〉するすべての単調関数からなる集合。
  • $`{\bf Partial}({\bf N}, {\bf N})`$ ： 集合 $`{\bf N}`$ のあいだの、すべての部分関数からなる集合。

次の事実は容易に示せます。

  • $`{\bf Ord}(\DNat, \DNat)_{\bot\text{-presv}} \subseteq {\bf Ord}(\DNat, \DNat)`$
  • $`{\bf Partial}({\bf N}, {\bf N}) \cong {\bf Ord}(\DNat, \DNat)_{\bot\text{-presv}}`$
  • $`{\bf Partial}({\bf N}, {\bf N}) \to {\bf Ord}(\DNat, \DNat)`$ という単射写像がある。

$`{\bf Partial}({\bf N}, {\bf N}) \to {\bf Ord}(\DNat, \DNat)_{\bot\text{-presv}}`$ という方向の同型写像を $`\widehat{-}`$ として、部分関数 $`f`$ の代わりにボトムを保つ単調関数 $`\widehat{f}`$ を考えることにします。$`\widehat{f}`$ は部分関数を表しますが、それ自体はもはや部分関数ではありません（全域関数です）。「部分関数を考える必要があるが、部分関数を考える必要はない」とは、この事情を言っています。

部分関数 $`f`$ のグラフを次のように定義します*1。（$`\mrm{def}(f)`$ は $`f`$ の定義域です。）

$`\quad \mrm{Graph}(f) := \{(n, m)\in {\bf N}^2 \mid n\in \mrm{def}(f) \land m = f(n) \}`$

すると次が成立します。

$`\quad \widehat{f} \sqsubseteq \widehat{g} \Iff \mrm{Graph}(f) \subseteq \mrm{Graph}(g)`$

これは、部分関数のあいだの包含関係（グラフの包含関係と同一視）が、単調関数のあいだの情報順序関係に移ることを意味します。

自然数の集合と自然数のあいだの部分関数は、順序集合と単調関数の世界に埋め込んで議論してもいいし、そのほうが便利です。自然数の集合以外に真偽値の集合も順序集合と単調関数の世界に持ち込みます。

  • $`{\bf N}, {\bf B}`$ の代わりに $`\DNat, \DBool`$ を考える。
  • $`{\bf N} \to {\bf N}, {\bf N} \to {\bf B}`$ などの部分関数の代わりに $`\DNat \to \DNat, \DNat \to \DBool`$ などの単調関数を考える。

以下では、「自然数のあいだの関数」や「自然数上の述語」は、実は $`\DNat \to \DNat, \DNat \to \DBool`$ などの単調関数のことです。順序集合と単調関数の世界に引っ越して考えます。

表示的意味論とボトム付きωCPOの圏

スコット〈Dana Scott〉に始まる表示的意味論〈denotational semantics〉の基本的方針は、次のようなものでしょう；

  • 計算可能な部分関数というちょっと扱いにくいものを、順序や位相のある世界に引っ越しさせて、単調関数や連続関数とみなして扱う。

引っ越し先の世界では、順序や位相に基づく伝統的議論ができるので、使える道具が増えることになります。

今回の引っ越し先の世界は、ボトム〈最小元〉付きωCPO（ω完備順序集合 | 可算完備順序集合）とω連続単調関数からなる世界です。この世界はひとつの圏とみなせて、$`\omega{\bf CPO}_\bot`$ と書きます。

  • 圏 $`\omega{\bf CPO}_\bot`$ の対象： ボトム〈最小元〉を持つωCPO*2
  • 圏 $`\omega{\bf CPO}_\bot`$ の射： ボトム〈最小元〉を持つωCPOのあいだのω連続な単調関数

圏 $`\omega{\bf CPO}_\bot`$ については、「ωCPO（可算完備順序集合）で考える形式言語理論」に説明があります。

圏 $`\omega{\bf CPO}_\bot`$ は次のような良い性質を持ちます。

  1. $`X, Y \in |\omega{\bf CPO}_\bot|`$ ならば、直積 $`X\times Y`$ は再びボトム付きωCPOになる（ $`X\times Y \in |\omega{\bf CPO}_\bot|`$ ）。
  2. $`X, Y \in |\omega{\bf CPO}_\bot|`$ ならば、ω連続単調関数の集合 $`[X, Y]`$ は再びボトム付きωCPOになる（ $`[X, Y] \in |\omega{\bf CPO}_\bot|`$ ）。

順序集合 $`\DNat, \DBool`$ はボトム付きですが、ωCPOになることもすぐ確認できます。したがって、

$`\quad \DNat, \DBool\in |\omega{\bf CPO}_\bot|`$

圏 $`\omega{\bf CPO}_\bot`$ の性質により次が言えます。

  1. $`\DNat \times \DNat \in |\omega{\bf CPO}_\bot|`$
  2. $`\DBool \times \DBool \in |\omega{\bf CPO}_\bot|`$
  3. $`[\DNat, \DNat] \in |\omega{\bf CPO}_\bot|`$
  4. $`[\DNat, \DBool] \in |\omega{\bf CPO}_\bot|`$
  5. $`[\DNat\times \DNat, \DBool] \in |\omega{\bf CPO}_\bot|`$
  6. $`[\DBool\times \DBool, \DBool] \in |\omega{\bf CPO}_\bot|`$
  7. ‥‥

特に我々が注目するのは $`[\DNat, \DNat]`$ なので名前〈固有名〉を付けておきます。FN は "Functions on the set of Natural numbers" のつもりです。

$`\quad \FN := [\DNat, \DNat] = \{ f \mid f : \DNat \to \DNat \In \omega{\bf CPO}_\bot \}`$

階乗関数をどう定義するか

今回の例題である階乗関数は、$`{\bf FN} = [\DNat, \DNat]`$ の要素として定義します。より具体的に言えば、階乗関数を、$`{\bf FN}`$ 上の不動点方程式の最小解として特定します。

「不動点方程式／不動点不等式と不動点オペレーター」で使った書き方を使うと、階乗関数を定義する不動点方程式は次のようです。

$`\Condition f = \mrm{FactDef}(f) \On {\bf FN}\\
\Where \mrm{FactDef} : {\bf FN} \to {\bf FN} \In \omega{\bf CPO}_\bot
%`$

ここで、$`\mrm{FactDef}`$ は階乗関数を定義するための関数です。「タルスキーの最小プレ不動点定理（訂正）」で導入した $`\mrm{FP}(-), \mrm{least}(-)`$ を使って階乗関数書くと：

$`\quad \mrm{fact} = \mrm{least}(\mrm{FP}(\mrm{FactDef}))`$

関数 $`\mrm{FactDef} : {\bf FN} \to {\bf FN}`$ がω連続単調関数ならば、ナスター／タルスキーの不動点定理から、その最小不動点の存在が保証されます。したがって、
$`\quad`$ 関数 $`\mrm{FactDef}`$ の最小不動点としての $`\mrm{fact}`$
の一意的存在が言えます。

つまり、「階乗関数は確かに存在する」と主張できます。

階乗関数定義関数

階乗関数を定義する不動点方程式を書き下すと次のようです。

$`\quad f = \text{if } n = 0 \text{ then } 1 \text{ else } n \times f(n - 1)`$

これを、次の形だと思って、$`\mrm{FactDef}`$ の定義をちゃんと書きます。

$`\quad f = \mrm{FactDef}(f)`$

作業はすべて圏 $`\omega{\bf CPO}_\bot`$ 内で行います。

最初に、if-then-else という制御構造を表す関数を $`\omega{\bf CPO}_\bot`$ 内に定義します。キーワード $`\Keyword{Declare}`$ で関数・値の宣言、キーワード $`\Keyword{Define}`$ で関数・値の定義を示します。

$`\For X, Y \in |\omega{\bf CPO}_\bot|\\
\Declare \mrm{ifThenElse}_{X, Y} : [X, \DBool] \times [X, Y] \times [X, Y] \to [X, Y] \In \omega{\bf CPO}_\bot \\
\For p \in [X, \DBool],\, f, g \in [X, Y] \\
\Declare \mrm{ifThenElse}_{X, Y}(p, f, g) \in [X, Y]\\
\For x \in X\\
\Define \mrm{ifThenElse}_{X, Y}(p, f, g)(x) \in Y := \\
\quad \text{case }p(x)\text{ of }\\
\qquad \mrm{True} \Imp f(x)\\
\qquad \mrm{False} \Imp g(x)\\
\qquad \bot \Imp \bot\\
\quad \text{end}
%`$

この関数がω連続単調関数であることは別途証明が必要ですが割愛します。$`\mrm{ifThenElse}_{\DNat, \DNat}`$ を単に $`\mrm{ifThenElse}`$ と書くことにします。

次に、if文の条件内の n = 0 に相当する述語を定義します。

$`\Declare \mrm{isZero} : \DNat \to \DBool \In \omega{\bf CPO}_\bot \\
\For x \in \DNat\\
\Define \mrm{isZero}(x) \in \DBool := \\
\quad \text{case }x\text{ of }\\
\qquad 0 \Imp \mrm{True}\\
\qquad \bot \Imp \bot\\
\qquad \text{otherwise } \Imp \mrm{False}\\
\quad \text{end}
`$

この述語がω連続単調関数であることは別途証明が必要ですが割愛します。

if文のthen部にある定数 1 に相当する関数を定義します。

$`\Declare \mrm{forceConstOne} : \DNat \to \DNat \In \omega{\bf CPO}_\bot \\
\For x \in \DNat\\
\Define \mrm{forceConstOne}(x) \in \DNat := 1
`$

force が付いているのは、引数が $`\bot`$ でも正常値である $`1`$ を返しているからです。この関数もω連続単調関数ですが、ボトムを保存しません。

自然数から 1 を引く関数〈predecessor〉を定義します。

$`\Declare \mrm{pred} : \DNat \to \DNat \In \omega{\bf CPO}_\bot \\
\For x \in \DNat\\
\Define \mrm{pred}(x) \in \DNat := \\
\quad \text{case }x\text{ of }\\
\qquad 0 \Imp \bot\\
\qquad \text{otherwise } \Imp x - 1\\
\quad \text{end}
`$

次は自然数の掛け算です。

$`\Declare \mrm{times} : \DNat\times \DNat \to \DNat \In \omega{\bf CPO}_\bot \\
\For x, y \in \DNat\\
\Define \mrm{times}(x, y) \in \DNat := \\
\quad \text{case }x, y\text{ of }\\
\qquad \bot, y \Imp \bot\\
\qquad x, \bot \Imp \bot\\
\qquad \text{otherwise } \Imp x \times y\\
\quad \text{end}
`$

素材の準備ができたので、目的の関数 $`\mrm{FactDef}`$ を組み立てます。$`- \circ - `$ は反図式順の関数結合〈関数合成〉、$`\langle - , - \rangle`$ は関数のデカルト・ペアリングです。

$`\Declare \mrm{FactDef} : {\bf FN} \to {\bf FN} \in \omega{\bf CPO}_\bot \\
\For f \in {\bf FN} = [\DNat, \DNat]\\
\Define \mrm{FactDef}(f) := \\
\quad \mrm{ifThenElse}(\mrm{isZero}, \mrm{forceConstOne}, \mrm{times}\circ \langle\mrm{id}_{\DNat}, f\circ \mrm{pred}\rangle)
%`$

[補足]

関数結合〈関数合成〉やデカルト・ペアリングも、圏 $`\omega{\bf CPO}_\bot`$ 内の関数として定義したいと思う人がいるかも知れません。やろうと思えばできます。

関数結合する操作を圏 $`\omega{\bf CPO}_\bot`$ 内の関数とみなしたものを $`\mrm{comp}`$ とすれば、次のように定義します。

$`\For X, Y, Z \in |\omega{\bf CPO}_\bot|\\
\Declare \mrm{comp}_{X,Y,Z} : [X, Y]\times [Y, Z] \to [X, Z] \In \omega{\bf CPO}_\bot \\
\For f \in [X, Y], g \in [Y, Z]\\
\Declare \mrm{comp}_{X,Y,Z}(f, g) \in [X, Z]\\
\For x \in X\\
\Define \mrm{comp}_{X,Y,Z}(f, g)(x) \in Z := g(f(x))
`$

通常は下付きの $`{_{X,Y,Z}}`$ は省略して単に $`\mrm{comp}`$ と書きます。これもω連続単調関数です。

[/補足]

圏論的意味論

階乗関数を定義する関数 $`\mrm{FactDef}`$ が思ったより複雑だったかも知れません。また、$`\mrm{FactDef}`$ がω連続単調関数であることの確認は省略しています。が、$`\mrm{FactDef}`$ がω完備順序集合 $`{\bf FN}`$ 上のω連続単調自己関数であると前提すれば、唯一の最小不動点として階乗関数は特定できます。

$`\mrm{FactDef}`$ に限らず、ω連続単調自己関数 $`F:{\bf FN} \to {\bf FN}`$ があれば、その最小不動点としての関数が一意に決まります。例えば、$`\mrm{id}_{\bf FN} : {\bf FN} \to {\bf FN}`$ はω連続単調自己関数なので最小不動点を持ちます。それは次の関数です。

$`\quad \lambda\, x\in \DNat. \bot\;:\DNat \to \DNat \In \omega{\bf CPO}_\bot`$

部分関数として考えるとまったく未定義な関数です。しかし、部分関数も関数の仲間に入れているので立派な(?)関数です（もちろん、実用上は全域関数を定義するような定義関数のクラスを知りたいですが）。

関数 $`\mrm{FactDef} : {\bf FN} \to {\bf FN}`$ は、関数を受け取って関数を返す高階関数です。そのことを強調して、汎関数とか作用素と呼ぶこともあります。関数を定義するための汎関数／作用素なので、定義汎関数／定義作用素〈defining {functional | operator}〉です。最初の節で述べた「再帰的に関数を定義する手法」の実体〈デノテーション〉は、ω連続単調な定義汎関数だったわけです。

最初に引っ越し作業をしたので、関数や定義汎関数が棲んでいる場所は圏 $`\omega{\bf CPO}_\bot`$ です。この圏のなかには、階乗関数とその定義汎関数以外に有用なヤツが棲んでいそうです。調べる価値がありそう -- 実際、$`\omega{\bf CPO}_\bot`$ とその派生物は圏論的意味論〈categorical semantics〉の重要な対象物です。

*1:部分関数の定義によっては、グラフは部分関数そのものです。

*2:ωCPOの定義に「ボトム付き」を含めることもあります。