参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

まず、群Gの内部自己同型。a∈G を固定して、 g∈G |→ aga-1 として、この写像をΦa:G→G とする。Φaは群の圏の射になり Φ:G→Aut(G) という写像になる。Aut(G) は IsoGrp(G, G) のこと。上記のΦ、またはΦaを内部自己同型と呼ぶが、随伴作用（adjoint action）と…

用語法が混乱してくるのは必然だろうから、仕方ないとは重々承知なのだが、それでも腹立たしい。最近だと、「モジュラー」関係→ユニモジュラー - 檜山正幸のキマイラ飼育記 メモ編, modular, module, moduli, modulus, modulo - 檜山正幸のキマイラ飼育記 メ…

HがGの部分群のとき、y-1x∈H で定義される同値関係を左同値と呼ぶようだ。左同値関係の同値類を左コセットと呼ぶ。ところが、左コセットは右作用の軌道なのだ。H左コセットをH[x]と書くと： H[x] = xH なぜなら：y∈H[x] ⇔ x H〜 y ⇔ x-1y∈H ⇔ y∈xH 。最後は…

対称群のなかで偶置換の全体を交代群と呼ぶ。って、この用語法もどうかしてるぜ。どこが交代なんだよ。特殊線形群との類似で言えば、特殊対称群とかのほうがマシでしょう。交代複線形写像との関係もピンとこないし。

modular, module, moduli, modulus, modulo - 檜山正幸のキマイラ飼育記 メモ編 で述べたように、モジュラー群とはPSL(2, Z)を意味することが多いと思うが、ユニモジュラー群（unimodular group, 単模群）と特殊線形群を同義で使っている例があった。具体的…

なんとmaximaはネットワーククライアントになる。サーバーじゃなくてクライアント！ここが既にハマリ所だが、使用されているソケットにクライアントとして接続しに行くと、次のように死ぬ。 bin > .\maxima.bat -s 4000 Connecting Maxima to server on port…

√2 * √3 = √6 はそのままではできない。rootscontract関数に渡す必要がある。 rootscontract(sqrt(2)*sqrt(3)); しかし、√2 * √2 = 2 は自動的に計算される。定義によるからだと思うが、メカニズムはよく分かってない。

maximaのdotfile - 檜山正幸のキマイラ飼育記 メモ編 の件、あのファイルはtcl構文だろう。 http://wiki.tcl.tk/724 http://www.interq.or.jp/japan/s-imai/tcltk/array.html tcl/tkベースのmaximaのためだとすると、wxMaximaには関係ないだろう。maxima-ini…

diff(x^2, x) 変数xがバインドされていると変なことになる。xを純粋な変数にしたいなら kill(x) しないといけない。「関数表示だから、暗黙にラムダ変数だろう」という常識が効かないで、大域変数として値を探してしまうのだ。

めちゃくちゃ久しぶりにmaxima、コンソールでプロンプト出てない。なんか文字入力しないとプロンプトでないと、と言う。何考えてんだ。以前はリターンでもプロンプトが出たが、最新バージョンでは有意な文字入力しないとダメみたい。改悪、つうか、最初から…

見た目（綴り）が似てるので、それだけけで勘違いしやすい。とりあえずモジュラー群とは“SL(2, Z)の半分折り”だと思っていいんだろう。 モジュラー群 モジュラー群PSL(2, Z)は、リーマン球面（複素射影直線）、ガウス上半平面（複素半直線）に、1次分数変換…

加法的は、足し算（可換モノイド演算）とゼロを保存すること。これはいい。線形は加法的とは違う！ fが線形 ⇔ D(f:X→Y):X×X→Y = π;f 、ここでπは自明バンドル X×X→X の射影。この「線形」は名前も良くないが概念としても良くない。名前は「アフィン線形」と…

::> 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ファイルを疑う。

impI, assoc, transとかは、誰でもどこでも使いそうな名前なので、まずバッティングするだろう。find_theorems name: で検索して、修飾されたフルネームで指定するのが安全。

型の表記として、 [A, B] => B は許されている。 命題の表記として、[| P; Q |] ==> R は許されていない。まさかの未定義！ Pureを生で使ってはいけないのは、こういう変な癖があって使いにくいからか。この奇妙な文法の背景が分からない。

一番上はOK、NGとコメントしてあるのは構文エラー definition "right_unit_law == (!!n.(n + 0 == n))" definition "right_unit_law1 == !!n.(n + 0 == n)" (* NG *) definition "right_unit_law2 == (!!n. n + 0 == n )" definition "(right_unit_law3) == …

Pureをいじっているが、性悪なシステムだな。 接頭辞PROPの意味が分からない。他の構文とは違う、かなり特殊。 型propには定数がなくて、true, falseもない。 PureとIFOLで関数適用の構文が違うのが非常にストレスだし、間違う。 prop型の定数はaxiomatizati…

isar-refとかimplementtion文書で： stateが状態（名詞）と述べる（提示する、主張する）のときがある。Isar/VMでは、述べるの意味のstateが状態の名前として使われている。"state"という名前で「述べる」の意味のstateがある。 argumentが引数のときと、議…

NGと書いてあるところだけダメ。 (* on top of Pure *) axiomatization A:: "'a ⇒ prop" and B:: "'a ⇒ prop" and P :: "prop" and Q :: "prop" term "op ==> P Q" term "P ==> Q" (* NG *) term "(A a)" term "(B b)" term "op ==> (A a) (B b)" term "(A a…

IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、setup Pure_Thy.old_appl_syntax_setupというコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされ…

Isabelle/jEditを終了してもスマトラPDFは残るが、このスマトラPDFがいると、Isabelle/jEditは起動しないようだ。事情は謎。

クッソーッ、ハマったわ。MLファイルを単に開いてもOutputには何も出ない。以前は出ていたので、ホントにワケわかんないで、再インストールとか再起動とかは何度もしてしまった。たぶん2時間以上はかけている。 単にMLファイルをロードしただけではダメ。 開…

C++では、Javaのような言語仕様としてのインターフェースはない。だけど、純粋仮想関数を並べればインターフェースの代用になる。代用になるのだが、インターフェースは言語仕様ではなくて手法なので、落とし穴がある。インターフェースのつもりのクラスに仮…

対処法は分かったが理由がサッパリ分からない謎の現象。これを詮索している余裕がないので、とりあえず起きたことを記しておく。後で再現できるかどうかは分からない。まず、2つのソースコードがある。1行しか違ってない！ $ diff -u t_params.cpp t_params2…

F:C→D の逆関手は G:D→C で、F*G = C, G*F = D であるもの。ちなみに、FからGは神託構成になる。別な言い方をすると、GはFを含むイプシロン項で表現される。Gが亜群だとする。亜群では、(-)-1が反変関手となる、Inv:G→G が、Inv(f) := f-1 で定義される。こ…

stricmp問題 - 檜山正幸のキマイラ飼育記 メモ編 の件。共通インクルードファイルのなかで、#include されていた。このため、共通インクルードファイルを直接・間接にインクルードしているファイル（すべてのソースファイル）で、 #include "common.h" // 間…