Axiomに関するいくつかの懸念事項

N2892 Some Concerns About Axiomsから。


【概要】
私は現在定義されているaxiomについていくつか懸念している。
これらの懸念は、私が明確な答えを見つけることができない2つの質問として表現することができる。
私の質問の概要は以下のとおり:
なぜaxiomを書きたいと思うのだろうか、もし書いた場合それをどのようにして正しくできるだろうか。
これらの質問に対する答えがなければ、私は現在定義されるようなaxiomが問題になるかもしれないと思う。



【質問1】
axiomのコードに(保証された)効果がないのであれば、そのコードを書く時間は無駄ではないだろうか。
axiomはコンパイラ、あるいはビルドシステムの他の部分も明示的にコントロールしないし、影響しない。
つまり、私は確実にコードの振る舞いを変更するためにaxiomを使用することができない。
Working Draftに以下のセクションがある:

14.10.1.4 Axioms [concept.axiom]


4 axiomが2つの式の等式を明示する場合、実装は式をもう一方に置き換えることが許可される。...
7 実装がaxiomによって式を置き換えるかどうかは処理系定義である。そのような置換を除いて、axiomの存在はプログラムの目に見える振る舞いに効果がないものとする。

私はプログラマが、コンパイラが有用な最適化を適用するかもしれないことを望んで
axiomを書くように動機づけられそうもないと思っている。
多くの場合、私自身は自明の置換を適用し、保証を持ち、容易に理解されていて、
可視の効果が得られている。
それが可能でない、あるいは実用的ではない状況で、axiomを書くことはせいぜい
コードを最適化する(おそらく)間接・非汎用的な方法だろう。
さらに、axiomはそれを含むコンテキストにのみ影響し、また、
ほとんどのコードはテンプレートにはない。


保証された効果がないという点ではインラインも同じだが、インラインはよく理解されており、
コンパイラは何がインラインでなければならないか、何をインライン化するべきかについて、
多くの情報を持っている。
(実際、明示的なinline指定子の使用は、最近では(おそらく)必要ない)
また、インラインの場合はプログラマへのコストが非常に小さく
(1関数につき1キーワードを付けるだけ)、それを誤解する可能性も非常に低い。
さらに、インラインはテンプレートだけではなく全てのコードに利用可能である。



【質問2】
axiomを書いたとして、それが正しいことを知ることができるのだろうか。


axiomが使用されることは保証されないが、セクション14.10.1.4(Axiomの仕様)から
それが大きな効果をもたらすことがわかる。
したがって、コンセプトを1つ書いたらaxiomを使ってそれを正しくしたほうがいいが、
axiomを書くのを支援する入門的な説明(ガイダンス)がない。


また、言語の他の機能はコンパイラ/リンカー/ランタイムエラーによって、
結果を観測することにより、それが正しいかどうかを知ることができるが、
axiomのコードが正しいかどうか知ることができるのは、構文的なチェックしかない。
axiomのセマンティクスが正しいかどうか知る唯一の方法は、
起こらないかもしれない最適化によるパフォーマンス向上で、それを計測するのは難しい。


例えば以下はWorking Draftからの抜粋だが

// 23.2.6.2 Member container concepts [container.concepts.member]


auto concept MemberContainer<typename C> {
    ...
    size_type C::size() const {
        return distance(this->begin(), this->end());
    }
    ...
    axiom MemberContainerSize(C c) {
        (c.begin() == c.end()) == c.empty();
        (c.begin() != c.end()) == (c.size() > 0);
    }
}

私が以下のようなコードを書いたら何が起こるだろうか?
(明瞭さのためContainer-MemberContainerマッピングを無視した。)

template<MemberContainer C> void process_front(const C& c)
{
    if (c.begin() != c.end())
    {
        ... // c.front()を使って何かする
    }
}

void my_algorithm()
{
    forward_list<...> fl;
    ... // flに何かを入れる
    while (fl.begin() != fl.end())
    {
        process_front(fl);
        fl.pop_front();
    }
}

私は、これはかなり合理的なコードであるように見える。
任意のコンテナの第1要素で何かをするprocess_frontルーチン、および何らかの方法で
forward_listを使用してループからprocess_frontを呼ぶアルゴリズムを持っている。
ここで使用しているイディオムは、一般的なSTLコンテナのイディオムである。
そうすると、問題は何だろうか。


MemberContainerコンセプトはautoなので、forward_listのためのコンセプトマップが生成されるだろう。
しかし、forward_listはsize()メンバなしで慎重に設計されたので、
ユーザーはsize()がO(1)であると仮定したコードを書かないだろう。*1
これは、size()メンバがdistance()によってデフォルトO(n)実装を使用して、
MemberContainerによって提供されるということを意味する。
MemberContainerSize公理があるために、コンパイラは自由に
process_frontの中のsize() > 0でbegin() != end()を代用することができる。
したがって、not-emptyに対するO(1)テストのように見えるものはO(n)サイズ計算になる。


私の見解によれば、この問題は理解するのが非常に難しい。
私がもしデバッガでステップ実行してdistance()の中にたどり着かなければ、
このコードをパッと見てもそれについて考えるとは思えない。
さらに悪いことに、公理置換を行わないコンパイラの方が速く動作してしまう。
さらにさらに悪いことに、公理置換はおそらく、デバッグモードでは起こらず最適化の際に起こってしまう。
私はこの置換が悪い考えであるとコンパイラが理解するかどうかわからないが、
そのような知能はおそらく未定義動作の領域にあるだろう。
(コンパイラベンダが特定の最適化を保証するのが好きではないので。)


先の例は単に正しくない振る舞いをするのではなく、不完全な最適化を生成する。
しかし、以下のaxiomを考えてみてほしい:
(さらに23.2.6.2のMemberContainerコンセプトから)

axiom MemberFrontInsertion(C c, value_type x) {
    x == (c.push_front(x), c.front());
}

この置換の意味は落ち着いている。
コンパイラは、xが(c.push_ront(x), c.front())よりはるかに効率的であると
容易に決定することができ、この公理はそれらが等価であると言っている。
push_front、front式は誰かが書く合理的なもので、それがxと暗黙に取り替えられれば、
それを含んでいるコードの振る舞いは表面的に類似しているだろう。
したがって、見当たらない挿入は見つけるのが非常に難しくなる。


ここでのポイントは、axiomを書くことが確かに微妙な要素であるということである。
おそらく、上記のMemberContainerSize公理を書いた人は、
誰もが、コンパイラが私の例証したpessimize(最適化の逆で、効率を悪いものにする)をしない、
あるいはできなかった、ということを知っていることを想定しているのだろうが、
私はユーザーにそのレベルの専門知識を要求することが合理的であるとは思わない。


【結論】
私は、これらの両方の質問に対する説得力のある答えがなければ、
axiomを削除するか、それらの定義を変更するべきであると信じている。
現在定義されているように、それは構文チェックされたコメントだが、
コメントとは違い、それは可視・潜在的に劇的な振る舞いをすることができる。
私は、この振る舞いが利益より責任のほうがはるかに大きいと信じている。


axiomで有用的なことをするサードパーティツールの見込みはおもしろく、無視できないが、
そのようなツールは特定のプログラマにとって利用可能かもしれないか、
利用できないかもしれない、もしくは有用かもしれない。
さらに、これらのツールはまだ存在していないので、私はそれらがどんな情報を必要とするか
いま知ることができるかどうか疑問である。


axiomを使用するツールは、コンパイラの置換振る舞いに依存しない。
おそらく、axiomの効果がコメントである場合、それらは実際にコメントであるべきである。
コメント中の自明な関係を表現するための標準構文は、サードパーティツールが、
私が議論する問題を引き起こさずに動作することを可能にするだろう。また、構文を今後変更する
必要があれば、後方互換性を促進するバージョン情報を含むのは容易だろう。


他のオプションは公理置換を行うことをコンパイラに禁じるだろう。
私は、この機能性が一旦私たちがどのように公理が働かなければならないかより良い考えを持てば、
事態を壊さずに、あとで加えられるかもしれないと信じる。
置換言語なしで、上記の質問に対する答えは簡単である:
1:もしそれらを利用した解析ツールを使用していなかったら置換しない、および
2:それはあなたのコードに重要ではないが、解析ツールでそれらをチェックすることができる


axiomの削除について挙がった懸念はおおざっぱに以下のようになった(意味が歪められていないことを望む):
axiomが言語の形式仕様の一部であるので、一旦それらがライブラリに入ってしまうと
それを変更することができない。
また、それが既存のコードを変更するので、あとからそれらを加えることができない。
したがって、私たちはそれらを最初に正しい状態にしたほうがいい。
私は、これが全く正確ではないと信じている。
定義による(正しい)axiomがコードの振る舞いを変更しないので、
それらが最初に正確である限り、および変更または追加が正確な限り、
それらの変更は既存のコードに影響しない場合がある。


これは私を同じ結論に導く。
現在定義されるように、公理はそれらがコードに可視の効果がないことを保証するのに
正しくなければならない。
私たちはまだどのようにこれらを正しくするべきか確信があるように思えない。
また、私たちは、私たちを支援するための実装をしていない。
したがって、今のところ、私たちはそれらを削除するべきか、定義を変更するべきである。



*1:forward_listの醍醐味は、Cでの実装にオーバーヘッドを持っていない、最小のforward-linked listを提供することなので、サイズ計算はO(n)にならなければならないだろう。