# Coq — non-terminating programs [duplicate]

People usually say Coq does not allow writing non-terminating functions. I have a question regarding that.

Does Coq allow writing exactly all terminating functions? In other words, what are the completeness and soundness properties of Coq's procedure for checking well-foundness of fixpoint definitions?

• Questions about specifics of programming languages are usually off-topic here; the underlying conceptual question that answers yours already has answers on the site, though. – Raphael May 2 '14 at 21:31

There is no effective enumeration of all decidable languages. For suppose that $P_i$ was an effective sequence of programs (meaning that the mapping $i \mapsto P_i$ is computable) such that each $P_i$ always halts, and every decidable language is $L(P_i)$ for some $i$. Consider the program $P$ which, on input $i$, runs $P_i$ on input $i$ and accepts if $P_i$ rejects. The program $P$ always halts and so $L(P)$ is decidable, hence $L(P) = L(P_i)$ for some $i$. But by construction, $i \in L(P)$ iff $i \notin L(P_i)$. This contradiction shows that no such effective enumeration is possible.