fix(MultiTapeTM): rename InExactTimeAndSpace

[fynngodau]

In MultiTapeNTM, since Step is defined such that a halted configuration steps to itself, we have the surprising situation that ComputesInExactTime allows one to add arbitrarily many steps, i.e. the following is provable:

theorem make_more_steps (h : ComputesInExactTime tm i o k) : ComputesInExactTime tm i o (k+1) := sorry

proof

theorem make_more_steps (h : ComputesInExactTime tm i o k) : ComputesInExactTime tm i o (k+1) :=
  let ⟨p, hh⟩ := h
  ⟨
  { cfgs := p.cfgs.concat p.last
    last := p.last
    isChainFromTo := {
      isChain := by
        have fact := p.isChainFromTo.isChain
        rw [List.concat_eq_append]
        apply List.isChain_append.2
        aesop
        rw [show x = p.last by grind [p.isChainFromTo.getLast_eq]]
        unfold Step
        simp [left]
      ne_nil := by simp
      head_eq :=
        by grind [p.isChainFromTo.head_eq]
      getLast_eq := by simp
    }
  },
  hh.left,
  hh.right.left,
  have fact := hh.right.right
  by
    simp only [ComputationPath.time,List.concat_eq_append] at fact ⊢
    rw [List.length.eq_def] at fact ⊢
    have fact2 := p.isChainFromTo.ne_nil
    generalize eq : p.cfgs = cc
    rw [eq] at fact
    match cc with
    | [] => nomatch (fact2 eq)
    | hd :: tl => grind
⟩

This does not match the intuitive understanding of an "exact" runtime. To resolve this situation, this PR aligns the terminology used in MultiTapeNTM with the one used in MultiTapeTM, and thus renames to ComputesInTime etc..

For both convenience and clarity, considering the above theorem, the definition wrt. the time bound is also changed from = to ≤.

---

Notes:

• Zulip discussion
• We still have inconsistent naming compared to SingleTapeTM (and Relation as used therein):
  • SingleTapeTM's WithinTime = MultiTapeTM's InTime (both ≤, whereas MultiTapeTM's space boundaries are exact =!)
  • MultiTapeTM.Nondeterministic vs. SingleTapeTM.NonDeterministic (capitalization of the D)

[crei]

But this is still exact space, isn't it? I think we don't really need exact space, so maybe just change this to \le.

[fynngodau]

I would agree with this if we also change the semantics of MultiTapeTM.ComputesInTimeAndSpace.

[fynngodau]

Actually, in that case I would like to rename everything to Within so it's consistent with SingleTapeTM.