feat(Computability): Framework for encoding arbitrary types on Turing machines

[Sfgangloff]

Description:

This issue addresses the first TODO in Cslib/Computability/Turing/SingleTapeTM.lean:

"Encoding of types in lists to represent computations on arbitrary types."

Currently, TimeComputable and PolyTimeComputable are restricted to functions of type List Symbol → List Symbol. To expand this to standard computable functions (e.g., over Nat, Bool, pairs, and eventually Rat for Computable Analysis), we need a standardized way to represent arbitrary types on the TM tape.

Proposed Architecture

I propose introducing a TapeEncodable typeclass that bundles the encoding function, the decoding function, and the proof of round-trip correctness:

class TapeEncodable (α : Type) (Symbol : Type) where
  encode : α → List Symbol
  decode : List Symbol → Option α
  decode_encode_eq : ∀ (a : α), decode (encode a) = some a

Implementation Plan

I would like to break this into a few manageable PRs:

• Phase 1 (This week): Introduce the TapeEncodable typeclass and provide the trivial instance for List Symbol.

• Phase 2: Provide basic instances (e.g., for Bool, Nat, and α × β).

• Phase 3: Generalize TimeComputable and PolyTimeComputable to accept arbitrary types α and β given [TapeEncodable α Symbol] and [TapeEncodable β Symbol].

I will start with PR 1.