少し追記。 型コンテキストを型判断と呼ぶ用語法は採用しない。 型シーケント $`\Gamma \vdash M:\sigma`$ を型判断〈typing judgement〉と呼ぶのは許容しよう。 型判断の意味はセマンティック・デカルト閉圏の射になる。特に集合圏では単なる写像。型コンテ…

まず、次は同義語扱いしたほうがいい。 変数の型宣言 型コンテキスト 0-指標 ポイント1-射だけの1-指標 構造体定義 レコード定義 テーブルスキーマ 例えば、 variable x, y : Real, c : Color type-context {x:Real, y:Real, c:Color} 0-signature _ { 0-mor…

MEDL（Mathematical Entity Description Lang.）とDIDL（Drawing Instruction and Description Lang.）について。DIDLはある程度は汎用の絵図記述言語。だが、直接的な目的は証明記述。「証明」は曖昧語なので、テクニカルタームとしては導出〈derivation〉…

従来： システム組み込み ユーザー定義 ワイヤー 公理 仮説、仮言、仮定 ケーブル 公理系 仮説、仮言、仮定 ノード 公理、推論規則 定理 オペレータ 推論規則 ？ 同値性 ？ ？ 今後： システム組み込み ユーザー定義 ワイヤー 命題 命題 ケーブル 構造化命題…

vocabulary of (predicate)s 多様体 { 境界を許す広義多様体 境界を許さない狭義多様体 } context Extended for 多様体 { 多様体 := 境界を許す広義多様体 境界無し多様体 := 境界を許さない狭義多様体 境界有り多様体 := 境界を許す広義多様体 ∧ ￢境界を許…

descriptionモジュールとterminologyモジュールにするか。モジュール名・名前空間があるが、description〈desc〉とterminology〈term〉は異なる名前空間〈名前コンテンナ〉。 description TransitionSystem signture RightTransitionSystem within (C in Mon…

module TransitionSystem signture RightTransitionSystem within (C in MonCAT) { sort A sort S operation t: S×A → S } signature DetTransitionSystem := TransitionSystem within Set signature ParTransitionSystem := TransitionSystem within Partia…

指標による定義： module TransitionSystem signture RightTransitionSystem within (C in MonCAT} { sort A sort S operation t: S×A → S alias alphabet := A alias state-space := S alias right-transition := t alias transition := right-transition }…

vocabulary Panda { パンダ レッサーパンダ ジャイアントパンダ } context Now for Panda { パンダ := ジャイアントパンダ レッサーパンダ := レッサーパンダ _ := パンダ } context Old for Panda { パンダ := レッサーパンダ _ := ジャイアントパンダ _ :=…

アルファベット アルファベットの要素： {アクション | 入力 | 刺激}?{ラベル | レター | 記号 | シンボル | 信号}、インストラクション{記号 | ラベル | ニモニック}? 遷移、作用、実行 遷移系、マシン、エンジン 状態{空間 | 集合} ムーブ、ムーブペア、ム…

穴あきストリング図 ケリー／マックレーン・グラフ 多様体 ボックス＝サークル バー＝ストリング 境界 ポート＝ピン 符号、符号付き色 境界条件 ワイヤー リンク 複体構造のセル ワイヤリング リンキング 球体と同相の多様体（ボール、ブロブ）の境界（球、…

ドット＝ポート＝ピン＝ソケット＝スロット エッジ＝アーク≒ワイヤー≒ケーブル＝バス ボックス＝サークル＝スフィア≒カローラ＝ブーケ≒インターフェース 入れ子ダイアグラム＝星座＝メタツリー オープンエッジ≒ハーフエッジ＝ダート＝フラグ

僕はA案だが。 A案 B案 C案 指標 指標 セオリー セオリー セオリー 代数 モデル 代数 モデル

コンポジショナル・ドキュメンテーション 横結合〈horizontal composition〉とスライス 縦結合〈vertical composition〉とスタック 横断結合〈traversal composition〉とゾーン〈クラスター〉 テンプレート、テンプレートスロット、テンプレート展開、テンプ…

リソース〈情報リソース〉：物理的な存在物 トピック〈概念トピック〉：概念的な存在物 トピックエントリー： リソースの一部で、トピックに対して記述している部分、曖昧かも知れない。 記述単位：メタデータや構造を提供する。コンテンツがアロケートされ…

デリバラブルは本来の意味として、デリバラブル・ジェネレーターで生成されるブツのこと。 名前空間のルートはパッケージ名とする。パッケージ名自体はURLなどで名付ける。 プロジェクト名、パッケージ名、ワールド名は一致させる。 パッケージの名前空間の…

コンテナスキーマの形状と位置集合〈set of positions〉の組 を仮にテンプレートと呼ぶと。以下は同義語。 コンテナスキーマのテンプレート 変数出現を持つ式と変数出現の集合 変数出現を持つ項と変数出現の集合 形状がストリング図のときは、ストリング図と…

一貫性関係は用語が安定してなくて困る。レインンスター〈Tom Leinster〉の"Higher Operads, Higher Categories"での言い方。 一貫性定理と厳密化定理をあまり区別しない。同値な定理だから。 結合律子、単位律子を "coherence isomorphism" と呼んでいる。W…

13年以上前2008-02-06の記事のコピーへの現時点〈2021-06-15〉での注釈。 茂木／伊藤『微分幾何とゲージ理論』のまえがき(P.2)に翻訳表が載っているのが非常に助かる。 写真がある。 https​://twitter.com/mamorumatsuo/status/956145613946568704 特に注意…

無条件分布 ＝ 分布 ＝ (dom(ω) = 1 のマルコフ射) 条件付き分布 ＝ マルコフ射 分布＝法則 （同義語として） 条件付き法則 ＝ 条件付き法則 無条件法則 ＝ 無条件分布 ＝ 分布 ＝ 法則 言葉の使い方（語学）。 無条件分布は条件付き分布である。（包含関係…

上が新しい。 用語ペアの具体例 - (新) 檜山正幸のキマイラ飼育記 メモ編 用語ペアの関係性 - (新) 檜山正幸のキマイラ飼育記 メモ編 否定の接頭辞、拡張的形容詞 - (新) 檜山正幸のキマイラ飼育記 メモ編 排他的否定、拡張的否定、制限的否定 - (新) 檜山正…

曖昧多義語の例：確率変数 単なる可測写像 確率空間からの可測写像 確率空間のあいだの測度保存写像 特に、同時確率分布の射影写像 確率空間、または確率空間の台集合を変域とする変数 確率測度 標本空間 可測空間 可測写像の域 可測写像の余域 確率空間の台…

固有名：他でもないそのモノだけを指す名前 種別名：いくつかの個体達に共通する性質の名前。その性質により個体が分類される。 役割名：構造物や組織体の構成素／構成員の役割の名前 実際には、これらの名前の用法が頻繁に入れ替えられる。 固有名 → 役割名…

正方形： square {rectangle}? 正方体 ： regular cube 文字化け ： {character | text} garbling, garbled character 文字落ち ： {character | text} lost, lost character 文字 ： character, letter, atomic symbol

標本空間 ： 対象、可測空間、サンプリングとは無関係、スカラーや単位区間が標本空間になるとは限らない。 事象 ： シグマ代数の要素、シャープ述語の外延 {スカラー値}?変量 ： 標本空間からスカラーへの純関数 述語 ： 標本空間から“スカラーの単位区間”…

ベクトル空間を単に空間と呼ぶことがある。ベクトル空間は自由ベクトル空間〈基底付きベクトル空間〉とする。 空間＝自由ベクトル空間＝基底付きベクトル空間 「格子」を付けると「整数環上の」の意味になる。 格子空間＝格子自由加群＝基底付き格子自由加群…

https://leanprover.github.io/reference/tactics.html#basic-tactics This tactic applies to a goal whose goal has the form t ~ u where ~ is a reflexive relation, この言い回しにはさんざん悩まされた。「ゴール」に意味が。 証明状態 メインゴール …

Lean ILean 復CCC 論理 : ⇒ → → → → [,] ⊃ 空白 :: : (なし) ∧ ∧ × ∧ true true 1 T false false 0 ⊥ 空白区切り 空白区切り カンマ区切り カンマ区切り (なし) (なし) ストリング図 横棒図 命題 命題 対象 論理式 命題リスト 命題リスト 対象リスト 論理式…

システムの健全性 システムの十全性 システムの完全性 モデルと文の充足〈満足〉関係 文の充足可能性

論理 型 命題 型 命題Pの証明 型Tの式 証明内の根拠 式内の定数名 含意 関数型 前件 域型〈ソース型〉 後件 余域型〈ターゲット型〉 シーケント プロファイル 仮定 コンテキスト 結論 ターゲット 証明 証拠式 定理記述 オブジェクト定義 公理記述 定数宣言 …