Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

share|improve this question

marked as duplicate by Raphael May 2 at 21:31

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.

    
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 at 21:31
add comment

2 Answers 2

up vote 3 down vote accepted

Coq cannot always know whether a program will terminate, because that would be a solution to the halting problem.

Coq is able to notice that a certain class of programs will terminate. The main heuristic it uses is that if one of the arguments to the function must get smaller on each recursive call, the program must terminate.

If you have a function that terminates, but Coq cannot tell that it terminates, you can add an extra argument that always get smaller on recursive calls. Doing this amounts to providing a proof that the function terminates.

So basically, Coq accepts any program that the user can prove the termination of.

share|improve this answer
add comment

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.

share|improve this answer
add comment

Not the answer you're looking for? Browse other questions tagged or ask your own question.