[Merged by Bors] - feat(computability/tm_to_partrec): partrec functions are TM-computable #2792
Conversation
|
|
||
| namespace to_partrec | ||
|
|
||
| inductive code |
There was a problem hiding this comment.
How is this related to partrec_code?
There was a problem hiding this comment.
It is similar in spirit, being a data type that mirrors the construction of partrec, but the basis here is different, using operations on list nat instead of nat -> nat as in partrec or vector nat n -> nat as in partrec'.
There was a problem hiding this comment.
What I actually wanted to ask is whether we should merge the two codes. The difference in denotation (list/vector) shouldn't matter for the codes.
There was a problem hiding this comment.
Oh I see. We could push this modification of the basis up, it is true, although the proof of exists_code relies on partrec', which is a different simplification of the basis used in nat.partrec.code (so there are actually three different bases here: the one on nat ->. nat, vector nat n ->. nat and list nat ->. nat). It's not just that the denotations are different, the basic operations show some awareness of the base type: the nat -> nat version contains functions left, right, pair using the cantor pairing function, the vector -> nat version uses an n-ary composition operation, and this version uses list functions like head and cons. They are all equivalent, of course, but the point of having distinct inductives is so that we can formally state this equivalence and get a usable resulting theorem.
digama0
changed the title
bryangingechen
added
the
awaiting-review
|
The changes outside of the main file look fine to me, and the docs in the main file look very nice. I didn't carefully look through the details of the formalization. @digama0 do you have more changes planned or are you happy with the current state? |
|
@robertylewis The |
|
Okay, I think I've addressed everything, and I'm happy to see this merged whenever. |
|
bors merge |
github-actions
bot
added
ready-to-merge
#2792) A construction of a Turing machine that can evaluate any partial recursive function. This PR contains the bulk of the work but the end to end theorem (which asserts that any `computable` function can be evaluated by a Turing machine) has not yet been stated.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
leanprover-community#2792) A construction of a Turing machine that can evaluate any partial recursive function. This PR contains the bulk of the work but the end to end theorem (which asserts that any `computable` function can be evaluated by a Turing machine) has not yet been stated.
A construction of a Turing machine that can evaluate any partial recursive function. This PR contains the bulk of the work but the end to end theorem (which asserts that any
computablefunction can be evaluated by a Turing machine) has not yet been stated.