用可计算信息格调和Shannon与Scott的信息理论

本文提出了对两种不同信息理论的调和。第一种由Claude Shannon在一部鲜为人知的著作中最初提出，描述了信道的信息内容如何定性但仍抽象地用信息元素（即数据源域上的等价关系）来描述。Shannon证明了这些元素构成一个完备格，其序关系表达一个元素比另一个更具信息性。在安全和信息流语境中，该结构被独立地多次重新发现，并被用作推理信息流的基础。第二种信息理论是Dana Scott的域理论，一个通过特定拓扑上连续函数赋予程序意义的数学框架。Scott的偏序同样表示一个元素比另一个更具信息性，但就计算进展而言，即一个元素是另一个更定义化或演化后的版本。为对程序中的信息流给出令人满意的解释，有必要将两种理论结合考虑，以理解程序作为信道（依Shannon）所传达的信息，以及由其定义性编码（依Scott）所传达的信息。我们通过定义可计算信息格（LoCI）——一个由预序而非等价关系构成的格——来融合这些理论。LoCI保留了Shannon理论的丰富格结构，过滤掉无计算意义的元素，并细化其余信息元素以反映Scott序捕捉的信息呈现方式。我们展示了新理论如何促成终止不敏感信息流性质的首个一般性定义，这是一种被静态程序分析普遍针对的弱化形式的信息流性质。