Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(computability/tm_computable): define computable (in polytime) for TMs, prove id is computable in constant time #4048

Closed
wants to merge 45 commits into from
Closed

[Merged by Bors] - feat(computability/tm_computable): define computable (in polytime) for TMs, prove id is computable in constant time #4048

wants to merge 45 commits into from

Conversation

MadPidgeon
Copy link
Collaborator

We define computability in polynomial time to be used in our future PR on P and NP.
We also prove that id is computable in constant time.

MadPidgeon and others added 30 commits August 29, 2020 14:52
@MadPidgeon
Initial commit
ec416a2
@pimsp
Fixed proof of encodek_nat
80c5ca9
@MadPidgeon
minor golf
de00daa
@MadPidgeon
Merge branch 'computability' of https://github.com/leanprover-communi…
8c36f73 
…ty/mathlib into computability
@pimsp
minor golf
acdc360
@pimsp
Fixed merge conflicts
1947bbc
@MadPidgeon
More golfing
ecc57cf
@pimsp
Added unary encoding
c328e76
@pimsp
Merge branch 'computability' of https://github.com/leanprover-communi…
8e5408c 
…ty/mathlib into computability
@pimsp
Fixed minor typo
7abf2c6
@MadPidgeon
Birdy
ced9d32
@pimsp
Added documentation
50c1d7d
@pimsp
Merge branch 'computability' of https://github.com/leanprover-communi…
c609574 
…ty/mathlib into computability
@pimsp
Shortened proof of encodek_num
f8121b1
@MadPidgeon
Completed encoding of basic data types to strings for Turing machines
619ae73
@pimsp
Fixed linter problems
22e2c29
@pimsp
Merge branch 'computability' of https://github.com/leanprover-communi…
1d8443d 
…ty/mathlib into computability
@pimsp
Incorporate changes requested by TwoFX
6d13f0c
@MadPidgeon
Initial commit
4572b18
@MadPidgeon
Initial commit that actually type-checks
f0a2009
@MadPidgeon
cleanup1
f690c6b
@pimsp
refactor all
69d496c
@MadPidgeon
golf + add conversion lemmas
87f36ee
@pimsp
Refactored equality of alphabets to equivalence of alphabets
543c122
@pimsp
Replaced sorry with proofs and added evals_to.refl and .trans
8cd3cb4
@pimsp
Put everything in namespace computability to avoid cluttering root na…
a63c3bd 
…mespace
@pimsp
Merge branch 'computability' into computability-list
ece5f0d
@pimsp
Cleaned up code and started with docstrings
8d0309a
@pimsp
Finished docstrings of defs and structures
d1ff7ab
@pimsp
Added module documentation
13d85df
@robertylewis robertylewis added the awaiting-author A reviewer has asked the author a question or requested changes label Sep 6, 2020
@pimsp pimsp added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 6, 2020
@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 7, 2020
@pimsp
Copy link
Collaborator

pimsp commented Sep 7, 2020

Why is this in the root namespace again? If you put it in the fin_tm2 namespace you can use dot notation. I would suggest putting evals_to and such in the turing namespace, because they are more generic but still generally in computability theory.

Oops, putting everything in turing does make more sense, yeah. That (and your comment just above the quoted comment) has been fixed in the comment of a few seconds ago.

@pimsp pimsp added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 13, 2020
@digama0
Copy link
Member

digama0 commented Sep 14, 2020

LGTM

@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 14, 2020
bors bot pushed a commit that referenced this pull request Sep 14, 2020
@MadPidgeon @pimsp
feat(computability/tm_computable): define computable (in polytime) fo…
ed71b2d 
…r TMs, prove id is computable in constant time (#4048)

We define computability in polynomial time to be used in our future PR on P and NP.
We also prove that id is computable in constant time.

<!-- put comments you want to keep out of the PR commit here -->


Co-authored-by: Pim <spelier.pim@gmail.com>
@bors
Copy link

bors bot commented Sep 14, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(computability/tm_computable): define computable (in polytime) for TMs, prove id is computable in constant time [Merged by Bors] - feat(computability/tm_computable): define computable (in polytime) for TMs, prove id is computable in constant time Sep 14, 2020
@bors bors bot closed this Sep 14, 2020
@bors bors bot deleted the computability-list branch September 14, 2020 10:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 digama0 left review comments

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@jcommelin jcommelin jcommelin left review comments

@pimsp pimsp pimsp left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@MadPidgeon @pimsp @digama0 @robertylewis @bryangingechen @jcommelin