3 ms·
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 execu
by 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 agoNot 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?
- more_original 12y agoYou 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.