paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Grilliot's trick in Nonstandard Analysis

非标准分析中的 Grilliot 技巧
LMCS vol.Volume 13, Issue 42017匹配度 1/10 · 论文属于数理逻辑/可计算性理论中的非标准分析与图灵跳跃泛函构造,未涉及静态分析、程序验证、浮点/贝叶斯程序分析或 LLM/Agent,与用户当前研究画像几乎没有交集。引用 1 inbox
Sam Sanders
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:利用非标准分析中的标准外延性技巧,从非标准不连续泛函导出图灵跳跃泛函的有效蕴含。

本文研究如何从非标准分析中提取有效内容。Grilliot 技巧可将图灵跳跃泛函 (∃²) 由给定的有效不连续二型泛函显式定义;作者提出与之类似的标准外延性技巧:从某些非标准不连续泛函的存在性推出限制在 Π₁⁰ 公式上的 Transfer 原理,再由这个一般非有效的蕴含消去非标准分析,得到用不连续泛函表达图灵跳跃泛函的有效蕴含。其优点是无需刻意关注有效内容即可获得有效内容。文章还讨论了一类直接来自标准部分公理的新泛函,它们似乎超出已有分类。

问题
如何从非标准分析的存在性论证中系统提取有效/可计算内容,并显式定义图灵跳跃泛函。
方法
通过标准外延性技巧,从非标准不连续泛函推出 Π₁⁰ 限制的 Transfer,再消去非标准原理以得到有效蕴含;同时考察标准部分公理产生的新泛函类。
评估
以数学证明和概念分类为主,说明该技巧能重现 Grilliot 型结果并给出新泛函类,未涉及实现或实验评估。
原文摘要(Abstract)

The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional $(\exists^2)$ in terms of a given effectively discontinuous type two functional. In this paper, we discuss the standard extensionality trick: a technique similar to Grilliot's trick in Nonstandard Analysis. This nonstandard trick proceeds by deriving from the existence of certain nonstandard discontinuous functionals, the Transfer principle from Nonstandard analysis limited to $\Pi_1^0$-formulas; from this (generally ineffective) implication, we obtain an effective implication expressing the Turing jump functional in terms of a discontinuous functional (and no longer involving Nonstandard Analysis). The advantage of our nonstandard approach is that one obtains effective content without paying attention to effective content. We also discuss a new class of functionals which all seem to fall outside the established categories. These functionals directly derive from the Standard Part axiom of Nonstandard Analysis.Comment: 21 pages

链接与引用

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

BibTeX
@article{Sanders17,
  title = {Grilliot's trick in Nonstandard Analysis},
  author = {Sam Sanders},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 4},
  year = {2017},
  doi = {10.23638/lmcs-13(4:23)2017}
}