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

微分幾何計算は、形式体系とその意味論を使えば良かったのだ。灯台下暗し！ なぜに気付かない。こんなときは、自分の頭を殴りたくなる。型記号 Vector Scalar Covector 型演算 × (-)n 定数記号 ∂i : Vector ωi : Covector ∂ : Vectorm ω : Covectorm πi : Sc…

構文論はコンピュータッド理論といえる。各次元の基本記号（セル | アトム）を決めて、基本記号のプロファイルは、下の次元の基本記号から構成される項（複合セル | ダイアグラム）で記述する。各次元の基本記号（セル）の意味（割り当て）が決まれば、アン…

ポンプの補題とその使い方： 回文の例 - 檜山正幸のキマイラ飼育記 (はてなBlog) へのuさんのコメント。言語Lに対する次の命題を想定しているようだ。 P(L) ≡ ∀w∈L.∀x, y, z.(w = xyz ⇒ x, y, z∈L) ￢P(L) ≡ ∃w∈L.∃x, y, z.(w = xyz ∧ ￢(x, y, z∈L)) Σ = {0…

ってことだと思う。 ダニエル・キレン Quillen equivalence in nLab 次のビデオだと、Quillenは「クーレン」に聞こえる。 https://www.youtube.com/watch?v=52HujNvYbAY