feat(MultiTapeTM): Nondeterministic multi-tape Turing machines - #802
feat(MultiTapeTM): Nondeterministic multi-tape Turing machines#802barni120400 wants to merge 1 commit into
Conversation
7450891 to
f44edbc
Compare
A nondeterministic multi-tape Turing machine is a `MultiTapeTM` whose transition function is replaced by a transition relation. Configurations, transition outputs and the effect of a single step move to a shared `MultiTape/Basic.lean`; no existing statement changes meaning. The semantics is a labelled transition system on configurations, a step labelled by the symbol it emits. A `Computation` is a chain of such transitions, with time, output and space read off it. `MultiTapeTM.toNTM` embeds the deterministic machine and `toNTM_computes` shows the embedding preserves computation in bounded time and space. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
f44edbc to
1ef9de2
Compare
|
I already posted this on zulip while github was down. Thanks for the pull request! I basically have two overall design questions: First, do we really want to base the definitions on LTSs? It will look a bit alien to people used to the way NTMs are introduced in textbooks, and I'm also not sure that the output symbol is a natural label. Secondly, and I think this also addresses the label question: I think it would be nice if a The main reason I removed it was to be able to count the number of reachable configurations. In the PR that does this, though, I also extracted a "storage configuration" which is the fields of the configuration without the input head position. So we need to be able to speak about a subset of the fields already. After all, the output is written on a tape, so one could argue that it should be part of the configuration. |
| transition function is replaced by a transition relation: `Tr q input work out` holds when `out` is | ||
| one of the transitions permitted in that situation. Configurations, transition outputs and | ||
| `TransitionOut.apply` are shared with the deterministic machine. | ||
|
|
There was a problem hiding this comment.
Not sure if this is the right place, but I think we should clarify that in contrast to deterministic machines, it is possible that there is no successor configuration. This is not the same as halting because it does not reach a configuration with state = none. Maybe we should also cross-check what the textbooks say about this possibility.
| Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : | ||
| TransitionOut k Symbol State → Prop |
There was a problem hiding this comment.
| Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : | |
| TransitionOut k Symbol State → Prop | |
| Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : TransitionOut k Symbol State) : Prop |
Since we are making big modifications here anyway, maybe we can find a better name for TransitionOut as well?
|
|
||
| /-- A computation of `ntm` from configuration `c`: a chain of transitions of `lts`, in the style of | ||
| `SimpleGraph.Walk`. -/ | ||
| inductive Computation (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : |
There was a problem hiding this comment.
Do you think (assuming we have #779), this could also be defined via List.isChain - something like
structure Computation (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where
configurations : List (Cfg k Symbol State input)
isChain : configurations.isChain ntm.Step
```
| simp [Step, LTS.UnlabelledTr, lts_tr_of_halt h_halt] | ||
|
|
||
| /-- The initial configuration corresponding to an input string. -/ | ||
| @[simp] |
There was a problem hiding this comment.
I found this simp annotation a bit annoying for deterministic TMs, maybe we should remove it for both.
|
Superseded by #820, which implements the same thing along the lines we settled on in the Zulip thread: the output tape lives in the configuration, so a computation path is a series of configurations rather than a labelled transition system. |
3 participants
This adds nondeterministic multi-tape Turing machines next to the deterministic ones from #384. The transition function is replaced by a transition relation ([Papadimitriou94] 2.7); nothing else about the model changes, so configurations and the effect of a single step move to a shared
MultiTape/Basic.lean. No existing statement changes meaning.The semantics is a labelled transition system on configurations, labelled by the emitted symbol. A computation is a chain of such transitions, in the style of
SimpleGraph.Walk, recording the trajectory that space depends on and the labels that the output depends on.MultiTapeTM.toNTMembeds the deterministic machine and preserves computation in bounded time and space.