ダメ出し
加法的は、足し算（可換モノイド演算）とゼロを保存すること。これはいい。線形は加法的とは違う！ fが線形 ⇔ D(f:X→Y):X×X→Y = π;f 、ここでπは自明バンドル X×X→X の射影。この「線形」は名前も良くないが概念としても良くない。名前は「アフィン線形」と…
ベイズ・ネットワークの定義では、普通、ノードは確率変数だと言われる。この意味での確率変数を「事象」と記述してある本がある。意味不明だったが、次のように解釈できる。まず、確率変数を確率空間のあいだの確率（測度）保存可測写像の意味で使う。この…
確率分布を確率空間の意味で使うこともあるようだ。https://www.youtube.com/watch?v=bHBTEsYC-YM の講義だと、σ代数の生成系を「事象族」、「確率」＝確率測度で、「事象族と確率」の組み合わせを「確率分布」と呼んでいるので、確率分布は確率空間と同義。…
カルバートソン／スターツが、どうして「モデル分布族」を「標本分布」と呼ぶのか？（サンプリング - 檜山正幸のキマイラ飼育記 メモ編） 不思議だったが、次のような事情かも知れない。 パラメトリック・モデル分布族とは、パラメータ空間＝仮説空間の各点…
標本空間のサンプルの話は今は置いとく。『統計数学』p.72では、確率標本という言葉を使っているが、おそらくはrandom sample(ing)だろう。 http://stats.stackexchange.com/questions/99126/are-random-sample-and-iid-random-variable-synonyms 基本的には…
有限測度 -- 全空間の測度が有限 有限集合上の測度 -- 有限測度とは呼ばない 有限加法的な測度 -- σ加法性がない。これは測度とは呼ばないかも知れない。前測度でもない。finitely additive measures という言葉はある。→ http://www.ams.org/journals/tran/…
最初見てサッパリだったが、たぶん次のような意味。 argx{xを含む命題 P(x)} 命題P(x) を満たすようなxの値。存在することは事前に保証されている。複数の候補があれば適当に選ぶ。イプシロン記号と同じ。 argmaxx{xを含む式 f(x)} f(x)の最大値を与えるxの…
environは地獄だ。environはノービスには書けない。エキスパートが書いてあげるのが前提みたいだ。スライド http://mizar.org/cicm_tutorial/mizar.pdf "Mizar Hands-on Tutorial" by Adam Naumowicz, Artur Korni lowicz, Adam Grabowski (July 29, 2016) …
メタ情報 - 檜山正幸のキマイラ飼育記 メモ編 あたりから：http://fm.mizar.org/contents.html からMML IDで探す。 例 Volume 1, 1990 http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf 例 Volume 2, 1991 http://fm.mizar.org/1991-2/pdf2-3/oppcat_1.pdf テ…
::> 121: Disagreement of argument types ::> 191: Unknown schemeこれの原因は、environ部の不備だった。schemes NAT_1; だけではスキームのインポートが出来ない。 constructors NAT_1; が必須、これがないとUnknown schemeが出る。registrations NAT_1; …
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？） しかし、 Make Environment, Mizar Ver. 8.1.04 (Win32/FPC) Copyright (c) 1990-2015 Associatio…
アイダースコアが入れられない！ たぶん識別子構文は英数字だけなのだろう。
ホントによくハマる。 まず、vocファイルを書く。空でもいいから書く。 vocabulariesディレクティブに自分の名前を書く！！！ 新しい名前を定義するときは必ずvocファイルにも書く。 名前（トークン）を知らないと言われたらvocファイルを疑う。
environ :: From NAT_1 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1; notations T…
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/printout/mizar4ja_prn.pdf では、 vocabulary （単数？） notation （単数？） constructors definitions theorems schemes requirements それ以外に次を確認している。 registr…
NAT_1とO_RING_1のマージ例。そのまま2つをコピペしてもエラー。次のようにディレクティブごとに揃える。 environ :: From NAT_1, O_RING_1 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYT…
environ部のディレクティブは2度以上書けるようだが、同じアーティクルが2度以上指定されると、 *810: Directive name repeated これがシンドイ。コピペしかないのに、コピペに不便な仕様。
http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…
名前がないからどうにもならないが、名無し／メタ情報なしでも、 特定シンボル（述語名、関数名、モード名、属性名）を含む定理 特定のプロファイルの特定のシンボルを含む定理 特定のアーティクルで定義された特定のシンボルを含む定理 存在命題、全称命題…
地獄の作業例。 reserve i,j,k,l,m,n for natural number; i+k = j+k implies i=j; proof defpred P[natural number] means i+$1 = j+$1 implies i=j; A1: P[0] proof assume B0: i+0 = j+0; B1: i+0 = i by INDUCT:3; B2: j+0 = j by INDUCT:3; hence thesi…
Valdis Laanって人は目ぼしい結果を並べるだけで証明を書かない。イライラする。http://www.kirj.ee/public/proceedings_pdf/2011/issue_4/proc-2011-4-221-237.pdf で自分の論文 http://kodu.ut.ee/~vlaan/preprints/generatorssli.pdf を参照しているが、…
オカシイ、オカシイ。除去規則（elim rule）がIsar satement formatだとobtainsで書かれる。これはオカシくはない、つうかまっとうなんだが、逆に通常の除去規則の書き方はいったいなんなんだ？ ということになる。disjEの例だと： ?P ∨ ?Q ==> (?P ==> ?R) …
ウッヒャーー、またしても新用法を発見。subgoalがsolveすべき対象である命題（＝論理式＝ルール＝定理）で、goalはそれらsubgoal達の集合の意味で使っている。つまり、ゴール＝サブゴールズ。しかし、サブゴールの結論をゴールと呼ぶことがあるから。「ゴー…
どうかしてるぜ！Isabelleマニュアルの分かりにくさも尋常ではないが、それを執拗に詮索している僕も常軌を逸しているかもな。どうかしてるぜ。Isabelleコミュニティの人は、「どうかしているぜ」な用語の曖昧さ／乱用を自覚してるのだろうか？ あまり意識し…
theoremなどを使って証明した最後に結果（定理のステートメントに対応する命題シェマ）が表示されるが、axiomatizationで公理を導入すると命題シェマが表示されない。find_theorems nama: コマンドを使う必要がある。find_* コマンドを使って状況確認するっ…
証明支援系って、ほんとにマダマダ - 檜山正幸のキマイラ飼育記 メモ編 現状がこれでは、先が長くて気が遠くなる。 証明オブジェクトは人間が見ても意味不明（Coq）か、見えない（Isabelle）。 リーズニングの記録としての証明スクリプト（＝タクティクの列…
おまえは何を考えているんだ？ 教えてくれ！ - 檜山正幸のキマイラ飼育記 メモ編 apply(assumption) でゴールが解けてしまうことが多いが、具体的な仮定（コンテキストが持っている定理）がどれかワカランことがある。autoだけでなくて、なんかの根拠をつか…
型推論してくれるのはいいけど、その結果がどうであるかを知りたい。 autoで証明してくれるのはいいけど、何をしたのか教えてくれ。 resolutionで、ユニフィケーションの結果を教えてくれ。 何を考えてるかワカランぞ、教えてくれ。教えてくれないのか？ お…
マダマダというか、ダメダメというか。とっても使いにくい。30年間作り続けてこのレベルってことは、あと30年くらいはかかるのかな、生きてネーよ、チクショー。次が欠けている。 情報検索機能 アウトライン機能 リソース管理機能 ビジュアライズ機能 情報の…
Pureをいじっているが、性悪なシステムだな。 接頭辞PROPの意味が分からない。他の構文とは違う、かなり特殊。 型propには定数がなくて、true, falseもない。 PureとIFOLで関数適用の構文が違うのが非常にストレスだし、間違う。 prop型の定数はaxiomatizati…
