License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ISAAC.2018.23
URN: urn:nbn:de:0030-drops-99715
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9971/
Go to the corresponding LIPIcs Volume Portal


Geary, Cody ; Meunier, Pierre-Étienne ; Schabanel, Nicolas ; Seki, Shinnosuke

Proving the Turing Universality of Oritatami Co-Transcriptional Folding

pdf-format:
LIPIcs-ISAAC-2018-23.pdf (8 MB)


Abstract

We study the oritatami model for molecular co-transcriptional folding. In oritatami systems, the transcript (the "molecule") folds as it is synthesized (transcribed), according to a local energy optimisation process, which is similar to how actual biomolecules such as RNA fold into complex shapes and functions as they are transcribed. We prove that there is an oritatami system embedding universal computation in the folding process itself.
Our result relies on the development of a generic toolbox, which is easily reusable for future work to design complex functions in oritatami systems. We develop "low-level" tools that allow to easily spread apart the encoding of different "functions" in the transcript, even if they are required to be applied at the same geometrical location in the folding. We build upon these low-level tools, a programming framework with increasing levels of abstraction, from encoding of instructions into the transcript to logical analysis. This framework is similar to the hardware-to-algorithm levels of abstractions in standard algorithm theory. These various levels of abstractions allow to separate the proof of correctness of the global behavior of our system, from the proof of correctness of its implementation. Thanks to this framework, we were able to computerise the proof of correctness of its implementation and produce certificates, in the form of a relatively small number of proof trees, compact and easily readable/checkable by human, while encapsulating huge case enumerations. We believe this particular type of certificates can be generalised to other discrete dynamical systems, where proofs involve large case enumerations as well.

BibTeX - Entry

@InProceedings{geary_et_al:LIPIcs:2018:9971,
  author =	{Cody Geary and Pierre-{\'E}tienne Meunier and Nicolas Schabanel and Shinnosuke Seki},
  title =	{{Proving the Turing Universality of Oritatami Co-Transcriptional Folding}},
  booktitle =	{29th International Symposium on Algorithms and Computation  (ISAAC 2018)},
  pages =	{23:1--23:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-094-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{123},
  editor =	{Wen-Lian Hsu and Der-Tsai Lee and Chung-Shou Liao},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9971},
  URN =		{urn:nbn:de:0030-drops-99715},
  doi =		{10.4230/LIPIcs.ISAAC.2018.23},
  annote =	{Keywords: Molecular computing, Turing universality, co-transcriptional folding}
}

Keywords: Molecular computing, Turing universality, co-transcriptional folding
Collection: 29th International Symposium on Algorithms and Computation (ISAAC 2018)
Issue Date: 2018
Date of publication: 06.12.2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI