「デジタル語彙目録:: 名前の管理」から：
ありていに言って、デジタル語彙目録作成は、
$`\qquad`$ひたすら名前との戦い
です。
本日も名前と戦っています。
デジタル語彙目録作成のために色々と試行錯誤しまして、紆余曲折ありまして、名前空間の構造や相互参照のやり方など、おおよその見当はついてきました。Obsidian（というソフトウェア）の画面キャプチャ画像をたくさん使って、現状を説明します。
内容：
ハブ記事：
語彙エントリー
全単分解〈全射-単射・分解 | surjection-injection {decomposition | factorization}〉という概念があります。写像〈関数〉を、全射と単射に分解することです。この概念に対するデジタル語彙目録の語彙エントリーがどんなものか、サンプルとしてお見せしましょう。
最上部のSurj Inj Decompという名前はノートの名前です。Obsidanでは、Markdownファイルをノート〈note〉と呼ぶのです。ノートの名前はファイル名から拡張子.mdを取り除いた名前で、事実上ファイル名です。ノート名〈ファイル名〉は、OSやアプリケーション（Obsidian）が取り扱う（コンピュータにおいて物理的な）名前で、概念の名前ではありません。
概念の名前は、見出し〈ヘディング〉に現れているSurjInjDecompです。ノート名とほぼ同じ名前にしてますが、それが必須ということではありません。概念に付けられたASCII文字列の名前をネームと呼ぶことにします。漢字の「名前」とカタカナの「ネーム」は、ここでのテクニカル・タームとしては別な意味です。「名前」は一般的な識別子のことで、「ネーム」は語彙エントリーが主題として扱う概念に付けられたASCII文字列の名前です。
ネームSurjInjDecompの前に付いているtypeは、このネームが型に付けられた名前であることを示します。概念記述の背景として、圏論的多宇宙依存型理論〈categorical multi-universe dependent type theory〉を使います。この型理論において名付けるべき対象物は型か関数のどちらかです。ネームSurjInjDecompは型の名前です。
ネームは、名前空間ツリーに配置されて管理されます。SurjInjDecompは、名前空間Basic配下に位置づけられます。ネームが入る名前空間は、namespaceで宣言されます（見出しの上）。よって、名前空間で修飾された長い名前は/Basic/SurjInjDecompです（実際はもっと長い名前になります、後述）。Basicの所にマウスをホバーすると、次のようなポップアップが現れます。
/Basic/SurjInjDecompという型は、なんらかの記述フォーマット〈記述構文 | 記述言語〉で記述されます（「曖昧さを減少させるために、式にフォーマット指定」参照）。その記述フォーマットは、described-inで指定します。今の場合の記述フォーマットはcategorical-signatureです。categorical-signatureの所にマウスをホバーすると、次のようなポップアップが現れます。
圏論的指標
/Basic/SurjInjDecompという型を、categorical-signatureフォーマットで記述するのですが、箇条書きを使っています。ひとつの箇条項目にひとつの構成素宣言を書きます。ひとつの箇条項目はさらに4つの部分に分かれます。
- 構成素の役割りを識別するASCII文字列の名前、ラベル〈label〉と呼ぶ。
- ラベルの別名であるシンボル。シンボル〈symbol〉とは数式内で使うLaTexコードの名前。シンボルが不要なら省略してよい。
- 構成素のプロファイル宣言
- 構成素（の型の）宇宙または銀河の宣言
4つの列を持つ表〈テーブル〉に書き直してみると次のようです。$`\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\In}{\text{ in }}`$
| 番号 | ラベル | $`\text{シンボル}`$ | $`\text{プロファイル}`$ | $`\text{宇宙・銀河}`$ |
|---|---|---|---|---|
| 1 | dom |
$`A`$ | $``$ | $`\mbf{Set}`$ |
| 2 | cod |
$`B`$ | $``$ | $`\mbf{Set}`$ |
| 3 | fun1 |
$`f`$ | $`:A\to B`$ | $`\mbf{Set}`$ |
| 4 | mid |
$`X`$ | $``$ | $`\mbf{Set}`$ |
| 5 | fun2 |
$`p`$ | $`: A\to X`$ | $`\mbf{Set}`$ |
| 6 | fun3 |
$`i`$ | $`: X\to B`$ | $`\mbf{Set}`$ |
| 7 | decomp |
$``$ | $`:: f \Rightarrow p;i : A\to B`$ | $`\mbf{Set}`$ |
| 8 | surj-ok |
$``$ | $`: \top \to \text{is-surj}(A, X, p)`$ | $`\mbf{Logic}`$ |
| 9 | inj-ok |
$``$ | $`: \top \to \text{is-inj}(X, B, i)`$ | $`\mbf{Logic}`$ |
ASCII文字列のラベルを使わずに、ラベルの別名であるシンボル（LaTeXで書く名前）だけを使って従来の構文で指標を書くと以下のようになります。シンボルが指定されてなくても、ASCII文字列と同じ綴りの名前のLaTeXバージョン*1が使えるとします。
signature $`\mathrm{SurjInjDecomp}`$ {
$`A \In \mbf{Set}`$
$`B \In \mbf{Set}`$
$`f: A\to B \In \mbf{Set}`$
$`X \In \mbf{Set}`$
$`p: A\to X \In \mbf{Set}`$
$`i: A\to X \In \mbf{Set}`$
$`\text{decomp} :: f \Rightarrow p;i : A\to B \text{ in }\mbf{Set}`$
$`\text{surj-ok} : \top\to \text{is-surj}(A, X, p) \In \mbf{Logic}`$
$`\text{inj-ok} : \top\to \text{is-inj}(X, B, i) \In \mbf{Logic}`$
}
Markdownで書かれた指標（上の画面キャプチャ）において、{/ と /} で囲まれた箇条項目は、省略可能〈optional〉な項目（「名前が指すモノ： 単射を例として」の最初の節を参照）です。例えば、$`A, B`$ を指定しなくても、$`f`$ の情報から $`A, B`$ は確実に推測できます。
さてところで、/Basic/SurjInjDecompという型を新たに定義するために、幾つかの名前（固有名であるシンボル）を使っています。
$`\quad \mbf{Set}`$
$`\quad \mbf{Logic}`$
$`\quad \top`$
$`\quad \text{is-surj}`$
$`\quad \text{is-inj}`$
これらのシンボルも名前なので、どこかで定義されている必要があります。そのような、“定義をするための事前の定義”はプレリュード（と呼ばれる記述）でされていると想定します。どのプレリュードを使うかは、語彙エントリーの頭のほうにあるprelude宣言で指定します。
ありとあらゆる名前が、どこかで定義（未定義用語だと宣言することも定義）されていて、正体不明の名前が紛れ込むことを排除します。
名前のフルネーム
概念に付けられた名前/Basic/SurjInjDecompは、ソフトウェアで管理される管理名〈managed name〉です。「デジタル語彙目録:: 名前の管理」で述べたように、管理名はURIとします。ネームのパス名だけでなくて、名前空間ツリーに責任を持つ組織や個人を識別するプレフィックスを付けます。
プレフィックスを$prefixとします。例えば、https://www.chimaira.org/hiyamaがプレフィックスの例です。プレフィックスまで含めた/Basic/SurjInjDecompのフルネームは、$prefix/Basic/SurjInjDecompです。より具体的にはhttps://www.chimaira.org/hiyama/Basic/SurjInjDecompとかですね。
URIを使って、概念に対して一意非曖昧〈unique unambiguous〉な名付けをします。もともと、デジタル語彙目録の動機（「デジタル語彙目録:: 動機と概要」参照）は同義語・多義語の問題ですから、一意非曖昧な名付けが出来ることは必須の要求です。
名前空間
名前空間ツリーは、Obsidianのなかのフォルダーツリーの形で実現しています。
ファイル名がほぼ名前空間名〈namespace name〉になっています。ファイル名の先頭についているのが絵文字ステッカー、末尾に付いているのはアイコンです。絵文字ステッカーとアイコンはひとつにまとめたいのですが、ソフトウェア（Obsidian）の都合でしょうがなく2つくっつけています。この絵文字／アイコンは、ファイルが名前空間であることを示す目印です。
同様に、記述フォーマット達もファイルにより表現されます。絵文字／アイコンは、パトカーのサイレンみたいな形です。
名前空間の絵文字／アイコンが揃ってないのは、単に僕が探して揃える作業をサボっているからです。こういう作業、意外とめんどくさい。
名前空間を表すファイルをObsidianで開くと次のようです。
実際のファイル名は先頭にns_が付いています。当該の名前空間に登録されたネーム、ラベル（定義されたラベルと使用されたラベル）が一覧になって出ます。左の列は、当該の名前空間の配下にある語彙エントリーのノート名〈ファイル名〉です。語彙エントリー（のノート）Nat remainderは次節で説明します。
この一覧表は、Obsidianプラグイン Dataview が自動生成します。
事例の事例
型には、その事例があります。型が集合だとは限りませんが、型は集合としての側面（外延と呼ぶ）を持ちます。よって、集合としての要素を持ちます。その要素を実例〈example〉と呼びます。「インスタンス」という言葉は、かなり複雑多様な意味を持つので、ここでは使わないことにします。
型理論では、$`x`$ が型 $`T`$ の実例であることを $`x:T`$ と書きます*2が、コロンの用法が圏論と整合しないので、次の代替記法も使います。
- $`x \text{ inhabits }T`$
- $`x \text{ is-a }T`$
- $`x \in: T`$
inhabitsという言い方に関しては「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」を参照してください。
型/Basic/SurjInjDecomp（プレフィックスは省略）の実例を記載した語彙エントリーは次のようになります。
Nat remainderと名付けられた実例は、型/Basic/SurjInjDecompの実例です。言い方を変えると、Nat remainderのアビタ〈居住地〉が/Basic/SurjInjDecompです。このことがhabitat宣言に書いてあります。アビタである型/Basic/SurjInjDecompは、語彙エントリーSurjInjDecomp（実際のファイル名には空白があるけど、ここでは詰めた）にあります。ここにマウスホバーすると、型の定義（である指標）をポップアップで見ることができます。
これはすごく便利です。読むときだけでなく、実例を書いている最中も非常に助かる。
この実例を書くために使ったフォーマットはcategorical-procedureですが、described-in categorical-procedureの所にマウスホバーすれば、もちろんcategorical-procedure〈圏論的手続き〉フォーマットの説明がポップアップします。
名前に関して、大文字・小文字や空白がイイカゲンなんですが、それは「デジタル語彙目録:: 名前の管理」で述べた正規化を仮定しているからです。まー、それにしてもイイカゲン過ぎますが、それはソフトウェア・チェックがなくて手作業だからです(苦笑)。
相互関係のグラフ
Obsidianのグラフビューは、Obsidianのウリの機能なのですが、実際に使ってみるとたいしたことないです。ノートのあいだの相互関係の視覚化としては非力・貧弱すぎて、あまり使えません。それというのも、グラフのノードやエッジに、ノート名〈ファイル名〉以外のラベルや装飾を付けられないからです。すべてのエッジが何の装飾もラベルもない線なので、見ても「どんな関係か」がサッパリわかりません。
今までに出てきた2つの語彙エントリーと1つの名前空間と2つのフォーマットをグラフビューで表示すると次のようになります。
ノードの形を変えたり色を付けたりもできないので、ファイル名の絵文字ステッカーで名前空間ノードとフォーマットノードを識別しています。グラフではわかりませんが、エッジの意味は次のようです。
Surj Inj Decomp-(namespace)→BasicSurj Inj Decomp-(described-in)→categorical-signature
Nat remainder-(namespace)→BasicNat remainder-(described-in)→categorical-procedureNat remainder-(habitat)→Surj Inj Decomp
おわりに
Obsidianとプラグインをやりくりして何とかデジタル語彙目録らしきものをでっち上げてみたのですが、Obsidian、もうちょっと機能が欲しい。もちろん、ノート取りアプリ／Markdownエディタとしてはとても強力で素晴らしいのですが、デジタル語彙目録作成にはだいぶ痒い。
名前の管理をしてくれるデータベースをバックエンドとして、LSP〈Language Server Protocol〉で通信しながら編集・閲覧とか出来たらいいのだけど。今のところ、適当な本体機能／プラグインが見つからないですね。当面、有り物をツギハギするしかないな。
とはいえ、ツギハギが可能となったのはObsidianとプラグインが存在したからで、感謝。
