魏劳赫变成了布劳威里人
Weihrauch goes Brouwerian
摘要：
我们证明了Weihrauch格可以转化为一个Brouwer代数的连续应用程序的两个封闭运营商在适当的顺序：第一次完成，然后并行化。完备闭包算子是我们引入的一个新的闭包算子。它将任何问题转换为一个完整的问题，在完成各自的类型，我们允许任何值以外的原始域的问题。这个闭包算子本身是有趣的，因为它生成了Weihrauch约简的一个全版本，它的定义类似于Weihrauch约简的通常版本，但是是根据全实现子定义的。从逻辑的角度来看，完成可以被看作是一种使问题独立于其前提的方法。除了完备算子和全Weihrauch约简外，我们还需要研究描述这些概念所需的预完备表示。为了证明平行化的全Weihrauch格构成一个Brouwer代数，我们引入了一个新的乘法蕴涵。虽然并行化的全Weihrauch格形成了具有这种蕴涵的Brouwer代数，但全Weihrauch格在两个不同的方面不能成为直觉线性逻辑的模型。为了查明这一失败的代数原因，我们引入了Weihrauch代数的概念，使我们能够制定准确和整洁的条款失败。最后，我们证明了Medvedev Brouwer代数可以嵌入到我们的Brouwer代数中，这也意味着我们的Brouwer代数的理论是Jankov逻辑。
英文摘要：
We prove that the Weihrauch lattice can be transformed into a Brouwer algebra by the consecutive application of two closure operators in the appropriate order: first completion and then parallelization. The closure operator of completion is a new closure operator that we introduce. It transforms any problem into a total problem on the completion of the respective types, where we allow any value outside of the original domain of the problem. This closure operator is of interest by itself, as it generates a total version of Weihrauch reducibility that is defined like the usual version of Weihrauch reducibility, but in terms of total realizers. From a logical perspective completion can be seen as a way to make problems independent of their premises. Alongside with the completion operator and total Weihrauch reducibility we need to study precomplete representations that are required to describe these concepts. In order to show that the parallelized total Weihrauch lattice forms a Brouwer algebra, we introduce a new multiplicative version of an implication. While the parallelized total Weihrauch lattice forms a Brouwer algebra with this implication, the total Weihrauch lattice fails to be a model of intuitionistic linear logic in two different ways. In order to pinpoint the algebraic reasons for this failure, we introduce the concept of a Weihrauch algebra that allows us to formulate the failure in precise and neat terms. Finally, we show that the Medvedev Brouwer algebra can be embedded into our Brouwer algebra, which also implies that the theory of our Brouwer algebra is Jankov logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
