Maximilian Wuttke: Bachelor's Thesis
Formalising Multi-Tape Turing Machines in Coq
Advisor: Yannick Forster
We give a formalisation of multi-tape Turing machines in the proof assistant Coq. We make it concrete what it means that a machine is correct by using correctness relations following Asperti and Ricciotti. We implement basic machines and introduce building patterns like sequential composition, if-then-else, do-while, and match that can be used to easily build compound machines. Transformation operations can add new tapes or symbols, or can mirror the behaviour of a machine.
We introduce a class of encoding predicates to define what it means that a tape encodes a value of an encodable type. Using that class of predicates we define correctness relations to make it precise what it means that a machine computes a function.
We define machines that do pattern matching over lists, tuples, sum types, and natural numbers; and machines which can construct new values. We show that these machines can be used to define and prove correctness and termination of machines that compute addition and multiplication.
Initial Seminar Talk:
(21th Dezember 2017)
Second Seminar Talk:
(20th April 2018)