ガーッ！ 形式体系だった！！

論理 幾何っぽい 教育 形式言語理論 多義語

微分幾何計算は、形式体系とその意味論を使えば良かったのだ。灯台下暗し！ なぜに気付かない。こんなときは、自分の頭を殴りたくなる。

型記号

  1. Vector
  2. Scalar
  3. Covector

型演算

  1. ×
  2. (-)n

定数記号

  1. ∂i : Vector
  2. ωi : Covector
  3. ∂ : Vectorm
  4. ω : Covectorm
  5. πi : Scalar
  6. εi : Scalarm
  7. ∇i : Scalar → Scalar

オペレータ記号

  1. -[-] : Vector, Scalar → Scalar
  2. -[-] : Vector, Scalarm → Scalarm
  3. -・- : Vector, Scalar → Vector
  4. -・- : Scalar, Vector → Vector
  5. -・- はイッパイオーバーロード

典型な形式体系

  1. euclid(A) AはRmの開集合
  2. coord(s:M⊇→Rm) sはMのチャート
  3. euclid(s:M⊇→Rm) sはMのチャート
  4. manifold(M)

意味論の例

  1. 〚Scalar〛euclid(A) := C∞Rm(A)
  2. 〚Scalar〛coord(s) := C∞M(def(s))
  3. 〚Scalar〛euclid(s) := C∞M(img(s))
  4. 〚Scalar〛manifold(M) := C∞M(M)