feat(Computability/MultiTapeTM): input/output tape predicates#162
feat(Computability/MultiTapeTM): input/output tape predicates#162SamuelSchlesinger wants to merge 1 commit intocrei:multi-tape-tmfrom
Conversation
…position bound Adds read-only input and write-only output tape abstractions for multi-tape Turing machines, plus a proof that the input-tape head position stays within [-1, |input|] across reachable configurations. - StackTape/BiTape: migrated `*_nil` lemmas into BiTape, extended StackTape API used by the new invariants. - MultiTapeTM.HasInputTape / HasOutputTape: predicates characterising read-only input and write-only output tapes. - HeadBoundInvariantAt: Prop-valued structure carrying the position bound, canonical-tape equality, and left/right reachability chains; .initCfg and .step lemmas prove inductivity. - HasInputTape.step_tape0_decompose: factors a step through its predecessor state, eliminating `change`-tactic gymnastics in invariant-preservation proofs. - head_position_bounded: quantitative head-position bound derived from the invariant via iter_step.
| @[simp, scoped grind =] | ||
| lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl | ||
|
|
||
| @[simp, scoped grind =] |
There was a problem hiding this comment.
I'm not sure, but do these really need the grind annotation? cons itself is already marked grind and the proof is rfl, so I think this should not be needed.
| -/ | ||
| structure HasInputTape {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) : Prop where | ||
| /-- Every transition writes back the symbol it read on tape `0`. -/ | ||
| readPreserving : ∀ q reads, ((tm.tr q reads).1 0).IsReadPreserving (reads 0) |
There was a problem hiding this comment.
I think this is a bit hard to read, especially since IsReadPreserving in the end is super simple. Do you think it would be better to change IsReadPreserving to instead take a transition function and a tape number?
| For `n < s.length`, the head reads `some s[n]`; for `n ≥ s.length`, the head reads | ||
| `none` and the tape has `s.reverse` on the left. | ||
| -/ | ||
| def canonicalInputTapeNat (s : List Symbol) (n : ℕ) : BiTape Symbol where |
There was a problem hiding this comment.
Would it be easier to define this as
def canonicalInputTapeNat (s : List Symbol) (n : ℕ) : BiTape Symbol :=
move_right^[n] (mk₁ s)
?
in my other branches, I have a function
def move_int (t : BiTape Symbol) (δ : ℤ) : BiTape Symbol := ...
which could also come in handy here.
| -/ | ||
| def canonicalInputTape (s : List Symbol) (p : ℤ) : BiTape Symbol := | ||
| if 0 ≤ p then canonicalInputTapeNat s p.toNat | ||
| else ⟨none, ∅, StackTape.map_some s⟩ |
There was a problem hiding this comment.
It's a bit surprising to me that this cuts off for negative numbers but not for positive numbers beyond the input length. is that intended, or should this be the equivalent of move_int (mk₁ s) p?
|
|
||
| /-- One-step move-right on the canonical configuration at natural-number position `n`, | ||
| when still within the input region. -/ | ||
| lemma canonicalInputTapeNat_move_right {s : List Symbol} {n : ℕ} (h : n < s.length) : |
There was a problem hiding this comment.
If we use move_int instead of this custom definition, these lemmas could be generally useful.
| further in direction `d` without returning first. The condition is finitary — both the | ||
| reachability relation and the existential in `MovesOffBlankInDir` range over finite types. | ||
| -/ | ||
| def IsBoundedInDirectionOnTape |
There was a problem hiding this comment.
This all assumes that we do not write on the first tape. Do you think this could be more self-contained by adding this to MoveThenStays?
| in `t` steps has its tape-`0` content in canonical shape `canonicalInputTape s p` for some | ||
| integer position `p ∈ [-1, s.length]`. In particular, the head on tape `0` stays within | ||
| one cell of the input region throughout the trace. -/ | ||
| theorem HasInputTape.head_position_bounded |
There was a problem hiding this comment.
I haven't read through the full file, but I think I understood that this machinery starts with the initial configuration. I try to avoid tm.initCfg because it makes a lot of assumptions that makes the theorems that use it unusable for composition (all tapes except the first are empty, for example). If instead, we just assume "we start with a configuration where the head is inside the input", the theorem could be directly applied in a proof for tm composition.
2 participants
The stuff we talked about in Discord.