Turing machines in 50 Lines Of Coq

turing.v

Require Import List.
Import ListNotations.

Notation "0" := false : bool_scope.
Notation "1" := true : bool_scope.
Local Open Scope bool_scope.

Inductive tape :=
| Tape (l : list bool) (b : bool) (r : list bool)
.

Definition empty_tape := Tape [] false [].

Inductive dir := L | R.

Inductive trans {S : Type} :=
| Trans (write : bool) (move : dir) (next : S)
.
Arguments trans : clear implicits.

Definition machine (S : Type) : Type := bool -> S -> option (trans S).

Definition step {S : Type} : machine S -> S * tape -> option (S * tape) :=
  fun t '(s, Tape l b r) =>
    match t b s with
    | None => None
    | Some (Trans w m s') => Some (
      let tape' :=
        match m with
        | L =>
            match l with
            | [] => Tape [] 0 (w :: r)
            | b' :: l' => Tape l' b' (w :: r)
            end
        | R =>
            match r with
            | [] => Tape (w :: l) 0 []
            | b' :: r' => Tape (w :: l) b' r'
            end
        end
      in (s', tape'))
    end.


(* Example: busy beaver with three states (plus the halting state).
   https://en.wikipedia.org/wiki/Busy_beaver
 *)

Inductive three := A | B | C | H.

Definition busy3 : machine three :=
  fun b s =>
    match b with
    | 0 =>
        match s with
        | A => Some (Trans 1 R B) | B => Some (Trans 0 R C) | C => Some (Trans 1 L C)
        | H => None
        end
    | 1 =>
        match s with
        | A => Some (Trans 1 R H) | B => Some (Trans 1 R B) | C => Some (Trans 1 L A)
        | H => None
        end
    end.

(* Run a machine to completion, returning [Some] of the final tape,
   or [None] if we run out of fuel. *)
Fixpoint step_for (fuel : nat) {S : Type} (t : machine S) (s0 : S) (p0 : tape)
  : option tape :=
    match fuel with
    | O => None
    | S fuel =>
        match step t (s0, p0) with
        | None => Some p0
        | Some (s', p') => step_for fuel t s' p'
        end
    end.

Compute (step_for 15 busy3 A empty_tape).