Library ProgrammingTuringMachines.TM.Prelim

Library ProgrammingTuringMachines.TM.Relations

• Relations
  • Relational operators on labelled relations
  • Relations over Vectors
  • Reflexive transitive closure and relational power

Library ProgrammingTuringMachines.TM.TM

• Definition of Multi-Tape Turing Machines
  • Definition of the tape
  • Definition of moves
    • Rewriting Lemmas
  • Machine step
  • Rewriting tactics
  • Nop Action
  • Mirror tapes
  • Helping functions for tapes
  • Mapping tapes
  • Lemmas about tape_move_left' and tape_move_right'
  • Definition of Multi-Tape Turing Machines
    • Configurations of TMs
    • Machine execution
    • Realisation
    • Termination/Runtime
    • Canonical relations
  • Automation of the generation of relations

Library ProgrammingTuringMachines.TM.Basic.Basic

Library ProgrammingTuringMachines.TM.Basic.Null

• 0-tape Turing machine that does nothing.
  • Tactic Support

Library ProgrammingTuringMachines.TM.Basic.Mono

• Basic 1-Tape Machines
  • Helper functions
  • Do a single action
    • Derived Machines
  • Read a symbol
  • Tactic Support

Library ProgrammingTuringMachines.TM.Combinators.Combinators

• Combinators
  • Simple Combinators
  • Tactic Support

Library ProgrammingTuringMachines.TM.Combinators.Switch

• Switch Combinator

Library ProgrammingTuringMachines.TM.Combinators.SequentialComposition

Library ProgrammingTuringMachines.TM.Combinators.If

Library ProgrammingTuringMachines.TM.Combinators.While

• • Correctness of While
  • Termination of While
  • (Co-) Induction Principle for Correctness (Running Time) of While

Library ProgrammingTuringMachines.TM.Combinators.Mirror

• Mirror Operator

Library ProgrammingTuringMachines.TM.Lifting.Lifting

Library ProgrammingTuringMachines.TM.Lifting.LiftTapes

• Tapes-Lift
• Tactic Support

Library ProgrammingTuringMachines.TM.Lifting.LiftAlphabet

• Alphabet-Lift

Library ProgrammingTuringMachines.TM.Compound.TMTac

• Tactics that help verifying complex machines

Library ProgrammingTuringMachines.TM.Compound.Multi

• Simple compound multi-tape Machines
  • Nop
  • Diverge
  • Move two tapes
  • Copy Symbol
  • Read Char
  • Tactic Support

Library ProgrammingTuringMachines.TM.Compound.WriteString

Library ProgrammingTuringMachines.TM.Compound.MoveToSymbol

• Move to a symbol and translate read symbols

Library ProgrammingTuringMachines.TM.Compound.CopySymbols

• Copy Symbols from t0 to t1

Library ProgrammingTuringMachines.TM.Code.Code

• Codable Class

Library ProgrammingTuringMachines.TM.Code.CodeTM

• Value-Containing
  • Right tapes
  • Definition of the computation relations
  • Computes relation with two arguments

Library ProgrammingTuringMachines.TM.Code.WriteValue

Library ProgrammingTuringMachines.TM.Code.ChangeAlphabet

• Alphabet-lift for "programmed" Turing Machines
  • Definition of the lifted machine
  • Function Computation of the lifted machine
  • Tactic Support

Library ProgrammingTuringMachines.TM.Code.Copy

• Copying Machines and Helper functions for verifying machines using CopySymbols ane MoveToSymbol

Library ProgrammingTuringMachines.TM.Code.ProgrammingTools

• All tools for programming Turing machines

Library ProgrammingTuringMachines.TM.Code.CaseNat

• Constructor and Deconstructor Machines for Natural Numbers
  • Deconstructor
  • Constructors
  • Tactic Support

Library ProgrammingTuringMachines.TM.Code.CaseSum

• Constructor and Deconstructor Machines for Sum Types and Option Types
  • Deconstructor for Sum Types
  • Constructors for Sum Types
  • Tactic Support for Sum Types
  • Deconstructor for Option Types
  • Constructors for Option Types
  • Tactic Support for Option Types

Library ProgrammingTuringMachines.TM.Code.CaseList

• Constructor and Deconstructor Machines for Lists
  • Deconstructor
    • Corectness
    • Termination
  • IsNil
  • Constructors
    • nil
    • cons
  • Compatibility of running time functions with encoding mapping
  • Tactic Support

Library ProgrammingTuringMachines.TM.Code.CaseFin

• Constructors and Deconstructors for Finite Types

Library ProgrammingTuringMachines.TM.Code.CasePair

• Constructors and Deconstructors for Pair Types
  • Deconstructor
  • Constructor
  • Compatibility of running time functions with mapping of encodings
  • Tactic Support

Library ProgrammingTuringMachines.TM.Code.SumTM

Library ProgrammingTuringMachines.TM.Code.NatTM

• Machines that compte natural functions
  • Addition
    • Correctness of Add
    • Termination of Add
  • Multiplication
    • Correctness of Mult
    • Termination of Mult

Library ProgrammingTuringMachines.TM.Code.ListTM

• Machines that compute list functions
  • Implementation of nth_error
  • Other Implementation of nth_error
  • Append
  • Length

Library ProgrammingTuringMachines.TM.LM.Semantics

• Semantics of the Heap Machine

Library ProgrammingTuringMachines.TM.LM.Alphabets

• Alphabets

Library ProgrammingTuringMachines.TM.LM.CaseCom

• Constructors and Deconstructors for Comens

Library ProgrammingTuringMachines.TM.LM.LookupTM

• Heap Lookup

Library ProgrammingTuringMachines.TM.LM.JumpTargetTM

• Implementation of ϕ (aka SplitBody)

Library ProgrammingTuringMachines.TM.LM.StepTM

• Step Machine of the Heap Machine Simulator

Library ProgrammingTuringMachines.TM.LM.HaltingProblem

• Reduction of the Halting Problem of the Heap Machine to the Halting Problem of Turing Machines