真空中を音が伝わる速さ

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

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

ある論文を読んでいて,「集合 X の部分集合族 K が与えられたとする。このとき〜」と書いてあって,その後には K を用いた概念が定義されているのだけど,その部分を最後まで読んでも何を意図しているかよくわからなかった。もっと先を読んでみると,どうや…

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

型検査(推論?)がうまくいってもよさそうだけどうまくいかない話です.挙動は Coq 8.5pl2 で確認しました.他のバージョンでどうかは調べていません.Set Implicit Arguments してから,なんか依存型を定義します. Coq < Set Implicit Arguments. Coq < I…

かたい電車

15分間隔で電車が走っている路線でA駅からB駅へ向かい,その後30分間隔で電車が走っている路線に乗り換えてC駅に行くことを考える.A駅でいつもより一本(つまり15分)早い電車に乗るとどうなるか.おそらくB駅における乗り換えでいつもより15分長く待って,…

ホーア論理の代入の規則

わりとわかりにくくて混乱しやすい気がするホーア論理の代入の規則ですが,見方を少し変えるとわかりやすくなります。普通の規則。同値変形してこうする。要するに「代入後の x の値を x' とすれば A[x'/x] である」が事前条件です。Hoare triple の意味を考…

数学の本の話

数学の本はアウトラインがわかればあとは自分でよく考えるだけで本を閉じたまま詳細を構成することができる。しかし数学以外の本はそうとは限らない。例えば歴史の本は歴史の大まかな流れがわかっていても細部を自分の頭で考えても埋めることはできない,気…

Hilbert algebra の性質の証明

ちょっと気になってやってみたのをどこかにメモしたくなったので書いた。関数解析じゃなくて論理の方の Hilbert algebra です。 Hilbert algebra の公理 が Hilbert algebra とは if then 性質 で順序が入り,1 が最大元 などが成り立つ。証明は下に書くけど…

resolution の完全性についての疑問

一階述語論理の resolution の規則って, として を の MGU としたときに と書けて(resolution に を使うのはあまり普通ではないかもしれないけど),これだけで反駁完全なのだと思っていました。しかしどうもそうではないようだという気がしてきて,どうやっ…

ダウンロードしてみた本リスト

先日 Springer でいろいろな本が無料ダウンロードできるようになっていた。今はもうできなくなったらしい。どういうことだったのかはよく分からない。twitter を見ても,よく分からないと言っている人がたくさんいる。何冊か落としたのでメモ。 Marker, Mode…

contraction がいらないシーケント計算

「論理と計算のしくみ」を読んでいたら,シーケント計算の推論規則を ∧右,∨左,⊃左は additive ∧左,∨右 は multiplicative にすると命題論理では contraction が不要になるということを知りました。こういう組み合わせは証明論的にはだいぶ気持ち悪いよう…

Awodey 本の訳に変なとこがある

Awodey 本の邦訳について,訳の質が低いという趣旨のレビューがついています。自分で確認したわけではないのですが,このレビュアーの書いていることを信じるならば,確かにあまり丁寧に訳されてはいないようだという印象は受けます。そこに挙げられている点…

既約性

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

圏論ぐらい普通に生きてればわかる人

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

掛け算と割り算は随伴

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

多項式の微分は積の微分から出てくる

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

積分

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

Lean をインストールしてみた

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

普通に日本語を話す

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

well-definedness と universal map

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

Extensional axiom of choice という公理があるらしい

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

世界が 11 次元だとすると重箱の隅は 1024 個もあるのでつつき放題

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

数遊び

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

掛け算の順序を区別するなら割り算は二つ必要

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

Coq 8.5 を入れてみた

先日 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 の proof script のインデント

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

議論の構造の proof script への反映のしかた

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

emacs のカーソルの色が勝手に変わる

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

25 * 1.2 = 30

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

HoTT のモデルとそれにつながりそうな文献

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