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.

[fmontesi]

Sorry it took me a while to circle back to this.

I don't have first-hand experience in the formalisation of Turing machines, so I might well be off, but I think it'd still be good to have answers to my questions for future reference and other people who will use this.

[fmontesi]

You could also use Symbol or Label for alpha here, as we do in automata/lts.

[chenson2018]

I've been meaning to ask about this actually. This is one area where we allow deviations from the Mathlib style guide, using names instead of Greek letter for type variables. This is fine, but is it a requirement or just something we allow? There are some places that I find the names pretty verbose and occasionally I do find it confusing.

My preference would be to allow this to be author discretion, especially when it's something like this that closely interacts with a Mathlib formalization. I've already done this for instance in Cslib.Foundations.Data.Relation, where I think we agree following the convention for relations is preferable. I think it is similarly nice here that this lines up with Mathlib's TM0, TM1, and TM2.

[fmontesi]

I'm still brainstorming myself about this, but this case is at least weird to see.
The key difference here is that a relation is clearly intended as a concept for 'whatever type', so there's no intuition to give about that type and something not descriptive as α works well. But in a TM, we have an opportunity to give intuition as to what these types are meant to represent within the machinery.

[chenson2018]

I think my example of relations has caused some confusion; let me try to be more clear. These particular symbols are specified (see the doc on Naming Conventions) for this usage in the several models of Turing machines that Mathlib has. I'll also note that these align somewhat with what is used in the literature.

The tradeoff here is between a longer descriptive name versus this connection to the literature and Mathlib notation. My personal position is that that latter is preferable for readability and consistency, but more generally I'm okay with this being at author's discretion (within reason). For instance, if it were up to me automata and LTS would also use Greek letters for type variables, but I felt like this is something that didn't need to be strictly dictated either way.

[chenson2018]

(I also found it helpful when reviewing that these aligned, as it made comparing them much easier)

[BoltonBailey]

I like \alpha because it evokes "alphabet" which is the term I'm most familiar with, but I have also heard "Symbol" so I'll switch to that.

[chenson2018]

I've unresolved this comment just because I'd like to continue the more general discussion. (This can move to Zulip if we'd like)

[chenson2018]

@fmontesi I think the answer to most of your questions here is consistency with Mathlib, which has several notions of Turing Machine that share for instance a naming convention.

(It doesn't hurt to reexamine design questions, just pointing out the context here.)