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.