3 ms·

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

• more_original 12y ago
  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.