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

型検査（推論？）がうまくいってもよさそうだけどうまくいかない話です．挙動は 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 とは if then 性質 で順序が入り，1 が最大元 などが成り立つ。証明は下に書くけど…

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