-
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
[Merged by Bors] - feat(computability/tm_to_partrec): prove finiteness #6955
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM. I don't have any comments on the technical contents, it seems to be as beautiful and elegant as Turing machines can be.
any_goals { | ||
cases finset.insert_subset.1 HS₁ with h₁ h₂, | ||
id { have h₃ := h₂ W } <|> try { simp [finset.subset_iff] at h₂ } }, | ||
{ exact supports_insert.2 ⟨⟨λ _, h₃, λ _, h₁⟩, q_ih H₁ h₂⟩ }, -- move |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should any_goals maybe preserve tags?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps, but I'm not planning on doing anything about that in this PR.
states in `code_supp c k`, so this is a finite state machine. Even though the underlying type of | ||
state labels `Λ'` is infinite, for a given partial recursive function `c` and continuation `k`, | ||
only finitely many states are accessed, corresponding roughly to subterms of `c`. -/ | ||
theorem tr_supports (c k) : @TM2.supports _ _ _ _ _ ⟨tr_normal c k⟩ tr (code_supp c k) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The non-standard inhabited instance is a bit ugly here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The TM2
functions assume that there is a single initial state given by the default
on the type. For this proof we need a family of TMs with different starting points, so we have to override the inhabited instance in the statement.
The proof in this file was incomplete, and I finally found the time to finish it. `tm_to_partrec.lean` constructs a turing machine that can simulate a given partial recursive function. Previously, the functional correctness of this machine is proven, but it uses an infinite state space so it is not a priori obvious that it is in fact a true (finite) turing machine, which is important for the Church-Turing theorem. This PR adds a proof that the machine is in fact finite.
This was already looking good the last time. bors d+ |
✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
The proof in this file was incomplete, and I finally found the time to finish it. `tm_to_partrec.lean` constructs a turing machine that can simulate a given partial recursive function. Previously, the functional correctness of this machine was proven, but it uses an infinite state space so it is not a priori obvious that it is in fact a true (finite) turing machine, which is important for the Church-Turing theorem. This PR adds a proof that the machine is in fact finite.
Pull request successfully merged into master. Build succeeded: |
The proof in this file was incomplete, and I finally found the time to finish it. `tm_to_partrec.lean` constructs a turing machine that can simulate a given partial recursive function. Previously, the functional correctness of this machine was proven, but it uses an infinite state space so it is not a priori obvious that it is in fact a true (finite) turing machine, which is important for the Church-Turing theorem. This PR adds a proof that the machine is in fact finite.
The proof in this file was incomplete, and I finally found the time to
finish it.
tm_to_partrec.lean
constructs a turing machine that cansimulate a given partial recursive function. Previously, the functional
correctness of this machine was proven, but it uses an infinite state
space so it is not a priori obvious that it is in fact a true (finite)
turing machine, which is important for the Church-Turing theorem. This
PR adds a proof that the machine is in fact finite.