feat(Computability): introduce TapeEncodable class for Turing machine types#591
feat(Computability): introduce TapeEncodable class for Turing machine types#591Sfgangloff wants to merge 7 commits into
Conversation
crei
left a comment
crei
left a comment
There was a problem hiding this comment.
While I think this is something that is definitely needed, I'm wondering a bit how we would actually encode e.g. a pair.
What I'm getting at is that in order to make this work in a generic way, we need things like "commas" and "parentheses" and a promise that the inner types respect the parentheses.
Of course we could see this as specific to the machine type, and then it would not matter too much if it is not generic.
| import Mathlib.Tactic.Basic | ||
|
|
||
| /-! | ||
| # Turing Machine Tape Encodings |
There was a problem hiding this comment.
I wonder if this should not be a bit more generic, unrelated to Turing machines. Also the class could be called "StringEncodable" (in contrast to the generic Mathlib Encodable that encodes to Nat).
There was a problem hiding this comment.
@crei Thanks, that makes sense. It is true that it may be usable in other contexts.
| /-- Attempts to parse a list of symbols back into the type -/ | ||
| decode : List Symbol → Option α | ||
| /-- Proof that decoding a freshly encoded value yields the original value -/ | ||
| decode_encode_eq : ∀ (a : α), decode (encode a) = some a |
There was a problem hiding this comment.
I wonder if encode_inj : encode.Injective would be nicer here?
There was a problem hiding this comment.
@SamuelSchlesinger I think for the case of Turing machines we want both an encoding and decoding procedure, to interpret the results. In other cases, it is true that we may want some weaker notions of encoding (say, for indexing), but I think that should be introduced at the same time as these use cases.
There was a problem hiding this comment.
Yes, Injective implies the existence of such a decoding, though making it explicit is fine too.
| instance : TapeEncodable (List Symbol) Symbol where | ||
| encode := id | ||
| decode := some | ||
| decode_encode_eq _ := rfl |
There was a problem hiding this comment.
I think it would be nice if we had instances for common types, which I understand is hard to do with a generic Symbol. Feels not so useful without that.
3 participants
Description
This PR addresses phase 1 of #590 (and resolves the first TODO in
Cslib/Computability/Turing/SingleTapeTM.lean).It introduces the
TapeEncodabletypeclass to establish a standardized framework for encoding arbitrary types onto aSingleTapeTMtape. Currently, computability in CSLib is restricted to functions of typeList Symbol → List Symbol. This typeclass is the required foundational step to allowTimeComputableandPolyTimeComputableto operate on standard computable types (likeNat,Bool, pairs, and eventuallyRat).Changes
Cslib/Computability/Turing/Encoding.lean.class TapeEncodable (α : Type) (Symbol : Type).TapeEncodable (List Symbol) Symbolto ensure backwards compatibility with existing machines.public import Cslib.Computability.Turing.EncodingtoSingleTapeTM.lean.Next Steps (Future PRs)
TapeEncodableinstances (Bool,Nat,α × β).TimeComputableto accept arbitrary typesαandβgiven[TapeEncodable α Symbol]and[TapeEncodable β Symbol].