非决定性的认识论

本文提出了一种用于非决定性程序执行的新语义，以替代命题动态逻辑（PDL）的标准关系语义。在这些新语义下，程序执行被表示为从根本上决定性的（即函数式的），而非决定性则作为智能体与系统之间的一种认识论关系出现：直观上，给定过程的非决定性结果恰好是那些无法被预先排除的结果。我们使用拓扑学及动态拓扑逻辑（DTL）框架对这些概念进行形式化。我们证明 DTL 可用于解释 PDL 的语言，且其解释方式能够捕捉上述直觉，此外在该设定中连续函数恰好对应于决定性过程。我们还证明了 PDL 的某些公理化系统在相应的动态拓扑模型类下保持可靠性与完备性。最后，我们利用子集空间逻辑的机制扩展该框架以引入知识，并证明公开宣告的拓扑解释与测试程序的自然解释精确一致。