Hacker News Reader

Comment by wereHamster | Hacker News Reader

> 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?

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.

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.

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.

I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.

Ah, 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.

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

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.

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.]

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/Ex...

> 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?

You can extract lazy values that represent infinite data. For example, you can define the stream of the factorial numbers as follows.

  CoInductive Stream (T: Type): Type :=
    Cons: T -> Stream T -> Stream T.

  Fixpoint fac(n : nat): nat := 
    match n with
    | 0 => 1
    | S n => n * (fac n)
   end.
 
  CoFixpoint facs : nat -> Stream nat := 
  fun n =>
   Cons (fac n) (facs (n+1)).

  Definition fs := facs 0.

It's extracted to the following Haskell code:

  data Stream t =
    Cons t (Stream t)

  fac :: Nat -> Nat
    fac n =
    case n of {
     O -> S O;
     S n0 -> mul n0 (fac n0)}

  facs :: Nat -> Stream Nat
    facs n =
    Cons (fac n) (facs (add n (S O)))

  fs :: Stream Nat
    fs = facs O

It should be possible to define a function that given a Turing Machine returns the stream of its states analogously. But to actually compute the states in Haskell you would have to write a driver function that actually forces their computation one after the other.

Even without corecursive data, you can define a function that for a given TM returns a function of type nat->state, which computes the state of the TM after k steps. In a way this value also represents the whole, possibly infinite, computation of the machine.

Isn't that coinductive recursion?

"corecursion" is usually a recursion that goes via multiple definitions.

In the context of Coq, the word "corecursion" is always used for coinductive recursion. I guess a Coq programmer would call what you describe "mutual recursion".

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.

> 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?

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 :)

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#...

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.

Reply on news.ycombinator.com