Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-27 08:57 2a48225a

View on Github →

feat(computability/tm_to_partrec): partrec functions are TM-computable (#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.

Estimated changes

added inductive turing.partrec_to_TM2.K'
added inductive turing.partrec_to_TM2.Γ'
added inductive turing.partrec_to_TM2.Λ'
added inductive turing.to_partrec.cfg
added inductive turing.to_partrec.code
added inductive turing.to_partrec.cont
modified def turing.TM2.step
modified def turing.TM2.step_aux
added theorem list.tail_subset
added theorem list.tail_suffix
added theorem roption.pure_eq_some
added theorem vector.cons_head
added theorem vector.cons_tail
added theorem vector.cons_val
added theorem vector.tail_val
added theorem function.update_comm
added theorem function.update_idem
deleted theorem vector.cons_val