Skip to content

feat(Computability): introduce TapeEncodable class for Turing machine types #591

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Sfgangloff wants to merge 7 commits into
base: main
Choose a base branch
from
Open

feat(Computability): introduce TapeEncodable class for Turing machine types #591

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
73e1fec
Create Encoding.lean
Sfgangloff May 21, 2026
826da9a
Update Basic.lean
Sfgangloff May 21, 2026
9fe102e
AI leftcover cleaning
Sfgangloff May 26, 2026
3e16d6b
fix: name change
Sfgangloff May 26, 2026
09067ea
fix: Change TabeEncodable -> StringEncodable
Sfgangloff May 26, 2026
6373e2a
feat: split to string encoding and encodable + examples of string enc…
Sfgangloff May 27, 2026
bb1e0df
fix: remove .md
Sfgangloff May 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module
public import Cslib.Foundations.Data.BiTape
public import Cslib.Foundations.Data.RelatesInSteps
public import Mathlib.Algebra.Polynomial.Eval.Defs
public import Cslib.Computability.Turing.Encoding

/-!
# Single-Tape Turing Machines
Expand Down
49 changes: 49 additions & 0 deletions Cslib/Computability/Machines/SingleTapeTuring/Encoding.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
Here is the exact code for the new file.
Comment thread
Sfgangloff marked this conversation as resolved.
Outdated

You can create a new file named Encoding.lean in the Cslib/Computability/Turing/ directory and copy-paste this directly into it. I've included the standard copyright header that matches the rest of the files in that folder.

Lean
/-
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
Comment thread
Sfgangloff marked this conversation as resolved.
Outdated
-/

import Mathlib.Tactic.Basic

/-!
# Turing Machine Tape Encodings
Copy link
Copy Markdown

@crei crei May 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Copy Markdown
Author

@Sfgangloff Sfgangloff May 26, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@crei Thanks, that makes sense. It is true that it may be usable in other contexts.


This file defines the `TapeEncodable` typeclass, which provides a framework
for encoding arbitrary types onto a Turing machine tape. This allows us to
define computability for functions on types other than just `List Symbol`.
-/

namespace Turing

variable {Symbol : Type}

/--
A typeclass for types that can be encoded onto a Turing machine tape.
Provides a canonical way to translate back and forth between a type `α`
and a `List Symbol`, alongside a proof that decoding an encoded value succeeds.
-/
class TapeEncodable (α : Type) (Symbol : Type) where
/-- Translates the type into a tape-compatible list of symbols -/
encode : α → List Symbol
/-- 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
Copy link
Copy Markdown
Collaborator

@SamuelSchlesinger SamuelSchlesinger May 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder if encode_inj : encode.Injective would be nicer here?

Copy link
Copy Markdown
Author

@Sfgangloff Sfgangloff May 26, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Copy link
Copy Markdown
Collaborator

@SamuelSchlesinger SamuelSchlesinger May 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, Injective implies the existence of such a decoding, though making it explicit is fine too.


/--
The trivial encoding for `List Symbol` itself.
This ensures backward compatibility with machines that already operate
directly on tape strings.
-/
instance : TapeEncodable (List Symbol) Symbol where
encode := id
decode := some
decode_encode_eq _ := rfl
Copy link
Copy Markdown
Collaborator

@SamuelSchlesinger SamuelSchlesinger May 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


end Turing