一句话:用经典可实现性模型刻画非确定性程度,并证明可实现性模型的布尔代数与底层计算模型非确定性程度之间的对偶。
本文研究如何用 Krivine 经典可实现性语言规约不同形式的非确定性,并把它们与可实现性模型的性质联系起来。作者提出一种抽象的多求值关系,用以细致描述各种非确定性行为,由此得到按非确定性程度排序的计算模型层级,类似于 Sazonov 的并行度层级。核心结果是:可实现性模型的特征布尔代数结构与底层计算模型的非确定性程度之间存在对偶关系,从而可用可实现性作为非确定性的一种分类器。
We show how the language of Krivine's classical realizability may be used to specify various forms of nondeterminism and relate them with properties of realizability models. More specifically, we introduce an abstract notion of multi-evaluation relation which allows us to finely describe various nondeterministic behaviours. This defines a hierarchy of computational models, ordered by their degree of nondeterminism, similar to Sazonov's degrees of parallelism. What we show is a duality between the structure of the characteristic Boolean algebra of a realizability model and the degree of nondeterminism in its underlying computational model.