Turing

Nuprl Section: Turing - Turing Machine concepts. Pavel Naumov, November 1996

 def finite Finite(T) == n:. n ~ T COM turing_1_contents Definition of Turing Machine COM proto_machine_def ========================================= def proto_machine PM{i} == q:Type proto_sigma:Type proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi))qqq def tm_q (p) == 1of(p) THM tm_q_wf p:PM{i}. (p) Type def tm_proto_sigma P(p) == 1of(2of(p)) THM tm_proto_sigma_wf p:PM{i}. P(p) Type def tm_sigma (tm) == P(tm)+Void def tm_proto_pi P(p) == 1of(2of(2of(p))) THM tm_proto_pi_wf p:PM{i}. P(p) Type def tm_pi (p) == Void+P(p) def tm_gamma G(p) == P(p)+P(p) def tm_blank _(p) == 1of(2of(2of(2of(p)))) THM blank_proto_pi p:PM{i}. _(p) Void+P(p) THM blank_pi p:PM{i}. _(p) (p) THM tm_blank_wf p:PM{i}. _(p) G(p) def tm_delta (p) == 1of(2of(2of(2of(2of(p))))) THM tm_delta_proto p:PM{i}. (p) (p)(P(p)+P(p))(p)(P(p)+P(p)) THM tm_delta_wf p:PM{i}. (p) (p)G(p)(p)G(p) def tm_s p.s == 1of(2of(2of(2of(2of(2of(p)))))) THM tm_s_wf p:PM{i}. p.s (p) def tm_t p.t == 1of(2of(2of(2of(2of(2of(2of(p))))))) THM tm_t_wf p:PM{i}. p.t (p) def tm_r p.r == 2of(2of(2of(2of(2of(2of(2of(p))))))) THM tm_r_wf p:PM{i}. p.r (p) COM tm_config_def =========================================== def tm_config Config(M) == (M)(G(M)) def conf_st t.st == 1of(t) THM conf_st_wf M:PM{i}, t:Config(M). t.st (M) def conf_tape t.tape == 1of(2of(t)) THM conf_tape_wf M:PM{i}, t:Config(M). t.tape G(M) def conf_hd t.hd == 2of(2of(t)) THM conf_hd_wf M:PM{i}, t:Config(M). t.hd def next_config M(Conf) == let delta = (M)( < Conf.st,Conf.tape(Conf.hd) > ) in < 1of(delta) ,(z.if z=Conf.hd 1of(2of(delta)) else Conf.tape(z) fi) ,if 2of(2of(delta)) Conf.hd+1 else Conf.hd-1 fi > THM next_config_wf M:PM{i}, C:Config(M). M(C) Config(M) def nth_config (rec) M(C)[n] == if n=0 C else M(M(C)[n-1]) fi THM nth_config_wf M:PM{i}, C:Config(M), n:. M(C)[n] Config(M) def accept_config M(C) == n:. M(C)[n].st = M.t & (k:n. M(C)[n].st = M.r) def turing_machine TM(M) == Finite((M)) & Finite((M)) & Finite((M)) & M.t = M.r