3 ms·
I haven't looked at the code but you can prove many functions in Coq terminate by showing they are structurally recursive. Concisely, you show a function only c
by seanwilson 12y ago
I haven't looked at the code but you can prove many functions in Coq terminate by showing they are structurally recursive. Concisely, you show a function only calls itself on smaller versions of the originally parameters so there must be a limit to how many recursive calls you can make.
For example, a function F to find the item X in the the list L might look like this:
1. If L is empty, return false.
2. If the front of L is X, return true.
3. Otherwise return the result of calling F on L with its front item removed.
The list must get smaller every recursive call so there's a limit to the recursion. Lots of functions recurse in this way (e.g. map, filter, reduce, max) and Coq can detect these automatically usually.
For more complicated cases, you can provide some numeric metric to Coq and write a proof that this metric must eventually reach some limit. For example, to prove quicksort terminates, you usually show the length of the lists called in the recursive calls are smaller each time.
So, in general, there's no procedure to show an arbitrary function terminates, but for the kind of functions people usually write, there are practical ways to prove termination.
- more_original 12y agoIn 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]