Hizbullah Abdul Aziz Jabbar: Master's Thesis
Mechanized Undecidability of Halting Problems for Reversible Machines
Advisor: Andrej Dudenhefner
Summary
A reversible machine is a machine whose computation can be traced back in time.
If one considers machines as step relations between configurations, then reversible machines are those whose step relations are left-injective.
Viewed this way, reversibility is a dual to determinism.
Interests in reversible machines stem from Landauer's principle, stating that any logically irreversible manipulation of information such as bit erasure or merging of two computation paths, must be accompanied by a corresponding entropy increase.
In other words, a reversible machine may in principle carry out its computations without releasing any heat.
This thesis aims to mechanize various results in related to reversible machines from the point of view of computability theory.
In particular, we aim to mechanize the undecidability of halting problems of reversible 2-counter machines and reversible cellular automata in Coq.
Goals
-
(Completed) Mechanization of a decision procedure for halting problems of reversible FRACTRAN programs.
-
(Partially completed) Mechanization of a many-one reduction from 2-counter machine to a reversible 2-counter machine using Morita's construction.
We argue in the thesis that the compression step can be done in a similar fashion to the storing history step.
- (Completed) Indegree reduction step
- (Completed) Storing history step
- (Not completed) Compression step
-
(Completed) Definition of one-dimensional and (reversible) two-dimensional cellular automata together with their halting problems.
-
(Completed) Many-one reduction from SBTM to one-dimensional cellular automata.
-
(Completed) Many-one reduction from one-dimensional cellular automata to weakly-reversible two-dimensional cellular automata.
Downloads
Legal notice, Privacy policy
