論理の用語法整理の試み

「原子」「複合」 を使う。次の表の欄に入る語は正式なテクニカルタームとして定義する。

	原子	(複合)	構成規則
項
論理式
証明
リーズニング

リーズニングが一番ゴタゴタで、

• 証明{図}?の構成規則の概念とかぶる。
• コンビネータ由来のリーズニングと、2-射由来のリーズニングがある。
• フォワードリーズニングとバックワードリーズニングがある。

テクニカルタームとしての定理は3種類。

1. 論理式定理： 論理式に名前を付けて、証明部として証明を付けたもの。
2. 証明定理： 証明に名前とプロフィールを付けて、証明部としてリーズニングを付けたもの。

論理式定理のとき：

• ステートメントとは論理式そのもの。
• 証明部は、結論がその論理式である絶対証明

証明定理のとき：

• ステートメントとはプロファイル〈2-プロファイル | シーケント〉のこと
• 証明部は、そのプロファイルがプロファイルであるリーズニング

ライブラリ：

• 論理式ライブラリは、論理式定理の集まり。インターフェイスは論理式定理のヘッドの集まり。
• 証明ライブラリは、証明定理の集まり。インターフェイスは証明定理のヘッド〈宣言〉の集まり。

日常語のテクニカルタームによる解釈

1. 命題 → 論理式
2. 命題 → 定理（日常語）
3. 定理 → 論理式定理（論理式ライブラリの要素）
4. 定理 → 証明定理（証明ライブラリの要素）
5. 公理 → 論理式定理で証明部が原子証明であるもの。
6. 公理 → 証明定理で証明部が原子リーズニングであるもの。

原子証明／原子リーズニングのためのキーワード。

• 事実〈fact〉
• 明らか〈obvious 'b'がある〉
• 自明〈trivial〉
• 後で〈deffered〉
• 信じろ〈believe | trust〉
• 神託〈oracle〉
• 仮定〈assume〉

原子 vs 複合

• 同義語・類義語： 基本、組み込み、ビルトイン、単純、アトミック、原子{的}?、プリミティブ、原始{的}?、既約、分解不能、素、生成｛的｝?
• 同義語・類義語 英語： basic, builtin, simple, atomic, primitive, reduced, irreducible, indecomposable, prime, {generating | generative}
• 反意語・反意語の同義語・類義語：組み合わせ、複合、複雑、可約、合成、構成された、定義された、生成された、導出された
• 反意語・反意語の同義語・類義語 英語： composite, combined, composed, compound, comlex, reducible, constructed, defined, generated, derived

仮に「原子{的}?」と「複合{的}?」を採用するとして、単項式・多項式と同様に、排他的か包含的かの問題が生じる。

• ペア (原子, 複合) は包含的であると決める。
• 形容詞「複合｛的｝?」は省略可能とする。

マイナス記号

1. 負号
2. 単項演算子（足し算の逆〈反対〉を取る、反数演算の記号）
3. 二項演算子（反数との和）

負号としてのマイナス記号はなくてもいい。が、負数はリテラル表記できなくなる。
二項演算子記号もなくてもいいが、煩雑になる。

用語ペアの関係性

関係性は：

1. 同義〈同一〉である。
2. 排他的である。
3. 包含的である。
4. 所属的である。
5. 同型である。
6. 埋入的である。
7. その他。

言語の基本： 国、地域、（人の）集団、文脈、状況、場面などで意味と用法が変わる。

例：

1. (単項式, 多項式)
2. (数, 単項式)
3. (数, 式)
4. (文字, 単項式)
5. (原子, 分子) 化学の意味で
6. (元素, 単体) 化学の意味で
7. (元素, 化合物) 化学の意味で
8. (単体, 化合物) 化学の意味で
9. (標本, 母集団) 統計の意味で
10. (標本, 標本空間) 統計の意味で
11. (標本空間, 母集団) 統計の意味で
12. (関数, メソッド) プログラミングの意味で
13. (ペア, タプル) プログラミングの意味で
14. (タプル, リスト) プログラミングの意味で
15. (有理数, 無理数)
16. (有理数, 分数)
17. (少数, 分数)
18. (整数, 2進数)
19. (2進数, 10進数)
20. (可換環, 非可換環)
21. (可換環, 環)
22. (関数, 写像)
23. (線形関数, 線形写像)
24. (線形形式, 線形写像)
25. (連続関数, 不連続関数)
26. (連続関数, 関数)
27. (連続関数, 三角関数)
28. (犬, 哺乳類) 常識的意味で
29. (要素, 集合)
30. (決定性関数, 非決定性関数)
31. (非決定性関数, 多値関数)
32. (コンパクト空間, 非コンパクト空間) トポロジーの意味で
33. (連結空間, 不連結空間) トポロジーの意味で
34. (基底, フレーム) 線形代数の意味で
35. (定数, 定数記号)
36. (定数, 変数)
37. (変数, 不定元)

セオリーが拡散した事情

• 定義1： 論理式の集合（生成系）
• 定義2： 演繹閉な論理式の集合（順序閉包）
• 定義3： 証明〈推論規則〉の集合（生成系）
• 定義4： リーズニング閉な証明〈推論規則〉の集合（リーズニング閉包＝圏）
• 定義5： 生成系を持つ圏
• 定義5'： 指標〈生成系〉を持つ圏

また、

• 定義6： 定理の集合
• 定義6'： 名前に対する証明の割当の集合
• 定義7： 証明記述言語の構文モナドのクライスリ射
• 定義8： クライスリ射のクライスリ拡張である関手

定義5'と定義8では、圏と関手の違いがあるので、統合は無理。セオリー圏とセオリー関手とでも呼び分けるしかない。

• セオリー圏： 生成系〈指標 | コンピュータッド〉を持つ圏。生成器は構文モナド。
• セオリー関手： 構文モナドのクライスリ射のクライスリ拡張として得られた関手。

色々な対応関係

暫定案、後で修正。

日本語だと複数形がないので、複数形の代わりに「ナントカセット」とする。

セオリー論	プログラミング	論理	ストリング図
指標	インターフェイス	推論規則セット	スパイダーセット〈アイコンパレット〉
ソート	型	命題	ワイヤー（のラベル）
オペレーション	サブルーチン	定理	名前付きストリング図
基本オペレーション	組み込みサブルーチン	公理	スパイダー
オペレーション宣言	サブルーチンプロトタイプ	定理宣言	-
オペレーションボディ	サブルーチンボディ	定理の証明	名前付きストリング図のストリング図
	リファクタリング	証明の書き換え	ストリング図の書き換え
構文モナド	プログラミング言語	論理言語	描画法
クライスリ射	ライブラリ	セオリー	ストリング図キット
クライスリ結合	ライブラリのマクロ展開	セオリーの定理展開	ストリング図の展開
モデル	マシン、エンジン	モデル

別な対応表

• 参考： 関数プロトタイプ - Wikipedia

プログラミング	論理
ユーザー、プログラマ	証明者〈prover〉
プログラミング	証明行為〈proving〉
テキストプログラミング言語	テキスト論理言語
グラフィカルプログラミング言語	グラフィカル論理言語
インターフェイス	指標〈シグネチャ〉
型	論理式〈命題〉
？	シーケント〈プロファイル〉
宣言〈プロトタイプ ｜ シグネチャ〉	宣言（借用）
サブルーチン定義	定理
サブルーチン定義ヘッド	定理ヘッド（借用）
サブルーチン定義ボディ	定理ボディ（借用）
プログラムコード	証明{図}?
呼び出し数	呼び出し数（借用）＝ノード数
ライブラリ	セオリー
組み込みサブルーチン	公理／推論規則
引数型	仮定
戻り値型	結論
ランタイムエンジン／ハードウェア	モデル
コンパイル／トランスパイル	トランスパイル（借用）

必要な用語：

• 絶対証明： 仮定が空な証明
• 絶対シーケント： 右片側シーケント、絶対証明のシーケント〈プロファイル〉
• 単純証明＝基本証明： ノード数が1の証明{図}? 公理、推論規則と同一視できる。
• 絶対単純証明＝絶対基本証明： 論理式リストと同一視できる。もちろん、公理、推論規則と同一視できる。
• {コンパクト}?カリー化： コンパクト論理におけるカリー化コンビネータ
• 絶対化： 与えられた証明図を絶対証明図にするリーズニング、演繹定理から（カリー化の繰り返しで）出来る。

非形式「証明」の解釈：

1. 証明図〈proof {figure | diagram}〉
2. 証拠式〈witness expression〉
3. リーズニング図 （証明図とリーズニング図の区別は出来てない）
4. 定理の証明部（構成素名、役割名）
5. 証明行為〈proving〉

非形式「定理」の解釈：

1. 指標内の宣言
2. ヘッド付き証明〈headed proof〉
3. ヘッド付き証明のヘッド
4. セオリー〈ライブラリ〉のインスタンス

非形式「公理」の解釈：

1. 指標内の宣言
2. ヘッド付き証明〈headed proof〉、ただし証明は単純証明
3. ヘッド付き証明のヘッド、ただし証明は単純証明
4. セオリー〈ライブラリ〉のインスタンス

公理証明、推論規則、基本証明、単純証明 が同義語、公理命題と公理絶対証明〈絶対推論規則 | 絶対基本証明 | 絶対単純証明〉は同一視可能。たくさんの同義語、ほんとは違うが習慣的に同一視することが混乱と誤解をまねく。

ベイズネットとストリング図と拡張ER図（AERR図）

以下の図は、http://www.chimaira.org/img5/graphical-model-2.svg 。

これは、次の記事内の図。

• 因果セオリー論の語法・記法・図法（修正案付き） - 檜山正幸のキマイラ飼育記 (はてなBlog)

次は、ベイズネットのグラフをストリング図に描き換えている。（http://www.chimaira.org/img5/schema-to-string.png）

これに触発されて描いた図が次。

• A attribute 実体または関連の属性、辺として図示
• E entity 実体＝集合、ノードとして図示
• R relationship 関連、ノードとして図示
• R refernece 参照、辺として図示

マルコフ圏で考えるので、値のコピーと値の破棄ができる。次のルールがある。

1. 実体ノードはID属性辺をひとつだけ持つ必要がある。
2. 実体ノードはその他の属性辺を持ってもよい。
3. 実体ノードは参照辺を持てない。
4. 関連ノードはID属性辺をひとつだけ持つ必要がある。
5. 関連ノードはその他の属性辺を持ってもよい。
6. 関連ノードは幾つかの参照辺を持ってもよい。
7. 参照辺とID属性辺が結合される。
8. AERRの全体はオープングラフ＝ストリング図になる。

意味論は、可換厳密モノイド圏＝厳密対称な対称厳密モノイド圏で行う。

功罪

1. 日常的な言葉を用語にする。例：やせた、広い、大きい、理論、一様、単調、建物
2. 難しい言葉・造語を用語にする。例： 亜真接続付き多様体、特恵近傍系、特殊フロベニウス代数装備圏

	メリット	デメリット
1	親しみやすい。簡単そうな印象を与える。	専門用語だと分かりにくい。地の文と混同する。
2	地の文と区別できる。安易な連想を避けられる。	違和感・嫌悪感を与える。意味不明。記憶しにくい。

多次元ガウス分布

正規分布のNを取ると、雑音のNや次元のnと紛らわしいのでGを使う

• マルコフ核 G_n(θ) = G_n(μ, Σ) : Rⁿ →* Rⁿ
• 密度関数 g_n(θ) = g_n(μ, Σ) : Rⁿ → R

θ = (μ, Σ) が属するパラメータ空間Θは、Θ = Rⁿ×SPDMat(n)、SPDMat(n) は半正定値行列の空間。

OneTabのページを削除

OneTabのページを放置していたが、やはりインターネットに公開されているのは気持ち悪い。念のためにローカルにページセーブして削除した。削除できるのは作ったときのクッキーが必要らしく、他のPCからは削除出来ないから要注意。

Applications as Networks

「分散アプリケーション指向」に変わるアプリケーション設計スタイルを表す用語。

あっ、chocoも

c:/ProgramData/chocolatey/ にchocolatyもインストールされていた。これもnode.jsと同日。おそらく、Pythonなどをインストールするためにchocoを使ったのだろう。

誰がPythonをインストールしたのか？

Path環境変数を見たら、\Python38 が入っていて、実際にPythonがインストールされていた。いったい誰が？ タイムスタンプを見ると7月13日にインストールされている。で、アプリケーション一覧を調べると同日にnode.jsをインストールしていた。

• Windowsでnpm installしてnode-gypでつまずいた時対処方法 - Qiita

この記事（古い）を見ると、node.jsにPythonやMSVC++が必要らしい。今では自動になっているのだろう。MSVC++も同日にインストールされていたし。

謎理論、謎用語

sumii先生情報：

> 「2x」や「x^2」は「多項式」ではない、
知りませんでした。確かに謎ですね。

文書処理：問題群

「文書処理」タグは、どうせ本編ネタだから、「本編ネタ」タグは付けないことにした。

• 文書処理：20年前の課題は今でも課題 - 檜山正幸のキマイラ飼育記 (はてなBlog)

1. 終電問題 -- バリデーションをいつするか？ どこまでするか？
2. ウメボシ問題 -- 主にエディットレット・フォーメーション
3. フリカケ問題 -- 属性ボキャブラリーに対する編集パイプライン（広義のエディットレット）の構成法
4. コピペ問題 -- 名前の通り
5. カーソル移動問題 -- 名前の通り、特に上下移動
6. 空白問題 -- 名前の通り、xml:space では解決できない
7. コメント・PI問題 -- 仕様上の文字データノードが、意味的には構造を持つことが問題
8. 検索とパターンマッチング問題 -- ユーザーに、文字列検索以上の構造検索をどうやってしてもらう？
9. エラー告知問題 -- ユーザーに、妥当性違反をどう伝えるか？（整型式性違反は起きない）
10. 属性編集問題 -- 名前の通り
11. 構造の曖昧性問題 -- 見出しタグで、章節を表すとか。
12. ツリー変形と揮発性フラグメント問題 -- 見出しをヒントに章節のラップ要素を入れることがある。このような要素は、編集が終わってセーブするときには取る（削除する）べきかもしれない。
13. 疑似要素問題 -- 正規表現でパターンマッチしたレンジなどを、あたかも要素のように扱うこと。例えば、URL文字列をハイパーリンクとして扱う。
14. 表示の更新と構造の同期問題 -- リモート編集の場合、投機的に表示更新する必要がある。編集失敗のときは、投機的変更を取り消す必要がある。
15. プラグイン問題 -- プラグインのお作法、相互運用整、バッチのような認証、管理、登録〈帳簿〉など色々

他に、編集作業中のフラグとか、アクセス制御などの目的のプロマティを属性としてDOMAPIに露出するか？ とかも問題。プロパティ・属性問題かな。