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 are already known for DC, for instance the lambda-term known as "bar recursion". We present here the first one, as far as we know, for AC.
翻译：古典真实性理论是Curry-Howard通信的一个框架,它能够将一个程序与Zermelo-Fraenkel设定的理论中的每一项证据联系起来。但是数学在物理、概率、统计等方面的几乎所有应用都使用了分析,即依赖选择的轴数(DC),甚至(完全)选择的轴数(AC)。因此,为这些轴数(AC)找到明确的程序非常重要。对于DC来说,各种解决方案已经众所周知,比如被称为“条状循环”的羊排术语。我们在这里为AC展示了第一个(据我们所知)方案。
相关内容
微信扫码咨询专知VIP会员