Require Import List Bool.
From Undecidability.Shared.Libs.DLW
Require Import sss.
From Undecidability.TM
Require Import SBTM.
Import SBTMNotations (tape).
Set Implicit Arguments.
Inductive pctm_instr : Set :=
| pctm_mv : direction -> pctm_instr
| pctm_wr : bool -> pctm_instr
| pctm_br : nat -> nat -> pctm_instr
.
Module PCTMNotations.
Notation MV := pctm_mv.
Notation WR := pctm_wr.
Notation BR := pctm_br.
Notation JMP j := (BR j j).
Definition rd (t : tape) : bool := let '(_,b,_) := t in b.
Definition wr (t : tape) b : tape := let '(l,_,r) := t in (l,b,r).
End PCTMNotations.
Import PCTMNotations SBTMNotations.
Definition pctm_state := (nat * tape)%type.
ρ // (i,t₁) -1> (j,t₂)
means instruction ρ at PC i transforms
the state (i,t₁) into the state (j,t₂)
Inductive pctm_sss : pctm_instr -> pctm_state -> pctm_state -> Prop :=
| pctm_sss_mv d i t : MV d // (i,t) -1> (1+i,mv d t)
| pctm_sss_wr b i t : WR b // (i,t) -1> (1+i,wr t b)
| pctm_sss_br i j p t : BR j p // (i,t) -1> (if rd t then j else p,t)
where "ρ // s -1> t" := (pctm_sss ρ s t).
when P = (i,l) with (i = start PC value for instructions in l)
and (l = list of instructions)
P // s ↓ means repeating steps as above in P, starting from s,
eventually leads to a PC value outside of P
Notice that this is equivalent to termination because the PCTM
small steps semantics is total, ie if there is an instruction at
the current PC, then a computation step can occur: no instruction
is blocking