問い #241

Sheaf-valued acceptance ## Trigger infinite-word pointsを束ねる geometric morphism \[ \gamma:\mathbf{Sh}(\Sigma^\omega)\longrightarrow\Sigma\text{-}\mathbf{Set} \] を考えたとき、domain toposのsubobject classifierを随伴で押し下げれば、各stateにinfinite-word predicateを与える「受理対象」が現れるという観察から独立したテーマとして分離した。 ## Idea \[ \mathsf{Acc}_\gamma:=\gamma_*\Omega_{\mathbf{Sh}(\Sigma^\omega)} \] と置く。任意の \(\Sigma\)-set \(Q\) に対し、随伴から \[ \operatorname{Sub}_{\mathbf{Sh}(\Sigma^\omega)}(\gamma^*Q) \cong \operatorname{Hom}_{\Sigma\text{-}\mathbf{Set}}(Q,\mathsf{Acc}_\gamma) \] を得る。左辺のsubsheafを各stateで評価すると、open languages \[ L_q\subseteq\Sigma^\omega \] の族が現れ、少なくともderivative law \[ a^{-1}L_q=L_{q\cdot a} \] を満たすはずである。 ただし \(\Omega_{\mathbf{Sh}(\Sigma^\omega)}\) が直接分類するのはarbitrary subsetsではなくopen predicatesである。したがって直接得られるacceptanceはco-safety semanticsである。constant sheaf \(\underline{2}\) はclopen / bounded-prefix semanticsに対応し、Büchi・co-Büchi・parityへ進むにはleast/greatest fixed points \(\mu,\nu\) を追加する必要がある。 一般のsubobject-classifier adjunction自体は標準的であり、新規性の候補ではない。研究上の中心問題は、次の像を具体的に決定することである。 \[ \operatorname{Sub}(\gamma^*Q) \longrightarrow \prod_{q\in Q}\mathcal O(\Sigma^\omega), \qquad A\longmapsto(L_A(q))_{q\in Q}. \] ## Questions - derivative lawに加えて必要なeventual-state descent conditionは何か。 - 次の形のimage theoremは成立するか。 \[ \operatorname{Sub}(\gamma^*Q) \cong \left\{ (L_q)_{q\in Q} \ \middle|\ L_q\in\mathcal O(\Sigma^\omega),\quad a^{-1}L_q=L_{q\cdot a},\quad \text{descent} \right\}. \] - Jónsson--Tarski chart \(\mathbf{Sh}(\Sigma^\omega)\simeq\mathbf{JT}_\Sigma/F(1)\) を使うと、\(\mathsf{Acc}_\gamma\) は \(\Omega_{\mathbf{JT}_\Sigma}^{F(1)}\) の像として具体的に計算できるか。 - \(\Omega\) が与えるco-safety fragmentを \(\mu/\nu\)-completionし、Büchi・Muller・parity acceptanceとtopos-theoretic invariantを結べるか。 - subtopos \(\mathcal F\hookrightarrow\Sigma\text{-}\mathbf{Set}\) を変えると、そこで許されるacceptance classesはどのように変化するか。 ## Goal 一般的な「output assignmentを随伴でbehaviorへ移す」原理を再発見することではなく、\(\gamma\) に固有のacceptance objectとdescent条件を明示計算する。functorial automata、automata internal to topoi、coalgebraic trace semantics、safety/co-safetyおよび\(\omega\)-regular acceptanceとの正確な比較を行い、既知理論との差分を定理にする。 ## Personal context [[v6m2qz]] はpoints / observersとCantor chartの幾何を扱い、この瓶はそのchart上のpredicates / acceptanceを扱う。[[afv3c6]] のsubtopoi分類とは、どのlogical localizationでどのacceptance predicatesが残るかという方向で接続するが、論文テーマとしては分離する。 ## Related work to compare - functorial automata and adjunctions between languages and automata - automata internal to elementary topoi - safety and co-safety languages on \(\Sigma^\omega\) - coalgebraic Büchi/parity trace semantics via least and greatest fixed points - slice-topos identity \(\pi_*\Omega_{\mathcal E/X}\cong\Omega_\mathcal E^X\)