Non-constructive Proofs and Productivity
Languages in the Dependent ML family allow users to ensure termination by using a termination metric, a number that is strictly decreasing on recursive calls in the definition of the function.
There is a counterpart to termination for co-recursive structures, where we need to show that a function produces values indefinitely. So, for the Collatz conjecture, we want to show termination for:
collatz n = collatz' n []
collatz' 1 r = 1:r
collatz' n r =
if n `mod` 2 == 0
then collatz' (n `div` 2) (n:r)
else collatz' (3*n + 1) (n:r)
But for the twin prime conjecture we want to show the productivity of:
data Stream a = Stream a (Stream a)
twins = twins' 3
twins' n =
if (primep n) && (primep (n+2))
then Stream (n,n+2) (twins' (n+2))
else twins (n+2)
I don't know if any of the members of the DML family can check productivity. Imagine they could, and imagine we had a non-constructive proof of the twin primes conjecture. Could we use that proof to allow a definition of twins to be marked productive?
Most of the time, we talk about the Curry-Howard correspondence in reference to intuitionist logic and functional programming, but non-constructive proofs of productivity seem like a good way to be able to use more powerful logic in programming, since they don't have to change the implementation of the function they are attached to.
2 comments:
Productivity of twins means that the stream is elementwise terminating, even though the spine does not terminate. So you can (in this case at least) define productivity in terms of termination.
In Coq you can define co-structurally recursive functions. Coq has a syntactic requirement of at least one additional constructor on the structurally co-recursive argument.
This restriction can be "stretched" by transforming programs with a measure function or relation that proves productivity, that can then be transformed into an auxiliary structurally co-recursive argument.
In coq you don't just label it as productive or terminating, you aren't even allowed to define it if it isn't one of those two!
Post a Comment