関数プログラミングの帰納的関数(7)

次に終了する について調べてみます。 を表す用語があるかと思ったのですが、ChatGPT では出てこないようです。

F# の再帰的呼び出しで無限に繰り返される関数を とします(再帰的呼び出し以外は有限回で終わるとする)。

関数の列 を

• は None を返す
• を の定義の の呼び出しを で置き換えたもの

とします(None を含む式の値は None とします)。

の値が None ではない が存在するような は何ですか

と入力すると以下の結果となりました。

関数 が無限に再帰を繰り返すという仮定のもとで、関数列 の性質を考えます。

1. 定義の整理

• 
• は の定義の の呼び出しを に置き換えたもの

つまり、 の定義における再帰的な部分は、 によって有限の回数しか呼び出されません。
そのため、 は深さ までの再帰しか展開せず、それ以上は None を返します。

2. の値が None でない場合

となるには、 の計算が None に到達せずに終了する必要があります。
つまり、 の定義において再帰が発生しない場合、または再帰が深さ 以内で止まる場合、 は None ではない値を持つ可能性があります。

したがって、ある に対して が None でない は、

• の定義において、 の計算が有限回のステップで終了するような である。

これは、 が無限再帰に入らずに結果を返すような です。

3. 具体的な例

たとえば、F# で次のような関数を考えます：

let rec f x =
    if x = 0 then 0
    else f (x - 1)

この場合、 は

• は None を返す
• は `if x = 0 then 0 else None` となる
• は `if x = 0 then 0 else if x - 1 = 0 then 0 else None` となる

よって、 または ならば となる が存在します。

4. 結論

一般に、 の定義において「ある入力 に対して、有限回のステップで計算が終わる」場合、そのような は存在する に対して となります。
逆に、 が常に無限ループに陥るような に対しては、すべての で になります。

復刊 帰納的関数

数学基礎論　増補版

数学基礎論 (ちくま学芸文庫)

計算理論の基礎［原著第3版］ 1.オートマトンと言語

計算理論の基礎［原著第3版］ 2.計算可能性の理論

計算理論の基礎［原著第3版］ 3.複雑さの理論