证明网络与语言处理

贾　青，贾　阳

(1.中国社会科学院 哲学研究所， 北京　100732； 2.河北师范大学 马克思主义学院，石家庄　050024)



证明网络与语言处理

贾青1，贾阳2

(1.中国社会科学院 哲学研究所， 北京100732； 2.河北师范大学 马克思主义学院，石家庄050024)

证明网络是证明的一种图像处理方式。在范畴语法中，由于证明网络具有便于给出语言句法分析这一特点，因此可以说证明网络是范畴语法中“句法分析即推导”这一口号的最佳体现方式之一。为了对证明网络有一个全面的了解，对其大体内容以及在语言处理上的优势做了概述。

范畴语法；证明网络；语言处理；句法分析

一般来说，在范畴语法(categorial grammar)，特别是范畴类型逻辑(categorial type logic)当中，一个系统会有4种不同的表示方式：自然推演表示、Gentzen表示、树模式表示和公理表示。然而，这4种表示或者推演方式所能表示的证明数量并不一定是相同的，因此就会出现一种表示方式比另一种少的问题。本文中所要介绍的证明网络(proof net)就能解决Gentzen演算中所表示的证明数量少于自然推演这一问题。

由于证明网络是在线性逻辑(linear logic)中发展起来的一种推导的图示表示方式。所以本文第一节中将介绍证明网络与线性逻辑的关系，进而在第二节中介绍兰贝克演算的证明网络表示方式。第三节则将证明网络引入语言分析，最后一节给出一些有待解决的问题和进一步的工作。

一、证明网络与线性逻辑

与自然推演相比，Gentzen演算中所能表示的证明数量要少一些。Gentzen演算与自然推演之间的这种一对多的关系被视为Gentzen演算的一个缺点。解决这一问题，主要有如下的两个方式：

[1] 引入Gentzen演算的范式(normal form)；

[2] 保留Gentzen演算原本的样子，转而使用证明网络这一方式。

由此，证明网络这一证明的图像处理方式就被引入到问题的解决中来。

证明网络是在线性逻辑(linear logic)中发展起来的一种推导的图示表示方式，所以在这一节中我们首先介绍一下线性逻辑以及证明网络的关系。

线性逻辑是一类逻辑系统的统称，其中就包括带乘法的线性逻辑(multiplicative linear logic)。Moot和Retoré指出带乘法的线性逻辑是在兰贝克演算的基础上添加交换性条件后得到的逻辑。为了得到一个单独的回旋(involutive)否定和两个蕴涵(左蕴涵和右蕴涵)，我们需要将交换性限制到循环式(cyclic)的交换性上去。如果将带乘法的线性逻辑简称为MLL，那么其证明网络表示中的一些重要定义和结论可被阐述如下：

在图论中，我们可以将一个图定义为一个二元组〈V,E〉，其中V是图中所有端点的集合，而E则是图中边的集合。

定义1.1在一个图G=〈V,E〉中，G的一个匹配(matching)是G本身的一个子图，即由G中的部分端点和部分边构成的集合，这一匹配中每两条边都是不毗连的(没有共同的端点)。

在一个匹配图中，每一个端点连出的边至多是一条。如果这个端点已连出一条边，那么这个端点就称为已匹配的。

图G的一个最大匹配是指边数最多的匹配。一个图的最大匹配可能不止一个，但是最大匹配的边数却是确定的且不可能超过图中端点的一半。

图G的一个完美匹配(perfect matching)是一个包括了图G中原来的所有端点的匹配，是最大匹配的一种。

定义1.2一个R&Β图是一个边带有颜色的图，其中的边要么是蓝色的(B)要么是红色的(R)，而图中的蓝边就定义了一个完美的图匹配。

对于一个R&Β图，我们可以理解为B边对应着公式，而R边则对应着连接词。Moot和Retoré指出上述定义的R&Β图表示对证明的图的认识会涉及到可选择的基本路径(alternate elementary path)的问题[1]。

因为B边是匹配的，所以这就相当于定义了下面这一性质：路径不包括相同的顶点两次(可能的例外情形是，路径上的第一个端点和第二个端点可能会是一个)。更精确地说，一个路径就是一个有穷的边的序列(ai)i∈[1,n]且这一序列满足下面的条件：

[1]i≠j⟹ai≠aj

[2] #(ai∩ai+1)=1

[3]ai∈B⟹ai+1∈R

[4]ai∈R⟹ai+1∈B

定义1.4一个前置网(prenet)是一个基础R&B图，即在连接(link)的基础上建立起来的R&B图。所谓连接可如图1所示。

图1　连接

图1中，α表示原子公式，α⊥表示α的否定。通过这一方式，每一个公式就成为了恰好一个连接和至多一个连接上的前提的结论。连接上，不是前提的公式就被称为前置网络的结论。

因此，我们可以在证明网络中引入原子公式(α)和原子公式的否定(α⊥)以及由已经得到的公式(A和B)得到复合公式(A⊗B或者A⊕B)。

定义1.5给定一个公式C，它的R&B子公式树T(C)就是一个R&B图且可被递归定义如下：

[1] 如果C=α，即一个命题变元，那么T(C)可表示为：

°

α

[2] 假定T(A)和T(B)，T(A⊗B)和T(A⊕B)可被定义如下：

那些对应着子公式树中命题变元的端点被称为子公式树的叶子。

定义1.6给定一个公式的序列Γ，一个带有结论Γ的前置网Π由下面的部分构成：

[1]Γ中公式的R&B子公式树；

[2] 一个B边构成的集合且这一集合中的B边都连接着两个叶子，这些叶子就表示公理且每一个叶子就恰好是一个公理。

一个前置网的结构如图2所示。

图2　前置网的结构

这样的一个前置网实际上就展现出了由前提或者公理得到结论Γ的过程，也即一个证明网络中的证明过程。

值得注意的是，Γ中公式的顺序或者Γ中公式的子公式树都不再是结构中的一部分，但是因为每一端点都带有标记，所以R&B子公式树就区分开了左右子树。

下面，我们给出一个前置网的例子：

并不是所有的前置网都对应着序列证明，而证明网络所要做的就是将对应序列证明的前置网与不对应序列证明的前置网区分开。

定义1.7一个证明网络是满足下面条件的前置网[2]：

二、证明网络与兰贝克演算

兰贝克演算是范畴语法的句法基础，其给出了范畴语法中的很多基本运算规则。在兰贝克演算之后，范畴语法，特别是范畴类型逻辑中的很多句法规则也是在兰贝克演算的基础上增加假设条件(如积算子的结合性等)或者将具有不同的兰贝克演算进行混合(如多模态的范畴类型逻辑)而得到的，所以本节中，我们将说明如何使用证明网络表示兰贝克演算。

对于兰贝克演算的证明网络表示，我们以下面这一推导为例来进行说明。首先看下面的Gentzen推理。

为了得到这一证明网络，需两个步骤：

[1] 在证明网络的叶子部分，同一公理会将前提原子公式与结论原子公式联系起来，与此同时前提和结论会被分别添加上标记•或°。由此，可得下面的证明框架：

[2] 在证明框架的基础上，我们就可以得到一个证明结构通过将每一个原子叶子与其互补的原子叶子连接起来，由此可得：

一个两极的类型Ap由类型A以及极端p=•(输入)或°(输出)构成。在与Gentzen演算和自然推演相关联的证明网络中，带有输入这一极的类型就对应着前提的类型，而带有输出这一极的类型则对应着结论的类型。

对于类型Ap，其两级类型树|Ap|可被定义如下：

如果P是一原子类型，那么|Pp|=Pp

对于任意复合公式，其两级类型数可被定义如下[3]：

可以看到，基本上来说，一个两级类型的两级类型树就是带有两级的句法分析树或公式分析树。依据类型树所对应的Gentzen演算中前提和结论中的新生公式及其子类型分布情况，两级翻译函数(polartranslationfunction)将两个极端从母节点转换到子节点上。

为了介绍证明网络的拉姆达项匹配情况，我们首先给出下面一系列定义：

定义2.1对于任意两级类型X，其补X-可被定义如下：X•-=X°和X°-=X•；两个两极类型是互补的，当且仅当他们是彼此的补。

一个证明框架上的公理连接(axiomlink)就是一对互补的叶子对。

考虑到新生的子类型是由单一子证明得到的还是由多个子证明得到的，我们需要一个全局式的正确的条件，以便附加到证明网络上使得我们能够区分证明中使用规则的数量。因此，p-连接就被用来表示仅使用了一个证明规则且母节点为⊗•， /°,°的连接。

一个范畴证明网络(categorialproofnet)的语义，也就是拉姆达项可被通过如下的方式获得：

[1] 将不同的参数与每一个输出分割点(outputdivisionnode)联系起来；

[2] 在唯一的输出根上，按照下面的规则向上匹配拉姆达项：

(1) 在根节点向上搜索，找到输出为蕴涵式的连接，然后执行拉姆达抽象的操作且这一操作是从相对于向上搜索的输出极的子节点参数得到的；

(2) 向上搜索，找到输出为积连接的母节点，形成一个有序对且有序对中的元素分别是向上搜索得到的右边的子节点(第一个构成元素)和左边的子节点(第二个构成元素)；

(3) 向上搜索直到到达一个原子连接的终端为止，然后在其另一端再向下；

(4) 向下搜索一个蕴含连接的(输入)子节点，执行函数应用的操作且这一操作的执行对象是向上搜索的第一个(输出)子节点上的结果；

(5) 从一个输入的积连接向下搜索左边的子节点，然后取其向下的母节点的第一个投射结果；

(6) 向下搜索一个输出蕴涵连接的输入子节点，返还相连接的参数且反弹；

(7) 向下搜索一个根，然后返还先联系的词库语义且反弹。

由此，证明网络就保持了范畴语法句法与语义推演并行的这一特点。

三、证明网络在语言学中的应用

在这一小节中，我们以量词辖域歧义问题为例来说明证明网络在语言学中的应用。

以下面的语句为例：

[1]Someoneloveseveryone.

[2]Everyoneislovedbysomeone.

对于句[1]和[2]分别有两种解读或者分析结果，分别是：

[1] ∃∀:(存在量词的辖域大于全称量词的辖域)

有一个人，其爱所有的人。

∀∃:(全称量词的辖域大于存在量词的辖域)

对于所有人而言，都存在一个人，这个人爱他她。

[2] ∃∀:(存在量词的辖域大于全称量词的辖域)

存在一个人，其被所有人爱着。

∀∃:(全称量词的辖域大于存在量词的辖域)

对于所有人而言，都存在一个人，他她被这个人爱着。

对于语句[1]和[2]的这两种解读，我们都可以借助证明网络将其表示如下：

对语句[1]的两种分析：

∃∀:有一个人，其爱所有的人。

∀∃:对于所有人而言，都存在一个人，这个人爱他她。

对语句[2]的两种分析：

∃∀:存在一个人，其被所有人爱着。

∀∃:对于所有人而言，都存在一个人，他她被这个人爱着。

四、结论

由上节中的例子可知，我们使用证明网络就能对自然语言中的辖域歧义问题进行处理，即分别给出歧义语句的不同理解，所以证明网络不但从形式化的角度，而且从句法的角度来看都是有意义的，在自然语言处理中也有着一定的应用。近年来，证明网络被更多地应用到自然语言的语句处理上去以便解决自然语言语句处理中的问题。但是鉴于篇幅原因，本文对这一发展方向并未过多涉及；另外，证明证明网络所体现出的各种代数性质问题也值得进一步研究和挖掘，以便于我们能够更为全面和抽象地把握证明网络这一证明的图像表示方式。

[1]MOOTR,RETORÉC.Thelogicofcategorialgrammars[M].London:Springer,2012.[2]MORRILLG.Typelogicalgrammar:categoriallogicofsigns[M].Dordrecht:KluwerAcademicPublishers， 1994.[3]VANBENTHEMJ，TERMEULENA.Handbookoflogicandlanguage(secondedition)[M].Amsterdam:Elsevier，2011.

(责任编辑张佑法)

Proof Net and Language Processing

JIA Qing1, JIA Yang2

(1.Institute of Philosophy, Chinese Academy of Social Sciences, Beijing 100732,China;2.School of Marxism, Hebei Normal University, Shijiazhuang 050024, China)

Proof net is a kind of image processing for proof. In categorial grammar, proof net, as a kind of syntactic parsingstructure, could be used to analyze nature language. Therefore, it perfectly demonstrates the slogan “parsing as deduction”. In order to have a fully understanding of proof net, This paper makes a sketch of its main contents and its advantage in language processing.

categorial grammar; proof net; language processing; syntactic parsing

2016-06-16

国家社会科学基金重大项目“自然语言信息处理的逻辑语义学研究”(10&ZD073)

贾青(1984—)，女，河北沧州人，副研究员，博士，研究方向：语言逻辑、哲学逻辑。

format：JIA Qing, JIA Yang.Proof Net and Language Processing[J].Journal of Chongqing University of Technology(Social Science)，2016(9):14-18.

10.3969/j.issn.1674-8425(s).2016.09.003

B81

A

1674-8425(2016)09-0014-05

引用格式：贾青，贾阳.证明网络与语言处理[J].重庆理工大学学报(社会科学)，2016(9):14-18.