Categorial generalization of algebraic recursion theory

DOI10.1016/0022-4049(93)E0184-6MaRDI QIDQ1898417zbMATH OpenFDO

Publication date 11 August 1997

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-4049(93)E0184-6

category of abstract programs and correctness proofs category of logical programs and correctness proofs fixpoints in categories least fixpoints multi-endofunctors operation spaces point-free recursion theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Abstract and axiomatic computability and recursion theory (03D75) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Review text

A categorical generalization of a point-free presentation of recursion theory, called ``algebraic recursion theory, is presented. Algebraic recursion theory studies least fixpoints (least solutions of systems of inequalities) in partially ordered universal algebras (poalgebras) with operations, monotone in each argument. The categorical generalization of this approach uses instead of a poalgebra a category \(C\) with a set of multi-endofunctors, and an appropriate generalization of inequalities; least fixpoints are taken in the sense of \textit{J. Lambek} [``A fixpoint theorem for complete categories, Math. Z. 103, 151-161 (1968; Zbl 0149.26105)]. The problem to be solved is formulated in the following way: given such \(C\), find a simple set \(B\) of inductively definable multi-endofunctors, such that for every \(F:C^{n+m}\to C^m\) (a) the least fixpoint of \(F\) exists and (b) is explicitly expressible by means of basic multi-endofunctors and these form \(B\). This problem is solved for so called DM-categories, suggested by the author. They are categorical generalizations of ``operation spaces [\textit{L. L. Ivanov}, Algebraic recursion theory (1986; Zbl 0613.03018)]. Their structure is a combination of monoidal and Cartesian structure. There are three main examples; one is defined using a category of all categories with certain properties (initial object, direct limits of \(\omega\)-sequences, etc.); two others are the category of abstract programs and correctness proofs and the category of logical programs and correctness proofs.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Categorial generalization of algebraic recursion theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1898417)