Skip to content

Instantly share code, notes, and snippets.

@casperbp
Last active May 7, 2024 09:25
Show Gist options
  • Save casperbp/8c075a83d7402ff524fe8920eac93ad2 to your computer and use it in GitHub Desktop.
Save casperbp/8c075a83d7402ff524fe8920eac93ad2 to your computer and use it in GitHub Desktop.
Coq implementation of a Turing Machine
(*** 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment