新→旧 の順 計算科学における半加法圏の位置付け テンソル半加法圏とプログラム意味論 個体と世界の関係：圏から論理半環を絞り出す クリーネ代数の「テスト」を圏論的に定義できるだろうか？ クリーニ代数と圏論 トレースを使ってクリーネスター（またはク…

P, Qなどを点で、LP,Qを平行移動とする。平行移動の公理は次でよいと思う。 [平坦性公理] LP,Q(R) = LP,S(Q) [平行性公理] LP,Q(R) = S ならば、LP,Q = LR,S [P,Q] ‖= [R, S] ⇔ LP,Q = LR, S と定義して、次の「平行四辺形定理」が成り立つ。 [P, Q] ‖= [R, …

初日（12-23）で観た。ウーン、ダメだったな。ガッカリ。4-アフターライフがシリーズ最低だと思ったが、最低記録更新かも。有終の美は飾れなかった。アンダーソン監督（脚本）のやめたかった感が満載。なんとしてでも終わらせるためにストーリーをでっち上げ…

これは出来が悪いなぁ。見どころは、冒頭のクローンアリス部隊による渋谷本部襲撃、アリス＆クレアvs処刑マジニくらいか。クローン部隊は、3-エクスティンクションの最後に出たネバダ地下のアリス達だが、クローン部隊の出番はここだけ。アリスの超能力も渋…

韓国の少女時代の子達はスタイルいいなーと思ってたが、以前、少女時代とローラが並んだ写真を見て唖然とした。手足の長さが違いすぎる。だが、そんなローラでさえ、ミラの横だとパッとしない。エイダ役のリー・ビンビンも一人だとすごくスタイルがいいが、…

ミラがプロモーションで日本に来ていたのでインタビュー動画なども見られる（ https://www.youtube.com/watch?v=UxPW-Tvt5vQ ）が、素のミラは、まーさすがにオバサンぽいところもある。が、ともかくキレイだし、話もシッカリしている。アクションはきつい年…

後の破綻ぶりに比べればマシな展開だが、 アンブレラ社の特殊部隊は、なぜマットとアリスを連れて行く？ 特にマットに必然性がなさ過ぎ。 ワンはアリスとスペンスを知っていて、関係者扱いした可能性はあるが、マットは意味不明。手錠をしたまま連れ回すなん…

昔、マカロニ・トレーニングをしたが、あれは端的に感情移入能力のトレーニング。感情移入能力とは、仮想的シミュレーション能力、想定能力などのことで、ほんとに必須。特に幾何的イメージを作る場合は、外形がこうである図形の内部はどうだろう、とか向こ…

体の向きを変えるトレーニング 自分で動くことをシミュレーション 自分ではなくて、小人さんをイメージ 入れ子になった自分をイメージ 自分も動く、小人さんも動く 部屋トレーニングと同じように自分の目の前に見えている色をイメージする 2階建ての部屋トレ…

transitive という言葉がある。推移的だが、可移的 (かいてき), 可遷的 (かせんてき) ともいう。transition＝遷移の遷と移だ。推移律の推移とは趣が違うので、「遷」「移」を使ったほうがいいだろう。transitiveの意味は、X の任意の元 x に対して Gx = X が…

ミラは平気で脱ぐなぁ。別に脱がなくてもいいと思うのだが。 1-インフェクションの初登場シーンはシャワールームで、ほとんど裸 1-インフェクションの最後と2-アポカリプスの最初の病院で、ほとんど裸 2-アポカリプスの最後でアイザックスに助けられた水槽内…

型クラス相当機能は分かったが、 型クラスのインスタンス化の方法が分からない。 インスタンス化に証明が伴うが、書き方が分からない。is を使って、X is C と書いて、この命題を証明するのか？

パターンがあるものは、3分間・URIテンプレート - 檜山正幸のキマイラ飼育記 で示す。 http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/ http://mizar.org/version/current/html/{小文字ID}.html http://mizar.org/JFM/pdf/{小文字ID}.pdf http://fm.miza…

http://mizar.org/version/current/html/ hidden tarski_0 tarski xboole_0 xboole_1 enumset1 xfamily xregular xtuple_0 zfmisc_1 subset_1 setfam_1 relat_1 fanct_1 ordinal1 ordinal2 ordinal3 relat_2 wellord1 wellord2 funct_2 funct_3 funct_4 grun…

適当な訳語がない。等力かな。集合が等力とは、1:1対応があること、基数が等しいこと。

$MIZFILE/mml.larにすべてのアーティクルの名前（list of articlesだろう）。mml.vctにすべてのシンボル。

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…

environがホントに難しいが、environ部を（もし）書けたら、明らかな命題を確認する。 INDUCT2: for n, m being Nat holds n + 1 = m + 1 implies n = m; INDUCT3: for n being Nat holds n + 0 = n; INDUCT4: for n, m being Nat holds n + (m + 1) = (n + …

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 これがシンドイ。コピペしかないのに、コピペに不便な仕様。

.aco XML、ボキャブラリの計数情報のようだ。 .ano テキスト、謎だが、これもボキャブラリの計数情報のようだ。 .atr XML、謎 .cho テキスト、.anoと似てる。 .dct テキスト、タグジャンプファイルと似てる、なんかのインデックスっぽい。 .dcx XML、シンボ…

配布ファイル： mizar-8.1.04_5.33.1254-i386-win32.exe ソフトウェアのバナー： Mizar Ver. 8.1.04 (Win32/FPC) doc/mml.txtの記述： Version 5.33.1254 配布ファイル名が、-〈システムバージョン〉_〈MMLバージョン〉- だった。

記述書式（format） 述語や関数を呼び出すときの記述形式、定義時に指定する。 座（ローカス、ローサイ）（locus, loci） 述語や関数のパラメータ宣言 パターン 記述書式と関係あるようだが現在は不明 Mizarでは公理と定理の区別がなく、すべて定理： 公理定…