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 の値は証明の中身…

Coq.Arith.MinMax 見てみた

Coq のモジュールシステムについて,使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに,モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思う…

pattern で ill-typed term が出てくる例

依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが,その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りま…

maximal induction principle の話

前回のうまくいかない elim の続きで,Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが,こういうことを細かく解説したものを読ん…

Ltac と proof term 5

tactic が proof term を生成していく様子を何度か観察しましたが,何のためにそんなことをしていたかというと,ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。例と…

auto の話

Coq.Sets.Ensembles がなんだかうまく使えないなあ,と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。具体的には何かというと, Coq < Goal forall x : A, forall X : Ensembl…

Ltac と proof term 4

append の結合性の別証明。f_equal を使ったらどうなるかやってみました。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs …

Ltac と proof term 3

今度は等式の証明でやってみました。append の結合性。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs…

Ltac と proof term 2

今度は算術でやってみました。 Coq < Goal forall n, n = 0 \/ 1 <= n. 1 subgoal ============================ forall n : nat, n = 0 \/ 1 <= n こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。 Unnamed_thm < induction n. 2 s…