二分探索
二分探索は,値の探索に使うという認識が一般的だと思いますが,実際にはもっと守備範囲が広いです。ということでなるべく一般的な形で書くとどうなるのかを整理した話を書いてみることにしました。why3 で書いて正しいことを検証してみたらけっこうすっきり理解できた気がします。
int 上の述語 f があるとします。f を真にする a と偽にする b がひとつずつわかっていて,a < b であるとしましょう(requires のところ)。そうすると,f x だが f (x+1) ではない x を求めることができる(ensures のところ,result が戻り値),というのが関数の仕様です。
中身はまあ普通の二分探索なのですが,上限 ub は必ず f を満たさないように,下限 lb は必ず f を満たすようにするとわかりやすくて不変条件が簡単に書けます。
ソートされた列 A から値 v のインデックスを求めるよくある二分探索は,f x として A[x] <= v をとった場合になります。
ちなみにコード中では f に特に条件を付けていませんが,真偽が頻繁に入れ替わるような述語に対して使うケースはあまり見た記憶がありません。ある値を境にしてそれより下で真,上で偽(あるいはその逆)になる述語を考えて,その境界の値を求めるのに使うことが多いです。また a, b は自分で与えないといけませんが,たいてい自明な上界と下界があります。
上のコードが正しいことのチェックは,例えば手元の環境では why3 prove -P cvc4 binsearch.mlw を実行すると
binsearch.mlw BinSearch WP_parameter binsearch : Valid (0.03.s)
と出て,正しいことが自動証明できました。int の長さが限られている言語だと足し算がオーバーフローした場合に正しく動かない気がしますが,そこまではチェックしてないようです。
今回は整数上でやりましたが,実数上でも適当なεに対して f x だが f (x+ε) ではない x を求める,のような形で書けるでしょう(たぶん正確にはちょっと違う)。
最短距離と自由豊穣圏
距離空間は豊穣圏であるという Lawvere の論文(http://www.tac.mta.ca/tac/reprints/articles/1/tr1abs.html)がありますが,それに似た感じで重みつきグラフから自由に生成された豊穣圏を考えると hom-object が最短経路になるらしいことに気付いて面白いと思ったので書いてみます.(よく見たら Lawvere の論文にも書いてありましたが,まあいいでしょう.)
R の monoidal structure
R は非負実数の集合に∞を追加した集合とする.これに普通と逆の順序を入れて圏とみなす.実数の普通の足し算はこの圏でのモノイド積になる(0が単位元).また,この圏における直和は inf で与えられる.特に始対象は∞である.モノイド積はすべての直和に対して分配律を満たす.
V-graph と重みつきグラフ
V を可算直和をもつモノイド圏で,分配律 と が成り立つものとする(Lawvere の論文には詳しい条件が書かれていないけど,後でこれくらい必要になる気がするので最初から仮定しておく).
V-グラフ は,集合 と,各 に対する対象の割り当て からなる.
特に V = R のときを考えると,V-グラフとは非負の重みつき単純有向グラフのことである.逆に非負の重みつき単純有向グラフ G が与えられたとき,辺がないところには重み ∞ の辺があると考えることで G を R-グラフとみなせる.
free V-category と最短距離
V-グラフに対して,V-category を対象がの要素全体で,hom-objectが となるようなものとする(0は始対象,1はモノイド積の単位元).ただし
とする.これは V-category になる(たぶん).Lawvere によると,この構成は V-Cat から V-graph への忘却関手の左随伴になっているそうだ(いかにもなってそうである).
重みつきグラフ G を R グラフとみなして上記の構成を行うと,は u から v への最短距離になる(が足し算でがinfであることを思い出せばわかる).
Graphillion で半順序の個数を数えてみた話
Graphillion で遊んでみた。
やったこと
有限集合上の半順序の個数を数えてみた(cf. OEIS A001035)。これを効率的に求めるのは未解決問題らしい。ちなみに有限集合上の位相の個数を数える問題とだいたい同じ。
要素数 n を固定して,Graphillion を使って [1..n] 上の半順序をわりと愚直に列挙した。
実行時間は n=6 で 0.3s, n=7 で 8.6s くらい。n=8 になると三時間ぐらい走らせても終わらなかったのでやめた。ちなみに OEIS を見る限り少なくとも n=18 までは既知らしいので,こういうアプローチで新しい値を見つけるのは無理がありそう。
やりかた
a <= b だったら a から b へ辺を伸ばすことにすると,半順序は有向グラフとみなせる。そこで n 点からなる完全グラフの部分グラフで,半順序になっているようなものを列挙すればよい。Graphillion は基本的な集合演算をサポートしているので,基本的には順序の条件をそのまま書くだけでよい。
ただし,Graphillion は無向グラフを扱うライブラリなのに対して,ここでは有向グラフを扱いたい。そこで,source と target を別の点にして有向グラフをむりやり無向グラフで表すことにした。
一応ちゃんと書くと以下のとおり。有向グラフ に対して無向グラフ を となるように作る。ただし は のコピーで, が全単射とする。
実際のコードでは,G の点を正の整数,G' の点を負の整数で表した。あと半順序は反射的反対称的推移的関係だけど,対角線部分はあっても情報が増えないので,非対称的推移的関係(strict order; 日本語だと強順序?)にした。こっちのほうが辺の数が減って少し効率がよくなるようだ。
from graphillion import GraphSet def posets(n): univ = [(i, j) for i in range(1, n+1) for j in range(-n, 0)] GraphSet.set_universe(univ) x = GraphSet({}) # asymmetry for i in range(1, n+1): x = x.excluding((i, -i)) # transitivity for i in range(1, n+1): for j in range(1, n+1): if i != j: for k in range(1, n+1): if j != k: y = x.including([(i, -j), (j, -k)]).excluding((i, -k)) x = x - y return x import sys print(len(posets(int(sys.argv[1]))))
実行してみた。
$ time python3 posets.py 6 130023 real 0m0.328s user 0m0.293s sys 0m0.028s $ time python3 posets.py 7 6129859 real 0m8.648s user 0m8.251s sys 0m0.324s
出てきた数字は合ってる。
感想とか
ZDD を使うとコンパクトに表現できるかと思ったが,期待したほどコンパクトにはならなかったようだ。ZDD で効率的に表現できるのは基本的には疎な組合せ集合(正確にはちょっと違うと思う)なのだけど,考えてみれば順序全体ってそれほど疎ではないかもしれない。
強引に無向グラフにしてるところにちょっと無駄がある感じはして,Graphillion を使わないで ZDD を自分で操作すればもうちょっと効率よく列挙できそうには思う。
あとは,順序の表現を単に strict order にしたけど,推移律から推論できる辺を除くなどすればもっと辺の数を節約することはできるかもしれない。あるいは,実は BDD のほうがいいとか,(Z)SDD を使うといいとかはあるかもしれない。
Emacs 上でカーソル位置にある文字の T-Code での入力方法を勝手に表示する
Emacs で日本語を入力するときに T-Code を少し使ってるのですが,ある文字の打ち方を知りたいときにわざわざ 55 って打つのがめんどくさいのでカーソルを合わせたら勝手に表示されるようにしたいとずっと前から定期的に思っていて,今日も思ったので40分くらい調べたらできました。
(defun mylib-show-tc-stroke () (if (and (eq major-mode 'text-mode) (not (eq last-command 'skk-insert))) (let ((c (char-after))) (if (and (integerp c) (< 128 c)) (tcode-query-stroke (point)))))) (setq mylib-show-tc-stroke-timer (run-with-idle-timer 0.2 0.2 'mylib-show-tc-stroke))
関数の中でいろいろ条件つけてるのは適当に書いたのでそんなによくないかも。
あとこれだと勝手にウィンドウが分割されて画面の半分が Help 用のバッファになったりするのであまりスマートでなくて,もうちょっといい感じになったらいいのにと思います。
関数のオーダーの上の順序と足し算
https://twitter.com/yoshihiro503/status/920979507053412353 から始まってなんか議論になっている感じだったのを見て,ちょっと考えてみた話.要するに,関数のオーダー全体の集合は自然な順序が入って join-semilattice になる.あと足し算もできる(実は join と一致する).
以下詳細.
は正の実数全体の集合として,に対してそのオーダーを
とする.オーダー全体の集合をと書くことにする.この集合には包含関係で半順序が入る.
は全順序ではない*1が,任意の二元は最小上界をもち,それはで与えられる(は各点ごとのmax).
証明: は明らか.もしとすると,, *2となるがとれる(このは共通にとれる).このときであるからすなわちである.であることはだから明らか.
オーダーの和をと定義すると,が成り立つ.
証明: 左から右への包含関係は明らか.逆にもしならば,あるが存在してとなる.このときと分解してやればそれぞれ, となるのでである.
真空中を音が伝わる速さ
「真空中を音が伝わる速さはおよそ 340m/s である」という主張は正しいか正しくないかということを,ちょっと前に道を歩いていたらふと気になって考え始めたことがあって,そのことを今日思い出したので記録。
まず大前提として,真空中を音が伝わることはない,という事実があります。これを踏まえたうえでこの文の真偽をあえて考えるとどうなるか,という話です。したがってこの文は,有名な「現在のフランス国王は禿である」と同じタイプの主張を述べたものである,と考えられそうです。*1
大雑把に考えて次の二つの解釈があるでしょう。
- (1) 「もし真空中を音が伝わるならば,その速さはおよそ 340m/s である」
- (2) 「真空中を音が伝わり,かつその速さはおよそ 340m/s である」
「真空中を音が伝わる速さ」という名詞句の指示対象が存在することを,仮定と読むか主張の一部と読むかの違いです。それぞれの場合の真偽はどうなるかというと,普通に(直観主義論理で)考えて,(1) と読めば真,(2) と読めば偽になるでしょう。
ここに書いたことだけだとフランス国王の場合と何も変わらない気がしますが,まったく同じ構造というわけではないような気もするので,もうちょっと議論の余地があるのかもしれません。
*1:と書いたところで,じゃあこれ以上新しく解説することはないのではと思いましたが,せっかくなのでちょっと書きます