Think Stitch
PRINCIPIA  最近の更新


ループには再帰が隠れてる?

「再帰は難しい」とか「関数型は命令型より難しい」、「いや、むしろ命令型の方が関数型より難しい」などという話はよく聞きます。 加えてついさっき、「命令型と関数型でそんなに考え方が違うのか?」という趣旨の(と思われる)発言を目にしたので、ちょっと書きたくなりました。 いえ、議論に参戦するつもりはないです(うーん、あるのかな?こういう前置きはあまり意味がないし、たいていは反対だったりするし、自覚もないんですよね、困ったことに)。 ループと再帰のちょっとした関係についてです。

命令型のプログラムや文は、状態間の関係として表せるという話を以前にしました。 非決定性がない場合は事前状態から事後状態への関数として表せるということになります。 (計算プログラムの非決定性については機会があったら書いてみたいと思います。) 文 S を関数と同一視するとこんな感じです。s, s' はそれぞれ事前、事後の状態です。 (エスばかりで見にくくてすみません。)

s' = S(s)

例えば代入文の場合、といいたいのですけど、実は代入文はやっかいなので省略します。

if 文はちょっと簡単です。if B then S1 else S2 fi という文があるとすると、

s' = if B(s) then S1(s) else S2(s) fi

となります。こっちの if は式としての if です。 C 言語の b ? x : y みたいなものです。

さて、では while 文はどうなるでしょう。 while B do S od という文があるとします。 原理的にはこれも s' = L(s) と表せるはずです。 (ループ不変条件のところで「軌道を求める」といったのは、この関数 L のことです。)

もし最初に B が成り立っていなかったら、ループ本体は一度も実行されません。 この場合、状態は変わりません。 B が成り立っている場合は S が1回実行されて、またテストに戻ります。 テストに戻るということは、while 文に戻るということです。 したがって次の関係がいえるでしょう。

while B do S od
= if B then S; while B do S od else SKIP fi

これを、先ほどの if の規則を使って状態の関数に書き直すと、次のようになります。

L(s) = if B(s) then L(S(s)) else s fi

文の連接は関数の合成になります。 空文 SKIP は状態を変化させないので、事前の状態 s がそのまま返ります。

ご覧の通り、while 文に対応する関数 L(s) は再帰的な関係式を満たします。 これが L(s) の定義といってもいいくらいです。

この式を使って実際に L(s) の表式を求めることは、簡単な場合を除いて無理でしょう。 これを使うとループの性質、特に正当性を証明することができますけど、ループ不変条件を使うものよりも難しいでしょう。 これはエネルギー保存の法則を使って結果を出すのと、運動方程式を完全に解いてから結果を出すのとの違いです。後者の方がずっと難しいわけです。

ループを考えているときはステップでどうなるか、いつ抜けるか、と考えているわけで、結局は再帰や数学的帰納法と同じことを考えているのだろうと思います。 もしそうじゃなかったら・・・何かを見落としているのかもしれないかなあと思いました(結局主張しているんですね)。

この再帰方程式には解はあるのか、とか、いくつあるのか、とか、複数あるならどれがいいのか、とか、解があるためには S はどうでなければいけないか、などなど面白い話がたくさんあるそうですけど、 前回の反省を生かして、これでやめておきます。

2013/08/21
© 2013,2014,2015 PRINCIPIA Limited