feat: Multi-tape Turing machine - #384
Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
A few style and golfing reviews:
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
|
@chenson2018 could you take another look, please? @SamuelSchlesinger has another PR lined up that introduces different kinds of tapes and thus allows to define the function computed by a multi-tape TM, which is quite useful, I think. |
|
This has been stale for some months now. I changed the code such that all multi-tape Turing machines now have an explicit read-only input tape and an explicit write-only output tape, so that we can properly define space-bounded computations below linear space. I hope this increases the motivation to merge this PR. The parameter |
Shreyas4991
left a comment
Shreyas4991
left a comment
There was a problem hiding this comment.
Initial review. Focusses on the definitions for now
|
|
||
| * `MultiTapeTM.configs`: a sequence of configurations by execution step | ||
| * `RelatesInSteps tm.TransitionRelation cfg cfg' t`: a proof that `tm` transforms the configuration | ||
| `cfg` into `cfg'` in exactly `t` steps |
There was a problem hiding this comment.
The reference textbooks that you mention need to be cited here in the module doctoring
Shreyas4991
left a comment
Shreyas4991
left a comment
There was a problem hiding this comment.
I am sticking to design comments for now.
| rcases m with _ | d <;> decide | ||
|
|
||
| /-- The output of the transition function. -/ | ||
| structure TransitionOut (k : ℕ) (Symbol State : Type*) where |
There was a problem hiding this comment.
I am of the opinion that we should use an inductive type here, and separate move (tape : Fin k) (dir : Dir), read (tape : Fin k), write etc.
Shreyas4991
left a comment
Shreyas4991
left a comment
There was a problem hiding this comment.
Small tactic nitpicks
…dd generic ComputableInTimeAndSpace definition.
|
I removed the bundling and generally removed the |
5 participants
This introduces a multi-tape Turing machine built in a similar way to the single-tape Turing machine in #269
I did not define how a function is computed by a multi-tape Turing machine. Instead I would like to focus on tuples of tapes being transformed by Turing machines. The idea is that this allows us to build complex Turing machines from basic building blocks by composition without the need to serialize and de-serialize all the time.
Especially when talking about logarithmic space it will become necessary to define dedicated read-only input and write-only output tapes, but this is not yet included.
I have not yet properly combined the common parts between single- and multi-tape Turing machines and am hoping for some ideas there.