Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.

A Synthetic Genetic Reversible Feynman Gate in a Single E.coli Cell and its Application in Bacterial to Mammalian Cell Information Transfer

Reversible computing is a nonconventional form of computing where the inputs and outputs are mapped in a unique one-to-one fashion. Reversible logic gates in single living cells have not been demonstrated. Here, we created a synthetic genetic reversible Feynman gate in a single E.coli cell. The inputs were extracellular chemicals, IPTG and aTc and the outputs were two fluorescence proteins EGFP and E2-Crimson. We developed a simple mathematical model and simulation to capture the essential features of the genetic Feynman gate and experimentally demonstrated that the behavior of the circuit was ultrasensitive and predictive. We showed an application by creating an intercellular Feynman gate, where input information from bacteria was computed and transferred to HeLa cells through shRNAs delivery and the output signals were observed as silencing of native AKT1 and CTNNB1 genes in HeLa cells. Given that one-to-one input-output mapping, such reversible genetic systems might have applications in diagnostics and sensing, where compositions of multiple input chemicals could be estimated from the outputs.

Synthesis Strategy of Reversible Circuits on DNA Computers

DNA computers and quantum computers are gaining attention as alternatives to classical digital computers. DNA is a biological material that can be reprogrammed to perform computing functions. Quantum computing performs reversible computations by nature based on the laws of quantum mechanics. In this paper, DNA computing and reversible computing are combined to propose novel theoretical methods to implement reversible gates and circuits in DNA computers based on strand displacement reactions, since the advantages of reversible logic gates can be exploited to improve the capabilities and functionalities of DNA computers. This paper also proposes a novel universal reversible gate library (URGL) for synthesizing n-bit reversible circuits using DNA to reduce the average length and cost of the constructed circuits when compared with previous methods. Each n-bit URGL contains building blocks to generate all possible permutations of a symmetric group of degree n. Our proposed group (URGL) in the paper is a permutation group. The proposed implementation methods will improve the efficiency of DNA computer computations as the results of DNA implementations are better in terms of quantum cost, DNA cost, and circuit length.