feat(Computability): Single-tape TM complexity

[BoltonBailey]

Currently, time complexity in mathlib is defined in terms of (a kind of) multi-tape Turing machine Turing.FinTM2. This (currently Draft) PR develops time complexity in terms of Single-Tape Turing Machines. There are a few reasons to do this:

• Having definitions of time complexity for both single-tape and multi-tape TMs is a prerequisite to prove theorems relating these definitions of complexity (in particular, the theorem that the definition of polynomial time computability is equivalent between these notions).
• The Multi-tape "TM2" definition seems to be based on "Wang B-Machines" (wiki) which involves both a program of function labels, as well as a set of states.
  • I think it's a bit more common to see a simpler presentation of single-tape (and multitape) Turing machines which only provides a set of states.
  • It seems to me that the B-Machine-like definition makes it a bit complicated to make progress. For example, if I want to compose Turing Machines, then I have to be able to construct a new program and state set, which involves mapping the Turing.TM2.Stmt type to the sum type of the tapes. I have to do something similar for single-tape TMs, but the Stmt type is less complicated, so this is less involved.
• If we want to continue on and define space complexity, it seems convenient to have only a single tape, so that we don't have to do lots of reasoning over summations.

---

[github-actions]

PR summary 76f94b4301

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Computability.BinEncoding (new file) Mathlib.Computability.EncodingTo (new file)	670
Mathlib.Computability.SingleTapeBinTMComputable (new file) Mathlib.Computability.SingleTapeTMComputable (new file)	869

---

Declarations diff

+ BinEncoding
+ BinEncoding.encode_injective
+ BinTM0
+ ComputableInTime.toComputable
+ EncodingTo
+ EncodingTo.encode_injective
+ EvalsTo
+ EvalsTo.refl
+ EvalsTo.trans
+ EvalsToInTime.map
+ EvalsToInTime.small_change
+ EvalsToInTime.succ_decompose
+ EvalsToInTime.succ_iff
+ EvalsToWithinTime
+ EvalsToWithinTime.map
+ EvalsToWithinTime.mono_time
+ EvalsToWithinTime.refl
+ EvalsToWithinTime.trans
+ FinEncodingTo
+ FinTM0
+ ListBlank.space_used
+ Outputs
+ OutputsInTime.toOutputs
+ OutputsWithinTime
+ Stmt.mapEquiv
+ Tape.move?
+ Tape.space_used
+ Tape.space_used_move
+ Tape.space_used_write
+ Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2,
+ binEncodingBool
+ compComputer_q₀_eq
+ comp_left_simulation
+ comp_left_simulation_general
+ comp_right_simulation
+ comp_transition_to_right
+ encodingNatΓ'
+ finEncodingToBoolBool
+ finEncodingToNatBool
+ finEncodingToNatΓ'
+ idComputable
+ inclusionBoolΓ'
+ inclusionBoolΓ'_injective
+ inhabitedEncodingTo
+ inhabitedFinEncodingTo
+ inhabitedΓ'
+ initCfg
+ initList
+ instance : Fintype tm.Γ
+ instance : Inhabited tm.Γ
+ instance Γ.fintype {α : Type u} {Γ : Type 0} (e : FinEncodingTo α Γ) : Fintype Γ
+ liftCompCfg_left
+ liftCompCfg_left_or_right
+ liftCompCfg_right
+ map_liftCompCfg_left_or_right_step
+ map_liftCompCfg_left_step
+ map_liftCompCfg_right_step
+ output_length_le_input_length_add_time
+ sectionΓ'Bool
+ sectionΓ'Bool_inclusionBoolΓ'
+ unaryBinEncodingNat
+ unaryFinEncodingToNat
+ Γ'
++ Cfg
++ Computable
++ ComputableInPolyTime
++ ComputableInPolyTime.id
++ ComputableInPolyTime.toComputableInTime
++ ComputableInTime
++ ComputableInTime.comp
++ ComputableInTime.id
++ EvalsToInTime
++ EvalsToInTime.refl
++ EvalsToInTime.trans
++ OutputsInTime
++ Stmt
++ compComputer
++ decodeBool
++ decodeNat
++ decodeNum
++ decodePosNum
++ decode_encodeBool
++ decode_encodeNat
++ decode_encodeNum
++ decode_encodePosNum
++ encodeBool
++ encodeNat
++ encodeNum
++ encodePosNum
++ encodePosNum_nonempty
++ encodingNatBool
++ haltList
++ idComputer
++ inhabitedStmt
++ instance : Fintype tm.Λ
++ instance : Inhabited tm.Λ
++ step
++ unaryDecodeNat
++ unaryEncodeNat
++ unary_decode_encode_nat

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).