Computable functions #
This file contains the definition of a Turing machine with some finiteness conditions (bundling the definition of TM2 in TuringMachine.lean), a definition of when a TM gives a certain output (in a certain time), and the definition of computability (in polytime or any time function) of a function between two types that have an encoding (as in Encoding.lean).
Main theorems #
idComputableInPolyTime
: a TM + a proof it computes the identity on a type in polytime.idComputable
: a TM + a proof it computes the identity on a type.
Implementation notes #
To count the execution time of a Turing machine, we have decided to count the number of times the
step
function is used. Each step executes a statement (of type stmt); this is a function, and
generally contains multiple "fundamental" steps (pushing, popping, so on). However, as functions
only contain a finite number of executions and each one is executed at most once, this execution
time is up to multiplication by a constant the amount of fundamental steps.
- K : Type
- kDecidableEq : DecidableEq s.K
- kFin : Fintype s.K
- k₀ : s.K
- k₁ : s.K
- Γ : s.K → Type
- Λ : Type
- main : s.Λ
- ΛFin : Fintype s.Λ
- σ : Type
- initialState : s.σ
- σFin : Fintype s.σ
- Γk₀Fin : Fintype (Turing.FinTM2.Γ s s.k₀)
- m : s.Λ → Turing.TM2.Stmt s.Γ s.Λ s.σ
A bundled TM2 (an equivalent of the classical Turing machine, defined starting from
the namespace Turing.TM2
in TuringMachine.lean
), with an input and output stack,
a main function, an initial state and some finiteness guarantees.
Instances For
The type of statements (functions) corresponding to this TM.
Instances For
The type of configurations (functions) corresponding to this TM.
Instances For
The step function corresponding to this TM.
Instances For
The initial configuration corresponding to a list in the input alphabet.
Instances For
The final configuration corresponding to a list in the output alphabet.
Instances For
A "proof" of the fact that f
eventually reaches b
in at most m
steps when repeatedly
evaluated on a
, remembering the number of steps it takes.
Instances For
Reflexivity of EvalsTo
in 0 steps.
Instances For
Transitivity of EvalsTo
in the sum of the numbers of steps.
Instances For
Reflexivity of EvalsToInTime
in 0 steps.
Instances For
Transitivity of EvalsToInTime
in the sum of the numbers of steps.
Instances For
A proof of tm outputting l' when given l.
Instances For
A proof of tm outputting l' when given l in at most m steps.
Instances For
The forgetful map, forgetting the upper bound on the number of steps.
Instances For
- tm : Turing.FinTM2
- inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ Γ₀
- outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ Γ₁
A Turing machine with input alphabet equivalent to Γ₀ and output alphabet equivalent to Γ₁.
Instances For
- tm : Turing.FinTM2
- inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
- outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
- outputsFun : (a : α) → Turing.TM2Outputs s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a))))
A Turing machine + a proof it outputs f.
Instances For
- tm : Turing.FinTM2
- inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
- outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
- outputsFun : (a : α) → Turing.TM2OutputsInTime s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a)))) (Turing.TM2ComputableInTime.time s (List.length (Computability.Encoding.encode ea.toEncoding a)))
A Turing machine + a time function + a proof it outputs f in at most time(len(input)) steps.
Instances For
- tm : Turing.FinTM2
- inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
- outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
- time : Polynomial ℕ
- outputsFun : (a : α) → Turing.TM2OutputsInTime s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a)))) (Polynomial.eval (List.length (Computability.Encoding.encode ea.toEncoding a)) s.time)
A Turing machine + a polynomial time function + a proof it outputs f in at most time(len(input)) steps.
Instances For
A forgetful map, forgetting the time bound on the number of steps.
Instances For
A forgetful map, forgetting that the time function is polynomial.
Instances For
A Turing machine computing the identity on α.
Instances For
A proof that the identity map on α is computable in polytime.
Instances For
A proof that the identity map on α is computable in time.
Instances For
A proof that the identity map on α is computable.