feat(MultiTapeTM): Any function constant with finitely many exceptions is computable in constant time and space - #854
feat(MultiTapeTM): Any function constant with finitely many exceptions is computable in constant time and space#854crei wants to merge 9 commits into
Conversation
| The empty list has to be added explicitly for the case where `α` is empty: `finiteFunTM` uses | ||
| the elements of this set as its states while reading the input, so the set has to contain the | ||
| starting state `[]` even if there is no input to read. -/ | ||
| noncomputable def encPrefixes (encIn : α ↪ List Bool) : Finset (List Bool) := |
There was a problem hiding this comment.
This one seems a bit of a shame to make noncomputable;
|
It turns out, almost the same machine can compute any function that is constant with a finite number of exceptions. There are two very important functions in this class: Equality and inequality comparison with a constant. This function is a building block in defining a "while" combinator, so I think it's worth it expanding the file. |
crei
changed the title
| exact Cfg.ext_zero_tapes rfl rfl (by simp) | ||
|
|
||
| /-- A constant time bound for the machine `almostConstTM`. -/ | ||
| public def almostConstTime (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (f : α → β) |
There was a problem hiding this comment.
Should there be an @[expose] here? Same with finiteFunTime.
| (Function.uncurry Bool.and) | ||
| (fun _ => c) (fun _ => 0) := by | ||
| intro encIn encOut | ||
| apply encodedComputableInTimeAndSpace_of_finite |
There was a problem hiding this comment.
Function.uncurry fullAdder leaves the output as a function of carry. Could we use fun (a, b, carry) => fullAdder a b carry so the example computes the sum/carry pair from all three input bits?
|
You may have mispushed? |
|
Indeed! sorry ;) |
The merge of `origin/main` split the configuration out into `Configuration.lean` and reworked how a step is taken: `TransitionOut` became `Action`, and the configuration update moved out of `step` into a separate `Action.apply`. The field rename went unnoticed because `almostConstTM` builds its transitions with positional anonymous constructors and the field order did not change, but `step` now stops at `(tm.tr …).apply cfg`, so a `simp only [step, …]` no longer reduces the record projections.
| output : List Symbol | ||
| deriving Inhabited | ||
|
|
||
| /-- Two configurations of a machine without work tapes are equal if their states, input head |
There was a problem hiding this comment.
Another pull request moved this part of Deterministic.lean into its own file, so this lemma is also just moved.
3 participants
This is a starting point of a Turing machine combinator library, it adds one of the leaves:
Any function that is constant with finitely many exceptions is computable in constant time and zero space, relative to any encoding. The same holds for any function with a finite domain.
This result captures many functions we want to compose later or with a combinator library: Any function on tuples of
Bool, for example and "equality comparison with a constant". Together with a "fold" and "composition" combinators, this already allows us to evaluate CNFs or computeNat.succon binary encoded numbers.