Definition:Basic Primitive Recursive Function/Projection Function

From ProofWiki
Jump to navigation Jump to search

Definition

The projection functions $\pr_j^k: \N^k \to \N$ are basic primitive recursive functions, defined as:

$\forall \tuple {n_1, n_2, \ldots, n_k} \in \N^k: \map {\pr_j^k} {n_1, n_2, \ldots, n_k} = n_j$[1]

where $j \in \closedint 1 k$.


They are each URM computable by a single-instruction URM program.


Notation

  1. The usual notation for the projection function omits the superscript that defines the arity of the particular instance of the projection in question at the time, for example: $\pr_j$. However, in the context of computability theory, it is a very good idea to be completely certain of exactly which projection function is under discussion.