Generating reversible circuits from higher-order functional programs

TL;DR

This paper introduces a novel method for generating reversible circuits from higher-order functional programs using a monadic trace representation, enabling the synthesis of circuits that match the original program's boolean function.

Contribution

It adapts Bennett's approach to higher-order programs, providing a new technique to synthesize reversible circuits from functional code using monadic traces.

Findings

Successfully generated large oracles with Quipper.

Proved that traced circuits compute the same boolean function as the original program.

Demonstrated the approach's effectiveness on 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.