• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Parametrized bar recursion: a unifying framework for readability interpretations of classical dependent choice
【24h】

Parametrized bar recursion: a unifying framework for readability interpretations of classical dependent choice

机译：参数化酒吧递归：古典依赖选择的可读性解释的统一框架

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

During the last 20 years or so, a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work, we present the many variants of bar recursion used in this context as instantiations of a parametrized form of backward recursion, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrized dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi-Bezem-Coquand functional, modified realizability and the more recent products of selection functions of Escardo and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.
机译：在过去的20年左右，已经开发出广泛的古典分析的可实现性解释。在许多情况下，这些通过以某种形式的条形递归扩展基本递归函数的基本递归函数的基本解释系统来实现，这意味着可数或可数依赖性选择的负平移。在这项工作中，我们介绍了这种上下文中使用的条形递归的许多变体作为对位递归的参数化形式的实例化，并在某些条件下给出统一的证明，这伴随该伴随的依次实现了相应的参数化依赖选择原则。从这个证据来看，大多数现有的酒吧递归可实现的解释选择的声音，包括基于Berardi-Bezem-Coquand功能，修改的可实现性和Escardo和Oliva的选择功能的更新产品，因此是一个简单的推论。我们不仅可以比较了一个熟悉的可实现性解释，可以比较熟悉的框架，而是表明这些代表了依赖选择原则的大型潜在解释的简单实例。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号