In total functional programming programs are restricted to total computable functions. A well-known class of total functions are the primitive recursive functions ($PR$). However the Ackermann function and others aren't part of $PR$. Is there a well-defined class of total functions which is broader than $PR$?

Bonus question: I heard lately about Walther and substructural recursion, but I can't find any information whether they are just another definition of $PR$ or different classes of total functions. Could you please clarify? Also a little example on how the definition differ from $PR$ would be great.


marked as duplicate by Raphael Jun 8 '16 at 21:02

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

  • 3
    $\begingroup$ What about R itself? Granted, there can be no programming language capturing exactly R, but that's not what you are asking. Or is it? In that case, see this related question. $\endgroup$ – Raphael May 29 '16 at 10:35
  • $\begingroup$ Basically I'm looking for a definition of total recursive functions which can capture more total functions than PR. Since R can not be captured, there must be various attempts to define larger subsets of R which can be captured. $\endgroup$ – Peter May 29 '16 at 12:44
  • $\begingroup$ Did you check the question I linked? $\endgroup$ – Raphael May 31 '16 at 15:43
  • $\begingroup$ The questions mentions Calculus of Construction (CoC, used by Coq), System F and System T. So, is CoC the largest set of well-defined total functions? $\endgroup$ – Peter Jun 8 '16 at 19:01
  • $\begingroup$ I don't know. Seems to me that would be a whole different question which you should post separately. (Should we close this one as a duplicate?) $\endgroup$ – Raphael Jun 8 '16 at 19:08