A recursive second order initial algebra specification of primitive recursion (Q1338890)

Theoretical results on the scope and limits of first order algebraic specifications can be used to show that certain natural algebras have no recursively enumerable equational specification under first order initial algebra semantics. A well known example is the algebra \({\mathcal P} {\mathcal R}\) of primitive recursive functions over the natural numbers. In this paper we show that \({\mathcal P} {\mathcal R}\) has a recursive equational specification under second order initial algebra semantics. It follows that higher order initial algebra specifications are strictly more powerful than first order initial algebra specifications.