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...
 chriswarbo on Feb 13, 2015 > 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".

Search: