A Calculus of Circular Proofs and its Categorical Semantics
DOI:
https://doi.org/10.7146/brics.v8i15.20472Resumé
We present a calculus of proofs, the intended models of which
are categories with finite products and coproducts, initial algebras
and final coalgebras of functors that are recursively constructible
out of these operations, that is, mu-bicomplete categories. The
calculus satisfies the cut elimination and its main characteristic is
that the underlying graph of a proof is allowed to contain a
certain amount of cycles. To each proof of the calculus we associate
a system of equations which has a meaning in every mu-bicomplete
category. We prove that this system admits always a unique
solution, and by means of this theorem we define the semantics of
the calculus.
Keywords: Initial algebras, final coalgebras. Fixed point calculi, mu-calculi.
Bicompletion of categories. Models of interactive computation.
Downloads
Publiceret
Citation/Eksport
Nummer
Sektion
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
