feat(MultiTapeTM): Any function constant with finitely many exceptions is computable in constant time and space - #854
Open
crei wants to merge 6 commits into
Open
feat(MultiTapeTM): Any function constant with finitely many exceptions is computable in constant time and space#854crei wants to merge 6 commits into
crei wants to merge 6 commits into
Conversation
eric-wieser
reviewed
Sep 2, 2026
| 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) := |
Collaborator
There was a problem hiding this comment.
This one seems a bit of a shame to make noncomputable;
Collaborator
Author
|
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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.