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

モジュラーオペラッドを原圏〈urcategory | 原始圏 | ウル圏〉と呼ぶ。ウル〈ur-〉の意味は、https://www.etymonline.com/jp/word/ur- 「原始的な、初期の」という意味の接頭辞で、ドイツ語の「ur-」から派生しました。 ドイツ語の元々の意味は「外側、原始…

http://www.tac.mta.ca/tac/volumes/28/1/28-01.pdf を見てたら、 律子を coherent isomorphisms と呼んでいた。これは coherence isomorphisms と同義だ。 参照 → 一貫性の用語 - (新) 檜山正幸のキマイラ飼育記 メモ編また、sort を圏の種別の意味で使って…

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

全部事実上同義語。 平叙文 疑問文 型判断 型質問 シーケント 質問シーケント 関数定義 関数定義要求 定理記述 定理証明要求 クロージャ 大きいラムダ式 大きいタプル 大きいlet式

証明項の帰結という言葉を入れてみる。 型理論 論理 計算項 証明項 計算項の型 証明項の帰結 型付け〈typing〉 帰結付け〈consequencing〉 型{付け}?判断 帰結{付け}?判断 型チェック 命題チェック? 帰結チェック? 項の検証? 証明{項}?の検証 項の型推論 証…

関数の意味： 関数そのもの＝集合圏の射 関数定義 関数{定義}?ヘッド＋関数{定義}?ボディ 関数定義ボディは計算項 定理・証明の意味： 定理（証明）そのもの＝演繹圏の射 定理記述 定理{記述}?ヘッド＋定理{記述}?ボディ 定理記述ボディは証明項 「証明」の…

例によって用語がややこしい。 型述語は、value is string のような構文。タイピング述語、タイピング関係といったほうが良いが、「型述語」。これは、型ガード関数や型アサーション関数の戻り値位置に書く形式。 型ガードが実は述語〈ブール値をとる関数〉…

https://www.cs.vu.nl/~jbe248/lv2017/10x4.pdf より：the {type checking | proof verification} problem Γ |-? t:A the {typability | type {synthesis | inference}} problem Γ |- t:? the {{type | proposition} inhabitation | proposition provability…

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

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

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

レコードセットに名前が付いた集まり。各レコードセットは、圏の対象か射を表す。レコードは型定義で制約されている。つまり、型付きレコードセットの名前付き集まり。名前と型は別物。データセットから2-圏／二重圏を作るには、構造データ〈プロファイル・…

https://www.youtube.com/watch?v=r3yMSl5NB_Q を見ていたら出てきた。ELT〈Every Little Thing 〉ではない、ETL。Extract, Transform, Load → https://neo4j.com/blog/graph-etl-basics/以前書いた セレクト・モディファイ・フィル とまったく同じことだ。

次の階層を考える。 データ 解釈コンテキスト ボキャブラリーと型 データを解釈するには解釈コンテキストが必要。それをどう与えるか？ データとは別に与える → アウトオブバンドな解釈コンテキスト データ内にコンテキスト情報が入っている → インバンドな…

典拠コントロール〈Authority Control〉という言葉があるのだけど： 典拠コントロールの現 状と将来 Wikipediaのこの説明が分かりやすいかな。 各種の主題（著者・件名など）やその他の概念について、一貫した見出し・識別子を付与し、適切な相互参照を指示…

https://www.ifla.org/wp-content/uploads/2019/05/assets/cataloguing/frbr-lrm/ifla-lrm-august-2017_rev201712.pdf の Table 3.1 User Tasks Summary から： Find To bring together information about one or more resources of interest by searching o…

https://service.infocom.co.jp/das/loddiary/2017/01/20170127001583.html で神崎さんが使っている「資料オブジェクト」とはなんだろう？ 画像という著作の体現形だろうか個別資料だろうか？もし、商品としての著作を個別資料として購入したりすれば、「購…

https://id.ndl.go.jp/information/work/ より： 1-1. 著作典拠とは著作典拠とは、書誌データの検索の手がかりとなる「著作」の情報を整理してまとめたものです。「著作」とは、文字や音声などで表現される前の作品のアイディアそのものを表す概念です。たと…

著作と書誌情報の構造 - (新) 檜山正幸のキマイラ飼育記 メモ編 の「著作、表現形、体現形、個別資料」の区別はデジタルリソースでは難しいな。次のように呼ぶことにする。 著作：抽象的、著作権は著作に対するものなのだろう、おそらく。 α出版物： だいた…

曖昧、明瞭化したい。 作業 作業工程 過程、プロセス ワークフロー タスク アーティファクト〈成果物〉 デリバラブル〈成果物〉 プロダクト〈製品〉 プロダクション〈作成 | 製造〉 ビルド デプロイ デリバー イシュー チケット

確かムーアは論理式の集合の上の閉包作用素として演繹系を定義したと思う。アクツェルの推論系〈inference system〉の定義は以下のよう： 判断〈judgement〉の集合 U 演繹ルール〈deduction rule〉は A⊆U と c∈U の組 (A, c) 、これを A/c とも書く。 A を演…

情報隠蔽〈information hiding〉＝カプセル化〈capsulation〉＝ボクシング＝パッケージング 情報公開〈Information disclosure〉＝脱カプセル化〈de-capsulation〉＝アンボクシング＝アンパッケージング パターン＝テンプレート＝ワイヤリングスキーマ カプ…

Σ〈$`\Sigma`$〉なんらかの意味の指標、D〈$`D`$〉はドクトリンだとして、$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{ \text{ in } } \newcommand{\mrm}[1]{ \mathrm{#1} } %`$$`\quad \cat{C} = \mrm{Th}^D(\Sigma)`$とする。$`\cat{E}`$ を同…

困っている。 何がプレーンレンズ〈バニラレンズ〉か分からない。 元祖レンズの有法則／無法則は、まーハッキリしている。 単相レンズ〈monomorphic lens〉と双相レンズ〈ニ相レンズ | bimorphic lens〉の区別はあるが、一般的とも言えない。ヘッジーズ〈Hea…

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

型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, F) \to I) = \Pi(I, F)`$ 関数型ファミリーのセクション $`x \in \mathrm{Sect}(\pi:\Sigma(I, [F, G]) \to I) = \Pi(I, [F, G])`$ 一番は依存リストで、ニ番はインデックス付き関数〈indexed…

coherence nLab 一貫性の用語 続・一貫性の用語法 Wikipedia にある程度従うことにして： {一貫性の}?基本射〈elementary morphisms〉： 注目する生成射。 一貫性〈coherence〉： "various compositions of elementary morphisms are equal." であること。圏…

「依存アクテゴリーが面白い」という記事を書きました。実際僕は「面白い」と思っています。プロセスやシステムの記述と計算に使えそうだ、というところが心惹かれる理由でしょうかね。依存アクテゴリーはけっこう複雑な構造なので、定義を書き下すだけでも…

型・関数 命題・導出 0-射 型 0-射 命題 0-オペレータ 積 0-オペレータ 連言 0-オペレータ 指数 0-オペレータ 含意 0-射 指数型 0-射 含意命題 1-射 関数 1-射 導出 1-射 データ 1-射 保証〈ワランティー〉 1-射 入射〈余射影〉 1-射 証拠 1-射 射影〈成分〉…