A structural approach to reversible computation
A structural approach to reversible computation
复制标题
DOI：
10.1016/j.tcs.2005.07.002
复制
发表时间：
2005-12-01
影响因子：
1.1
通讯作者：
Abramsky, S
中科院分区：
文献类型：
--
作者：
Abramsky, S
可逆性是计算与物理之间相互关系的一个关键问题，并且随着小型化朝着其物理极限发展，它变得越来越重要。到目前为止，大多数关于可逆计算的基础性工作都集中在对低级机器模型的模拟上。相比之下，我们开发了一种更具结构性的方法。我们展示了高级函数式程序如何能够组合式地（即以一种语法制导的方式）映射到一种简单的自动机中，而这种自动机很容易被看出是可逆的。自动机的大小与函数项的大小呈线性关系。从数学角度来说，我们正在构建一个函数式计算的具体模型。这种构建直接源于交互几何和线性逻辑中产生的思想——但即使不了解这些主题也能理解。事实上，它是对这些主题的一个很好的介绍。同时，从我们的分析中出现了可逆和不可逆计算形式之间一种有趣的逻辑划分。（c）2005爱思唯尔有限公司。保留所有权利。
Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic-but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis. (c) 2005 Elsevier B.V. All rights reserved.