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…

昨日 (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…

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

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

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

久しぶりに 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 princ…

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