×

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

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.

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
PDF BibTeX XML Cite
Full Text: DOI

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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.