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.