关于Zorn引理的计算内容
On the computational content of Zorn's lemma
摘要：
我们给出了一个计算的解释佐恩引理的一个抽象的例子制定为一个wellfoundedness原则的语言中的算术在所有有限类型。这是通过哥德尔的功能解释实现的，并且需要引入一种新的形式的递归在非良基偏序上，其存在于全连续泛函模型中使用域理论技术证明。我们表明，一个实现器的功能解释开放归纳的字典序序列如下作为一个简单的应用程序，我们的主要结果。
英文摘要：
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven using domain theoretic techniques. We show that a realizer for the functional interpretation of open induction over the lexicographic ordering on sequences follows as a simple application of our main results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
