The Set of Primitive Recursive Functions

Grzegorz Bancerek

University of Bialystok, Shinshu University, Nagano

Piotr Rudnicki

University of Alberta, Edmonton

Summary.

We follow [31] in defining the set of primitive recursive functions. The important helper notion is the homogeneous function from finite sequences of natural numbers into natural numbers where homogeneous means that all the sequences in the domain are of the same length. The set of all such functions is then used to define the notion of a set closed under composition of functions and under primitive recursion. We call a set primitively recursively closed iff it contains the initial functions (nullary constant function returning 0, unary successor and projection functions for all arities) and is closed under composition and primitive recursion. The set of primitive recursive functions is then defined as the smallest set of functions which is primitive recursively closed. We show that this set can be obtained by primitive recursive approximation. We finish with showing that some simple and well known functions are primitive recursive.

This work has been supported by NSERC Grant OGP9207, NATO CRG 951368 and TYPES grant IST-1999-29001.

MML Identifier: COMPUT_1

Contents (PDF format)

1. Preliminaries
2. Sets of Compatible Functions
3. Homogeneous Relations
4. Primitive Recursiveness
5. The Set of Primitive Recursive Functions
6. Examples

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. Countable sets and Hessenberg's theorem. Journal of Formalized Mathematics, 2, 1990.

[3] Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.

[4] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[5] Grzegorz Bancerek. Cartesian product of functions. Journal of Formalized Mathematics, 3, 1991.

[6] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[7] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[10] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[12] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[13] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[14] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[15] Mariusz Giero. More on products of many sorted algebras. Journal of Formalized Mathematics, 8, 1996.

[16] Katarzyna Jankowska. Transpose matrices and groups of permutations. Journal of Formalized Mathematics, 4, 1992.

[17] Jaroslaw Kotowicz. Monotone real sequences. Subsequences. Journal of Formalized Mathematics, 1, 1989.

[18] Jaroslaw Kotowicz, Beata Madras, and Malgorzata Korolkiewicz. Basic notation of universal algebra. Journal of Formalized Mathematics, 4, 1992.

[19] Jaroslaw Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 5, 1993.

[20] Rafal Kwiatek. Factorial and Newton coefficients. Journal of Formalized Mathematics, 2, 1990.

[21] Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec, and Pauline N. Kawamoto. Preliminaries to circuits, I. Journal of Formalized Mathematics, 6, 1994.

[22] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.

[23] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[24] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.

[25] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[26] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[27] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[28] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[29] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.

[30] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[31] V. A. Uspenskii. \em Lektsii o vychislimykh funktsiakh. Gos. Izd. Phys.-Math. Lit., Moskva, 1960.

[32] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[33] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.