# Useful algorithm not primitive recursive

The Ackermann function is the textbook example of a function which is total recursive but not primitive recursive.

If we want to implement it in some programming language we will need to use a priori unbounded loops (generally using while or goto).

I am looking for an algorithm used in real situations (e.g. in computational geometry or whatever field) that would implement a recursive function which is not primitive recursive (it doesn't need to be total). Such an algorithm would inherently require using a while loop.

Does such an algorithm exist?

• The typechecker for Coq programs :)
– cody
Jan 2 at 18:32
– cody
Jan 2 at 22:49
• A primitive recursive algorithm that is interesting nonetheless is a mutual recursion, the one found in quicksort's partition. Jan 3 at 18:22
• @KennethKho I assume you mean not primitive recursive? Quicksort's partition is primitive recursive though, and one can easily encode mutual recursion in primitive recursion (by taking in an extra bit to encode "which" function to call).
– cody
Jan 3 at 19:09

This question comes up from time to time, but I couldn't find an answer that I entirely loved so here's a take:

The main source of examples of non-primitive recursive functions that are still somehow total are evaluators for total languages which include primitive recursion!

This comes up whenever we want to give users the ability to express a wide range of programs, but want to prevent non-termination for whatever reason. The evaluator can easily be seen to be non-p-r for diagonalization reasons.

An example is in the Coq (soon to be Rocq) programing and proof language: with dependent types it may be necessary to evaluate a program at compile time, but the set of programs expressible includes much more than primitive recursive functions.

For example here is a program that evaluates factorial 5 at type-checking time:

Fixpoint fact (n : nat) :=
match n with
| 0 => 1
| S k => n * (fact k)
end.

/* This doesn't type-check with any other value than 120. */
Definition compute_fact_5 : fact 5 = 120 := eq_refl 120.