feat: Single Tape Turing Machines

[BoltonBailey]

I have now marked this ready for review but it's quite a large PR, reviewers please tell me if I should reorganize things or submit in a different way.

This PR adds a model of Single Tape Turing machines, which inputs and outputs List α for a finite alphabet type α, with the following features:

• In Cslib/Foundations/Data
  • A file for StackTape, a stack-like data structure for optional alphabet symbols that extends infinitely (in one direction) with blank (none) symbols. Represented as a finite list that tructates the infinite stream of none elements
  • A file for BiTape, a bidirectionally infinite Tape, made from two StackTape
• In Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
  • structures representing computability within a time bound, and polynomial time computability.
  • Machine that computes the identity function, c.f. Mathlib's Turing.idComputer
  • Machine that computes the composition of the function computed by two individual machines. (Mathlib currently doesn't have this)
    • Proof this machine preserves polynomial time computation

This PR was authored with the support of Claude Code and Project Numina's Lean MCP fork

---

My Design Notes

While Mathlib has a definition of polynomial time computability based on a more complicated model of TMs, I think it makes sense to have one based on a simple single-tape model here.

Longer term, I would like to try to create a unified framework for talking about TMs with variable amounts of tapes / stacks, so that we can eventually prove theorems about the time and space overhead incurred by switching from one model to another (e.g. 2 tape TMs simulate k-tape TMs with log overhead, 1 tape TMs simulate 2-tape TMs with quadratic overhead, 2-stack machines simulate 1 tape TMs ).

I ultimately did not reuse much if any of the Mathlib infrastructure around Tapes, because of the injectivity issue I described in the docstring.

[BoltonBailey]

I am experiencing some kind of CI error with mk_all, is it right that I should be changing CSLibTests.lean?

[chenson2018]

I am experiencing some kind of CI error with mk_all, is it right that I should be changing CSLibTests.lean?

Are you passing the --module flag?

[BoltonBailey]

No, the error message just told me to run lake exe mk_all

The file 'Cslib.lean' is out of date: run lake exe mk_all to update it

[chenson2018]

No, the error message just told me to run lake exe mk_all

The file 'Cslib.lean' is out of date: run lake exe mk_all to update it

The docs upstream are likely out of date given how recent this change is.

[chenson2018]

It looks like you've addressed my suggestions, thank you! Do you mind identifying some of the theorems you are repeatedly passing to grind and adding annotations to them?

[BoltonBailey]

Ok I have gone and added grind annotations to the point where I think I haven't used any one lemma more than once, so I guess that's the letter of what you've said. I haven't looked heavily into the different variety of grind annotations though, so I'm a bit nervous that I've left ones out, but I also don't want to add too many annotations (would that cause grind to explode or something?). LMK if you want me to do more research into how to annotate so I can give the best annotations here.

[BoltonBailey]

Like for example length_tail_le {α} (l : StackTape α) : l.tail.length ≤ l.length.

It would seem nice if this would be triggered whenever l.tail.length appears, but not when l.length appears, is there a way of annotating this?

Edit, I guess this is what grind_pattern is for!

[chenson2018]

Edit, I guess this is what grind_pattern is for!

Yeah in this case I think what you're asking for is grind_pattern length_tail_le => l.tail, which I believe is equivalent to @[grind! .].

[chenson2018]

Can you also please use scoped with the annotations you have added? (remember that if they are inconveniently nested deep in a namespace, you can add them afterward as an attribute to avoid this)

Edit: I am not sure when, but I remember hearing there will be something like simp sets to make this nicer in the future. We aggressively scope grind annotations for performance reasons.

[chenson2018]

Thanks again for the contribution! I think all my feedback has been addressed. I will wait to merge in case @fmontesi has any comments.