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 (\`a la Shannon) but also by the definedness of its encoding (\`a 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.

翻译：本文提出对两种信息理论的调和。第一种理论最初由克劳德·香农在一项鲜为人知的工作中提出，描述如何通过信息元素（即数据源域上的等价关系）对信道的信息内容进行定性但依旧抽象的描述。香农证明这些元素构成一个完备格，其中序关系表达了一个元素何时比另一个元素更具信息量。在安全与信息流背景下，这一结构已被独立重新发现多次，并用作推理信息流的基础。第二种信息理论是达纳·斯科特的域理论，这是一种数学框架，用于将程序的意义解释为特定拓扑上的连续函数。斯科特的偏序同样表示一个元素何时比另一个元素更具信息量，但其意义在于计算进展，即一个元素何时是另一元素的更确定或更演化版本。为对程序中的信息流给出满意解释，有必要同时考虑这两种理论，以理解程序作为信道（香农式）所传递的信息，同时也理解其编码的确定程度（斯科特式）。我们通过定义可计算信息格（LoCI）来结合这些理论，该格是预序的格而非等价关系的格。LoCI保留了香农理论的丰富格结构，过滤掉无计算意义的元素，并细化剩余的信息元素以反映斯科特序如何捕捉信息的呈现方式。我们展示新理论如何促成首个通用的终止不敏感信息流属性定义，这是一种静态程序分析常针对的弱化信息流属性形式。