Think Stitch
PRINCIPIA  最近の更新


ループ不変条件

惑星という言葉にはなぜ「惑」という字が使われているのか、ということについては中学生のときに理科で習いました。 プトレマイオスの頃は地球が宇宙の中心だと考えられていたと。 でもそうすると惑星がなんで行きつ戻りつ妙な動きをするのわからない。 しかたがないので周転円とかややこしいしくみを考えた。しかしうまくいかない。 そこにコペルニクスが現れて、地動説を唱えた。いやいや地球が動いてるんでしょと。 そうだとすると惑星が行きつ戻りつするのは地球が動いているからであって、惑星それ自体は太陽の周りを単純に回っているに過ぎないと。 その後ガリレオとかケプラー(とそのお師匠さんのティコ・ブラーエさん)がより精密な観測と計算をして、軌道は厳密には円ではなくて楕円だとか、面積速度の法則だとかを見つけます。

これらはみな、「運動とは何か」ということを理解するための探究だったわけです。 この問題に最終的に決着をつけたのはニュートンでした。 要するに運動を理解するとはどういうことかというと、運動を記述することだと。 運動を記述するとは、物体の位置を時間の関数として表すことです。 理論的にはこれが手に入れば、あとは付随するいろいろなものも求められます。 (解析的に求められないとか、まあいろいろありますけど、原理的には、ということです。) 次元を1つ増やして、時間の関数として表すことによってはじめて静的な紙の上に動きを表現できたわけです。 次元を増やしているということは、外から俯瞰しているということです。

コンピュータも「動く」といいますけれども(プログラムは「走る」ともいいますが)、これは物体の運動とは違う動きですよね。 (電子は動くでしょうけど、電子の動きがコンピュータやプログラムの動きではないでしょう。視点、レベルが違いますから。) 物体の運動学と同じ考え方を借りると、プログラムの動きも静的な紙の上に表現することができます。 時間座標を空間座標に置き換えればいいわけです。 ただ、物体の運動と異なるのは、時間のステップもプログラムの取りうる位置、つまり状態も離散的だという点です。 ただ離散的だというだけでなく、一様でもありません。 そこで時間から位置の関数の代わりに、状態と遷移の関係として動きを表現します。つまり状態遷移モデルです。

なんだか怪しい(あるいは作為的で強引な)話に聞こえるかもしれません。 でも運動を記述する、そして記述されたものをいろいろ分析するという意味で、物体の運動学とプログラムには似ているところがあります。 もし興味がありましたら、もう少しお付き合いください。

動きの中で変わらないものに着目する

高校に入って微分方程式を習いました。 数学の先生がすばらしい先生で、毎回感動してため息が出るような授業をしてくれました。 ある授業で運動方程式の話になります。左辺は質量×加速度、右辺は力です(1)。この両辺に速度をかける(2)。 ここでよく見てごらん、左辺は合成関数の微分をした形になっている。つまり速度の2乗を時間微分したものだ。 右辺もある関数を時間微分した形にできる(3)。 これを左辺に移項して、微分の線形性を使ってまとめると、2つの項の和を時間微分したものが 0 という形に書ける(4)。 これは時間微分の中身が定数だということだ。これを E と置こう(5)。

これは不思議なことだ。物体は動いているのだから、時々刻々速度は変化する。だから第1項も変化する。 位置だって変化するのだから第2項も変化する。それにも関わらず、この2つの和は一定で、運動の間変化しないというのだから。 運動の間変化しない量がある。これをエネルギーという。第1項を運動エネルギー、第2項をポテンシャルエネルギーというと習いました。 イメージを図示するとこんな感じです。

ご存知の方も多いと思いますが(これだけ数式を出しておいて、ご存じない方がここまで読んでくれるはずはないわけで)運動の間変化しない量はエネルギーだけではありません。 系によりますが、運動量とか角運動量とか、名前の付いているものもついていないものもあります。 これらをまとめて保存量または不変量といいます。

保存量の有意義なところは、運動の記述である位置と時間の関係を求めるよりも簡単に求めることができて、運動に関する様々な側面の理解に役立つことです。 例えば、ある高さからほとんど初速 0 でスタートしたジェットコースターが、斜面でどこまで登れるか。 摩擦がなければスタート地点と同じ高さです。なぜならそこでは速度が 0 で、ポテンシャルエネルギーは高さだけで決まるからです。 すばらしい。簡単にわかります。もし運動方程式を解いて記述を求めていたら、さらに高さの最大値を求める論証をしなければなりません。 さらに重要なことは、運動の記述からは証明できても「なぜ」という質問の答えは得られません。 保存量は運動の「理解」に役に立ちます。

ではプログラムの「運動」についても同様のものがあるでしょうか。あります。それは不変条件と呼ばれるものです。 不変条件にもいろいろありますが、ここで話をしたいのはループ不変条件と呼ばれるものです。

先に事前条件と事後条件の話をします。事前条件はプログラムを実行する前に成立している条件、事後条件はプログラムが終了したときに成立していなければならない条件です。 事後条件はゴールです。プログラマはこれを満たすようにプログラムを作らなければなりません。 事前条件はプログラマに与えられた条件です。スタート時点でこれが成り立っていることを仮定してよいということです。 事前条件と事後条件を次のように書きます。S はプログラムで、一般には複数の文(ステートメント)からなります。(命令型プログラムを考えています。)

{事前条件: Q}
  S
{事後条件: R}

事前条件も事後条件も、プログラムの変数を含んだ論理式です。これを表明(アサート)といい、括弧 { } で括って表します。 これはいわゆる assert と同じものです。プログラムのその位置で、括弧の中に記述された論理式が成り立たなければならないという表明です。

プログラムが複数の文から成る場合は次のようになります。セミコロン ; は文のセパレータです。

{事前条件: Q}
  S1;
  S2;
  ...
  SN
{事後条件: R}

事後条件と同じように、各文を実行した後でも成立しなければならない条件があるはずでしょう。こんなふうに。

{事前条件: Q}
  S1;
{R1}
  S2;
{R2}
  ...
{RN-1}
  SN
{事後条件: R}

実際のプログラムでは、必要と思うところにだけ assert を入れますが、原理的にはすべての文の後に成立すべき条件があるはずです。 すると事前条件と事後条件のペアがプログラム S 全体の動作を定めているように、1文についてもその前後の表明が文の動きというか意味を定めていることになります。

{Rk-1}
  Sk
{Rk}

条件 Rk-1 が成り立つ状態で文 Sk を実行したら Rk が成り立つ状態になるということです。 プログラミングとは、事前条件からスタートして、この3組のブロックを積み重ね、事後条件に至る道筋を作るパズルゲームです。

文が代入文とか if 文の場合は簡単だと思います。ではループはどうでしょうか。

{Q}
  while B do S od
{R}

原理的には、ループの前である条件が成立するとき、ループの後でどうなるかを求めることができるはずです。 これは運動の記述、つまり位置を時間の関数として表すことと同じです。 困ったことに容易には計算できないという点も似ています。 ここで不変条件が活躍します。 不思議なことに、ループのステップが実行されるたびに変数の値は変化していくのに、その間ずっと成立する条件があります。 この条件を P とします。不変条件 P は次を満たすような条件です。

{P}
  while B do
    {P & B}
    S
    {P}
  od
{P & !B}

まずループに入る前に成り立っているとします。 もしループに入れば、ループのテスト B が成り立っているということなので、ループ本体 S を実行する前には P & B が成り立っています。 この状態で S を実行すると、実行後にも P が成り立っているとします。 S がこの条件を満たしていれば、ループを何度実行してもずっと P が成り立っていることになります。 最終的にループのテスト B が成り立たなければループを抜けます。このときは P & !B が成り立っていますね。

もし Q => P (=> は含意、「ならば」)が成り立ち、かつ P & !B => R が成り立つならば、ループは前後の表明を満たすことになります。 複雑で、不必要に精密な状態の軌道を求めなくても、不変条件からループの正しさがわかるというわけです。

ループ不変条件の例

簡単な例をご紹介します。 整数の配列 v の総和を求めるとしましょう。 言語は Isabelle の Hoare ライブラリのものです。

lemma "VARS i s
  {True}
  s := 0;
  i := 0;
  WHILE i ~= length v
  INV {i <= length v & s = sum v 0 i}
  DO
    s := s + v ! i;
    i := i + 1
  OD
  {s = sum v 0 (length v)}"

v ! i は配列の要素 v[i] のことです。 関数 sum v i j は配列 v のインデックス i から j (j そのものは除く)までの部分和を表します。 すると求めるのは総和ですから、事後条件は s = sum v 0 (length v) となります。 この関数はプログラムの一部ではなくて、表明を記述するために定義した数学的な関数です。 Isabelle では論証に使うために別途定義します(してあるとします)。 length v は配列の大きさです。 事前条件はないので、 True となっています。

ループ不変条件の主要な項は s = sum v 0 i です。 まず初期状態では i = 0, s = 0 ですから明らかに成り立ちます。 次にループを抜けた後では、ループの条件 i ~= length v が不成立ですから、その否定 i = length v が成り立ちます。 これとループ不変条件を合わせると、事後条件 s = sum v 0 (length v) になることがわかります。

問題はループ本体です。本体を実行する前には i < length v & s = sum v 0 i が成り立っています。 この状態で本体を実行すると、両辺に v ! i が加わるので、やはりループ不変条件が成り立ちます。 このようにしてループの正しさを確認することができます。

もう1つのループ不変条件

ループ不変条件は1つとは限りません。もう1つご紹介しましょう。

lemma "VARS i s
  {E = sum v 0 (length v)}
  s := 0;
  i := 0;
  WHILE i ~= length v
  INV {i <= length v & s + sum v i (length v) = E}
  DO
    s := s + v ! i;
    i := i + 1
  OD
  {s = E}"

今回は欲しい結果を表すために補助的な名前 E を使っています。 一般に、数学でもそうですが、欲しいものに名前をつけるというのは優れた戦略です。 いまの場合、欲しいものは総和ですから E = sum v 0 (length v) となります。 したがって事後条件は s = E です。

ここで私が習った高校の先生ならばこういうでしょう。

みてごらん、スタートが sum v 0 (length v) = E でゴールが s = E だ。 実はこの2つは、ある1つのものの極端な姿だ。 それは s + sum v i (length v) = E だ。 スタート時点では s = 0 なので sum v 0 (length v) = E になる。 ゴールの時点ではループ条件が不成立だから i = length v なので、sum v i (length v) は 0 になり、 s = E となる。 ループが進むにしたがって、つまり i が増えるたびに、sum v i (length v) から v ! i が減って、代わりに s に加わる。 両方の項は変化するけれども和は一定で変わらない。

エネルギー保存の法則とそっくりじゃありませんか?

2013/08/12   作成
2013/08/18   誤記、文言を修正
© 2013,2014,2015 PRINCIPIA Limited