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