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

TypeScriptで宣言空間という独特の言葉を使う。「名前空間」と呼ばない理由は： 「名前空間」はファイルとは別なモジュールを意味するので、コンフリクトを避けた。 名前の容れ物というより、名前の分類基準に近い。 宣言された名前がどの種別かは： 変数名…

パッケージマネージャーとビルドツールは必要。 パッケージ直下の階層の存在物はモジュールでいいと思う。モジュールは物理ファイルに対応がわかりやすい。 スケルトンが何であるか？ の位置付けがよく分からない。 ビルドツールとバンドラーの境界線は確か…

宣言・定義ペアの完全な記述は under D assuming Σ declare k-x-mor f :k Γ →k A in M define f := Eここで： D はドクトリン。ドクトリンはメタ指標と文法からなる。ドクトリン配下の指標は、ドクトリンが定義した文法により記述する。 シグマは背景指標。…

セクションという呼び名が適切かどうか分からない（暫定）だが、そう呼ぶとして、セクションの構成素は： 背景指標 Γ 新規導入指標 Σ 定義済み指標 Δ 構成手続き φ : Γ+Σ → Δ セクションから、次の構成手続きも出来る。 φ': Γ+Σ → Γ+Δ Σは、次の可能性がある…

A Graphical User Interface Framework for Formal Verification https://drops.dagstuhl.de/opus/volltexte/2021/13899/pdf/LIPIcs-ITP-2021-4.pdf Design of point-and-click user interfaces for proof assistants https://www.chimaira.org/archive/ICFE…

Dは文書空間 D = {(v, l)∈V×L | v = dec(l)} とする。文書空間D内の文書族は、集合 S から Dへの写像。index family of documents のこと。一例として、I を文書IDの集合、Σ をツリー構造のパスセグメントラベルの集合。J をフラグメントIDの集合として、A =…

マルチパッケージをシングルリポジトリに突っ込むモノレポ構成は、文書作成に向いているかもね。ツールの類は ./node_modules/ にまとめて入れて、作業は ./packages/foo/ で行うとか。./packages/foo/ 自体もパッケージ構造を持つし、ワーキングフォルダに…

確認：欲しいもの - (新) 檜山正幸のキマイラ飼育記 メモ編 スケルトン - (新) 檜山正幸のキマイラ飼育記 メモ編 上記記事から言えることを以下に。スケルトンを静的に解釈すれば構造記述だが、動的に解釈すればDSLスクリプトになる。スクリプトは実行される…

まず、全体的にnpmエコシステムとunifiedエコシステムにはどっぷりと完全に依存する。npm, unifiedと一蓮托生。npmパッケージング・フォーマットとか配布〈ディストリビューション〉プラットフォームの仕様・機能・作法に従うし、べったり依存の方式を採用す…

スケルトン - (新) 檜山正幸のキマイラ飼育記 メモ編 にて： 再現性／追跡性を担保するにはバージョン管理の使用が必要になる。 過去の確認： git tag タグを表示 git log 通常のログ表示 git reflog HEADの移動履歴表示 チェックアウトする： git checkout …

なんか名前を付けないと呼べないから、コースや本の設計書的なヤツをスケルトンと呼ぶことにする。設計書の記述構文とファイルの両方ともスケルトンと呼ぶ。スケルトンは、（間接的に）実行可能なDSLプログラム。したがって、プログラミング言語のお作法で作…

原稿ファイル〈記事〉が置いてあるディレクトリをワーキングフォルダと呼ぶことにする。ワーキングフォルダ内の文書ファイル達〈ストックされた記事達〉は、なんらかの知性構造〈intelligence structure〉を持つと考える。欲しいもの／やりたいことは： 知性…

パフォーマーの起動〈invocation〉 関数呼び出し（プロファイルが必要） オブジェクトのメソッド呼び出し（メソッド名＋プロファイルが必要） パフォーマーの失敗結果〈failure result〉 エラー戻り値（規約が必要） 例外（モラルが必要； Error型データを投…

ハイパー文書の定式化には次が必要 文書空間： おおよそ文書型／データ型に相当する。外延的／構造的に定義する。 文書： おおよそ文書空間の要素。特定の文書型／データ型を持つ。 文書コレクション： 同じ文書空間に所属する文書の集まり。文書空間の部分…

まず、ソフトウェアコンポネントを、 プラグイン ドライバー に分ける。プラグインの種類を、 パーザー トランスフォーマー コンパイラ〈シリアライザー | ストリンギファイア〉 の3種に分ける。プラグインは、 アタッチャー パフォーマー に2つの部分からな…

https://github.com/redotjs/redot/blob/main/packages/redot-parse/redot-parse.js "use strict"; // generated by dot.pegjs var parser = require("./dot.js"); function parse(doc, file) { try { return parser.parse(file.contents || doc); } catch (…

https://github.com/retextjs/retext/blob/main/packages/retext-stringify/lib/index.js /** * @typedef {import('nlcst').Root} Root */ import {toString} from 'nlcst-to-string' /** @type {import('unified').Plugin<void[], Root, string>} */ export default function rete</void[],>…

unifiedドライバー（主にunified）と各種プラグインプロセッサ達が作る内部世界があって、それと外部世界を繋ぐグルーになるのが外部連結フレームワーク（と呼んでおく）。まず、unifiedエンジン（unifiedエンジン - (新) 檜山正幸のキマイラ飼育記 メモ編）…

ドライバー内蔵ではないプラグインパーザーの例： https://github.com/retextjs/retext/blob/main/packages/retext-english/lib/index.jsまず、使っているパッケージは https://www.npmjs.com/package/unherit と https://www.npmjs.com/package/parse-engli…

A = (A, ・, ε) はアクセッサのモノイドとaする。このモノイドは無限でもいいメンバー抽出演算子記号〈member extraction operator symbol〉からの自由半群。集合 X は、文書コレクション、つまり、親の文書空間の部分空間。文書コレクション X + {⊥} にモノ…

https://m-hiyama-memo.hatenablog.com/entry/2022/04/11/145718 の続き。https://github.com/unifiedjs/unified-engine より： import {engine} from 'unified-engine' import {remark} from 'remark' engine( { processor: remark, files: ['.'], extensio…

unifiedの分かりにくさ - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。unifiedフレームワークを整理する。 まず、テキストフォーマット＝テキスト型＝文字列型の部分集合型 がある。その例は、MD, HTML, JSON, TEXT など。 テキストフォーマットはファイ…

Tenjinの方針は“ありもの利用”だから、unifiedは使う。 いわゆる“unified plugin”はすべてそのまま利用したい。 remark-cli のようにコマンドラインから使いたい。 したがって、remark-cli と同じ作りにする必要がある。 設定ファイルもunifiedと共用できる…

https://github.com/remarkjs/remark から： import {visit} from 'unist-util-visit' /** @type {import('unified').Plugin<[], import('mdast').Root>} */ function myRemarkPluginToIncreaseHeadings() { return (tree) => { visit(tree, (node) => { if …

unifiedの分かりにくさは、プロセッサ〈プラグイン〉とドライバーの区別がハッキリせず、それらの役割が述べられてないことだろう。 プロセッサは何らかの文書処理をする。 プロセッサの入力と出力は前もって決められた〈仕様化〉された構造（mdast, hastな…

プラグインをドライブするものはドライバーと呼ぼう。unifiedはドライバーだが、remarkやretextもドライバーになっている。ドライバーの使い方は、 driver() .use(pluginA) .use(pluginB, pluginPramForB) .freeze() .process(input) .then(writerCallback);…

レッスンとコース - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き。知識は単にタームの集まり。タームの表現は単なる文字列。レッスン・レパートリーはレッスンの集まり。1-指標になっている。ソートは知識（タームの集まり）で、レッスンがオペレーション…

https://datatracker.ietf.org/doc/html/rfc6901 簡単な仕様だけど、「エスケープの趣味が悪い」という事情で嫌われるかも。 エスケープ文字は ~（チルダ）、チルダ＋番号1文字でエスケープシーケンス。 ~0 は チルダ自身 ~1 は スラッシュ 特殊な意味を持つ…

ハイパーリンクの使用法 トランスクルード： imgのsrc属性のようなもの。文書の一部として組み込む。JSON参照$ref はトランスクルード目的。遷移ではない。 関係性の記述： RDF や html meta-link とか。rel属性で関係の種類を指定する。静的で記述的。 ハイ…