[FOM] A System for Primitive Recursive Functions

[Rex Butler]

A System for Primitive Recursive Functions
------------------------------------------
[In ZFC, say, to begin.]

Let V = {v0,v1,v2,...} (Viewed as variable names).

Defined are primitive recursive functions of the form F: N^A --> N^B where
A and B are finite subsets of V.

A Preliminary:
Given finite subsets V1 and V2 of V and any function f: V1 --> V2 there
is a 'coordinate-wise' function N^_(f): N^V2 --> N^V1 by applying the
contravariant functor [N^_(f)](beta) = (beta o f).


The Initial Functions

1.  The coordinatewise functions, as above.

2.  Z: N^{} --> N^{v0} where

      Z({}) = (v0,0).

3.  S,P: N^{v0} --> N^{v0} where

      S({v0,y)}) = {(v0,y + 1)} and
      P({v0,y)}) = {(v0,y .- 1)}.

Closure Rules

1.  Composition

2.  Product:

      Given f: N^V1 --> N^V2 and g: N^W1 --> N^W2 the function given by

        (f x g)( {(v1,y1),...,(vm,ym) , (w1,z1),...,(wn,zn)} )
          equals
        f( {(v1,y1),...,(vm,ym)} ) union g( {(w1,z1),...,(wn,zn)} )

      where V1 = {v1,...,vm} is disjoint from W1 = {w1,...,wn} and
      V2 is disjoint from W2.

3.  Iteration: (As usual, except the iteration variable is passed along)

      Given f: N^A --> N^A such that v_m is not in A = {a1,...,an},

        rho(f): N^(A union {v_m}) --> N^(A union {v_m})

          where:

        rho(f)({(v_m,0),(a1,y1),...,(an,yn)})
          equals
        {(v_m,0),(a1,y1),...,(an,yn)}

          and

        rho(f)(  {(v_m,N+1),(a1,y1),...,(an,yn)} )
          equals
        f( rho(f)({(v_m,N ),(a1,y1),...,(an,yn)} )
           minus  {(v_m,N )} )
        union {(v_m,N+1)}.


Allowing multiple variables in the codomain as well as in the domain gives
the system a categorical flavor.  One motivation for this definition
is the desire that composition be allowed directly, rather than through
'generalized composition' which in the present sense is a bit of a misnomer.
Also, the stated modification allows the reduction of primitive recursion
to the special case of (parameter preserving) iteration, at the cost of the
addition of the function P.

A PRA proof system PRA_C based on these lines should be possible with the
following property: all rules have a single antecedent and a single consequent
except (and via) the categorical rule that
  |- f_1 = f_2 and |- g_1 = 1g_2 iff |- f_1 x g_1 = f_2 x g_2.

I am not directly aware of any category theory analogue to the formal
syntactic systems as found in universal algebra, though given such,
the syntactic presentation of the definition above would likely be
quite painless (A syntactic presentation of a strict monoidal category
containing the coordinate-wise functions would be a big start).

Any comments/suggestions are welcome.


Rex Butler