一昨日、ε記号、μ記号、ν記号の話をしました。「μ」は再帰的計算の2つの場面で出てきます（もっと他でも出てくるかも知れないけど）。再帰関数の定義で出てくるμ演算子は不動点方程式の最小解とは少し違いますが、似たような概念なので同じ「μ」を使っているのでしょう*1。そして、再帰関数の意味論を作るときに出てくるμは最小不動点演算子です。
まず、自然数上の再帰関数（計算可能関数）の定義を見てみます。p(n) が自然数に関する計算可能な述語だとします。つまり、p(0), p(1), p(2) などが真偽値（0と1でもかまいません）として計算できるとします。そのとき、p(k) = true となる最初の数kは次のように書けます。
- ε↓n.p(n)
ε↓は、「ε記号、μ記号、ν記号」で導入した記号で、ある条件を満たす要素のなかで最小のものです。普通の集合の記法を使って書けば次のようです。
- min({n∈N | p(n)})
Nの部分集合Aに対して、min(A)は、Aが空でない限り存在しますので、∃n.p(n) を仮定すれば、ε↓n.p(n) はwell-definedです。ε↓n.p(n) を μn.p(n) とも書きます。「ε記号、μ記号、ν記号」で説明したμ記号とは（似てるけど）少し違う意味なので注意してください。∃n.p(n) でないなら μn.p(n) は未定義です。実際の計算では、無限に走って止まらないプログラムになります。また、述語 λn.p(n) が止まらないなら、μn.p(n) も止まりません。
いま、p(n)は真偽値を値とする関数としましたが、pの値は自然数値で、p(k) = 1 である最小のkを求めるとしても同じです。p(k) = 0 とするときもあります。pを一般の計算可能関数fにして、f(k) = 0 である最小のkとすることもあります。いずれにしても、本質は変わりません。
pにn以外のパラメータ m1, ..., mN があると、m1, ..., mN|→μn.p(n, m1, ..., mN) はN変数の関数（未定義になる所もある）を定義します。これがだいたい、再帰的な部分関数の定義方法です。
さて、一般に部分関数 f:N→N を考えます。f, g がそのような部分関数のとき、部分関数のあいだの順序⊆を、f⊆g ⇔ Graph(f)⊆Graph(g) で定義します。Graph(f)は関数のグラフで、定義の右側に出てくる⊆は集合の包含関係です。
- Graph(f) = {(n, m)∈N×N | f(n) = m }
グラフが空集合になる空な部分関数を⊥とすると、⊥は順序⊆の最小元となります。この順序に最大元はありませんが、全域関数は極大元になります。
関数の再帰的な定義は、部分関数fを受け取って部分関数を作り出す手順 F(f) で記述できます。手順Fを、部分関数の空間上の高階関数と考えます。すると、再帰的な定義は、f = F(f) という不動点方程式で書けて、この不動点方程式の最小解が再帰的な定義の意味を与えます。つまり、手順Fで定義される関数は、μf.F(f) と書けるのです。ここでのμは、μf.F(f) = min({f∈部分関数 | f = F(f)} です。
高階関数Fの最小不動点 μf.F(f) は、⊥から始めて順次少しずつ求めることができます。
- f0 = ⊥
- f1 = F(f0)
- f2 = F(f1)
- f3 = F(f2)
- ...
与えられたkに対して、ある程度大きなNを取れば、fN(k) の値は確定します。このNは、実行時のスタックサイズだと思えばよいでしょう。サイズNのスタックを準備すれば、あるkに対する f(k) を計算できますが、任意のf(n)が計算できるとは限りません。Nをどんどん増やせば、fの全貌に近づける、というわけです。
再帰を不動点方程式の形に書くと、順序や極限の議論になりますが、うまいこと細工すると等式的（equational）な定式化もできるようです。等式的不動点理論は面白いな、と思っているんですが、あんまり理解してません。理解できたらネタにするかも（永久にネタにできない可能性あり）。
