一句话：用双序与有序具体数据结构上的非确定顺序算法，统一刻画有界与无界非确定性的外延/内涵语义，并分析 may/must 测试的完全抽象性。
论文研究带非确定性的函数式程序的外延与内涵语义。外延上把程序视为保持结构的双序（biorder）间函数，内涵上用有序具体数据结构上的非确定顺序算法刻画，并证明二者等价：每个单调稳定函数都有唯一顺序算法计算，且算法连续性对应两种序条件。作者为含有限与无限选择算子的顺序函数式语言给出 may-testing 与 must-testing 指称语义，证明计算充分，即便无界情形的 must-testing 不连续。对有界情形，证明连续模型相对 may/must 测试完全抽象，并给出可作无类型 λ 演算基础的泛型；对无界情形，指出模型含不可由项定义的 computable 函数，故不完全抽象。
We give extensional and intensional characterizations of functional programs with nondeterminism: as structure preserving functions between biorders, and as nondeterministic sequential algorithms on ordered concrete data structures which compute them. A fundamental result establishes that these extensional and intensional representations are equivalent, by showing how to construct the unique sequential algorithm which computes a given monotone and stable function, and describing the conditions on sequential algorithms which correspond to continuity with respect to each order. We illustrate by defining may-testing and must-testing denotational semantics for sequential functional languages with bounded and unbounded choice operators. We prove that these are computationally adequate, despite the non-continuity of the must-testing semantics of unbounded nondeterminism. In the bounded case, we prove that our continuous models are fully abstract with respect to may-testing and must-testing by identifying a simple universal type, which may also form the basis for models of the untyped {\lambda}-calculus. In the unbounded case we observe that our model contains computable functions which are not denoted by terms, by identifying a further "weak continuity" property of the definable elements, and use this to establish that it is not fully abstract.
@article{paperbot1263,
title = {Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism},
author = {James Laird},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:11)2021}
}