Complexity Theory

[BoltonBailey]

~~A definition of mu-recursive functions (currently on the naturals).~~ It's my hope that this can be the start of computational complexity in mathlib. Anyone who is interested in seeing complexity theory happen should feel welcome to contribute.

Here are a few potential TODOs:

• [x] Create a mapping from mu_recursive, which describes algorithms, to the functions those algorithms compute. Edit: as gebner commented, this already exists in nat.partrec_code.
• [x] Define a non-computable partial function to return the time a particular function takes on a particular input / a proposition to say that a particular function on a particular input terminates in a particular amount of time.
• [ ] Prove useful lemmas for managing statements about time complexity.
• [x] mu-recursive functions are currently from tuples of naturals to naturals. Is there a convenient way of extending this to functions from lists of arbitrary symbols? Note: we are now working with lists of naturals instead.

---

• [x] depends on: #11868 [instances for part]
• [x] depends on: #12001 [lemmas for instances for part]
• [x] depends on : #12109

[gebner]

We already have (essentially) this definition, it's called nat.partrec.code.

Create a mapping from mu_recursive, which describes algorithms, to the functions those algorithms compute.

This is the nat.partrec.code.eval function.

[BoltonBailey]

We already have (essentially) this definition, it's called nat.partrec.code.

Create a mapping from mu_recursive, which describes algorithms, to the functions those algorithms compute.

This is the nat.partrec.code.eval function.

I like that this version has explicit arity, but perhaps it's better not to reinvent the wheel too much. I'm changing the title of this PR to make it more broadly complexity-theory focused.

[leanprover-community-bot-assistant]

This PR/issue depends on:

• ~~leanprover-community/mathlib#11868~~
• ~~leanprover-community/mathlib#12001~~ By Dependent Issues (🤖). Happy coding!

[BoltonBailey]

See discussion here this might not work.

[prakol16]

@BoltonBailey I've implemented this using a new definition of code here: https://github.com/prakol16/lean_complexity_theory_polytime_defs/tree/main/src

Should I use this PR to try to merge them or do you want me to make a new one?

[BoltonBailey]

@prakol16 Seeing as how you're using a different code definition I would suggest making a new PR or PRs. Feel free to reuse any of the code here if it's useful there. I may end up eventually closing this PR without merging.