真空中を音が伝わる速さ

「真空中を音が伝わる速さはおよそ 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…

An exercise in dependent types (解答編)

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

An exercise in dependent types

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

HoTT のモデルに関する文献

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

Glivenko の定理の代数的証明

なんかいいやり方があったような気がしたけど思い出せなくて考えてたらできたメモ。いまいち証明できた気分にならないので,もしかすると正しくないのかもしれない。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 のどっちもいえないので,二つの成立しないものが ∨ でつながってても正しくなさそう,と…

neighborhood sheaf semantics 補足

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

一階述語様相論理の sheaf semantics とか

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

induction principle を自分で書く

昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。なんかこういうのを考えていて, Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov…

複雑な(?) inductive に対する induction principle

……が,期待通りに生成されないと思ったけどよく考えてみるとどうなるべきなのかわからなかった話。 準備 例として,石取りゲームみたいなのを考えます。いくつかの石があって,一度に三つまで取ってよいということにしましょう。そうすると,プレイヤーのと…

型健全性が保証する性質を余帰納的に書いてみた

型健全性というと type preservation と progress が成り立ってればよいというのがよくある話ですが,それでなぜ健全といえるのかというところをわざわざ形式的に書いてみた話です。といっても,わかりやすい説明をしようという気はあまりなくて,知ってる人…

42 vs. 105

道を歩いているとき,無意識のうちに数字をいじっていることに気付いたのでその内容を思い出しながら書いてみる試み。42 と 105 は確かどっちも異なる三つの素数の積である。2, 3, 5, 7 から三つ選んでかけるとそれらが出てくる。だけどどっちもそこそこ小さ…

match goal の中で dependent destruction すると fail する

久しぶりに Coq を触っててしばらくはまった話。とりあえず準備。 Require Import Program. Set Implicit Arguments. Inductive fin : nat -> Set := | First : forall n, fin (S n) | Next : forall n, fin n -> fin (S n).fin n はサイズ n の有限集合の型…

Choice Principle と選択公理

「構成的プログラミングの基礎」という本を読んでいたら choice principle のことが書いてあって,この間書いた直観主義と選択公理のことと一見噛み合わない内容だったので,どういうことか考えてみた話を。 Choice Principle 次の公理のことを choice princ…

直観主義と選択公理の話

下記の講義ノートを読んでいたら選択公理のことが書いてあって,それがおもしろかったのでこの記事を書こうとしています。http://math.andrej.com/2005/08/23/realizability-as-the-connection-between-computable-and-constructive-mathematics/直観主義と…

乗法的「または」について

線型論理のおはなし。線型論理は少しかじった程度でまったく詳しいわけじゃないのでこれから書く内容が的外れである可能性もあると思いますが,以前からなんとなく思っていることを書いてみます。線型論理には「かつ」と「または」がそれぞれ二種類あり,加…

代数トポロジーの入門講義

http://www.youtube.com/course?list=EC6763F57A61FE6FE8なんとなく英語を聞きたくなって適当に検索したら出てきたので見たのですが,いい講義なんじゃないかと思いました。大学の数学の講義って,どこもそうなのかは知らないのですが少なくともぼくが受けた…