feat(Automata, LTS, and Turing): saturated multistep transitions, mapLabel for LTS, and Nondeterministic Turing Machines (NTM)#615
feat(Automata, LTS, and Turing): saturated multistep transitions, mapLabel for LTS, and Nondeterministic Turing Machines (NTM)#615fmontesi wants to merge 11 commits into
Conversation
Shreyas4991
left a comment
Shreyas4991
left a comment
There was a problem hiding this comment.
This PR seems fine to me. The only question is whether we shouldn't just define the basic operations as move, read, write, etc, as opposed to a single step transition.
Pro:
The TM can be programmed by a lean function that chains these operations
Possible Con:
We will have to count read, write, and move as separate operations. However this is a small constant factor blow up which has no meaningful consequences in complexity theory or computability theory.
Discussion Thread
| namespace Cslib.Computability.Turing.SingleTape | ||
|
|
||
| /-- The transition labels used by a single-tape Turing Machine. -/ | ||
| structure TrLabel (State Symbol : Type*) where |
There was a problem hiding this comment.
This could be an inductive type. We can replace the transition function with the basic operations on a TM. For more discussion see Zulip thread for this PR
| 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.
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.
| open Relation | ||
|
|
||
| namespace Turing | ||
| namespace Cslib.Turing |
There was a problem hiding this comment.
Is the idea here that we don't want to extend Mathlib's Turing namespace?
| /-- An NTM yields a small-step operational semantics on configurations, which codifies an execution | ||
| step. -/ | ||
| @[scoped grind =] | ||
| def SingleTapeNTM.Red (m : SingleTapeNTM State Symbol) |
There was a problem hiding this comment.
This might be common for automata, but I myself would be able to understand this better if the documentation string would reference the abbreviation "Red" in some way ;)
|
Closed in favour of #683 |
3 participants
This PR:
LTS.SMTrfor LTS, which correctly invokes tau-closure for empty strings.Both changes have been discussed at the last CSLib General Meeting and are part of a larger discussion towards integrating machine models and transition systems (postponed to later work).