基本資料： タギングシステムとタクソノミーシステム - (保存用) 檜山正幸のキマイラ飼育記 メモ編 上記過去記事と少し用語を変えて： タグ空間：まま アイテム空間：まま タクソノミー： タグ空間とアイテム空間のあいだの関係 有限集合と関係の圏を $`{\bf…

リソース〈情報リソース〉：物理的な存在物 トピック〈概念トピック〉：概念的な存在物 トピックエントリー： リソースの一部で、トピックに対して記述している部分、曖昧かも知れない。 記述単位：メタデータや構造を提供する。コンテンツがアロケートされ…

デリバラブルは本来の意味として、デリバラブル・ジェネレーターで生成されるブツのこと。 名前空間のルートはパッケージ名とする。パッケージ名自体はURLなどで名付ける。 プロジェクト名、パッケージ名、ワールド名は一致させる。 パッケージの名前空間の…

Web IDL のソースは、https://w3c.github.io/webidl2.js/checker/ でチェックできる。はてなのシンタックスハイライトもある。 [Exposed] interface Description { getter sequence<DOMString> names(); attribute DOMString? id; getter sequence<DOMString>? requires(); };</domstring></domstring>

単一の記述プロファイル〈メタデータ〉は次のものから構成される。 記述のラベル〈名前〉 name ID id 語彙域 requires 事前要求記述 predecessors 語彙余域 provides 事後要求記述 successors コンテンツ〈メディアコンテンツ〉はアロケート〈allocate | fil…

出版物スケルトングラフ：スロットが埋められてない、伝統的書籍構造 執筆者アウトライン：スロットが埋められてない、流れや構成 スケルトン／アウトラインに対して、記述仕様〈description spcification〉があればバリデーションはできる。記述仕様は、記…

まず、階付き集合として、 $`G_0`$ ： 頂点の集合 $`G_1`$ ： 有向辺の集合 $`G_2`$ ： 有向二角形的多角形の集合 集合の要素を 0-セル、1-セル、2-セルと呼ぶ。各k-セルには次を付ける〈attach | add〉ことができる。 ID 一意 （XML id） ニックネームラベ…

記述の圏と語彙文脈ツリー$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\u}[1]{\underline{#1} } \newcommand{\cat}[1]{\mathcal{#1} } %`$語彙目録〈lexicon〉を対象として、記述〈description〉を射とする圏 を $`{\bf Desc}`$ とする。圏 $`{\bf De…

構文側： パッケージ名前空間 0次： コンテナ名〈モジュール名〉 1次： コネクタ名〈ビュー名〉 コンテナ名前空間 0次： 指標名 1次： 手続き名 指標名前空間 0次： ソート名 1次： オペレーション名 2次： 2-オペレーション名 (n + 1)次： 等式名 モデル側…

だいたいは分かるが念の為： AST ： 抽象構文木、構造のみ CST ： 具象構文木、テキストの情報をけっこう残す unist ： unifiedの構文木仕様、「ユニスト」でいいかな。 mdast ： Markdown（MD）のunisit特殊化、「ムダスト」でいいかな。 haast ： HTMLのun…

Tenjinが目指すのはコンポジショナル・ドキュメンテーション。 モジュラーである。抽象的モジュールを記述と呼ぶ。 CD圏の意味で結合とテンソル積ができる。 指標＝生成系で定義される自由CD圏がある。 自由CD圏の射は文書の論理的アウトライン＝リーディン…

ソフトウェアとして、リファレンス・マネージャーが必要かも。 リファラー →(リファレンス)→ リファレント IDはリファレントの生成時に決まり、パーマネント。それに対してニックネームがある。 リファレント側指定ニックネーム リファラー側指定ニックネーム…

リーディングパスと制御フロー 直列 ; 選択 AND, OR 入り口ガード 予備知識チェック 出口ガード 習得度チェック バックトラック 栞〈カーソル〉 ナビゲーションは、適切なリーディングパス／制御フローを提供するためのメカニズム。ナビゲーションは、適切な…

書籍構造： 伝統的な書籍（traditonal paper-based book）としての構造 論理構造： 記述すべき内容が持つ構造。論理アイテムから構成される。 ナビゲーション構造： 読者が読み進めるための構造 構造の生成〈供給〉と利用〈需要〉の関与者： 執筆者〈author …

アイテムの種類 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。そもそも大分類として： 資源アイテム： ファイル、ディレクトリなど、資源識別子で識別できるもの。その一部分であるテキストブロックなど。 文書アイテム： 部・章・節のような、伝統的な…

シェルスクリプトの仕様を記述する。 過去スクリプトの使い方 1 - (新) 檜山正幸のキマイラ飼育記 メモ編

失効2022-03-7にメールが来ていた。 Title: Let's Encrypt certificate expiration notice for domain "www.chimaira.org" From: Let's Encrypt Expiry Bot <expiry@letsencrypt.org> Hello, Your certificate (or certificates) for the names listed below will expire in 1 days (</expiry@letsencrypt.org>…

definition, variant definition axiom, fact theorem, lemma, proposition, corollary proof, variant proof remark warning, caution question exercise example convention construction note, info bibliography entry lead paragraph slogan （stacks p…

ID付与単位＝参照単位をアイテムと呼ぶ。IDサーバは、その管理範囲において一意性が保証されたIDを生成発行する。必ず新しいIDが生成発行される。 IDサーバーのAPI： createID():ID IDに対してニックネームを付けられる。ニックネームは生成・改名・削除〈CU…

まずはこれから： https://ncatlab.org/nlab/show/clone [0810.3162] Clone Theory: Its Syntax and Semantics, Applications to Universal Algebra, Lambda Calculus and Algebraic Logic [1205.3050] Operads, clones, and distributive laws

https://arxiv.org/abs/1505.00048 "PROPs for Linear Systems"(2015) by Simon Wadsley, Nick Woods より

[1505.00048] PROPs for Linear Systems [2012.01847] String Diagram Rewrite Theory I: Rewriting with Frobenius Structure [2104.14686] String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure [1812.05765] Graphical Regula…

Tenjinの0-指標はインターフェイス記述に使えるからIDLでもある。次が例題になる。 最小抽象ファイルシステム仕様をセミフォーマルに書いてみる - 檜山正幸のキマイラ飼育記 (はてなBlog)

if if if

Tenjin, a semiformal concept description language for STEM documents目標は、グチャグチャな古典微分幾何とか記述できるレベル。

https://www.sciencedirect.com/science/article/pii/S1567832610000068 The proof monad, 14p。対話的手続き的証明系のモナド定式化。ローカルに落とした、~/archive/ProofMonads.pdf これ読んでみたが、予想と違うことが書いてあった。証明モナドはモッジ…

ブログでのタグは： STEM 半形式証明スクリプト xgerby stringer ブックマークでのタグでは： proof-lang string-logic proof-shell tenjin tenjin-dev gergy tagging muses muses-dev とか。理論的背景は： https://math.mit.edu/~dspivak/informatics/olog…

次のタグに関する実験をする。 STEM 半形式証明スクリプト xgerby stringer 実験の情報は、muses〈ミューゼス〉というタグにまとめる。今日のメモ： node.js のアップデートは、バイナリパッケージの再インストールだった。 npm のアップデートは nmp update…

レンダリング関係： 数式が使える。 ストリング図が描ける。 ペースティング図が描ける。 graphvizグラフが描ける。 構造関係： gerbyのような参照が出来る。 命題・証明の依存関係が出力可能。 指標が書ける。バンドルではなくて散在記述〈scattered descri…