Proving the Turing Universality of Oritatami Co-Transcriptional Folding

We prove that the Oritatami model of molecular folding is capable of embedding arbitrary computations in the folding process itself, by a local energy optimisation process, similar to how actual biomolecules such as DNA or RNA fold into complex shapes and functions. This result is the first principled construction in this research direction, and motivated the development of a generic toolbox, easily reusable in future work. One major challenge addressed by our design is that choosing the interactions to get the folding to react to its environment is NP-complete. Our techniques bypass this issue by allowing some flexibility in the shapes, which allows to encode different " functions " in different parts of the sequence (instead of using the same part of the sequence). However, the number of possible interactions between these functions remains quite large, and each interaction also involves a small combinatorial optimisation problem. One of the major challenges we faced was to decompose our programming into various levels of abstraction, allowing to prove their correctness thoroughly in a human readable/checkable form. We hope this framework can be generalised to other discrete dynamical systems, where proofs of such large objects are often difficult to get.