STEM
信頼できる談話環境〈trustable discourse environment〉とは、そのなかでの発話行為、または記載（何かが書いてある）がそのまま事実と解釈してよい環境。一番外側の記述は、信頼できる談話環境のなかにあると考える。そうでないと、「‥‥はほんとうか？」の…
Tenjinが目指すのはコンポジショナル・ドキュメンテーション。 モジュラーである。抽象的モジュールを記述と呼ぶ。 CD圏の意味で結合とテンソル積ができる。 指標＝生成系で定義される自由CD圏がある。 自由CD圏の射は文書の論理的アウトライン＝リーディン…
ソフトウェアとして、リファレンス・マネージャーが必要かも。 リファラー →(リファレンス)→ リファレント IDはリファレントの生成時に決まり、パーマネント。それに対してニックネームがある。 リファレント側指定ニックネーム リファラー側指定ニックネーム…
リーディングパスと制御フロー 直列 ; 選択 AND, OR 入り口ガード 予備知識チェック 出口ガード 習得度チェック バックトラック 栞〈カーソル〉 ナビゲーションは、適切なリーディングパス／制御フローを提供するためのメカニズム。ナビゲーションは、適切な…
書籍構造： 伝統的な書籍（traditonal paper-based book）としての構造 論理構造： 記述すべき内容が持つ構造。論理アイテムから構成される。 ナビゲーション構造： 読者が読み進めるための構造 構造の生成〈供給〉と利用〈需要〉の関与者： 執筆者〈author …
アイテムの種類 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。そもそも大分類として： 資源アイテム： ファイル、ディレクトリなど、資源識別子で識別できるもの。その一部分であるテキストブロックなど。 文書アイテム： 部・章・節のような、伝統的な…
次のタグに関する実験をする。 STEM 半形式証明スクリプト xgerby stringer 実験の情報は、muses〈ミューゼス〉というタグにまとめる。今日のメモ： node.js のアップデートは、バイナリパッケージの再インストールだった。 npm のアップデートは nmp update…
レンダリング関係： 数式が使える。 ストリング図が描ける。 ペースティング図が描ける。 graphvizグラフが描ける。 構造関係： gerbyのような参照が出来る。 命題・証明の依存関係が出力可能。 指標が書ける。バンドルではなくて散在記述〈scattered descri…
命題が提示されると、提示されただけで真、または提示されただけで偽と即断しがち。真偽不明だと保留するのは苦手。 見た目上の相関があると、必然的相関だと考えがち。偶然的相関〈疑似相関〉だと考えるのは苦手。→ http://tylervigen.com/spurious-correla…
自然言語の印象・連想に影響されないで、必ず形式的な定義を確認する。 用語・記法には、合理的な根拠も一貫したルールもないので、個別に暗記する。 細部に神経を使う。例えば、空集合や単元集合、空集合／単元集合からの写像、空集合／単元集合への写像な…
命題が出現する文脈として、定理、予想、問題などがあるがハッキリと区別するために： assertion ： 「正しい」という判断を伴った主張。 judgement ： assertion と同じ。 demand ： 「正しい」ことが不明なので、証明の要求。 enquiry ： demandと同じ。問…
カリー化： 引数なし関数： f() = f(*) = f( () ) 要素とポインティングマップ： a = a() = a(*) タプルと関数： 要素と単元集合の意図的混同 要素と単元リストの意図的混同 引数内の囲み括弧省略： f( (x, y) ) = f(x, y) ニセの和（区切り記号としてのプラ…
話が通じない原因が全単射と可逆写像を別物だと思っていたことだった。たくさんの言葉があると、すべて同義語とは判断しにくいらしい。 全単射 双射 バイジェクション 可逆{写像 | 射} 同型{写像}? 1：1対応
"Canonical Structures for the working Coq user" by Assia Mahboubi, Enrico Tassi （https://hal.inria.fr/hal-00816703v1/document）の最初の段落： One of the key ingredients to the concision, and intelligibility, of a mathematical text is the …
多プロファイル 成分・書字順 成分・反書字順 成分・カリー化 f: → X f(*, x) f(x | *) f()(x) f: X → f(x, *) f(* | x) f(x)() f: → X, Y f(*, (x, y)) f(x, y | *) f()(x, y) f: X, Y → f((x, y), *) f(* | x, y) f(x, y)() f: X → Y f(x, y) f(y | x) f(…
上が新しい。 用語ペアの具体例 - (新) 檜山正幸のキマイラ飼育記 メモ編 用語ペアの関係性 - (新) 檜山正幸のキマイラ飼育記 メモ編 否定の接頭辞、拡張的形容詞 - (新) 檜山正幸のキマイラ飼育記 メモ編 排他的否定、拡張的否定、制限的否定 - (新) 檜山正…
format or template plan and materials performance or execution performer schedule media or channel
コンピューターサイエンスの学習は、職業エンジニアになることを阻害する https://zenn.dev/nakanishi/articles/d3d8ff5529832f2acf6c 言っていることは正しいし、こういう意見の人はけっこう多いけど、まとまった文章がないから助かる。記事を消してしまう…
印象 連想 憶測 共感 信頼
「用語ペアの関係性」の続き。 ⊆： 包含的 ⊆→ ： 規準的埋め込み可能 ⊥： 排他的 ∪： 総称 環、可換環、非可換環 用法 1： 環 ＝ 可換環 ⊆ 非可換環 用法 2： 可換環 ⊆ 非可換環 ＝環 用法 3： 可換環 ⊥ 非可換環、環 ＝ 可換環∪非可換環 数、単項式、多項式…
形容詞を 原子＝基本＝単純 として使おうと思っても： 原子論理式 ＝ 基本論理式 ＝ 単純論理式 ： OK 原子定理 ＝ 基本定理 ＝ 単純定理 ： 定理という名詞の意味から、基本定理、単純定理は別な連想が働く。 同義語扱いを増やすと、区別したいときに困る。…
基底変換、なにそれ？ - 檜山正幸のキマイラ飼育記 (はてなBlog) 「空間」と呼ぶが、空間ではないし（位相はないし）、群作用の特殊例。 随伴系はなぜ難しいか - 檜山正幸のキマイラ飼育記 (はてなBlog) 「ペア」と呼ぶがペアだけでは意味がない。
まだまだ改善の余地がある。コンパクト論理に限定するとして、 論理式＝生成対象の集合 F から作った自由コンパクト圏 原子証明＝生成射＝シーケントの集合 S から作った自由コンパクト圏 コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent r…
形式的に定義しない言葉 証明 → 証拠{図 | 式}またはリーズニング{図 | 式} 公理 → 原子定理 命題 → 論理式、定理 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式} 形式的に定義する言葉 項、原子項 論理式、原子論理式 文脈 シーケント 証…
多義語・曖昧語がオーバーロードのときもあれば、総称のときもある。オーバーロードと総称の境界はハッキリしない。 総称語は全体を意味するのであって、個別ケースにはあまり使われない。 オーバーロードされた語は個別ケースに使われるが、複数ケースで同…
「原子」「複合」 を使う。次の表の欄に入る語は正式なテクニカルタームとして定義する。 原子 (複合) 構成規則 項 論理式 証明 リーズニング リーズニングが一番ゴタゴタで、 証明{図}?の構成規則の概念とかぶる。 コンビネータ由来のリーズニングと、2-射…
同義語・類義語： 基本、組み込み、ビルトイン、単純、アトミック、原子{的}?、プリミティブ、原始{的}?、既約、分解不能、素、生成｛的｝? 同義語・類義語 英語： basic, builtin, simple, atomic, primitive, reduced, irreducible, indecomposable, prime…
負号 単項演算子（足し算の逆〈反対〉を取る、反数演算の記号） 二項演算子（反数との和） 負号としてのマイナス記号はなくてもいい。が、負数はリテラル表記できなくなる。 二項演算子記号もなくてもいいが、煩雑になる。
関係性は： 同義〈同一〉である。 排他的である。 包含的である。 所属的である。 同型である。 埋入的である。 その他。 言語の基本： 国、地域、（人の）集団、文脈、状況、場面などで意味と用法が変わる。例： (単項式, 多項式) (数, 単項式) (数, 式) (…
日常的な言葉を用語にする。例：やせた、広い、大きい、理論、一様、単調、建物 難しい言葉・造語を用語にする。例： 亜真接続付き多様体、特恵近傍系、特殊フロベニウス代数装備圏 メリット デメリット 1 親しみやすい。簡単そうな印象を与える。 専門用語…
