有界最小化
bounded minimalization
『(理論)12 計算モデルの基礎理論』.icon p.53と『C言語による計算の理論』.icon p.74を参考にしているが、記法に長短があるので組み合わせたものをここにメモっているmrsekut.icon
記号$ \muの意味
$ P(\vec{n},x)を$ n+1変数の述語とする
$ (\mu x\lt m)[P(\vec{n},x)] という式は
$ P(\vec{n},x)=真となる自然数$ x(\lt m)が
存在する場合は、その中で最も小さいもの
存在しない場合は、$ m
つまり、この式は$ \exist x\lt m[P(\vec{n},x)] の真偽を見て、$ m以下の自然数を返す
$ Pを述語ではなく、原始帰納述語とする場合は、条件の部分を 「$ P(\vec{n},x)\land (x\lt m)を満たす自然数$ xが」とすると良い
有界最小化の定義
全域関数$ g:\mathbb{N}^{n+1}\to\{0,1\}から、
$ \lambda m\vec{n}.(\mu x\lt m)[g(\vec{n},x)] を構成する操作のことを有界最小化と言う
補足
$ gの出力は$ \{0,1\}でなくても、真偽が判定できるなら$ \mathbb{N}でもいい
ex. 0なら真、0以外なら偽
$ f=\lambda m\vec{n}.(\mu x\lt m)[g(\vec{n},x)] も原始帰納関数
$ fは帰納的に定義できる
code:hs
f 0 n = 0
f m n
| f (m-1) n < m-1 = f (m-1) n
| f (m-1) n == m-1 && g (m-1) n = m - 1
| f (m-1) n == m-1 && not (g (m-1) n) = m
where
g x n = undefined
簡便化したものを考える
nが空配列とすると、存在を無視していいので
code:hs
f :: Int -> Int
f 0 = 0
f m
| f (m-1) < m-1 = f (m-1)
| f (m-1) == m-1 && g (m-1) = m - 1
| f (m-1) == m-1 && not (g (m-1)) = m
where
g x = x >= 5 && odd x
gをoddとかにするとわかりやすい
fは「m以下で、「5以上で、奇数となる最小の自然数$ x」が存在するなら$ x、存在しないなら$ m」を返す
f 10なら、10以下で、「5以上の自然数の最小の奇数」なので5を返す
f 100やf 5でも同様
f 4やf (-10)のように、5以下の値に適用すると、それ自体を返す
参考