alternative characterization of primitive recursiveness


One useful feature regarding the extended notion of primitive recursiveness described in the parent entry is that it can be used to characterize the original notion of primitive recursiveness. As in the parent entry, we use the notation

๐’ฎ:={f:โ„•mโ†’โ„•โˆฃanyย mโ‰ฅ1},๐’ฑ:={f:โ„•mโ†’โ„•nโˆฃanyย m,nโ‰ฅ1}.

In addition, let

๐’ฑโข(m,n):={fโˆˆ๐’ฑโˆฃf:โ„•mโ†’โ„•n}.

Finally, denote ๐’ซโขโ„› the set of primitive recursive functionsMathworldPlanetmath in the traditional sense (as a subset of ๐’ฎ), and ๐’ซโขโ„›โ€ฒ the set of primitive recursive vector-valued functions (a subset of ๐’ฑ). It is clear that ๐’ซโขโ„›=๐’ซโขโ„›โ€ฒโˆฉ๐’ฎ.

Let ๐’Ÿ be the smallest subset of ๐’ฑ such that

  1. 1.

    ๐’Ÿ contains the zero function z, the successor function s, and the projection functions pmk (see the definition of primitive recursive functions for more detail),

  2. 2.

    ๐’Ÿ is closed underPlanetmathPlanetmath functionalPlanetmathPlanetmathPlanetmath compositionMathworldPlanetmathPlanetmath in ๐’ฑ,

  3. 3.

    ๐’Ÿ is closed under extensionPlanetmathPlanetmathPlanetmath of coordinates: that is, if f1,โ€ฆ,fnโˆˆ๐’ฑโข(m,1) are in ๐’Ÿ, so is f:=(f1,โ€ฆ,fn)โˆˆ๐’ฑโข(m,n), given by fโข(๐’™)=(f1โข(๐’™),โ€ฆ,fnโข(๐’™)),

  4. 4.

    ๐’Ÿ is closed under iterated composition: if fโˆˆ๐’ฑโข(m,m) is in ๐’Ÿ, and so is gโˆˆ๐’ฑโข(m+1,n), given by gโข(๐’™,n)=fnโข(๐’™) (where f0 is the identity function).

We now state the characterization.

Proposition 1.

๐’ซโขโ„›โ€ฒ=๐’Ÿ.

Proof.

First, observe that condition 1 is satisfied by both ๐’ซโขโ„›โ€ฒ and ๐’Ÿ. To see that ๐’ŸโŠ†๐’ซโขโ„›โ€ฒ, note that condition 3 is just the definition in the parent entry, and conditions 2 and 4 are discussed and proved, also in the parent entry. So we have one inclusion. To see the other inclusion ๐’ซโขโ„›โ€ฒโŠ†๐’Ÿ, we need to verify the two closure properties:

  1. 1.

    functional composition (in ๐’ฎ): suppose g1,โ€ฆ,gmโˆˆ๐’ฑโข(k,1) and hโˆˆ๐’ฑโข(m,1) are in ๐’Ÿ, we want to show that f:=hโข(g1,โ€ฆ,gm)โˆˆ๐’ฑโข(k,1) is in ๐’Ÿ too. First, form g=(g1,โ€ฆ,gm). Then gโˆˆ๐’Ÿ by extension of coordinates. Then f=hโˆ˜gโˆˆ๐’Ÿ by functional composition (in ๐’ฑ).

  2. 2.

    primitive recursion: suppose gโˆˆ๐’ฑโข(k,1) and hโˆˆ๐’ฑโข(k+2,1) are both in ๐’Ÿ, we want to show that fโˆˆ๐’ฑโข(k+1,1) given by fโข(๐’™,0)=gโข(๐’™) and fโข(๐’™,n+1)=hโข(๐’™,n,fโข(๐’™,n)) is in ๐’Ÿ too. First, define a function Hโˆˆ๐’ฑโข(k+2,k+2) by

    Hโข(๐’™,y,z):=(๐’™,sโข(y),hโข(๐’™,y,z)).

    Then H is formed by extension of coordinates via the projection functions pik+2 (with i=1,โ€ฆ,k) producing the first k coordinates (the coordinates of ๐’™), the function sโˆ˜pk+1k+2 producing the k+1st coordinate sโข(y), and h producing the last coordinate. Since each of the coordinate functions is in D, so is H.

    Next, the function Fโˆˆ๐’ฑโข(k+3,k+2) given by Fโข(๐’™,y,z,m)=Hmโข(๐’™,y,z) is in D by iterated composition. We now verify by inductionMathworldPlanetmath on n that

    Fโข(๐’™,0,gโข(๐’™),n)=(๐’™,n,fโข(๐’™,n)).
    • โ€“

      F(๐’™,0,g(๐’™),0)=(๐’™,0,g(๐’™), and its third coordinate is fโข(๐’™,0), as desired.

    • โ€“

      Suppose now that Fโข(๐’™,0,gโข(๐’™),n)=(๐’™,n,fโข(๐’™,n)). Then

      Fโข(๐’™,0,gโข(๐’™),n+1) = Hโข(๐’™,n,fโข(๐’™,n))
      = (๐’™,sโข(n),hโข(๐’™,n,fโข(๐’™,n)))
      = (๐’™,n+1,fโข(๐’™,n+1)).

    As a result, fโข(๐’™,n)=pk+2k+2โˆ˜Fโข(๐’™,0,gโข(๐’™),n) is in ๐’Ÿ also.

Therefore, ๐’ซโขโ„›โ€ฒโŠ†๐’Ÿ, and the proof is completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. โˆŽ

Remark. According to the characterization above, one sees that primitive recursion is in a sense a special form of iterated composition. The above characterization is helpful in proving, among other things, that every URM-computable function is recursive, and that the Ackermann function is not primitive recursive.

Title alternative characterization of primitive recursiveness
Canonical name AlternativeCharacterizationOfPrimitiveRecursiveness
Date of creation 2013-03-22 19:06:44
Last modified on 2013-03-22 19:06:44
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 5
Author CWoo (3771)
Entry type Result
Classification msc 03D20