Categorial generalization of algebraic recursion theory. (English) Zbl 0867.03015

Zashev, J.

J. Pure Appl. Algebra 101, No. 1, 91-128 (1995).

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 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” [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.

Reviewer: S.V.Solov’ev (Durham)

MSC:

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

Keywords:

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

Citations:

Zbl 0149.26105; Zbl 0613.03018

References:

[1]	Ivanov, L.L., Algebraic recursion theory, (1986), Ellis Horwood Chichester · Zbl 0613.03018
[2]	Lambek, J., A fixpoint theorem for complete categories, Math. Z., 103, 151-161, (1968) · Zbl 0149.26105
[3]	Mac Lane, S., Categories for the working Mathematician, (1971), Springer Berlin · Zbl 0232.18001
[4]	Prawitz, D., Ideas and results in proof theory, () · Zbl 0226.02031
[5]	Skordev, D.G., Recursion theory on iterative combinatory spaces, Bull. acad. polon. sci. ser. sci. math. astr. phys., 24, 23-31, (1976) · Zbl 0328.02026
[6]	Skordev, D.G., Combinatory spaces and recursiveness in them, (1980), BAN Sofia, in Russian · Zbl 0452.03037
[7]	Skordev, D.G., Computability in combinatory spaces, (1992), Kluwer Academic Publishers Amsterdam · Zbl 0746.03039
[8]	Zashev, J., Recursion theory in partially ordered combinatory models, (), (in Bulgarian) · Zbl 0544.03020
[9]	Zashev, J., Recursion theory in B-combinatory algebras, Serdica bulg. math. publ., 13, 210-223, (1987), (in Russian) · Zbl 0654.03035
[10]	Zashev, J., Least fixed points in preassociative combinatory algebras, (), 389-397 · Zbl 0784.03028
[11]	Zashev, J., A type free abstract structure for recursion theory, Serdica bulg. math. publ., 17, 167-176, (1991) · Zbl 0782.03022
[12]	J. Zashev, Least fixed points in monoidal categories with cartesian structure on objects, Annuaire Univ. Sofia, Fac. Math. & Inf., to appear. · Zbl 0812.18006