Generating reversible circuits from higher-order functional programs
Abstract
Boolean reversible circuits are boolean circuits made of reversible elementary gates. Despite their constrained form, they can simulate any boolean function. The synthesis and validation of a reversible circuit simulating a given function is a difficult problem. In 1973, Bennett proposed to generate reversible circuits from traces of execution of Turing machines. In this paper, we propose a novel presentation of this approach, adapted to higher-order programs. Starting with a PCF-like language, we use a monadic representation of the trace of execution to turn a regular boolean program into a circuit-generating code. We show that a circuit traced out of a program computes the same boolean function as the original program. This technique has been successfully applied to generate large oracles with the quantum programming language Quipper.
Cite
@article{arxiv.1603.08213,
title = {Generating reversible circuits from higher-order functional programs},
author = {Benoit Valiron},
journal= {arXiv preprint arXiv:1603.08213},
year = {2016}
}
Comments
21 pages. A shorter preprint has been accepted for publication in the Proceedings of Reversible Computation 2016. The final publication is available at http://link.springer.com