有界与无界非确定性的外延与内涵语义
计算机科学中的逻辑
2023-06-22 v5
摘要
我们给出了带非确定性的函数式程序的外延与内涵刻画：作为双序之间的保结构函数，以及作为计算它们的有序具体数据结构上的非确定顺序算法。一个基本结果通过建立这两种表示等价来证明：展示了如何构造计算给定单调稳定函数的唯一顺序算法，并描述了顺序算法上对应于关于各序连续性的条件。我们通过为带有限与无限选择算子的顺序函数式语言定义 may-testing 与 must-testing 指称语义来说明。我们证明了这些语义在计算上是充分的，尽管无界非确定性的 must-testing 语义不连续。在有界情形，我们通过确定一个简单通用类型，证明了我们的连续模型关于 may-testing 与 must-testing 是完全抽象的，该类型也可作为无类型 λ-演算模型的基础。在无界情形，我们通过确定可定义元素的进一步“弱连续性”性质，观察到我们的模型包含不被项所表示的可计算函数，并由此证明它不是完全抽象的。
引用
@article{arxiv.1710.10203,
title = {Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism},
author = {James Laird},
journal= {arXiv preprint arXiv:1710.10203},
year = {2023}
}