-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Complexity Theory #11046
base: master
Are you sure you want to change the base?
Complexity Theory #11046
Conversation
We already have (essentially) this definition, it's called
This is the |
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. |
Add common instances for `part \alpha` to be inherited from `\alpha`. Spun off of #11046 Co-authored-by: YaelDillies <yael.dillies@gmail.com>
This PR/issue depends on: |
…er-community/mathlib into mu-recursive
See discussion here this might not work. |
@BoltonBailey Should I use this PR to try to merge them or do you want me to make a new one? |
@prakol16 |
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:
mu_recursive
, which describes algorithms, to the functions those algorithms compute. Edit: as gebner commented, this already exists innat.partrec_code
.part
]part
]