再帰定義について演習問題

Uniquely satisfiableだが止まらない再帰定義 - yoriyukiの日記
Uniquely satisfiableだが止まらない再帰定義 - 続き - yoriyukiの日記

Uniquely satisfiableだが止まらない再帰定義を挙げよ、ってわけですが。
例えばこんなのはいかがでしょうか?

f(n)= if n=1 and f(0)!=0 then 1 else f(n+1)-1

f(0)が0でない場合、f(1)が1になります。すると、f(0)=f(1)-1=0となって矛盾。というわけで、f(0)=0が必須。その後はf(n)=f(n+1)-1すなわちf(n+1)=f(n)+1にしたがって決まっていきます。まあ、要するにf(0)が0でない場合に他の場所と組み合わせて矛盾を起こすことで定数を代入したのと同じ効果をあげているわけです。

自分なりに気づいて割と気に入っているのが、帰納的でない関数によってuniquely satisfiableな再帰定義。P(n, m)をそれ自体は帰納的だけれども、\{n : \exists m (P(n, m))\}帰納的でなくなるような述語とします*1。(えーと、この場合述語でいいんだよね(普段このあたりの用語をきちんと区別していない…)。P(n, 0)はどんなnに対しても成り立たないと仮定します。んで、

f(n, m)= if P(n, m) then m
          else if P(n, f(n, m+1)) then f(n, m+1)
          else 0

とします。f(n, m)を存在するならばP(n, k)を満たすような最小のk\geq m、そうでなければ0になるような関数とすると、この再帰定義はfによって満たされます。もしfが帰納的ならば、f(n, 0)も帰納的になって定義に反しますから、fは帰納的ではありません。
個人的には面白いなぁと。まあ、帰納的でない関数なんて関数じゃない、っていう考え方もあると思いますが。

いや、動機としてはつまり、一般たらいまわし関数に関して「uniquely satisfiableを示せたら停止もいえているんじゃないの?」とか思ったっていうだけでありまして。上を見てもらえばこれが全然成り立っていないのはよくわかるかと。

*1:追記: 例えばP(n,m)を「nは論理式のゲーデル数、mはその証明図のゲーデル数である」とすればよいです。かがみさん、ありがとうございました。