一句话：通过Gödel函数解释为有限类型算术中的Zorn引理抽象实例给出计算解释，并引入非良基偏序上的新递归形式。
本文研究如何为在有限类型算术中表述为良基性原理的 Zorn 引理抽象实例赋予计算内容。作者采用 Gödel 函数解释（dialectica 解释）来提取 realizer，并为此引入一种在非良基偏序上的新型递归。该递归在全连续泛函模型中的存在性通过域论技术加以证明。作为主要结果的应用，作者进一步得到序列字典序上开放归纳（open induction）的函数解释 realizer。工作属于证明论与语义学的理论贡献，不涉及实现或实验评估。
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.