オートマトンの観測ホモトピー論

次のいずれかの構造をホモトピー様構造と呼ぶことにする。

  1. キレン・モデル構造
  2. ホモトピー的構造〈homotopical structure〉
  3. 相対構造

対応するホモトピー様構造を持つ圏〈category with homotopy-like structure〉は:

  1. キレン・モデル圏
  2. ホモトピー的圏
  3. 相対圏

いずれの場合でも、弱同値射の部分圏は持つ。Cホモトピー様構造を持つ圏だとして、その弱同値射の部分圏をWとする。局所化 C[W-1] を Ho(C) と書いて、Cホモトピー圏と呼ぶ。定義より、Cの弱同値射はHo(C)では同型射になる。



Automをなんらかの意味のオートマトンの圏だとする。Obs:Autom→Beh を、オートマトンにその振る舞いを対応させる観測関手とする。A, B in Autom に対して、

  • A ~obs B :⇔ Obs(A) = Obs(B)

と定義する。この同値関係を、観測同値(または振る舞い同値)と呼ぶ。

オートマトンの観測ホモトピー論の目標はシンプルで、次を実現したい。

  • 圏Automにホモトピー様構造を載せて、
    A ~obs B in Autom ⇔ A \stackrel{\sim}{=} B in Ho(Autom) とする。

上記を満たすホモトピー様構造を、観測関手と整合すると形容する。

オートマトンの観測ホモトピー論は、観測関手と整合するホモトピー様構造を持った圏の理論だが、そのような圏をすべて考えたいので、「観測関手と整合するホモトピー様構造を持った圏」の圏の理論となる。個々の圏ではなくて、圏の圏の構造が問題になる。特に、キレン同値のような“弱同値”が重要だから、結局は「オートマトンの観測ホモトピー論のホモトピー論」。