Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

TL;DR

This paper develops a fibrational framework linking initial algebras and final coalgebras, enabling the use of coinductive witnesses for inductive verification tasks, with applications to probabilistic liveness and automata.

Contribution

It introduces a general fibrational condition for the IA-FC coincidence, extending to monadic effects and providing new verification witness notions.

Findings

Fibrational IA-FC coincidence enables coinductive witnesses for inductive properties.

Framework applies to probabilistic liveness and tree automata verification.

Provides new upside-down witness notions for verification problems.

Abstract

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.