An exactification of the monoid of primitive recursive functions
type: Item
instance of: scholarly article
title: An exactification of the monoid of primitive recursive functions
zbMATH Open document ID: 1096.03048
published in: Studia Logica
publication date: 2006-03-17T00:00:00Z
review text: Let \(\mathcal{R}\)\ be a partially ordered category with involution \(\ast\), assuming that the hom-sets are \(\wedge\)-semilattices. The category \(\mathcal{R}\) is to be regarded as a category of relations, in which we can find a non-null subcategory \(\mathcal{C}\)\ of functions, namely, relations \(f:A\rightarrow B\) with \(ff^{\ast}\leq1_{B}\) and \(1_{A}\leq f^{\ast}f\). The authors are interested in two special cases. The first case is that \(\mathcal{C}\)\ is the monoid \(\mathcal{N}\)\ of primitive recursive functions \(\mathbb{N}\rightarrow\mathbb{N}\) and \(\mathcal{R}\)\ is the category of recursively enumerable relations on \(\mathbb{N}\). The second case is that \(\mathcal{C}\)\ is a regular category and \(\mathcal{R}\)\ is the category of relations constructed from spans in \(\mathcal{C}\). The authors note a similarity between the construction \(\widetilde{\mathcal{N}}\) from \(\mathcal{N}\) in the first case and the exact completion of \(\mathcal{C}\)\ in the second case, so that they want to bring these two constructions under one hat. One possible way with the first case would be to first embed \(\mathcal{N}\)\ in its regular completion and then apply the methods in the second case, which was already implicit in [\textit{P. J. Freyd} and \textit{A. Scedrov}, Categories, allegories. North-Holland Mathematical Library, 39. Amsterdam etc.: North-Holland. (1990; Zbl 0698.18002)]. This article aims to handle the first case by a one-step construction, which is very akin to the construction of the category of modest sets (\textit{G. Rosolini}, [Int. J. Found. Comput. Sci. 1, No. 3, 341--353 (1990; Zbl 0729.18003)] and \textit{E. S. Bainbridge} [Theor. Comput. Sci. 70, No. 1, 35--64 (1990; Zbl 0717.18005)]) as well as the idempotent splitting construction (Karoubi envelope) used in [\textit{J. Lambek} and \textit{P. J. Scott}, Introduction to higher order categorical logic. Cambridge Studies in Advanced Mathematics, 7. Cambridge etc.: Cambridge Universit…
Mathematics Subject Classification ID: 03D20
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 5013016
zbMATH Keywords: primitive recursive function
zbMATH Keywords: regular and exact category
zbMATH Keywords: pers
zbMATH Keywords: idempotent splitting completion
zbMATH Keywords: relation calculus
author: Philip Scott
author: J. Lambek
reviewed by: Hirokazu Nishimura
MaRDI profile type: Publication
full work available at URL: s11225-005-2765-x
OpenAlex ID: W2169540698
cites work: Functorial polymorphism
cites work: Exact categories and categories of sheaves
cites work: Q4304740
cites work: Regular and exact completions
cites work: Q3893911
cites work: Q5812175
cites work: Goursats Theorem and the Zassenhaus Lemma
cites work: Least fixpoints of endofunctors of cartesian closed categories
cites work: Q4896509
cites work: Diagram chasing in ordered categories with involution
cites work: Q3727946
cites work: Constructive natural deduction and its ‘ω-set’ interpretation
cites work: Q4003736
cites work: ABOUT MODEST SETS
DOI: 10.1007/S11225-005-2765-X
description: scientific article; zbMATH DE number 5013016