Library ProbTuring
States, letters
Alphabet extends letters with a blanc char
Inductive alph := Blanc | Let : letter -> alph.
Variable accept : state -> bool.
Inductive dir := L | R.
Record output := mkO {next:state;write:alph;move:dir}.
Variable trans : state -> alph -> distr output.
Record config := mkT {cur : state; tape:Z -> alph; pos : Z}.
Definition update (m:config) (o:output) : config
:= mkT (next o)
(fun z => if Zeq_bool z (pos m) then (write o) else tape m z)
(if (move o) then pos m + 1 else pos m - 1).
Instance run_mon : monotonic
(fun (f: config -> distr config) (m:config) =>
fif (accept (cur m)) (Munit m)
(Mlet (trans (cur m) (tape m (pos m)))
(fun out => f (update m out)))).
Save.
Definition Frun : (config -> distr config) -m> (config -> distr config)
:= mon (fun (f: config -> distr config) (m:config) =>
fif (accept (cur m)) (Munit m)
(Mlet (trans (cur m) (tape m (pos m)))
(fun out => f (update m out)))).
Lemma Frun_simpl : forall f m,
Frun f m = fif (accept (cur m)) (Munit m)
(Mlet (trans (cur m) (tape m (pos m)))
(fun out => f (update m out))).
Lemma Frun_cont : continuous Frun.
Definition run : config -> distr config := Mfix Frun.
End TuringMachine.