J. Xu and J.I. Zucker (2005):
First and second order recursion on abstract data types.
Fundamanta Informaticae, 67, 377-419.
(Based on Jian Xu's MSc Thesis, completed August 2003.)
[PDF]
Abstract.
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 equivalent. The main step in the proof is
showing the equivalence of both systems to a system Rec(A) of computation
by an imperative programming language with recursive calls. The result
provides a confirmation for a Generalized Church-Turing Thesis for
computation on abstract data types.