Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Coalgebraic Fuzzy geometric logic
The paper aims to develop a framework for coalgebraic fuzzy geometric logic by adding modalities to the language of fuzzy geometric logic. Using the methods of coalgebra, the modal operators are introduced in the languag…
Universal Reinforcement Learning in Coalgebras: Asynchronous Stochastic Computation via Conduction
In this paper, we introduce a categorial generalization of RL, termed universal reinforcement learning (URL), building on powerful mathematical abstractions from the study of coinduction on non-well-founded sets and univ…
Reinforcement LearningCoalgebras for categorical deep learning: Representability and universal approximation
Categorical deep learning (CDL) has recently emerged as a framework that leverages category theory to unify diverse neural architectures. While geometric deep learning (GDL) is grounded in the specific context of invaria…
Notes on Coalgebras in Stylometry
The syntactic behaviour of texts can highly vary depending on their contexts (e.g. author, genre, etc.). From the standpoint of stylometry, it can be helpful to objectively measure this behaviour. In this paper, we discu…
Optimising the topological information of the $A_\infty$-persistence groups
Persistent homology typically studies the evolution of homology groups $H_p(X)$ (with coefficients in a field) along a filtration of topological spaces. $A_\infty$-persistence extends this theory by analysing the evoluti…