Domain 论与可观测性质的逻辑

本文使用 Stone 对偶的数学框架，综合了理论计算机科学中若干迄今相互独立的发展：- Domain 论，由 Scott 引入的计算数学理论，作为指称语义的基础。- 由 Milner、Hennessy 等人基于操作语义发展的并发与系统行为理论。- 程序逻辑。Stone 对偶在语义（点空间 = 计算过程的指称）与逻辑（进程性质的格）之间提供了交汇点。此外，其底层逻辑是几何逻辑，在计算上可解释为可观测性质的逻辑——即那些仅凭关于进程执行的有限信息即可判定其是否成立的性质。这些思想引出以下研究纲领：1. 引入一种元语言，包含 - 类型 = 各种计算情境的论域。- 项 = 程序 = 模型或点的语法内涵。2. 给出该元语言的标准指称解释，将类型解释为 domain，将项解释为 domain 元素。3. 该元语言还被赋予一种逻辑解释，其中类型被解释为命题理论，项通过程序逻辑进行解释，该逻辑公理化地描述了项所满足的性质。4. 通过证明这两种解释互为 Stone 对偶来建立其联系。因此，语义与逻辑被保证相互协调，且事实上彼此在同构意义下相互确定。这为一系列应用开辟了道路。给定计算情境在我们的元语言中的指称描述，我们即可按既定步骤推导出该情境的逻辑。