Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points
share
Inductive and coinductive structures are everywhere in mathematics and computer science. The induction principle is well known and fully exploited to reason about inductive structures like natural numbers and finite lists. To prove theorems about coinductive structures such as infinite streams and infinite trees we can appeal to bisimulation or the coinduction principle. Pure inductive and coinductive types however are not the only data structures we are interested to reason about. In this paper we present a calculus to prove theorems about mutually defined inductive and coinductive data types. Derivations are carried out in an infinitary sequent calculus for first order intuitionistic multiplicative additive linear logic with fixed points. We enforce a condition on these derivations to ensure their cut elimination property and thus validity. Our calculus is designed to reason about linear properties but we also allow appealing to first order theories such as arithmetic, by adding an adjoint downgrade modality. We show the strength of our calculus by proving several theorems on (mutual) inductive and coinductive data types.
READ FULL TEXT