论文标题
全套选择的程序
A program for the full axiom of choice
论文作者
论文摘要
经典可实现性的理论是咖喱 - 霍德对应关系的框架，它使程序能够将一个程序与Zermelo-Fraenkel集理论中的每个证明相关联。但是，几乎所有数学在物理，概率，统计信息等中的应用。使用分析，即依赖选择的公理（DC），甚至是（完整的）选择的公理（AC）。因此，重要的是要找到这些公理的明确程序。已经找到了DC的各种解决方案，例如LAMBDA期间称为“ Bar Recursion”或LISP的指令“ Quote”。我们在这里提出第一个针对AC的程序。
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.
