さっきシャワーを浴びながら考えていたことなど。8 って 9 - 1 だから平方数（以下，平方数に 0 は含めないことにする）の差だなーということをまず思った。なんで 8 のことを考えていたかは省略する。というかよく覚えていない。平方数の差はたくさんあるの…

ssreflect を使っているとき，proofgeneral のデフォルトのままだと（といっても何が本当にデフォルトなのか把握できていませんが，少なくともそんなにいじってないはずの手元の環境では）インデントがあんまりうまくいってない感じが強いので何とかできない…

Coq の証明を書くときに，ただ tactics を一列に並べて書くと，まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので，証明の構造を proof script のテキスト上にも反映させ…

最近，emacs を使っているといつの間にかカーソルのデフォルト色が skk が on になっているときの色（正確には skk-cursor-hiragana--color）になっていた，ということが何度もあったので原因を調べてました。skk を off にしてもカーソルの色が on のときと…

新幹線の中でぼんやりしているときに起きた思考の流れ。仮に税率が 20% だとすると，二万五千円の物を買うとしたら税金が五千円かかる。意外と多い。合計三万円。多いので納得がいかない。でも要するに 25000 * 0.2 = 5000 ということであり，25000 * 1.2 = …

先日のメモを詳しくしてみた。ほとんど introduction しか読んでないので正しくないことを書いている可能性もそこそこあります。そういえば 2000 年代前半の文献をあまり見かけないのはなんでだろう。ここに挙げた文献の参考文献リストとか homotopy type th…

http://lkozima.hatenablog.com/entry/2014/09/15/013735 の続き。ホーア論理の健全性の証明をやろうとしていたのでした。一箇所ちょっと難しいところがあるような気がしたのでそれについて書こうとしていたのですが，あれこれ調べているうちに簡単な解決策…

プログラミング言語の理論を計算機上で記述する際にほとんど常に問題になることの一つに，対象言語の変数の扱い方があります。特に変数を束縛する構文を含む言語（関数型言語はほとんどそう）を扱いたい場合には避けて通れない問題です。何が難しいのか，ど…

モデルがないとよくわからない気がしたのでモデルを知りたい，ということで参考になりそうな文献を探してみました(まだ読んでない)。新しい順。 Awodey: Natural models of homotopy type theory (2014) http://arxiv.org/abs/1406.3219 van den Berg, Garne…

なんかいいやり方があったような気がしたけど思い出せなくて考えてたらできたメモ。いまいち証明できた気分にならないので，もしかすると正しくないのかもしれない。Theorem: 命題論理式 が claissical tautology ⇔ が intuitionistic tautology.右から左は…

stackexchange で見かけたやりとり。http://academia.stackexchange.com/questions/26310/should-i-write-a-peer-review-in-third-person論文を書くときは，主語として we を使うのが普通だが，査読の場合はどうか？I を使うのか，それとも this reviewer の…

大量の場合分けや長くて複雑な計算をやるような泥臭い証明が好きではない。そういう人は自分以外にもたくさんいるような気がする。別にはっきりした根拠はないけど，数学に対して「美しい」とか，それに近い形容をする人には，そういう傾向があるのではない…

素数判定 を書いたときに思ったことなど。ああいう内容をきちんと説明するには数式を使って書かなければならない気がするのですが，一方でそうやって説明してしまうとどうもしっくりこないところがあって，結局「こんな計算をします」ということだけ先に書い…

素数判定 なんとなく夜眠れないときに 101 あたりから順番に (97 までは覚えてる) 素数判定をしていたら 700 ぐらいまで行ったりしたときにいつのまにか使ってた判定方法を書いてみたくなったので書きます。何でもいいけどいま 689 という数字が浮かんだので…

(A ∨ B → A) ∨ (A ∨ B → B) は(古典論理で)恒真なのですが，これはわりと奇妙に見えます。そこで，なんで奇妙か考えてみた。簡単にいうと「A または B」からは A と B のどっちもいえないので，二つの成立しないものが ∨ でつながってても正しくなさそう，と…