Useful algorithm not primitive recursive

Question

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?

Answer 1

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.