Example of terminating program that cannot be written in safe Agda

Question

In Agda with --safe, it is impossible to write a nonterminating program. Acknowledging the halting problem, it follows that there are terminating programs that cannot be written in safe Agda. But I want a constructive proof. :-)

To be more clear, I want an example of a function that can be proved to always terminate but cannot have a pointwise equivalent written in safe Agda. (And a proof on why it can’t.)

It would be nice to have examples of functions with finite and infinite different possible outputs. It would be specially nice if the proofs are easy to follow!

• zamfofex: When I wrote the question, I had no idea about how to even begin writing such a program or what such a program could even be. An answer briefly explaining what the program would even be (such as Jesper’s) is sufficient. I did search for an example, but I couldn’t find anything. Usually people just use the halting problem argument rather than providing an example.

Answer 1

The canonical example of a function that is terminating but cannot be implemented in Agda is an evaluator for Agda terms itself. If it were possible to implement, then we could use it to prove that there are no well-typed terms of the empty type, i.e. that Agda is sound, which would imply Agda is inconsistent by Gödel's incompleteness. (Note that the above is assuming Agda is consistent in the first place, i.e. it is talking about an idealized version of Agda rather than its actual implementation.)

• zamfofex: I’m confused by "we could use it to prove [...] that Agda is sound". If we imagine an Agda typechecker written in Agda, how does that imply "proving bottom is empty"? Our typechecker wouldn’t allow bottom to be proved, but that doesn’t mean we have proved it can’t. I don’t fully understand what "proving bottom has no well typed terms" even means. Also, I think there is still a bit of indirectness on your proof. Which is fine enough, but it incites the question "where would it go wrong if we tried?" As in, where would we "get stuck" and why couldn’t we overcome it?
• Naïm Camille Favier: Conor McBride gives a more direct diagonal argument in this post. I think the argument Jesper had in mind is something like: the evaluator should take a closed term of type "⊥" (the internal bottom type) to a normal form of that type, of which there are none by definition; thus the evaluator at that type has the type ¬ "⊥", which says that Agda is consistent as a logical system.