9/14 のRuby開発者会議で、Range#overlap? が欲しい という話を議論した。
Range#overlap? というのは、ふたつの range オブジェクトが重なっているかというのを判定するメソッドである。 重なっているというのは、共通の要素をもっているかどうかと言い換えられるだろう。
この議論がちょっとおもしろかった。
まず、Rails にはすでに同じ機能が（微妙に違う名前で）存在するということでそれを眺めた。
class Range
# Compare two ranges and see if they overlap each other
# (1..5).overlaps?(4..6) # => true
# (1..5).overlaps?(7..9) # => false
def overlaps?(other)
other.begin == self.begin || cover?(other.begin) || other.cover?(self.begin)
end
end
その場にいたひとは、このコードをみてすぐには納得せず、いろいろ言い合って、納得したり、褒めたりしたが、少なくとも問題があるという話にはならなかた
ところが、さらにしばらく経って他の話題に移った後に、ささださんが、これは片方が空のときに問題がある、というのを指摘した。
たしかにそういわれてみると、(1..2).overlap?(2...2) が真になりそうである。((1..2).cover?(1) が真になるから) (この例はささださんのコメント <URL:https://bugs.ruby-lang.org/issues/19839#note-11> からとってきた)
ここで、Ruby の Range に十分に詳しくないひとのために、Range がどのようなものか簡単に説明しておく。
Range クラスのオブジェクトは、begin, end, exclude_end? という 3つの要素が入っている。
x という値が Range オブジェクト r の範囲内というのは、以下の条件を満たした時である。
(if r.begin == nil then true else r.begin <= x end) && (if r.end == nil then true else (if r.exclude_end? then x < r.end else x <= r.end))
この条件を検査するのが cover? メソッドで、r.cover?(x) とすると上記の検査をして真偽値を返す。
なおいちおう触れておくと、Range は比較 (<=> メソッド) を元にして動作するメソッドと succ メソッドを元にして動作するメソッドが混ざっており、cover? は前者である。 それらの異なる種類のメソッドは一貫性のない動作をすることもあるが、今回は比較のほうにしか興味がないのでそれはおいておく。
あと、構文として、exclude_end? が真の場合 begin...end と記述でき、偽の場合は begin..end と書ける。 (前者はドットが 3個、後者はドットが 2個である。この記法は perl 由来) begin と end が nil のときは単に書かないことができ、0.. とか ..10 などと書ける
というわけで、1..2 は 1 <= x <= 2 であるような x の範囲を示し、2...2 は 2 <= x < 2 であるような x の範囲を示す。 後者は 2以上かつ 2未満なので、そのような x は存在せず、空となる。
一方が空であれば、共通する要素は存在しないので overlap? は偽を返すべきだが、上の実装では真を返してしまう。
そのように原因が分かると、range が空かどうかを調べれば良いとなるが、その判定が問題である。
その日は気が付かなくて、後になって私が指摘したのだが、この判定は Ruby では無理なのである。 正確には、この判定をするには、あるオブジェクトが極小であることを判定することが必要になり、 そのためには、比較対象となるオブジェクトが、その情報を提供してくれるような仕掛けを作る必要があるのである。
極小である例としては ...-Float::INFINITY がある。 -Float::INFINITY は浮動小数点数のマイナス無限大で、... は end を含まないので、 この range の範囲はマイナス無限大よりも小さな値である。 しかし、Ruby には (ユーザが勝手に作らないかぎり) マイナス無限大よりも小さな値はないのでこの範囲内に値はなく、つまり空である。
...-Float::INFINITY は空だが、...0 は空でない、という違いを判定するには、あるオブジェクトが、それより小さな値を持たないかどうかを確認する必要があり、 ユーザが定義するクラスも含めてその確認を行うには、その確認を行うメソッドの名前を決めて、すべてのオブジェクトがそのメソッドを実装する必要がある。 (いろいろトリックをつかって多くの場合にメソッドを定義しないようにすることはできるだろうけど)
Ruby において、こういう極小値は、-Float::INFINITY 以外にもある。 まず空文字列と空配列 ("" と []) がそうである。 文字列や配列は辞書式順序で比較を行う <=> メソッドを持っており、"" や [] よりも小さな文字列や配列は存在しない。
さらに、true, false, Object.new といった、大小比較とは縁がなさそうなオブジェクトもじつは極小である。 これは、Kernel に <=> メソッドが定義されているので、（ほぼ）すべてのオブジェクトは <=> メソッドをもっているためである。 Kernel#<=> の定義は、自分自身とは等しく、それ以外のオブジェクトとは比較できない（大きくも小さくもない）というものである。 つまり、自分自身より小さなオブジェクトは存在しないので、極小である。（同時に極大でもある）
というわけで、極小をちゃんと扱うのは難しく、どうしたものかという問題があるのだが、 さらなる疑問として、range が空かどうか判定する問題はこれですべてだろうか、という点がある。 極小を判定するメソッドを用意すれば上の問題は解決できるが、他の問題は存在しないといえるだろうか。 range はなんというか場合分けが多くて、漏れなくすべてを確認したという気分になるのが難しいので、なかなか確信することができない。 （とくに overlap? はふたつの range の組み合わせなので場合が多くなる。空かどうかだけならひとつなのでそこまでではないけれど）
さて、そういう場合分けを扱うのは Coq の得意とするところなので、Coq でなにか証明してみようと考えた。 (まぁ、定理証明支援系なら Coq でなくても場合分けの管理はやってくれる気はする。)
しかし、そもそも何を証明すればいいのかという問題がある。 Ruby 全体を Coq に再現するのは非現実的なので、なにか単純化した世界で証明するわけだが、うぅむ。
いくつか試行錯誤して、証明できたりできなかったりして、半順序があるなんらかの世界の中で range が空かどうか判定できるか、というのを考えることにした。
Ruby のオブジェクトは Kernel#<=> があることから、ほぼすべてのオブジェクトで <=> メソッドを使える。 a <=> b と呼び出した結果が nil となって、a と b が大小関係にないということはある。
仮定として、ほぼすべてのオブジェクトが <=> メソッドをもつというところの「ほぼ」を消して、すべてのオブジェクトが <=> メソッドをもつとしよう。 さらに、<=> メソッドが半順序関係になっていると仮定しよう。
まぁ、Float::NAN <=> Float::NAN が nil になるので、実際には半順序関係ではないのだが、そういう数少ない例外を除去した範囲を考えよう。
まず mathcomp を使う。 順序のための記法を使うので order_scope を open する。 今回の証明のためのセクション (RubyValue) を始める。
From mathcomp Require Import all_ssreflect all_algebra. Open Scope order_scope. Section RubyValue.
Ruby の VALUE 型に相当する型として value を定義する。 value というのは porderType ring_display 型の値である。 porderType というのは半順序が成立する型の型である。(ring_display というのはよくわかってない) (型の型というのは不正確で、じつは record 型であり、coercion でそうみせかけている、といった話に興味があるなら mathcomp本を読みましょう。) 具体的な値は与えない。 具体的な値は与えないので、その型の中にどんな値があるか、どんな半順序関係が入っているかは謎である。 そういう謎な、使える前提が少ない状況で証明できたことは、広い範囲で成り立つだろう。
Parameter value : porderType ring_display.
とはいえ、value 型の中がなにもわからないと、range の範囲の判定で nil かどうかを調べることもできないので、 value の中には nil という値があり、nil は他のすべての値と大小関係にない、という仮定を入れよう。 (nil は list のコンストラクタで使われているので value の nil ということで vnil とする) (x >< y というのは、x と y が大小関係にない、つまり ~~((x <= y) || (y <= x)) である。~~ は論理否定。この条件は全順序なら常に偽だが、半順序なので真になることもある。)
Parameter vnil : value. Hypothesis vnil_not_comparable : forall x, x != vnil -> x >< vnil.
さらに、極小を判定する is_minimum 関数があると仮定しよう。 value -> bool 型の関数 is_minimum があると仮定して、その関数について (exists y, y < x) と ~~ is_minimum x が等価という仮定を入れる。 is_minimum x が偽なら x よりも小さな値 y が存在する、というわけである。
Parameter is_minimum : value -> bool. Hypothesis hyp_minimum : forall x, ((exists y, y < x) <-> ~~ is_minimum x).
Range は begin, end, exclude_end? の3要素からなるので、そういう record を定義する
Record Range := mkRange
{ rbeg : value; rend : value; r_excl_end : bool }.
cover という関数を定義する。 証明の都合で、begin の条件と end の条件を分けて定義する。
Definition cover_b b x :=
if b == vnil then
true (* beginless *)
else
b <= x.
Definition cover_e e excl x :=
if e == vnil then
true (* endless *)
else
if excl then
x < e
else
x <= e.
Definition cover r x := cover_b (rbeg r) x && cover_e (rend r) (r_excl_end r) x.
いくつか補題を証明する。
Lemma cover_b_b b : cover_b b b. Proof. rewrite /cover_b. case: ifPn; first by []. by rewrite Order.POrderTheory.le_refl. Qed. Lemma lt_cover_e x e excl : x < e -> cover_e e excl x. Proof. move=> x_lt_e. rewrite /cover_e. case: ifPn; first by []. move=> e_ne_nil. case: ifPn; first by []. move=> _. by apply Order.POrderTheory.ltW. Qed.
range が空であることを判定する empty という関数を定義する。 この中で is_minimum を使う
Definition empty r :=
let: {| rbeg := b; rend := e; r_excl_end := excl |} := r in
if e == vnil then
false
else if b == vnil then
if excl && is_minimum e then
true
else
false
else if excl then
~~(b < e)
else
~~(b <= e).
そして、調べたい性質である ~~ empty r と exists x, cover r x が等価であることを証明する。 まぁ、再帰があるわけでもないし、プログラム (empty と cover) を展開して、if 式が出てきたらその条件節で場合分けしてそれぞれ確かめていく、というのをやっているだけである。
Lemma empty_valid r : ~~ empty r <-> exists x, cover r x.
Proof.
split.
case: r => /= => b e excl.
case: ifPn.
move/eqP => -> _.
exists b.
rewrite /cover /=.
rewrite cover_b_b /=.
by rewrite /cover_e eq_refl.
move=> e_ne_nil.
case: ifPn.
move/eqP => ->.
case: ifPn; first by [].
rewrite negb_and.
move/orP.
case.
move/negbTE => -> _ {excl}.
exists e.
rewrite /cover /=.
rewrite /cover_b eq_refl /=.
rewrite /cover_e /=.
rewrite Order.POrderTheory.le_refl.
by case: ifP.
move/hyp_minimum => [] y y_lt_e _.
exists y.
rewrite /cover /=.
rewrite /cover_b eq_refl /=.
by apply lt_cover_e.
move=> b_ne_nil.
rewrite fun_if /= 2!negbK.
case: ifPn.
move=> _ {excl}.
move=> b_lt_e.
exists b.
rewrite /cover /=.
rewrite cover_b_b /=.
rewrite /cover_e b_lt_e.
by case: ifPn.
move=> _ {excl}.
move=> b_le_e.
exists b.
rewrite /cover /=.
rewrite cover_b_b /=.
rewrite /cover_e b_le_e.
by case: ifPn.
case=> x.
case: r => b e excl /=.
rewrite /cover /=.
move/andP => [].
case: ifPn.
by [].
move=> e_ne_nil.
case: ifPn.
move/eqP => -> _.
case: excl => /=.
rewrite /cover_e.
rewrite (negbTE e_ne_nil) => x_lt_e.
rewrite (_ : is_minimum e = false); first by [].
apply/negbTE.
apply (iffLR (hyp_minimum e)).
by exists x.
by [].
move=> b_ne_nil.
rewrite /cover_b (negbTE b_ne_nil) => b_le_x.
rewrite /cover_e (negbTE e_ne_nil).
case: excl; rewrite negbK.
by apply (Order.POrderTheory.le_lt_trans b_le_x).
by apply (Order.POrderTheory.le_trans b_le_x).
Qed.
End RubyValue.
証明できた。 というわけで、empty r が偽であることと cover r x なる x が存在することは等価であることを確信できた。
つまり、is_minimum があれば、正しい empty を実装することが可能である。
ここまでくるのに、いきなりこの証明を書いたわけではない。 まず、Rails の overlap を空の場合を考慮する修正をしたものを考え、 最初は nil と nat (自然数) だけがある世界での証明に挑戦して、証明できなかった。 次に、nil と int (整数) だけがある世界での証明に挑戦して、これは証明できた。
最初の nat で失敗した時にはよく考えなかったのだが、後から考えると、nat には 0 という極小値があるので、極小かどうかを判定する関数が必要なのである。 int は極小値がないので証明できたのはよかったが、nil と int しかないというのは Ruby のサブセットとしてあまりに小さい。 で、半順序がついているならなんでも、というのを考えてこうなった、というのが経緯である。
ふと Why3 が気になって https://why3.lri.fr/ にアクセスしたが、Forbidden になっちゃうなぁ
GitHub coq/coq/pull/17831: Avoid unicode subscripts in document