Library ProbTuring

Modeling Probabilistic Turing Machine



Section TuringMachine.

States, letters
Variable state : Type.
Variable letter : Type.

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.