再帰的定義とwhile文、for文

全域決定性関数に対するRecコンビネータのプロファイルは:

  g∈Total(X, Y)   h∈Total(N×Y×X, Y)
  --------------------------------------- RecX,Y
     f∈Total(N×X, Y)

ここで:

  • gは、初期値関数 g:X→Y
  • hは、再帰ステップを推進させる関数 h:N×Y×X→Y
  • fは、定義された関数 f:N×X→Y

再帰に対応するwhileプログラム(Whileコンビネータを使ったプログラム)の絵を次のように描いたが、間違っていた。

Minのほうの Min(p):N×X→Nは、

  • p:N×X→N
  • Min(p):X→N

の間違い。

Recの方は、カウンタ変数をデクリメントしてるが、これは良くない。インクリメントにすべき。デクリメントの位置もおかしいし、こりゃダメだ。

絵を描き直すのは面倒くさいので、コードで書くが、for文を使えば*1

// n, x は入力変数
nat n; // natは自然数型
X x;

// n, x は初期化される

// y, k は作業変数、k はインクリメントするカウンタ
Y y = g(x);
for (nat k = 0; k < n; k++) {
  y = h(k, y, x);
}
// ループを抜けた後の y が出力

for文は、while文で書けるから、RecはWhileで書ける。

ただし、2つの定義法で表現している関数が同じだというセマンティック側の証明が別途必要。

*1:for文はすごく便利だけど、これは、再帰の対応物として導入された繰り返し構文なんじゃないのかな。設計者の意図はそうじゃなかったにせよ、結果的にはそうなっている。