乱用の分類 構造・構成素の乱用、同型・等値の乱用

構造・構成素の乱用は、一番よくやるやつ。M = (M, *, e) とか。コジュール接続だと:

  • E = (E, S, ∇) where S = Γ(E)
  • S = (E, S, ∇)
  • ∇ = (E, S, ∇)

名前付き順序付きタプルを使って、 X = {v-bundle: E, sec-space, deriv: ∇} とすれば、

  • X.v-bundle = E
  • X.sec-space = S
  • X.deriv = ∇

v-bundle, sec-space, deriv を構造の構成素名、または役割名と呼ぶ。出現順で番号付けるとすれば:

  • X.1 = E
  • X.2 = S
  • X.3 = ∇

Coqと同様に、文脈型推論(出現する文脈の情報からの型推論)と強制グラフでオーバーロード解決が可能(たぶん)。

構造の定義のときに、構成素名〈constituent names〉と構成素順番〈constituent ordering〉を決める。乱用に使う強制アローを決めて、強制グラフを更新する。

用語法でも同じで、「V がベクトル空間である」から「(V, +, ・) がベクトル空間である」と読み替える。

同型・等値の乱用は、A \cong B を A = B と書くこと。これについては、同値類に落として解釈できることもあるが、矛盾が出ないかを注意深くチェックしなくてはならないので、かなり危険。合理化は難しい。典型事例は、V** = V 。