Generating reversible circuits from higher-order functional programs

DOI10.1007/978-3-319-40578-0_21MaRDI QIDQ3186607zbMATH OpenOpenAlexFDO

Authors Benoît Valiron

Publication date 10 August 2016

Published in Reversible Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.08213

Mathematics Subject Classification ID

Quantum computation (81P68) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Switching theory, applications of Boolean algebras to circuits and networks (94C11) Boolean functions (94D10)

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.

Recommendations

• scientific article; zbMATH DE number 2163011
• Verified compilation of space-efficient reversible circuits
• Realization and synthesis of reversible functions
• Constructive reversible logic synthesis for Boolean functions with special properties
• REVS: a tool for space-optimized reversible circuit synthesis

Cites work

• scientific article; zbMATH DE number 1579275 (Why is no real title available?)
• A structural approach to reversible computation
• Any AND-OR formula of size \(N\) can be evaluated in time \(N^{1/2+o(1)}\) on a quantum computer
• Functional Netlists
• Geometry of synthesis: a structured approach to VLSI design
• Information effects
• Lightweight monadic programming in ML
• Logical Reversibility of Computation
• Quantum Algorithms for the Triangle Problem
• REVS: a tool for space-optimized reversible circuit synthesis
• Synthesis and optimization of reversible circuits -- a survey

Cited in

(3)

• Reversible Functional Array Programming
• Termination of rewriting on reversible Boolean circuits as a free 3-category problem
• Describing and Optimising Reversible Logic Using a Functional Language

Describes a project that uses

Uses Software

• SyReC
• Esterel
• RevKit
• RevLib
• Quipper

This page was built for publication: Generating reversible circuits from higher-order functional programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3186607)