Revision #2533 → #3984 · back to history
modifiedGeneral recursive functionse53a924178d7
| Field | From #2533 | To #3984 |
|---|
| note | `Nat.Partrec` inductively defines the class of (partial) general recursive functions on ℕ. | `Nat.Partrec` inductively defines the class of (partial) general recursive functions on ℕ (verified via decl_exists). |
addedλ-calculus2c522d96652f
addedChurch numeralsef51392afe0b
addedTuring machineedfed19cbc48
modifiedTuring computable function93a314102b48
| Field | From #2533 | To #3984 |
|---|
| mathlib.module | Mathlib.Computability.TuringMachine.Computable | Mathlib.Computability.TMComputable |
| moderation_proposal.fields | — | {"mathlib":{"decl":"Turing.TM2Computable","module":"Mathlib.Computability.TuringMachine.Computable","match_kind":"exact"}} |
| moderation_proposal.reason | — | decl_exists reports `Turing.TM2Computable` now lives in `Mathlib.Computability.TuringMachine.Computable`, not in `Mathlib.Computability.TMComputable`. |
| note | `TM2Computable` (and the in-time/poly-time variants) defines what it means for a function to be computed by a finite TM2 Turing machine. | `Turing.TM2Computable` (and the in-time/poly-time variants) defines what it means for a function to be computed by a finite TM2 Turing machine. |
| provenance | ai | ai-moderated |
modifiedEquivalence of computability models96514acbf97a
| Field | From #2533 | To #3984 |
|---|
| note | Mathlib proves a Turing machine TM2 can simulate every `Partrec` function (and `Nat.Partrec.Code.exists_code` encodes Partrec into codes), but the λ-calculus model and a full three-way equivalence are not in Mathlib. | Mathlib proves a Turing machine TM2 can simulate every `Partrec` function (verified via decl_exists), but the λ-calculus model and a full three-way equivalence are not in Mathlib. |
modifiedRosser's identification66968cd3dfef
| Field | From #2533 | To #3984 |
|---|
| note | Mathlib relates `Partrec` and `Nat.Partrec` (and TM via `PartrecToTM2.tr_eval`), giving two of the three identifications but not λ-definability. | Mathlib relates `Partrec` and `Nat.Partrec` (verified via decl_exists) and TM via `PartrecToTM2.tr_eval`, giving two of the three identifications but not λ-definability. |
modifiedTheorem XXX (Kleene)e684b2f3750d
| Field | From #2533 | To #3984 |
|---|
| note | Mathlib proves `Nat.Partrec f ↔ ∃ c, eval c = f`, giving coextensiveness with code-evaluable functions; the full multi-way coextensiveness (μ-recursive, λ-definable, etc.) is not stated. | Mathlib proves `Nat.Partrec f ↔ ∃ c, eval c = f` (verified via decl_exists), giving coextensiveness with code-evaluable functions; the full multi-way coextensiveness (μ-recursive, λ-definable, etc.) is not stated. |
addedTuring complete12b06935b665
addedChurch–Turing–Deutsch principlec00dab4bae59
modifiedBusy Beaver and the halting problem76dac6c3dc6e
| Field | From #2533 | To #3984 |
|---|
| mathlib.decl | — | ComputablePred.halting_problem |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.Computability.Halting |
| note | Without a Busy Beaver definition in Mathlib, this equivalence is not formalized. | Mathlib formalizes the halting problem as non-computable (`ComputablePred.halting_problem`), but Busy Beaver and its equivalence to it are not formalized. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
addedHypercomputer11715bed9a2a