が既約であることと であることが同値みたいなんだけど，どうやって証明するんだかわからなくて気になってとりあえず調べてみたことを書きます。http://mathoverflow.net/questions/177789/is-xn-x-1-irreducible によると は既約なので，それを認めると，n …

世の中には二種類の人間がいる。普通に生きてれば圏論がわかる人と，そうでない人だ。とかいうのは仮に真だとしても圏論を勉強するうえで何の助けにもならないし，だいたいきれいに二つに分けられるはずもないのですが，しかしある程度は正しいことを言って…

m が正整数のとき となることを証明する。適当な仮定の下で の左随伴 L は と表される。そこで （普通の順序で圏とみなす）かつ の場合を考える。すると， における極限は最小値なので，確かにとなることがわかる。

多項式を微分すると指数が係数に出てくるのって，積の微分の公式 と を使って とかやると出てくる。ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

ぼくにとって，数学といえば積分らしい。それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボード…

Lean 本体 最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。 Emacs の lean-mode E…

「普通においしい」「普通に嫌い」「普通に言う」などの表現に違和感がある。自己の判断を述べる際に，なぜわざわざ「普通に」と付けるのか。どういう意味で普通だと言っているのかよくわからないし，そもそもそんな疑問が浮かぶ以前に，響きに違和感がある…

well-definedness 周りの議論ってわりと何してるのかわかりにくくない？ と思って考えてたら universality のほうがわかりやすい気がしてきりしたので書いてみた。以下 , は集合， は 上の同値関係。 well-defined とは 写像 が well-defined であるとはどう…

二年前に 直観主義と選択公理の話 という記事を書いたのですが，それに近い内容の論文を 2006 年に Martin-Löf が書いていたこと知りました。"100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" というタイトルの論文で，Springer か…

何がきっかけか忘れたのですが，一般に n 次元の重箱には隅が 2^(n-1) 個あるのだなということを思ったので，たいした話ではありませんが書いてみることにしました。n 次元重箱とは，n 次元立方体の境界から一つの側面の内部を除いた図形である。具体的には…

ある日の夜，寝ようとして布団に入った瞬間に，どういうわけか 676 という数字が浮かんできた。見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると ，ちょっ…

掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し，右側は「何単位分あるか」を表すのであり，それらを逆に書いてはいけないのだという。例えば，2×3=6 と書いたらそれは「三人がそれぞ…

先日 Coq 8.5 がリリースされたので入れてみた話。coq 自体のコンパイルは問題なくできたけど，その後 ssreflect のコンパイルに失敗した。make すると Error: The files /usr/local/lib/coq/parsing/pcoq.cmi and /usr/local/lib/coq/lib/compat.cmi make i…

さっきシャワーを浴びながら考えていたことなど。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 のどっちもいえないので，二つの成立しないものが ∨ でつながってても正しくなさそう，と…

http://lkozima.hatenablog.com/entries/2013/09/30 細かい計算をまったく追いかけてないので MC より弱いところではなんでできないのかよくわかってない。 のところ，計算してみたらわかった気がした。たぶん の健全性のところで使うのではないかと。もうち…

ひさしぶりに様相論理の論文を読みました。なんとなくまとめ。 TOPOLOGY AND MODALITY: THE TOPOLOGICAL INTERPRETATION OF FIRST-ORDER MODAL LOGIC http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=2189652 Neighborhood-Sheaf…