多義語

半グラフの半辺

厳密には同義語ではないが。 半辺 枝〈branch〉(望月) 開放辺〈open edge〉 非接続辺〈dangling edge〉 フラグ ダート 外線〈external line〉 外部辺〈external edge〉 テール 外フラグ〈outer flag〉 外部フラグ〈external flag〉 脚 ヘア〈毛〉 リード〈…

曖昧表現、一様化、同一視

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

矢印記号の使用案

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

宣言、束縛子

名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。宣言=型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名…

コンストラクタ

帰納的型の値コンストラクタ記号 帰納的型の型名は、パラメータを持つと型コンストラクタ 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。 オブジェクト指向のコンストラクタは、単元集合またはパラメータ集…

まったくもう

postulate 公準 prerequisite 要請 assumption 仮定 antecedent 前件 premise 前提〈プロミス〉 hypothesis 仮説 context 文脈 environment 環境

アンステージ、削除、リセット、リストア

gitの誤認例:.gitignore, --squash - (新) 檜山正幸のキマイラ飼育記 メモ編 にて: 今まで、変な説明を見ても記録しなかったが、これからは記録に残そう。 https://qiita.com/ryosuketter/items/a6047b0270ea999fd51b 今回は、ステージングエリアから、ワ…

git用語の曖昧語

オブジェクトIDを何と呼ぶか? ID : 省略 オブジェクト : 識別子と参照対象物を同一視 リビジョン番号 : コミットオブジェクトの場合はそうなる コミット : 識別子と参照対象物を同一視、かつ参照対象物が特定のタイプのとき SHA-1 : オブジェクトIDの…

唯一射と対角射

終対象への唯一射や、単位対象への構造射 delete morphism descarder eraser discharger terminal morphism vanishing morphism bang garbage morphism(gs圏のこじつけ) counit もう一方の射は、 comultiplication duplicator copy morphism diagonal morp…

計算の構造

構文論: 基本概念 別名 ラベル 名前, 変数, 不定元, 定数, 識別子 シング n-射, もの, 実体, 具体物 割り当て 束縛, 代入, 関連付け〈association〉 リテラル 定数, 名前, 記号 コネクティブ 演算{子}?記号 コンビネーション 項, 式, 図式 ※ 論理のリテラル…

知識ベースの構造

リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉 宣言文は名前〈ラベル〉へのプロファイルの割り当て ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。 ハード定義文は名前〈ラベル〉…

意味論と構文論の整理

名前とラベルは同義語。束縛と割り当ては同義語。広義のタイピングとプロファイリングは同義。束縛にはハード束縛とソフト束縛がある(後述)。 束縛される前のラベルは変数 ハード束縛された後のラベルはリテラル 束縛の種類: ハード束縛: 名前〈変数〉に…

シーケントの用語

とある論文で使っていた用語法: シーケントの左辺 = antecedent〈前件〉 シーケントの右辺 = succedent〈後件〉 イニシャルシーケント = 公理シーケント シーケントの推論規則用語: 上式 = premises〈仮定〉 下式 = conclusion〈結論〉 前件、後件、…

証明の同義語

https://arxiv.org/abs/2102.03044 の冒頭、同語義: {mathematical | logical | rigorous | formal | rational}* {derivation | proof} 単なる多義語ならいいのだけど、実際には曖昧語になっているのがタチが悪い。

演繹システム

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

命題

真偽値 述語(述語関数、述語記号) 論理式 閉じた論理式 命題論理、述語論理を区別する形容詞 命題を論理文とも呼ぶ。

命題証明関係

使う言葉: 述語 → (述語関数 | 述語記号) 命題〈単純命題〉 構造化命題〈structured proposition〉 導出〈derivation | デリベーション〉 シーケント リーズニング 背景指標 導出可能〈derivable | デライバブル〉 使わない言葉: 判断 証明 推論 推論規則 …

指標の別名

指標はラベル〈名前〉の宣言文だけを並べたもの。別名は: セオリー: 指標をセオリーと呼ぶ人がいる。 文脈〈コンテキスト〉: 型理論ではよく使う。特に型シーケントの仮定側を文脈と呼ぶ。 束縛: 型付きラムダリストに現れる宣言の並びは束縛と呼ばれる…

コンストラクタ

(n, k)→(m, l)-コンストラクタ F とは: C はn-圏、|C|_k は C のk-射の集合 D はm-圏、|D|_l は D のl-射の集合 F: |C|_k ⊇→ |D|_l が、CからDへの(n, k)→(m, l)-コンストラクタ 部分写像でないときはフルコンストラクタ 例: (0, 0)→(0, 0)-コンストラクタ…

コンステレーション関係

terminology _ vocabulary コンステレーション { サークル ポート マーカー 向き付きサークル〈oriented circle〉 順序付きサークル = 向き付きマーカー付きサークル 方向付きサークル〈directed circle〉 方向付き順序付きサークル〈directed ordered circl…

シグマ型とパイ型

用法1 用法2 用法3 シグマ型 依存ペア型 依存積型 依存和型 パイ型 依存関数型 依存指数型 依存積型 description _ procedure Sigma from a Type A and a Family (F : A → |Set|) produces a Type S { // 省略 } procedure Pi from a Type A and a Family (F…

用語や学習法関連

TrRun4: 檜山トレラン4 X01 アットマークによる識別ヒント - HackMD 檜山トレラン4 E01 名付けのジレンマ - HackMD 檜山トレラン4 D01 混乱しがちな言葉 - HackMD 檜山トレラン4 B02 名前の使用法と導入時の半形式的記述 - HackMD 檜山トレラン4 B08 0-文法 …

構造的データ

terminology 構造的データ /* 参考: * セクションとタプル https://m-hiyama.hatenablog.com/entry/2022/06/14/153042 */ vocabulary 構造的データ-明確 { {インデックス付けられた}?集合族 インデックス集合 定数値の集合族 インデックス集合の要素 集合族…

オケージョンとナローイング

terminology _ vocabulary 論理-明確な語句 { 述語記号 真偽値集合の要素 集合圏の真偽値集合のn-直積を域として真偽値集合を余域とする射 集合圏の特定対象のn-直積を域として真偽値集合を余域とする射 集合圏の真偽値集合を余域とする射 自由変数を含む古…

統一的ボキャブラリーと常識的ボキャブラリー

terminology _ vocabulary 圏と射-統一的 { 0-圏 1-圏 0-圏の0-射 0-圏の1-射 1-圏の0-射 1-圏の1-射 1-圏の恒等1-射 1-圏の2-射 } context 圏と射-常識的 for 圏と射-統一的 { 集合 := 0-圏 圏 := 1-圏 集合の要素 := 0-圏の0-射 集合の要素の等値性 := 0-…

ボキャブラリー/コンテキストの構文

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 { パンダ := レッサーパンダ _ := ジャイアントパンダ _ :=…