4 ms·
In Coq all functions terminate. Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program o
by more_original 12y ago
In Coq all functions terminate.
Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program of this type. If one allowed non-termination, then it would be easy to construct a program of any type (like in OCaml let rec f() = f() has type () -> 'a), so you could prove anything.
- seanwilson 12y agoI didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover. In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that Coq will accept is the difficult part.
- more_original 12y agoI see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
- seanwilson 12y agoAh, I meant that in the sense of, think of an algorithm you want to write, many of them are structurally recursive and they're straightforward to implement in Coq.
- deleted 12y ago[deleted]