μ演算子
定義
関数$ fが以下のように定義されるとき、$ fは$ gから最小化で得られた、と言う $ f(\vec{x})=\mu' y[(g(\vec{x}, y)=0) \wedge(\forall z<y)(g(\vec{x}, z) \downarrow)]
この右辺のことを$ \mu y[g(\vec{x}, y)] と表す
補足
$ g(\vec{n})\downarrowは$ \vec{n}が$ gの定義域に入っていることを表す
$ f(\vec{x})の返り値は、$ yもしくは未定義になる
$ f(\vec{x})=yであるとは、下図のようになっていること
下表になるような自然数$ n_0,\cdots,n_{y-1} \ne 0が存在する
https://gyazo.com/41735a5bd95dae2cfc97299022a106c9
記号$ \mu'の意味
$ P(\vec{n},x)を$ n+1変数の述語とする
$ \mu' y[P(\vec{n}, y)] という式は
$ P(\vec{n},y)を満たす自然数$ yが存在するなら、その中で最小の値
存在しないなら、値は定義されない
『C言語による計算の理論』.icon p.92では、「$ \mu」として紹介されている