8 ms·

> The purity of Coq ensures that each request is answered exactly once in finite time. How does Coq ensure that the request completes in finite time?

pja 12y ago
At a guess it demonstrates that there's no possibility for infinite loops or recursion. It's going to rely on a model of the storage mechanism (memory, disk, whatever) that will respond to requests for data in finite time, but that doesn't seem an unreasonable assumption to make in this case. You have to draw the lines around your proof system somewhere or else you're going to end up having to model the entire world.
- __alexs 12y ago
  > that doesn't seem an unreasonable assumption to make in this case Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too. Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
  - pja 12y ago
    I don't know whether this particular proof models IO timeouts - might have a poke at it and see what it's doing if I have time later. More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
    - clarus 12y ago
      Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l21 https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#... In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.
wk_end 12y ago
Coq isn't Turing complete - it has a termination checker that needs to be able to determine that your functions terminate.
- eli_gottlieb 12y ago
  Technically speaking, corecursion allows for writing Turing-complete programs, including nonterminating programs. It just requires that you explicitly specify where you use nontermination and prove that each iteration yields a well-typed result.
  - more_original 12y ago
    Yes, one can represent non-terminating programs. One can represent Turing machines as data, after all. But one cannot write a Coq function that will fully execute such programs. Each well-typed Coq function, when applied to concrete arguments, will terminate in a finite number of steps. One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps. [I guess that's what you're saying, but there seems to be some confusion here, so it's perhaps best to try to be explicit.]
    - eli_gottlieb 12y ago
      Not quite. IIRC, corecursive programs (and the coinductive data-types they return) are straightforwardly nonterminating: they can loop infinitely. The difference is that each iteration is proven to terminate and to yield a well-specified result, and arbitrary theorems can be proven about the generator function yielding each iteration's result. http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/bertot_sl2.pdf http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
    - chriswarbo 12y ago
      > One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps. I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive step function?
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 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 ago
    I 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 ago

pja 12y ago

At a guess it demonstrates that there's no possibility for infinite loops or recursion. It's going to rely on a model of the storage mechanism (memory, disk, whatever) that will respond to requests for data in finite time, but that doesn't seem an unreasonable assumption to make in this case. You have to draw the lines around your proof system somewhere or else you're going to end up having to model the entire world.

__alexs 12y ago
> that doesn't seem an unreasonable assumption to make in this case Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too. Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
- pja 12y ago
  I don't know whether this particular proof models IO timeouts - might have a poke at it and see what it's doing if I have time later. More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
  - clarus 12y ago
    Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#l21 https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#... In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.

wk_end 12y ago

Coq isn't Turing complete - it has a termination checker that needs to be able to determine that your functions terminate.

eli_gottlieb 12y ago
Technically speaking, corecursion allows for writing Turing-complete programs, including nonterminating programs. It just requires that you explicitly specify where you use nontermination and prove that each iteration yields a well-typed result.
- more_original 12y ago
  Yes, one can represent non-terminating programs. One can represent Turing machines as data, after all. But one cannot write a Coq function that will fully execute such programs. Each well-typed Coq function, when applied to concrete arguments, will terminate in a finite number of steps. One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps. [I guess that's what you're saying, but there seems to be some confusion here, so it's perhaps best to try to be explicit.]
  - eli_gottlieb 12y ago
    Not quite. IIRC, corecursive programs (and the coinductive data-types they return) are straightforwardly nonterminating: they can loop infinitely. The difference is that each iteration is proven to terminate and to yield a well-specified result, and arbitrary theorems can be proven about the generator function yielding each iteration's result. http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/bertot_sl2.pdf http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
  - chriswarbo 12y ago
    > One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps. I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive step function?

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 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 ago
  I 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 ago