From c5e25cbf41f800acc55b867107799b603757e1e4 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:05:09 +0000 Subject: [PATCH] refactor(encodings): retain degree bounds in option decoders --- .../MultiTape/Encodings/Decoder/Basic.lean | 33 +++++++++++++++---- .../MultiTape/Internal/DecoderBasic.lean | 15 +++++++++ 2 files changed, 42 insertions(+), 6 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Decoder/Basic.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Decoder/Basic.lean index b4f50f1fc..1ad978d32 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Decoder/Basic.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Decoder/Basic.lean @@ -25,6 +25,11 @@ output degrees. The basic constructors preserve totality and the round-trip law. * `Turing.MultiTapeTM.Decoder`: total decoding with independent cost and output degrees. * `Turing.MultiTapeTM.Decoder.computableInPolyTime`: the ordinary polynomial-time certificate. * `Turing.MultiTapeTM.Decoder.bits`, `.unary`, `.bool`, `.option`, `.pair`, `.map`: basic decoders. + +## Main results + +* `Turing.MultiTapeTM.Decoder.option_computableInDegree`: option decoding preserves the + supplied output degree, including zero, with cost degree `max 1 (max d e)`. -/ @[expose] public section @@ -66,18 +71,34 @@ def bool : Decoder encBool where decode_enc _ := rfl computable := ⟨1, 1, Internal.DecoderWords.bool_degree⟩ +private theorem option_decode_degree {decode : List Bool → α} {d e : ℕ} + (h : ComputableInDegree decode encBits enc d e) : + ComputableInDegree (fun w => if w.isEmpty then none else some (decode w.tail)) + encBits (encOption enc) (max 1 (max d e)) e := by + have hsome : ComputableInDegree (fun w => some (decode w.tail)) + encBits (encOption enc) (max 1 (max d e)) e := + ((ComputableInDegree.optionSome (enc₁ := enc) (enc := encOption enc)).comp + (h.comp Internal.DecoderWords.tail_degree)).mono (by omega) (by omega) + exact (ComputableInDegree.ite (f := fun _ => none) + (g := fun w => some (decode w.tail)) Internal.DecoderWords.empty_degree + (ComputableInDegree.const none) + (ComputableInDegree.of_encIn_eq Subtype.val (fun _ => rfl) hsome)).mono + (d' := max 1 (max d e)) (e' := e) (by omega) (by omega) + /-- Options are decoded as `none` from the empty word, and otherwise from the tail. -/ def option (D : Decoder enc) : Decoder (encOption enc) where decode w := if w.isEmpty then none else some (D.decode w.tail) decode_enc o := by cases o <;> simp [encOption, D.decode_enc] computable := by obtain ⟨d, e, hD⟩ := D.computable - have hsome := (ComputableInDegree.optionSome (enc₁ := enc) - (enc := encOption enc)).computableInPolyTime.comp - (hD.computableInPolyTime.comp Internal.DecoderWords.tail_degree.computableInPolyTime) - exact (ComputableInPolyTime.ite (encC := encBool) - Internal.DecoderWords.empty_degree.computableInPolyTime - (ComputableInDegree.const none).computableInPolyTime hsome).exists_degree + exact ⟨max 1 (max d e), e, option_decode_degree hD⟩ + +/-- Option decoding preserves any supplied encoded-output degree, including zero. Its cost +accounts for reading the input, running the decoder, and emitting the tagged decoded output. -/ +theorem option_computableInDegree (D : Decoder enc) {d e : ℕ} + (hD : ComputableInDegree D.decode encBits enc d e) : + ComputableInDegree (option D).decode encBits (encOption enc) (max 1 (max d e)) e := + option_decode_degree hD /-- Pairs are decoded from the framed first component and what follows it. -/ def pair {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} (D₁ : Decoder enc₁) diff --git a/ComplexityTests/Machines/Turing/MultiTape/Internal/DecoderBasic.lean b/ComplexityTests/Machines/Turing/MultiTape/Internal/DecoderBasic.lean index 10f6f8932..ddc0cf1f7 100644 --- a/ComplexityTests/Machines/Turing/MultiTape/Internal/DecoderBasic.lean +++ b/ComplexityTests/Machines/Turing/MultiTape/Internal/DecoderBasic.lean @@ -57,3 +57,18 @@ example {α β : Type} (a : α ↪ List Bool) (b : β ↪ List Bool) ⟨⟨fun _ => c, fun _ => 0, DegreeBounded.const c, DegreeBounded.const 0, h⟩, DegreeBounded.const 0⟩ exact ⟨u, ⟨fun _ => (), fun x => Subsingleton.elim _ x, 0, 0, hd⟩, hd⟩ + +-- Optional unary data retains linear cost and output; nested optional Booleans retain constant +-- output even on malformed tag words, rather than inheriting the cost degree as an output bound. +example : + ComputableInDegree (Decoder.option Decoder.unary).decode encBits (encOption encUnary) 1 1 ∧ + ComputableInDegree (Decoder.option (Decoder.option Decoder.bool)).decode + encBits (encOption (encOption encBool)) 1 0 ∧ + (Decoder.option (Decoder.option Decoder.bool)).decode [] = none ∧ + (Decoder.option (Decoder.option Decoder.bool)).decode [false] = some none ∧ + (Decoder.option (Decoder.option Decoder.bool)).decode [false, true] = some (some false) := by + have hbool : ComputableInDegree Decoder.bool.decode encBits encBool 1 0 := + ⟨Internal.DecoderWords.bool_degree.1, ⟨1, fun _ => by simp⟩⟩ + exact ⟨Decoder.unary.option_computableInDegree Internal.DecoderWords.unary_degree, + (Decoder.option Decoder.bool).option_computableInDegree + (Decoder.bool.option_computableInDegree hbool), rfl, rfl, rfl⟩