First and second order recursion on abstract data types

This paper compares two scheme-based models of computation on abstract many-sorted algebras A: Feferman's system ACP(A) of "abstract computational procedures" based on a least fixed point operator, and Tucker and Zucker's system μPR(A) based on primitive recursion on the naturals together with a least number operator. We prove a conjecture of Feferman that (assuming contains sorts for natural numbers and arrays of data) the two systems are …