SHF: Small: Information Effects

传统的计算模型是从计算设备的物理实现中显式的能量流(从而信息流)中抽象出来的。这种抽象层的好处是不言而喻的，但它导致了一个概念上的计算模型，不适合于对整个应用程序类别进行推理，包括旨在优化能源使用或旨在在任意攻击者存在的情况下保证信息隐私和安全的系统。更根本的是，计算模型变得不符合物理学的基本定律，这阻碍了探索、模拟和理解自然的相互作用、联系、复杂关系和相互依存的一般能力。为了解决这些问题，该研究基于“信息守恒”的物理原理建立了一个计算模型，用它来揭露信息操纵，并对信息流的安全性、保密性和类似应用进行推理。在技术上，该模型建立在线性逻辑和量子计算模型基础上的类型同构和范畴结构，并将信息视为既不能擦除也不能复制的线性资源。在理论方面，该模型预计将揭示比之前报道的更深入、更优雅的计算对称性。特别是，在信息保守的计算模型中，引入与延续相关的信息债务的概念是很自然的。这些概念可能有助于解决长期存在的与计算的二重性有关的理论问题。着眼于应用，因此为了对可能擦除和复制相对于其环境的信息的开放系统进行推理，模型扩展了基于箭头概念的层，该层允许以类型系统跟踪的方式显式擦除和复制信息。通过在主流编程环境中实现这种扩展模型，将有可能使用编程语言理论的既定工具来推理以系统方式处理信息处理的新的应用程序类。

Conventional models of computation abstract from the explicit flow of energy (and hence information) in physical realizations of computational devices. The benefits of such an abstract layer are self-evident, and yet it results in a conceptual model of computing that is unsuitable for reasoning about entire classes of applications including systems that aim to optimize the use of energy or that aim to guarantee privacy and security of information in the presence of arbitrary attackers. More fundamentally, the computational model becomes at odds with the basic laws of physics which hinders the general ability to explore, model, and understand nature's interactions, connections, complex relations, and interdependencies. To remedy these problems, the research builds a model of computation based on the physical principle of "conservation of information," uses it to expose information manipulation, and to reason about information-flow security, privacy, and similar applications.Technically, the proposed model builds on the type isomorphisms and categorical structures that underlie models of linear logic and quantum computing, and treats information as a linear resource that can neither be erased nor duplicated. On the theoretical side, the model is expected to unveil deeper and more elegant symmetries of computation than have previously been reported. In particular, in a computational model where information is conserved, it is natural to introduce notions of information debts that are related to continuations. Such notions could be useful to addressing long-standing theoretical problems related to the duality of computation. With an eye towards applications, and hence with the aim of reasoning about open systems which may erase and duplicate information relative to their environment, the model is extended with a layer based on the concept of arrows that allows explicit erasure and duplication of information in a way that is tracked by the type system. By implementing this extended model in a mainstream programming environment, it will become possible to reason about new classes of applications that deal with information manipulation in a systematic manner using the established tools of programming language theory.