Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. SUBSET-SUM
  5. 34.5. Reduction Machine
  6. 34.5. Choice digits: canonical merger source
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.ReductionMachine.ChoiceDigitMergeCore import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.ReductionMachine.VariableBudget import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.FixedPairSameInputConcat import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.ListMap import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.StatefulFlatMap

Choice digits: canonical merger source

The source contains one unary variable-count template, a separator, and the verified occurrence stream. It is generated by fixed same-input composition.

noncomputable sectionnamespace CLRS.Chapter34.Turing.SubsetSumReductionopen PolyBuilderopen _root_.CLRS.Chapter34.SubsetSumReduction

Canonical input consumed by the choice-digit merger.

def choiceDigitMergeInput (truth : Bool) (input : List CNFSym) : List ChoiceDigitMergeSym := List.replicate (reductionVariableCount (decodeCNF input)) .variableTick ++ [.separator] ++ (choiceOccurrenceCounts truth input).map .count

Two-cell transport code for the eight merger symbols.

def encodeChoiceDigitMergeSymPair : ChoiceDigitMergeSym → UnaryFrameSym × UnaryFrameSym | .variableTick => (.tick, .tick) | .separator => (.tick, .separator) | .count (.digit .zero) => (.tick, .frameEnd) | .count (.digit .one) => (.separator, .tick) | .count (.digit .two) => (.separator, .separator) | .count (.digit .three) => (.separator, .frameEnd) | .count (.digit .four) => (.frameEnd, .tick) | .count .itemEnd => (.frameEnd, .separator)
def decodeChoiceDigitMergeSymPair : UnaryFrameSym → UnaryFrameSym → ChoiceDigitMergeSym | .tick, .tick => .variableTick | .tick, .separator => .separator | .tick, .frameEnd => .count (.digit .zero) | .separator, .tick => .count (.digit .one) | .separator, .separator => .count (.digit .two) | .separator, .frameEnd => .count (.digit .three) | .frameEnd, .tick => .count (.digit .four) | .frameEnd, .separator => .count .itemEnd | .frameEnd, .frameEnd => .separator@[simp] theorem decode_encodeChoiceDigitMergeSymPair (symbol : ChoiceDigitMergeSym) : decodeChoiceDigitMergeSymPair (encodeChoiceDigitMergeSymPair symbol).1 (encodeChoiceDigitMergeSymPair symbol).2 = symbol := by cases symbol with | variableTick | separator => rfl | count symbol => cases symbol with | itemEnd => rfl | digit digit => cases digit <;> rflprivate def choiceDigitVariableTag (input : List Unit) : List ChoiceDigitMergeSym := input.map fun _ => .variableTickprivate def choiceDigitOccurrenceTag (input : List ChoiceCountSym) : List ChoiceDigitMergeSym := input.map .countprivate def choiceDigitSeparatorSpec : StatefulFlatMapSpec Unit CNFSym ChoiceDigitMergeSym where initial := () action _ _ := ([], ()) finish _ := [.separator]private def choiceDigitSeparator (input : List CNFSym) : List ChoiceDigitMergeSym := rewriteStatefulFlatMap choiceDigitSeparatorSpec inputprivate theorem choiceDigitSeparator_eq (input : List CNFSym) : choiceDigitSeparator input = [.separator] := by induction input with | nil => rfl | cons symbol input ih => simpa [choiceDigitSeparator, rewriteStatefulFlatMap, rewriteStatefulFlatMapFrom, choiceDigitSeparatorSpec] using ihprivate noncomputable def choiceDigitVariableSource_computableInPolyTime : _root_.Turing.TM2ComputableInPolyTime id id (fun input : List CNFSym => choiceDigitVariableTag (variableBudgetTicks input)) := by let composed := _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch variableBudgetTicks_computableInPolyTime (listMap_computableInPolyTime (fun _ : Unit => ChoiceDigitMergeSym.variableTick)) simpa [Function.comp_def, choiceDigitVariableTag] using Classical.choice composedprivate noncomputable def choiceDigitSeparator_computableInPolyTime : _root_.Turing.TM2ComputableInPolyTime id id choiceDigitSeparator := statefulFlatMap_computableInPolyTime choiceDigitSeparatorSpecprivate noncomputable def choiceDigitOccurrenceSource_computableInPolyTime (truth : Bool) : _root_.Turing.TM2ComputableInPolyTime id id (fun input : List CNFSym => choiceDigitOccurrenceTag (choiceOccurrenceCounts truth input)) := by let composed := _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch (choiceOccurrenceCounts_computableInPolyTime truth) (listMap_computableInPolyTime ChoiceDigitMergeSym.count) simpa [Function.comp_def, choiceDigitOccurrenceTag] using Classical.choice composedprivate noncomputable def choiceDigitPrefixSource_computableInPolyTime : _root_.Turing.TM2ComputableInPolyTime id id (fun input : List CNFSym => choiceDigitVariableTag (variableBudgetTicks input) ++ choiceDigitSeparator input) := fixedPairSameInputConcat_computableInPolyTime encodeChoiceDigitMergeSymPair decodeChoiceDigitMergeSymPair decode_encodeChoiceDigitMergeSymPair choiceDigitVariableSource_computableInPolyTime choiceDigitSeparator_computableInPolyTime

A fixed polynomial-time TM2 generates the canonical merger input from the same raw CNF word used by the occurrence counter.

noncomputable def choiceDigitMergeInput_computableInPolyTime (truth : Bool) : _root_.Turing.TM2ComputableInPolyTime id id (choiceDigitMergeInput truth) := by let joined := fixedPairSameInputConcat_computableInPolyTime encodeChoiceDigitMergeSymPair decodeChoiceDigitMergeSymPair decode_encodeChoiceDigitMergeSymPair choiceDigitPrefixSource_computableInPolyTime (choiceDigitOccurrenceSource_computableInPolyTime truth) exact { tm := joined.tm inputAlphabet := joined.inputAlphabet outputAlphabet := joined.outputAlphabet time := joined.time outputsFun := fun input => by have output := joined.outputsFun input rw [choiceDigitSeparator_eq] at output simpa [choiceDigitMergeInput, choiceDigitVariableTag, choiceDigitOccurrenceTag, variableBudgetTicks_eq, List.append_assoc] using output }
end CLRS.Chapter34.Turing.SubsetSumReduction