The theory of classical realizability is a framework for the Curry-Howard correspondence which enables to associate a program with each proof in Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore important to find explicit programs for these axioms. Various solutions have been found for DC, for instance the lambda-term called "bar recursion" or the instruction "quote" of LISP. We present here the first program for AC.
翻译：古典真实性理论是Curry-Howard通信的一个框架,它能够将一个程序与Zermelo-Fraenkel设定的理论中的每一项证据联系起来。但数学在物理、概率、统计等方面的几乎所有应用都使用了分析,即依赖选择的轴(DC),甚至完全的轴(AC)。因此,为这些轴(AC)找到明确的程序非常重要。 已经为DC找到了各种解决方案, 比如叫做“ 条重现” 或 LISP 的“ 引号” 的指示。 我们在这里为 AC 提供了第一个程序 。
相关内容
微信扫码咨询专知VIP会员