Coq implementation of a Turing Machine

turing.v

(*** Turing Machines in Coq *)

(** Some preliminary types we'll use *)
CoInductive CoList (A: Type) := CONS (a:A) (t:CoList A) | NIL.

Arguments CONS [A] _ _.
Arguments NIL [A].

CoInductive Delay A := HERE (a:A) | LATER (_:Delay A).
 
Arguments HERE [A] _.
Arguments LATER [A] _.

Section TuringMachine.
  (** State space [Q] and universe of symbols [S] *)
  Variable Q S : Type.

  (** TM actions *)
  Inductive Move := LEFT | RIGHT | STAY.

  (** Transition table for the TM *)
  Variable d : Q * S -> Q * S * Move.

  (** Set of final states *)
  Variable f : Q -> bool.

  (** The tape is given by two (potentially infinite) lists:

  - [right]: holds the current symbol as its first element, and
    everything that's to the right of the head in its tail; and

  - [left]: everything that's to the left of the current symbol.

  The TM returns its updated state and tape, after overwriting the
  current symbol on the tape and moving the current symbol pointer.

  If we try transition beyond the tape, the TM fails. *)
  Definition TM
             (left: CoList S)
             (right: CoList S)
             (q: Q) : option (Q * CoList S * CoList S) :=
    match right with
    | NIL => None
    | CONS s t =>
      match d (q, s) with
      | (q', s', move) =>
        match move with
        | STAY =>
          Some (q', left, CONS s' t)
        | LEFT =>
          match left with
          | NIL => None
          | CONS s'' t' =>
            Some (q', t', CONS s'' (CONS s' t))
          end
        | RIGHT =>
          Some (q', CONS s' left, t)
        end
      end
    end.

  (** The co-fixpoint below halts if TM finds a final state, or if we
  try to move the current symbol pointer beyond the tape.

  In theory, it's sound to unfold this computation infinitely.

  In practice, Coq doesn't allow us to force the lazily defined
  co-fixpoint.

  We could write Ltac to do it, but let's exploit some weird behaviour
  pertaining to normalization instead (below)... *)
  CoFixpoint compute
             (left: CoList S)
             (right: CoList S)
             (q: Q) : Delay Q :=
    if f q
    then HERE q
    else
      match TM left right q with
      | Some (q', left', right') =>
        LATER (compute left' right' q')
      | None =>
        HERE q
      end.

End TuringMachine.

(** Now for a "real" proof of Turing completeness (courtesy of Robbert
Krebbers).

You can encode non-terminating computations inside let-binders, provided
these aren't used in the body of the let.

This is because Coq (tested with 8.5) normalizes programs before doing
termination checking.

When executing the program, however, we still execute the binders. *)
Fixpoint for_example (n: nat) : unit :=
  let _ := for_example (S n) in
  tt.

(** Evaluating [for_example] causes a Stack Overflow. *)
(* Eval compute in for_example 0. *)

Section TerminatesInOneThousandSteps.

  Definition Q := nat.
  Definition S := nat.

  Definition d (input: Q * S) : Q * S * Move :=
    let (q, s) := input in
    (q + 1, q, RIGHT).

  Definition f (q: Q) :=
    match q with
    | 1000 => true
    | _ => false
    end.

  Fixpoint compute'
           (n: nat)
           (left: CoList S)
           (right: CoList S)
           (q: Q) : Q :=
    let _ := (if f q
              then q
              else
                match TM Q S d left right q with
                | Some (q', left', right') =>
                  compute' n left' right' q'
                | None =>
                  q
                end)
    in q.

  CoFixpoint zeros := CONS 0 zeros.

  Eval compute in (compute' 1 NIL zeros 0).

End TerminatesInOneThousandSteps.

(** This TM loops infinitely when we execute it. *)
Section Loops.

  Definition d' (input: Q * S) : Q * S * Move :=
    let (q, s) := input in
    (q + 1, q, RIGHT).

  Definition f' (q: Q) :=
    match q with
    | 0 => true
    | _ => false
    end.

  Fixpoint compute''
           (n: nat)
           (left: CoList S)
           (right: CoList S)
           (q: Q) : Q :=
    let _ := (if f' q
              then q
              else
                match TM Q S d' left right q with
                | Some (q', left', right') =>
                  compute'' n left' right' q'
                | None =>
                  q
                end)
    in q.

  Eval compute in (compute'' 1 NIL zeros 1).

End Loops.