feat(Machines): Single-Tape Nondeterministic Turing Machines (NTMs)#683
feat(Machines): Single-Tape Nondeterministic Turing Machines (NTMs)#683fmontesi wants to merge 3 commits into
Conversation
| tape := Turing.BiTape.mk₁ xs | ||
|
|
||
| /-- The space used by a configuration is the space used by its tape. -/ | ||
| def Cfg.spaceUsed (cfg : Cfg State Symbol) : ℕ := cfg.tape.spaceUsed |
There was a problem hiding this comment.
Moving my comment from the other PR:
I think this definition might be misleading because it implement a rather uncommon notion of space (although it might be equivalent in the end). This definition is mainly used to prove that the output length is bounded by the number of steps. So maybe we should rather rename it to "tapeSize" or something like that.
But we can also leave that for a later change when we introduce a notion of space.
|
|
||
| /-- An NTM yields a small-step operational semantics on configurations, which codifies an execution | ||
| step. -/ | ||
| def Red (m : SingleTapeNTM State Symbol) |
There was a problem hiding this comment.
Could you add a small comment that explains why it is called Red?
| /-- The transition labels used by a single-tape Turing Machine. -/ | ||
| inductive TrLabel (Symbol : Type*) | ||
| /-- Read `x` from the tape. -/ | ||
| | read (x : Symbol) |
There was a problem hiding this comment.
Why does read need a parameter. Shouldn't read just return whatever symbol is on the thread?
| (otape : Option (Turing.BiTape Symbol)) (μ : TrLabel Symbol) : | ||
| Option (Turing.BiTape Symbol) := | ||
| match μ, otape with | ||
| | read x, some tape => if x = tape.head then some tape else none |
There was a problem hiding this comment.
Why is the tape an option type? We always operate on the tape don't we?
| criterion as for deterministic TMs. We might want to revisit this in the future. | ||
| -/ | ||
| c'.tape = Turing.BiTape.mk₁ ys | ||
|
|
There was a problem hiding this comment.
Could you add another Prop that states that the NTM accepts an input in at most t steps?
3 participants
TrLabeland the usual derived 'yields' relation (Red).