Repository navigation
refactor(MultiTape): simulate machines through adapters - #1151
barni120400 wants to merge 4 commits into
Conversation
f33ed1b to
7c214a5
Compare
7c214a5 to
192855e
Compare
barni120400
changed the title
A machine follows another when it performs each of its transitions through an adapter: what the inner machine reads, computed from the symbols under the heads of the outer machine (`HeadSymbols`), and the outer action performing each inner action. `adapt` runs a machine through an adapter, and `Follows.runningStepHom` and `Follows.stepHom` turn a configuration map that agrees with the adapter into a homomorphism of step relations. `extendTapes`, `outputToTape` and `inputFromTape` run `tm` through their adapters, so their homomorphisms come from `follows_adapt`. `seq` and `repeatUntilBlank` relabel the actions of their inner machines with `Action.mapState` and follow them by definition, and `prependOutputHom` follows the machine itself. This replaces the step lemmas of each simulation and the deterministic `stepHom` and `runningStepHom`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
192855e to
c2d2b0d
Compare
| /-- How a machine with `k'` work tapes and states `State'` performs the transitions of a machine | ||
| with `k` work tapes and states `State`: the symbols the inner machine reads, computed from those | ||
| under the heads of the outer machine, and the outer action performing each inner action. -/ | ||
| structure Adapter (k k' : ℕ) (Symbol State State' : Type*) where |
There was a problem hiding this comment.
Can you explain the intuition why read maps one way and action maps the other way?
There was a problem hiding this comment.
And does it make sense to put the state-mapping function inside the adapter as well?
There was a problem hiding this comment.
This is a really good comment! The reason that we have the state-mapping outside is because "adapt" it not generic enough to express adapting a TM to another TM with more states, Like RepeatUntilBlank and Sequential. Indeed these two machines are not defined as an adapt of another machine.
In order to express all the plumbings with adapt, I add wire that is like adapt for two machines, and then things like "run a machine and then do something else" could be captured by adapt.
There was a problem hiding this comment.
The intuition is that Adapter describes how a given inner machine is related to a outer machine.
read adapts the symbols the outer machine sees to the symbols the inner machine sees.
action adapts the action the inner machine does to an action of the outer machine. The action of the outer machine may depend on the head symbols of the outer machine, so it is
HeadSymbols k' Symbol → Action k Symbol State → Action k' Symbol State'
|
|
||
| /-- `ntm'` follows `ntm` through `adapter`, in state `state q` while `ntm` is in state `q`: whatever | ||
| `ntm` may do in `q` on what `adapter` reads, `ntm'` may do the adapted action in `state q`. -/ | ||
| def Follows {k' : ℕ} {State' : Type*} (ntm' : MultiTapeNTM k' Symbol State') |
There was a problem hiding this comment.
This seems to be mostly about Tr and not about the full machine, otherwise we would not need so many additional hypotheses in runningStepHom, or am I wrong?
Adds `wire`, which runs two machines on the same tapes in one, in the states `State₀ ⊕ State₁`, and takes two wires, `next₀` and `next₁`, saying where the steps of each machine lead: within the same machine, to the other one, or to halting. Each half follows its machine through the adapter relabeling its next states (`Wire.follows_left`, `Wire.follows_right`), and the adapted transition `adaptedTr` is shared with `adapt`, whose `follows_adapt` becomes `Adapt.follows`. Defines `seq` as the wiring of its two machines, and `repeatUntilBlank` as the wiring of `tm` with `blankTest`, a one-state machine that halts on a blank cell and otherwise hands back to `tm`. The loop's first phase is that of `seq`: `Sequential.leftState` and `leftCfg` now take the state handed over to, so the loop reuses them in place of its own `runState`. The loop's states become `State ⊕ Unit`, replacing `RepeatUntilBlankState`, and the hand-written `Follows` proofs of both combinators are removed, as is `Action.mapState`, now used only to define `Adapter.mapState`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… seq Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
0fef8fe to
d0bfa21
Compare
…tion proofs Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
d0bfa21 to
9b2a4eb
Compare
Lets a machine follow another: it performs each transition of the inner machine through an adapter, which computes what the inner machine reads from the symbols under the outer heads (
HeadSymbols) and gives the outer action performing each inner action.Follows.runningStepHomandFollows.stepHomturn a configuration map that agrees with the adapter into a homomorphism of step relations, so it maps run paths.Defines
extendTapes,outputToTapeandinputFromTapeas the machine run through an adapter (MultiTapeTM.adapt), so their homomorphisms come fromfollows_adapt.seqandrepeatUntilBlankrelabel the actions of their inner machines withAction.mapStateand follow them by definition, andprependOutputHomfollows the machine itself. This replaces the step lemmas of each simulation and the deterministicstepHomandrunningStepHom, and shortens the proofs that use them.Depends on #1122: its commit is included temporarily and will leave this diff when it merges.
Composed with Claude Code.