2017-12-13

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 用のバッファになったりするのであまりスマートでなくて，もうちょっといい感じになったらいいのにと思います。

2017-10-20

関数のオーダーの上の順序と足し算

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:正確には，有限個を除いてすべて点でこの不等式が成り立つ．以下の不等号も同様．

2017-04-22

真空中を音が伝わる速さ

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

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

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

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

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

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

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

2016-12-31

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

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

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

2016-11-27

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 が何だったか後からわからなくなる可能性があるから，まあそれが自然かという気がします（オプションでいろいろ制御できる）．

2016-10-21

かたい電車

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

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

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

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

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

2016-10-17

ホーア論理の代入の規則

わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが，見方を少し変えるとわかりやすくなります。

普通の規則。

$\{A[e/x]\} \mathtt{x := e} \{A\}$

同値変形してこうする。

$\{\forall x'. x' = e \to A[x'/x]\} \mathtt{x := e} \{A\}$

要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考えればそれが事前条件になるのは当たり前ですね。

こっちのほうがわかりやすいし，この形で認識しておくと x' の条件を変えることでいろいろできます。例えば乱数。

$\{\forall x'. A[x'/x]\} \mathtt{x := rand()} \{A\}$

上限を指定したり。

$\{\forall x'. 0 \le x' < n \to A[x'/x]\} \mathtt{x := rand(n)} \{A\}$

配列。

$\{\forall x'. x'[i] = e \to (\forall j. i \ne j \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i] := e} \{A\}$

配列への同時代入（構文は適当）。

$\small\{\forall x'. (\forall j. 0 \le j \le 3 \to x'[i+j] = y[k+j]) \land (\forall j. \neg(i \le j \le i+3) \to x'[j] = x[j]) \to A[x'/x]\} \mathtt{x[i:i+3] := y[k:k+3]} \{A\}$