数遊び

ある日の夜,寝ようとして布団に入った瞬間に,どういうわけか 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なんとなく英語を聞きたくなって適当に検索したら出てきたので見たのですが,いい講義なんじゃないかと思いました。大学の数学の講義って,どこもそうなのかは知らないのですが少なくともぼくが受けた…

また ill-typed term が出てくる例

証明がうまくいかなくて工夫が必要な事例を集めようとしています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。 問題設定 Z -> Z な関数 f と,Z -> Prop な述語(「よい」整数の定義)が与えられます。 0 書けたら,sum の値は証明の中身…