Categorial generalization of algebraic recursion theory (Q1898417): Difference between revisions

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.