论文标题
用可计算信息的格子和解香农和斯科特
Reconciling Shannon and Scott with a Lattice of Computable Information
论文作者
论文摘要
本文提出了两种不同信息理论的对帐。最初在鲜为人知的作品中提出的第一个是克劳德·香农（Claude Shannon）提出的，描述了如何定性地描述频道的信息内容，但仍在抽象的信息元素（即与数据源域上的等效关系）方面抽象。香农（Shannon）表明，这些元素形成一个完整的晶格，当一个元素比另一个元素更有用时，订单表达了顺序。在安全性和信息流的背景下，此结构已经独立重新发现了几次，并用作推理信息流的基础。 信息的第二个理论是达娜·斯科特（Dana Scott）的领域理论，这是一个数学框架，将含义作为特定拓扑的连续函数赋予含义。斯科特（Scott）的部分顺序也代表了一个元素比另一个元素更具信息性，而在计算进度的意义上，即当一个元素是另一个元素是另一个元素的更定性或进化版本时。 为了使程序中的信息流令人满意地说明，有必要一起考虑这两种理论，以了解一个被视为渠道的程序传达了哪些信息（àlashannon），但也通过其编码的定义性（àlascott）。我们通过定义可计算信息的晶格（loci），即预订的晶格而不是等效关系来结合这些理论。 Loci保留了香农理论的丰富晶格结构，过滤了没有计算意义的元素，并完善了其余的信息元素，以反映Scott的订购方式如何捕获信息的显示方式。 我们展示了新理论如何促进对终止不敏感的信息流属性的第一个一般定义，这是静态程序分析通常针对的信息流属性的弱化形式。
This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon, describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, i.e. equivalence relations over the data source domain. Shannon showed that these elements form a complete lattice, with the order expressing when one element is more informative than another. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for reasoning about information flow. The second theory of information is Dana Scott's domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott's partial ordering also represents when one element is more informative than another, but in the sense of computational progress, i.e. when one element is a more defined or evolved version of another. To give a satisfactory account of information flow in programs it is necessary to consider both theories together, to understand what information is conveyed by a program viewed as a channel (à la Shannon) but also by the definedness of its encoding (à la Scott). We combine these theories by defining the Lattice of Computable Information (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon's theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott's ordering captures the way that information is presented. We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses.
