ループの不変の表明の理解ができていない

Question

下記はクイックソートの疑似コードなのですが、for文の不変の表明が成り立っていないような気がします。
コードの下に私なりにソートされるまでの様子を図にしてみました。
図のtはpivotを表しています。

質問

不変な表明には&&の左側に「l+1からmがx[l]未満である」と書かれていますがそもそも初めてfor文が実行されるタイミングでmとlが同じインデックスを示しているので、l+1はmより右にありますよね？もしそうであれば、l+1からmというのは逆方向を示していておかしくないですか。
同様に、右側も「m+1からi-1がx[l]以上である」と書いてありますが初めてfor文が実行されるタイミングではi-1はm+1よりも左側にある気がします。（わかりにくい文章で申し訳ありません）

不変の表明とは初めてTrueになったタイミングからループを抜けるまでずっとTrueになるということを意味しているのでしょうか
つまり、質問とはfor文のまわり初めの段階ではそもそも比較すらできていないのではないかということです。

よろしければ解答よろしくお願いいたします

void qsort1(l, u){　　 
    if (l >= u)
        return

    m = l 　
    for i = [l + 1, u]
　　/* 不変な表明:x[l+1..m] < x[l] &&
                                    x[m+1..i-1] >= x[l] */　
        if(x[i] < x[l])
            swap(++m, i)　

    swap(l, m) 
    qsort1(l, m-1) 
    qsort1(m+1, u)

Answer 1

それ不変表明なんですかね?
不変表明(invariant)は「ある操作の直前および直後に必ず満たされるべき条件」と考えますが。

Comments

[konnitiha2]

解答ありがとうございます。
参考にしている本にはこのように記載されています。
もう少し考えてみようと思います。
ありがとうございました。

Answer 2

存在しない場合は真となる

Answer 3

おっしゃる通り、ループ開始時点ではx[l+1..m]やx[m+1..i-1]というものに該当するものが存在しません。つまりこれらは空集合という事になります。
集合論では、空集合はあらゆる集合の部分集合という取り決めがあります。このため、論理学における「PならばQ」という命題において、Pを満たすものが存在しない場合(Pを満たす要素の集合が空集合である場合、あるいはPが常に偽である場合)、この命題は無条件で真となるのです。ミステリーにおいて、Aという人物に完全なアリバイがあって犯行が不可能だとしても(「Aが犯人」が偽だとしても)、Aが犯人と仮定するとそれっぽく辻褄が合ってしまうようなものです。

Comments

[episteme]

あー、そーゆーことか。理解した。
範囲 l+1～m 内の任意の要素 L, m+1～i-1 内の任意の要素 U について、
「常に成り立つ」から不変条件か。

んでもって i は最終的に u に到達するから、m を境に 小さい前半 と 大きい後半 に分割される、と。

[konnitiha2]

回答ありがとうございます。つまり不変の表明には論理学の考え方が使われいる。

私が貼った図の一番上の状態ではx[l+1..m]やx[m+1..i-1]が存在しない→空集合であるためTrue、
図の上から2-3こ目の状態では、x[l+1..m]やx[m+1..i-1]が存在し、不変の表明の式がちゃんとTrueになっている。

以上より、このfor文の不変の表明は正しいという認識で正しいでしょうか
追加で一点、x[m+1..i-1]の部分なんですが、x[m+1..i]ではだめなんでしょうか

[swordone]

そうです。

[episteme]

> x[m+1..i-1]の部分なんですが、x[m+1..i]ではだめなんでしょうか
C/C++の配列は 0-origin なので x[N] の最大添字は x[N-1] だからじゃないかと。

[konnitiha2]

お二人ともありがとうございました！