paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Classical realizability as a classifier for nondeterminism

经典可实现性作为非确定性的分类器
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 这篇论文属于纯形式语义/可实现性理论研究,讨论非确定性层级与可实现性模型布尔代数的对偶,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户画像的核心方向几乎没有交集。引用 3 inbox
Guillaume Geoffroy
crossref: 2026-09-12

AI 速览

一句话:用经典可实现性模型刻画非确定性程度,并证明可实现性模型的布尔代数与底层计算模型非确定性程度之间的对偶。

本文研究如何用 Krivine 经典可实现性语言规约不同形式的非确定性,并把它们与可实现性模型的性质联系起来。作者提出一种抽象的多求值关系,用以细致描述各种非确定性行为,由此得到按非确定性程度排序的计算模型层级,类似于 Sazonov 的并行度层级。核心结果是:可实现性模型的特征布尔代数结构与底层计算模型的非确定性程度之间存在对偶关系,从而可用可实现性作为非确定性的一种分类器。

问题
如何用经典可实现性的语言统一规约不同形式的非确定性,并刻画可实现性模型与计算模型非确定性程度之间的关系。
方法
引入抽象的多求值关系来描述各种非确定性行为,定义按非确定性程度排序的计算模型层级,并分析可实现性模型的特征布尔代数。
评估
这是一项理论工作;通过建立特征布尔代数结构与底层计算模型非确定性程度之间的对偶来验证分类框架。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4331,
  title = {Classical realizability as a classifier for nondeterminism},
  author = {Guillaume Geoffroy},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209140}
}