feat(Computability): introduce TapeEncodable class for Turing machine types#591
feat(Computability): introduce TapeEncodable class for Turing machine types#591Sfgangloff wants to merge 2 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.
| @@ -0,0 +1,49 @@ | |||
| Here is the exact code for the new file. | |||
| /- | ||
| Copyright (c) 2026 Silvère Gangloff. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Bolton Bailey, Pim Spelier, Daan van Gent |
| 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).
| /-- 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?
| 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].