[FOM] FoM: Recursive but not p.r. computable functions

[A.P. Hazen]

   Peter Smith's request was for a "natural" example, not cooked up by
diagonalization, of a recursive but not p.r. function, for pedagogical
purposes.  I don't KNOW of one, but I've got two pedagogical suggestions.
   (A) Continue using the classic example of the Ackermann function: the
proof that this is not primitive recursive is simple, easy to follow, and
beautiful, and the proof that it is recursive is simple, easy to follow,
and immediately intuitively convincing.  (I found the treatment in
Cutland's book "Computability" very clear.)
   Downside is that, though this is somewhat disguised when the Ackermann
function is given its usual elegant definition, the example is in origin a
diagonalization of the series of functions successor, addition,
multiplication, exponentiation, superexponentiation,
supersuperexponentiation....  (Tait, in his 1981 "Journal of Philosophy"
article "Finitism," uses the Ackermann function as an example of a function
naturally definable by a higher type recursion: this is very pretty and
informative (though if no one has pasted in the correction in your
library's copy, you might want to check errata in later issues of the
"Journal of Philosophy" for the formula left out when the article was first
published).)
   (B) For an example that is "naturally arising"-- a decision procedure
discovered by people interested in propositional logics, and actually
employed in computational research thereon-- and not cooked up by
diagonalization, let me  suggest the decision procedure for the relevance
logic LR, described in reference (1).  The proof that the decision
procedure 'works' (i.e. that we've got a (general) recursive total
function) is fairly simple and quite intuitive: the key lemma ("Kripke's
Lemma," essentially the well-foundedness of a certain orderingon multisets,
cf. ref (0)) is presented with a picture on pp. 171-173 of ref (2).  When
the authors of ref (1) implemented the decision procedure computationally,
the computer timed out on some formulas, but gave an answer on a reassuring
number of others.  The analysis of the complexity algorithm in ref (3),
however, gives a lower bound compatible with the function's being p.r. (but
still well into the "unfeasible") and an upper bound which could not be
p.r.  So the function MAY not be p.r., and certainly isn't OBVIOUSLY p.r.
---
References:
(0) R.K. Meyer and M.A McRobbie, "Multisets and Relevant Implication," in
"Australasian Journal of Philosophy" 1982 (perhaps in two parts?)
(1) P.B. Thistlewaite, M.A McRobbie, and R.K. Meyer, "Automated
Theorem-Proving in Non-Classical Logics," London: Pitman; New York and
Toronto: Wiley, 1988
(2) J.M. Dunn, "Relevance Logics and Entailment," in D. Gabbay and F.
Guenthner, eds, "Handbook of Philosophical Logic, v. III," Dordrecht:
Reidel, 1986
(3) A. Urquhart, "The complexity of decision procedures in relevance
logic," pp. 61-76 in J.M. Dunn and A.K. Gupta, eds, "Truth or Consequences:
essays in honor of Nuel Belnap," Dordrecht: Kluwer, 1990
---
Allen Hazen
Philosophy Department
University of Melbourne