Origin Sections NuprlLIB Doc

Turing

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

Selected Objects
deffiniteFinite(T) == n:. n ~ T
COMturing_1_contentsDefinition of Turing Machine
COMproto_machine_def=========================================
defproto_machinePM{i} == q:Type proto_sigma:Type proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi))qqq
deftm_q(p) == 1of(p)
THMtm_q_wfp:PM{i}. (p) Type
deftm_proto_sigmaP(p) == 1of(2of(p))
THMtm_proto_sigma_wfp:PM{i}. P(p) Type
deftm_sigma(tm) == P(tm)+Void
deftm_proto_piP(p) == 1of(2of(2of(p)))
THMtm_proto_pi_wfp:PM{i}. P(p) Type
deftm_pi(p) == Void+P(p)
deftm_gammaG(p) == P(p)+P(p)
deftm_blank_(p) == 1of(2of(2of(2of(p))))
THMblank_proto_pip:PM{i}. _(p) Void+P(p)
THMblank_pip:PM{i}. _(p) (p)
THMtm_blank_wfp:PM{i}. _(p) G(p)
deftm_delta(p) == 1of(2of(2of(2of(2of(p)))))
THMtm_delta_protop:PM{i}. (p) (p)(P(p)+P(p))(p)(P(p)+P(p))
THMtm_delta_wfp:PM{i}. (p) (p)G(p)(p)G(p)
deftm_sp.s == 1of(2of(2of(2of(2of(2of(p))))))
THMtm_s_wfp:PM{i}. p.s (p)
deftm_tp.t == 1of(2of(2of(2of(2of(2of(2of(p)))))))
THMtm_t_wfp:PM{i}. p.t (p)
deftm_rp.r == 2of(2of(2of(2of(2of(2of(2of(p)))))))
THMtm_r_wfp:PM{i}. p.r (p)
COMtm_config_def===========================================
deftm_configConfig(M) == (M)(G(M))
defconf_stt.st == 1of(t)
THMconf_st_wfM:PM{i}, t:Config(M). t.st (M)
defconf_tapet.tape == 1of(2of(t))
THMconf_tape_wfM:PM{i}, t:Config(M). t.tape G(M)
defconf_hdt.hd == 2of(2of(t))
THMconf_hd_wfM:PM{i}, t:Config(M). t.hd
defnext_configM(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 >
THMnext_config_wfM:PM{i}, C:Config(M). M(C) Config(M)
defnth_config(rec) M(C)[n] == if n=0 C else M(M(C)[n-1]) fi
THMnth_config_wfM:PM{i}, C:Config(M), n:. M(C)[n] Config(M)
defaccept_configM(C) == n:. M(C)[n].st = M.t & (k:n. M(C)[n].st = M.r)
defturing_machineTM(M) == Finite((M)) & Finite((M)) & Finite((M)) & M.t = M.r