有界和无界非确定性的外延和内涵语义
摘要：函数式程序具有非确定性的外延和内涵特征：作为在biorder之间保持结构的函数，以及作为在有序具体数据结构上计算它们的非确定性顺序算法。一个基本结果表明这些外延和内涵表示是等价的，通过展示如何构造计算给定的单调和稳定函数的唯一顺序算法，并描述与每个顺序连续性相对应的顺序算法上的条件。我们通过定义带有有界和无界选择运算符的顺序函数式语言的may-testing和must-testing指示语义来说明。我们证明了尽管无界非确定性的must-testing语义不连续，但它们在计算上是足够的。在有界情况下，我们通过确定一个简单的通用类型来证明我们的连续模型对于may-testing和must-testing是完全抽象的，该类型也可能成为无类型lambda演算模型的基础。在无界情况下，我们观察到我们的模型包含了不被术语表示的可计算函数，通过确定可定义元素的进一步“弱连续性”特性，并利用这一点证明它不是完全抽象的。
作者：James Laird
论文ID：1710.10203
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22