MLL证明网的编码理论研究
A Coding Theoretic Study on MLL proof nets
摘要：
编码理论对现实世界的应用非常有用。一个明显的例子是数字电视。基本上，编码理论是研究一种检测和/或纠正可能是真或假的数据的方法。此外，编码理论是数学的一个领域，其中数学的许多分支之间存在相互作用，例如，抽象代数、组合数学、离散几何、信息论等。本文提出了一种利用编码理论分析乘法线性逻辑证明网的新方法。我们定义家庭的证明结构，并为每个家庭引入一个度量空间。在每个家庭中，1。MLL证明网是真码元; 2.不是MLL证明网的证明结构是错误的（或损坏的）代码元素。我们的度量的定义优雅地反映了乘法连接词的对偶性。在本文中，我们表明，在框架中的一个错误检测是可能的，但一个错误纠正没有。我们的证明的不可能性的一个纠错是有趣的，在这个意义上说，证明理论的财产证明使用图论的论点。此外，我们表明，仿射逻辑和MLL + MIX是不适合这个框架。这就解释了为什么MLL比类似的逻辑更好。
英文摘要：
Coding theory is very useful for real world applications. A notable example is digital television. Basically, coding theory is to study a way of detecting and/or correcting data that may be true or false. Moreover coding theory is an area of mathematics, in which there is an interplay between many branches of mathematics, e.g., abstract algebra, combinatorics, discrete geometry, information theory, etc. In this paper we propose a novel approach for analyzing proof nets of Multiplicative Linear Logic (MLL) by coding theory. We define families of proof structures and introduce a metric space for each family. In each family, 1. an MLL proof net is a true code element; 2. a proof structure that is not an MLL proof net is a false (or corrupted) code element. The definition of our metrics reflects the duality of the multiplicative connectives elegantly. In this paper we show that in the framework one error-detecting is possible but one error-correcting not. Our proof of the impossibility of one error-correcting is interesting in the sense that a proof theoretical property is proved using a graph theoretical argument. In addition, we show that affine logic and MLL + MIX are not appropriate for this framework. That explains why MLL is better than such similar logics.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
