$`x = f(x)`$ $`x \ne f(x)`$ これの解釈： $`\forall x\in X.\, x = f(x)`$ $`\exists x\in X.\, x = f(x)`$ $`\forall x\in X.\, x \ne f(x)`$ $`\exists x\in X.\, x \ne f(x)`$ 関数レベルでの等式： $`\mathrm{id}_X = f`$ $`\mathrm{id}_X \ne f`$

気力がなくなる理由： 何のためにやるのか分からない。動機不足、不毛感、虚無感。 何をやったらいいか分からない。困惑感、不安感、無力感。 難しすぎる。どうせ無理。徒労感、劣等感。 目標と前提： ターゲット 前提（過程、仮説）、あるいは資源〈リソー…

「このデータは、Windows のエクスプローラーに保存されます。」のような言い方を聞いた。おそらくだが、「エクスプローラー」が「ファイルシステム」のような感じなのだろう。ソフトウェアの固有名詞と、そのソフトウェアが実現する一般的な機能やメカニズ…

類似 るいに るいじ 白湯 しろゆ ぱいたん コロナ禍 ころなうず ころなか 凡例 ぼんれい はんれい 破綻 はじょう はたん 嫡男 てきなん ちゃくなん 具象 ぐぞう ぐしょう 出汁 でじる だし

変な推論の分類を見た。それは無視して僕の分類。 演繹 vs. 経験的帰納法 「経験的」は「数学的」と区別して。 論理的推論 vs. アブダクション（日常的に多用される非論理的推論） 経験的帰納法とアブダクションの境界は難しい。が、アブダクションのなかに…

帰納的にデータ型を定義するとき：$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression \newcommand{\T}[1]{ \text{#1} } \newcommand{\B}[1]{ \m…

カリー／ハワード／ランベック対応を徹底するには： calc/compute（動作・行為）とprove（動作・行為）proof（すること）を同義とする。 function returns a velue of type T と theorem returns a witness of prop T を同義とする。 prop は広義の型の一種…

名前空間、知識記述〈knowledge description〉の名前空間と用語レキシコンの名前空間は別。 名前空間名と名前空間階層ツリー 名前の分類子、分類子による名前空間のパーティショニング。異なるパーティションの同一ローカル名は異なる。 「名前空間名」は名…

テンプレートは、穴〈スロット〉を埋めることにより具体物を作り出すことが目的。 穴〈スロット〉がないテンプレートをリテラル・テンプレート、あるいは単にリテラルと呼ぶ。それだけで具体物。 穴が実際にあるテンプレートは非リテラル・テンプレート。「…

in◯◯, un◯◯, non-◯◯, dis◯◯, ◯◯less◯◯, ◯◯ without ◯◯、非◯◯、不◯◯、無◯◯、◯◯なし◯◯ など。用法： 制限的用法 拡張的用法 排他的用法 冗長な用法 非可換／可換： 拡張的用法： デフォルトで環が可換のときの、非可換環。スーパー指標を追加して、既存指標「…

同義語句による置き換え〈replacement〉 例： pointing function ＝ example 変形ルールによる変形 例： example of type Nat named k → example k returns type Nat 省略可能な情報の省略と補完 例： type T → type T in U 注記情報の追加と削除（これも省…

$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression `$$`\text{volatile namespace}\\ \text{we define function }\NN{f1}\\ \quad \text{by pos…

define applying end が定義の構文だが、キーワード applying の直後に記述フォーマット名を付けてよい。つうか、付けるのが推奨。 applying record-schema-template-diagram ◯◯ end applying record-schema-template-text ◯◯ end applying standaard-arithm…

次は同義 $`\text{we define example of type }T \text{ named }e`$ $`\text{we define pointing function } e \text{ returns type }T`$ example〈事例 | 具体例〉は pointing function に展開されるが、of は語順を変えてしまう。of は戻り値型を先に記述…

トピックワードとは、記述本体内に散在して出現するワードで、トピックを表すキーワード。以下、実際に予定しているトピックワード。 基本データ型 基本データ値 複合データ型 複合データ値 自然数による非負有理数の構成 自由な帰納的構成 自由な相互再帰的…

使用法変種とは usage variant 、使用法により記号が変化する。本質的な意味は変わらない。 $`\mapsto`$ ： 割り当て単位〈assignment unit〉を記述する。 $`:\in`$ ： 割り当てが、所属宣言であることを示す。 $`:=`$ ： 割り当てが、代入単位であることを…

中括弧の使用法が、列挙記法〈外延的記法〉と内包的記法で違いすぎる。暫定的だが、記法を決める。 集合の列挙記法： $`\{a, b, c\}`$ 集合の名前隠蔽内包的記法： $`\{\!| x :\in X \mid \cdots |\!\}`$ 縦棒を追加、厳密にZFCの意味で使う。ただし、$`\{\!…

リスト／タプル囲み括弧（具体データ構成子記号／型項構成子記号の一部と考える） 引数囲み括弧（評価演算の二項演算子記号の一部と考える） 演算の優先度括弧（パーズツリーに影響する） まとまり括弧（パーズツリーに影響しない） 規則と注意 引数囲み括弧…

$`\newcommand{\Imp}{\mathop{ =\!\!\triangleright }} \newcommand{KER}{ \mathrel{\stackrel{\rightharpoonup}{\sim}} } % Kleene Equarity Right \newcommand{KEL}{ \mathrel{\stackrel{\leftharpoonup}{\sim}} } % Kleene Equarity Left \newcommand{\le…

主語 we 動詞 declare, define, approve〈アプルーブ〉 副動詞 request, respond 名前の修飾語 type, function typeへの副修飾語 logical, type-param, prop-param functionへの副修飾語 section, bundle, type-velued, prop-valued, partial 終止語 end そ…

主動詞： declare〈宣言する〉, define〈定義する〉, approve〈承認する〉 副動詞： request〈要求する〉, respond〈応答する〉 主語は We, One of us, I だが、省略可能。組み合わせは： declare 名前 仕様 ： 名前を宣言する。存在に関しては中立。 declar…

記述の事例： 圏論/小さいとは限らない【形】 -(同義)→ 圏論/大きい 圏論/小さくない【形】 -(同義)→ 圏論/真に大きい 圏論/大きい集合 -(同義)→ 集合論/クラス 圏論/小さい集合 -(同義)→ 集合論/集合 圏論/小さくない集合 -(同義)→ 集合論/真のクラス 一般/…

定義的等号と命題的等号の区別が問題になるが、もっと問題なのは、宣言的所属関係と命題的所属関係だろう。宣言的＝合意形成的、命題的＝問題提示的所属的所属関係も $`\in`$ で書かれる。$`:`$ も使うが、宣言的所属関係を $`:`$ で書くと、圏論のコロンの…

曖昧表現は： 名前・記号の借用 例： G = (G, *, 1) 省略 例： G = (G, *) 名前・記号の多義的使用〈オーバーロード〉 曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧…

次の計算系がある。 計算対象物 CC圏 CC複圏 CC多圏 （広義）射 ◯ ◯ ◯ コンビネータ △ ◯ ◯ アレンジメント △ ◯ ◯ CCは Cartesian Closed ◯：うまく定式化できる。 △：ある程度は定式化できる。 演算： 射に対して： 結合、直積、カリー化、評価 コンビネータ…

lambda ： ラムダ抽象 assume backlog ： バックログラムダ抽象 postulate / demand 要請、ラムダ抽象だがバックログだとマークする。ラムダ変数はバックログ変数＝スタブ＝ダミー。 prepare ： 引数の準備 next ： 区切り記号 and_also ： 区切り記号 end …

関数があるとき、引数型と戻り型の仕様が型プロファイル、単にプロファイルとも呼ぶ。プロファイル概念は集合圏の射以外でも考えられる。引数変数を含む項を使って関数を定義するときの $`\cdots \mapsto \cdots`$ は戻り値指定〈return value disignation〉…

視点移動とフットワーク： 階層的宇宙のなかで自分がどこのいるのか？ 区別する／区別しない（同一視する／しない）、どちらの立場か？ 例： 引数なし関数名と定数名 名前が定数名〈固有名〉か変数名〈不定名〉か？ スコープに依存（事項）。 名前のスコープ…

$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは：$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}