有界最小化
bounded minimalization
全域版の最小化
記号\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以外なら偽
gが原始帰納関数ならば、
f=\lambda m\vec{n}.(\mu x\lt m)[g(\vec{n},x)] も原始帰納関数
fは帰納的に定義できる
hsf :: N -> [N] -> N
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 :: N -> [N] -> Bool
g x n = undefined簡便化したものを考える
nが空配列とすると、存在を無視していいので
hsf :: 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以下の値に適用すると、それ自体を返す参考
『(理論)12 計算モデルの基礎理論』 p.53
『C言語による計算の理論』 p.74