Information effects
Information effects
复制标题
DOI：
10.1145/2103656.2103667
复制
发表时间：
2012-01
期刊：
影响因子：
37.8
通讯作者：
Roshan P. James;A. Sabry
中科院分区：
文献类型：
--
作者：
Roshan P. James;A. Sabry
计算是一个物理过程，就像所有其他物理过程一样，基本上是可逆的。从类型同构的概念出发，我们导出了一个类型化的、通用的、可逆的计算模型，在该模型中，信息被视为既不能复制也不能擦除的线性资源。我们使用该模型作为计算的语义基础，并证明了类型和效果系统可以捕捉常规不可逆计算和逻辑可逆计算之间的“鸿沟”。我们的类型和效果系统被构建为一种箭头元语言，它将信息的创建和擦除暴露为显式效果操作。不可逆计算源于与隐式信息环境的相互作用，因此使它们成为一个派生概念，很像物理学中的开放系统。我们列出了几个可以从信息影响的显式处理中受益的应用，例如定量信息流安全和差异隐私。
Computation is a physical process which, like all other physical processes, is fundamentally reversible. From the notion of type isomorphisms, we derive a typed, universal, and reversible computational model in which information is treated as a linear resource that can neither be duplicated nor erased. We use this model as a semantic foundation for computation and show that the "gap" between conventional irreversible computation and logically reversible computation can be captured by a type-and-effect system. Our type-and-effect system is structured as an arrow metalanguage that exposes creation and erasure of information as explicit effect operations. Irreversible computations arise from interactions with an implicit information environment, thus making them a derived notion, much like open systems in Physics. We sketch several applications which can benefit from an explicit treatment of information effects, such as quantitative information-flow security and differential privacy.