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, E) に対して無向グラフ  (G+G', E') (a, b') \in E' \iff (a, b) \in E となるように作る。ただし  G' G のコピーで, (-)'\colon G \to G'全単射とする。

実際のコードでは,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 と一致する).

以下詳細.

 \mathbb{R}_+は正の実数全体の集合として, f: \mathbb{N} \to \mathbb{R}_+に対してそのオーダーを
 
  O(f) = \{g : \mathbb{N} \to \mathbb{R}_+ \mid \exists n_0, \exists c
  > 0, \forall n \ge n_0, g(n) \le cf(n)\}
とする.オーダー全体の集合を \mathbb{O}と書くことにする.この集合には包含関係で半順序が入る.

 \mathbb{O}は全順序ではない*1が,任意の二元は最小上界をもち,それは O(f) \vee O(g) = O(\max(f, g)) = O(f+g)で与えられる( \max(f, g)は各点ごとのmax).

証明:  O(f), O(g) \subseteq O(\max(f,g))は明らか.もし O(f), O(g) \subseteq O(h)とすると, f \le ch,  g \le ch*2となる cがとれる(この cは共通にとれる).このとき \max(f,g) \le chであるから \max(f,g) \in O(h)すなわち O(\max(f,g)) \subseteq O(h)である. O(\max(f,g)) = O(f+g)であることは \max(f,g) \le f+g \le 2\max(f,g)だから明らか.

オーダーの和を O(f) + O(g) = \{ h \mid \exists h_1 \in O(f), \exists h_2 \in O(g), h = f + g\}と定義すると, O(f) + O(g) = O(f+g)が成り立つ.

証明: 左から右への包含関係は明らか.逆にもし h \in O(f+g)ならば,ある cが存在して h \le c(f+g)となる.このとき h = \frac{f}{f+g}h + \frac{g}{f+g}hと分解してやればそれぞれ \frac{f}{f+g}h \le cf, \frac{g}{f+g}h \le cgとなるので h \in O(f) + O(g)である.

*1:証明は簡単な演習問題

*2:正確には,有限個を除いてすべて点でこの不等式が成り立つ.以下の不等号も同様.

真空中を音が伝わる速さ

「真空中を音が伝わる速さはおよそ 340m/s である」という主張は正しいか正しくないかということを,ちょっと前に道を歩いていたらふと気になって考え始めたことがあって,そのことを今日思い出したので記録。

まず大前提として,真空中を音が伝わることはない,という事実があります。これを踏まえたうえでこの文の真偽をあえて考えるとどうなるか,という話です。したがってこの文は,有名な「現在のフランス国王は禿である」と同じタイプの主張を述べたものである,と考えられそうです。*1

大雑把に考えて次の二つの解釈があるでしょう。

  • (1) 「もし真空中を音が伝わるならば,その速さはおよそ 340m/s である」
  • (2) 「真空中を音が伝わり,かつその速さはおよそ 340m/s である」

「真空中を音が伝わる速さ」という名詞句の指示対象が存在することを,仮定と読むか主張の一部と読むかの違いです。それぞれの場合の真偽はどうなるかというと,普通に(直観主義論理で)考えて,(1) と読めば真,(2) と読めば偽になるでしょう。

ここに書いたことだけだとフランス国王の場合と何も変わらない気がしますが,まったく同じ構造というわけではないような気もするので,もうちょっと議論の余地があるのかもしれません。

*1:と書いたところで,じゃあこれ以上新しく解説することはないのではと思いましたが,せっかくなのでちょっと書きます

数学は可能な限り一般的であるべきか

ある論文を読んでいて,「集合 X の部分集合族 K が与えられたとする。このとき〜」と書いてあって,その後には K を用いた概念が定義されているのだけど,その部分を最後まで読んでも何を意図しているかよくわからなかった。もっと先を読んでみると,どうやら定義された概念が論文中で使われるのは X が位相空間で K は X の開基になっている場合だけのようだった。そして,K は開基なのだと思ってもう一度定義を読めば,「何だ,そういうことか」という内容だった。

ということがあって,一般的にできることは常に一般的な形で書くことがよいことなのだろうか,ということを考えた。不要な条件はなんとなく書きたくない,という気持ちになることはよくある。だから,そういう書き方をしたくなるのもわかる。でも,可読性を考えれば不必要な一般性は排除したほうがいいように思う。上の場合だったら,最初から X は位相空間で K はその開基とする,と書いてしまったほうがいい。論理的には必要でなくても,適当な条件が文脈として提供されていれば理解の助けになるというケースはよくある。それだったら,はじめからその条件のもとで議論したほうが,読み手にとってはわかりやすい。

Implicit argument が絡んで型検査を通らない例

型検査(推論?)がうまくいってもよさそうだけどうまくいかない話です.挙動は Coq 8.5pl2 で確認しました.他のバージョンでどうかは調べていません.

Set Implicit Arguments してから,なんか依存型を定義します.

Coq < Set Implicit Arguments.

Coq < Inductive Fin : nat -> Set :=
| F0 n : Fin (S n)
| FS n : Fin n -> Fin (S n).
Coq < Coq < Fin is defined
Fin_rect is defined
Fin_ind is defined
Fin_rec is defined

Coq < Fixpoint Fin' (n : nat) : Set :=
  match n with 0 => Empty_set | S n' => sum unit (Fin' n') end.
Coq < Fin' is defined
Fin' is recursively defined (decreasing on 1st argument)

自然数で添字付けられた集合族です.返ってくる物の中身はわりと何でもよくて,それぞれ Inductive と Fixpoint で定義されているところが重要な気がします.

それで,これらを引数に取る関数を何か作ります.ここでは面倒なので変数を宣言してしまいます.戻り値は Prop にしておきましたが,別に何でもよさそうです.

Coq < Parameter P : forall n (i : Fin' n), Fin n -> Prop.
P is assumed

Coq < Print P.
*** [ P : forall n : nat, Fin' n -> Fin n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

P の第一引数の n は implict になります.第三引数の型から推論できそうなのでまあそうでしょうという気がします.ちょっと使ってみます.

Coq < Check (P (inl tt) (F0 0)).
Toplevel input, characters 10-16:
> Check (P (inl tt) (F0 0)).
>           ^^^^^^
Error:
The term "inl tt" has type "(unit + ?B)%type"
while it is expected to have type "Fin' ?n".

うまくいかないようです.(inl tt) の型は (unit + ?B) だけど (Fin ?n) が要求されていると言われています.実際には,第三引数の型が (Fin 1) でこいつは inductive type なので第一引数が 1 であることが(たぶん)わかり,これを第二引数の型の n に代入すれば (Fin' 1) となりますが,これは (unit + unit) に簡約できます.以上のように推論すると型が合っていることがわかる気がしますが,そんなことはしてくれないようです.

明示的に型を書くか引数を与えてやるとチェックは通ります.

Coq < Check (P (inl tt : Fin' 1) (F0 0)).
P (inl tt : Fin' 1) (F0 0)
     : Prop

Coq < Check (P (n := 1) (inl tt) (F0 0)).
P (inl tt) (F0 0)
     : Prop

でもちょっと面倒だし,読みにくくなりがち.

試しに P の引数の順番を変えてみると,

Coq < Parameter P' : forall n (i : Fin n), Fin' n -> Prop.
P' is assumed

Coq < Print P'.
*** [ P' : forall n : nat, Fin n -> Fin' n -> Prop ]

Argument n is implicit
Argument scopes are [nat_scope _ _]

Coq < Check (P' (F0 0) (inl tt)).
P' (F0 0) (inl tt)
     : Prop

こっちは問題ないようです.ということは型検査アルゴリズムが項を処理する順番の問題とかだろうか.もし引数を左からチェックするのだとすると,最初の例では n がわからない状態で (inl tt) の型検査をすることになるので,型が合わないように見える.今の例だと先に (F0 0) を検査するので,n = 1 とわかり,その後 (inl tt) を見るので型が合うと判断できる.本当にそういう実装になってるかどうか知りませんが.

ついでに両方とも inductive でない方の型にしてみると,

Coq < Parameter P'' : forall n (i : Fin' n), Fin' n -> Prop.
P'' is assumed

Coq < Print P''.
*** [ P'' : forall n : nat, Fin' n -> Fin' n -> Prop ]

Argument scopes are [nat_scope _ _]

これは n が implicit でなくなります.Fin' n のような実引数が与えられると簡約されるものは,n が何だったか後からわからなくなる可能性があるから,まあそれが自然かという気がします(オプションでいろいろ制御できる).

かたい電車

15分間隔で電車が走っている路線でA駅からB駅へ向かい,その後30分間隔で電車が走っている路線に乗り換えてC駅に行くことを考える.

A駅でいつもより一本(つまり15分)早い電車に乗るとどうなるか.おそらくB駅における乗り換えでいつもより15分長く待って,いつもと同じ時間の電車に乗り換え,C駅に着くのはいつもと同じ時間になるだろう.あたりまえなんだけどあたりまえじゃない,という感触があって,おもしろい.

定期的に電車に乗っていた時期が昔からほとんどない.いつも歩いて移動している.だからだろうか,5分早く出れば5分,15分早く出れば15分早く着くのが当然のように思っている.しかし電車はそうではない.そのことに気付いたとき,そうか,電車はかたいのだ,と思った.

正則関数はかたい,と言われることがある.局所的な情報だけで全体が決まってしまう.それに対して連続関数はやわらかい.ウリゾーンの補題がそのやわらかさを示している.

それになぞらえて言うと,電車はかたく,徒歩はやわらかいのだ.飛行機は電車よりももっとかたい.同じ電車でも,都会では田舎よりもやわらかいだろう.