- Tenjin-MEDL(言語仕様), Tenjin-AA(API仕様)がある。
- MEDL = Mathematical Entity Description Language
- AA = Authoring Assistant software
- MEDLにはデータモデルとボキャブラリーが必要。
- データモデルとボキャブラリーが記述するものは: MEDLの世界と、世界内実体と、実体属性と実体間の関連
ボキャブラリーで決めるものは
- 世界の名前 → 指標の名前
- 型〈ソート〉の名前 → ソートの名前
- 関連の名前 → 射の名前
- 実体の型ごとの属性名 → 射の名前
- 関連の型ごとの属性名 → 高階射の名前
制約〈2-射〉、推論法則〈3-射〉もある。また、世界と世界のあいだの視標射=手続きもある。
Tenjin-MEDL が記述する世界達の世界内存在物=実体で、MathWorldの存在物をMathEntと呼ぶ。それを記述する世界の存在物をDescEntを呼ぶ。
大きな枠組み
存在物=実体=エンティティ=リソース を次のように分ける。
時間依存 | 時間非依存 | |
---|---|---|
デジタル | デジタルリソース | デジタルデータ |
現実 | 現実の事物 | (なし) |
概念 | ? | 普遍概念 |
とりあえず、現実の事物は時間に依存し、概念は時間に依存しないと考える。
略称を次のように決める。
- DigRes デジタルリソース
- DigData デジタルデータ
- RealRes 現実の事物
- ConEnt 概念的実体
MathEntはConEntの特別なもの。さらに、記述実体〈descripting entity〉をDescEntとする。
Tenjinが問題にするのは、
- DigRes かつ DescEnt である文書
- ConEnt のなかの MathEnt である数学的実体
物質的なRealResは扱わないので、単にDescEntと言えばDigResである。
DescEntは、MathEntを記述するが、その記述によりカバーできる範囲は[!カバレッジ]と呼ぶ。カバレッジはMathEntの集まりになる。
- 記述すること d : 記述実体 D → 概念世界 W
と考えると、カバレッジは像 d(D) ⊆ W となる。多様体の座標(むしろパラメータ表示)と座標近傍に対応する。
多様体の局所座標の変換と同様な変換を可能とするために、記述実体に対する部分記述実体と記述のあいだの変換の概念が必要になる。それが[!コネクター]になる。
概念実体を名指す名前の種類は:
- 指標固有名
- 指標のk-ラベル〈フィールド名〉
- 手続き固有名(しばしば無名となる)
- 手続きの余域指標の固有名(しばしば、手続き固有名の代わりに使われる)
- 手続きの余域指標のk-ラベル
- 手続きのk-ラベル=手続きの余域指標のk-ラベル
運用としては:
- 公理系の名前は指標固有名で与えられる。
- 公理系の個々の構成素、特に公理法則の名前は、指標のラベルで与えられる。
- 手続きが無名のときは、その余域指標の固有名が使われる。手続き名と指標名は別な名前空間として、ローカル名のオーバーロードを許す。
- 別なネーミングコンベンションとして、記述実体の(部分の)固有名を手続きの名前に使う。
- ローカル名としては、手続きラベルと余域指標ラベルは同じだが、宣言と定義の違いがある。余域指標のラベルは宣言=ステートメントだが、手続きのラベルは定義=証明も意味する。
- 現実的には、記述実体の名前から手続き名を作って、余域実体は無名とするのがよさそう。
- 定義の識別子/定理の識別子は、「手続き名+ローカルラベル」の形式でネーミング。
参照は:
- 公理系は指標固有名で参照。
- 公理は、「公理系名+ローカルラベル」
- 定義/定理は、「手続き名+ローカルラベル」
- 余域指標=目的指標〈objective signature〉に名前があれば、それを参照できる。
タームとトピック名とMathEntの識別子は一致させたほうがいいのかも知れない。MathEntの場合でも、次の区別がある。
- 指標名=構造体型名=型名≒分類タグ
- ラベル=フィールド名=プロパティ名=属性名=キー
- 名前空間名=スキーマ名=オントロジー名=ボキャブラリー名
指標名空間と手続き名空間は、パッケージ名空間の別な次元のパーティションと考える。オフィシャルな名前空間構造は:
- パッケージ名の名前空間
- パッケージ名の名前空間のパーティション名 0, 1, 2, ...
- パッケージ名/0/ の名前空間 = 指標名空間
- パッケージ名/1/ の名前空間 = 手続き名空間