2008/09/22 by Michael Pfender, Pfender, Michael
Computer Science · #03D75 #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.0809.3676
openalex publication_date 2008/09/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We give to the categorical theory PR of Primitive Recursion a logically simple, algebraic presentation, via equations between maps, plus one genuine Horner type schema, namely Freyd's uniqueness of the initialised iterated. Free Variables are introduced - formally - as another names for projections. Predicates χ: A -> 2 admit interpretation as (formal) Objects A|χ of a surrounding Theory PRA = PR + (abstr) : schema (abstr) formalises this predicate abstraction into additional Objects. Categorical Theory PRA \sqsupset PRA \sqsupset PR then is the Theory of formally partial PR-maps, having Theory PRA embedded. This Theory PRA bears the structure of a (still) diagonal monoidal category. It is equivalent to "the" categorical theory of μ-recursion (and of while loops), viewed as partial PR maps. So the present approach to partial maps sheds new light on Church's Thesis, "embedded" into a Free-Variables, formally variable-free (categorical) framework.