WEIHRAUCH GOES BROUWERIAN
WEIHRAUCH GOES BROUWERIAN
复制标题
魏赫劳赫走向布劳威尔式
DOI：
10.1017/jsl.2020.76
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Guido Gherardi
中科院分区：
文献类型：
--
作者：
Vasco Brattka;Guido Gherardi
摘要我们证明，可以通过适当的顺序将两个闭合操作员的连续应用转换为Brouwer代数：首先完成，然后再加并行化。完成的封闭操作员是我们介绍的新关闭操作员。它将任何问题转换为整个类型完成的总问题，我们允许在问题的原始域之外允许任何值。该封闭操作员本身就是感兴趣的，因为它产生了Weihrauch降低性的总版本，该版本的定义是像Weihrauch降低性的通常版本一样，但从总体实现者来说。从逻辑的角度完成，可以将其视为使问题独立于其前提的一种方式。除了完成操作员和总的Weihrauch降低性外，我们还需要研究描述这些概念所需的预定表示。为了证明并行的weihrauch晶格形成一个brouwer代数，我们引入了一个新的乘法版本。尽管平行的总静脉晶格构成了brouwer代数的含义，但总的weihrauch晶格并未以两种不同的方式成为直觉线性逻辑的模型。为了指出该失败的代数原因，我们介绍了Weihrauch代数的概念，该代数使我们能够以精确和整洁的术语制定失败。最后，我们表明，梅德韦杰夫·布鲁维尔代数可以嵌入我们的布鲁维尔代数中，这也意味着我们的布鲁维尔代数理论是jankov逻辑。
Abstract 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.
有限 PCFG 的否定消除（书籍章节）
DOI：
--
发表时间：
2005
期刊：
Logic-based Program Synthesis and Transformation, Springer LNCS 3573
影响因子：
--
作者：
Sato;T.;Kameya;Y
通讯作者：
Y
小野，剩余格子：子结构逻辑的代数一瞥
DOI：
--
发表时间：
2007
期刊：
Studies in Logic and the Foundations of Mathematics(Elsevier) 151
影响因子：
--
作者：
N. Galatos;P. Jipsen;T. Kowalski;H
通讯作者：
H