帰納変数 iが基本帰納変数 変数iに対して、 i := i±c という形の代入が一つのみ jがiに対する帰納変数 定数cとdが存在して jへの代入の後で、 常に、 j = c*i + d という等式が成り立っている
帰納変数の十分条件 以下の二つの条件が成り立つとき、 kも(iに対する)帰納変数になる。 jが(iに対する)帰納変数で、kへの代入が常に k := j*b k := b*j k := j/b k := j±b k := b±j のいづれか一つの形をしている jが基本帰納変数であるか、または、 jへの代入は一つでそれとkへの代入の間に iへの代入がない (b) ループの外側のjの定義はkに到達しない の二つの条件が成り立っている
帰納変数に対する強さの軽減 jとj‘がiに対する帰納変数で、 が成り立つとき、sを新しい変数として、 i := i±n ⇒ i := i±n j = c*i + d j' = c*i + d が成り立つとき、sを新しい変数として、 i := i±n ⇒ i := i±n s := s±c*n (c*nは定数) ... j := ... j := s j' := ... j' := s
帰納変数の削除 iが基本帰納変数で、分岐と更新 (i := i±n) のときのみに参照されるとする。 j = c*i+d (c>0) のとき、 r := c*x r := r+d ... ... if i≧x goto B ⇒ if j≧r goto B iの定義を削除(xが定数である場合が典型的)。 上記の帰納変数に対する強さの軽減を行う。 (jをsで置き換えて) j := s を削除。