关颖雄 康孝军 华东政法大学刑事司法学院 吉林大学哲学社会学院

guanyingxiong@ecupl.edu.cn kxj319@gmail.com

基于英文法律语言的Lambek演算*,†

关颖雄 康孝军 华东政法大学刑事司法学院 吉林大学哲学社会学院

guanyingxiong@ecupl.edu.cn kxj319@gmail.com

本文的主要研究对象是服务于英文法律语言处理的类型逻辑与范畴语法。首先，分析并总结英文法律语言主要的句法特征，由此提出刻画这些特征的类型逻辑与对应的范畴语法。同时，证明了本文所关注的类型逻辑是可判定的且其对应的范畴语法是上下文无关的。本文研究结果为英文法律语言自动处理提供了理论基础。

英文法律语言；类型逻辑；范畴语法

1 引言

法律语言学的研究可以追溯到威廉·布莱克斯通（Sir William Blackstone, 1758）。法律语言学的研究主要分为法医语言与法律语篇（legal discourse）研究。语篇是描述书面和口头交流的术语。法律语篇分析侧重于法律文本、代码和记录的调查分析。法律文件（合同、许可证等）、法庭诉状（传票、判决等）、法律报告和法律信函等构成其研究的语言材料来源。英文法律语篇中的句子包含有许多一般英语表达中不常见的词语、语言结构、语言规则和标点符号的特殊使用方式。英文法律语篇中的句法分析引起不少学者的关注，许多相关研究成果可参考B.Danet的文章（[4]）。

自然语言处理在日常生活或专业工作中都扮演着重要的角色，像法律语言这种特征明显的半结构化的语言在计算机处理中有更广泛的应用。随着大数据的发展，人们需要更快速、有效、准确的地处理大量的法律语篇数据。但传统的基于概率模型的方法难以胜任这一工作，一些传统的语法工具需要极其繁琐的构造，会使计算机处理时间复杂度提高。基于类型逻辑的范畴语法，有着许多优点。简单而言，范畴语法由一个词库和一个推理核心逻辑组成。大多数类型逻辑在自然语言处理中是可判定的，例如Lambek演算与pregroup语法演算。同时，范畴语法是易于修改的，在改变一个范畴语法时，并不需要改变其核心推理逻辑，只需要对词库进行修改即可。Lambek演算由著名的加拿大学者兰贝克（J.Lambek）于1958年提出，用于自然语言处理中的句法分析（[8]）。其核心思想就是：语言认知是数学计算，语法分析是逻辑推演。Lambek演算是自然语言处理一个重要的分支，很多学者都致力于这方面的研究。

本文从英文法律语篇材料和过往研究出发，分析总结了英文法律语篇中语言的句法特征，并根据这些特征反推出适合刻画英文法律语篇的类型逻辑及其对应的范畴语法，同时证明了本文考虑的类型逻辑是可判定的，并且基于该类型逻辑的范畴语法等价于上下文无关语法。值得注意的是本文第一次证明了带收缩（contraction）规则的非结合Lambek演算是可判定的。贾戈尔（G.Jager）论证了收缩规则在处理语法上的照应问题有重要的用途（[6]）。这种语言现象在法律英语中也相当普遍。然而，因为有穷地使用的结合律可被假设集所模拟，所以在Lambek演算上添加收缩规则会导致所得到的逻辑是不可判定的（[3]）。因此，本文所考虑的带假设集的非结合收缩的模态Lambek演算可以被看成该不可判定逻辑的可判定部分。同时，通过对[2]中插补性质的研究，得到一个更进一步的固定插补（fixed Interpolation）性质，该性质即为本文的定理2。

2 英文法律语言的句法特征分析

本文主要关注英文法律语篇中语言的句法特征，并且在此基础上研究使用运算和推演的手段描述法律英语语言的形式化工具。沃克（W.H.Kwok）对大量法律英文句子进行了分析，提出了法律英文句子大量使用了四种语言工具（[7]）：

1.带有非常规意思的常用词，比如“shall”在法律英文句子中更多的是表示一种义务，而不单纯是时态或意愿；

2.二项式表达或多项式表达；

3.名词化；

4.量词化。

这四种语法工具的大量使用通常会带来词法和句法上分析的一些困难。这里，我们将着重分析英文法律句子在句法上大量使用二项式或多项表达式时的特点，并通过构造合适类型逻辑，在范畴语法层面上对这种语言现象进行分析。法律英文句子的一个显著的语言特点就是句子长而且相当复杂。在法律英文句子中有大量的排列式短语存在，有各种短语的互相嵌套等。一般来说，在日常语言中，人们甚少大量使用二项式表达或多项式表达：即两个或多个形式相同的单词序列放在同一语法层次并通常由某种词汇链接。而在法律英文文献中，这种用法却被大量地使用。比如下面的例子：

对简单的二项表达式，如“in life and death”，可以通过在类型语法中对一些词语赋予特别的类型来解决。比如令“and”→(n p)/n，“life,death”→n。那么在经典的Lambek演算中，可以得到“life and death”→np，而在处理类似上面这个复杂例子的时候就无法通过简单更改类型语法词库的赋值来解决问题。贾戈尔（G.Jager）在2004年提出“语言资源的多次使用应该是在句法层面而不应该在词汇层面上进行；在类型逻辑语法下进行的分析应该在Lambek演算L的一个扩张系统中进行表述”（[5]）。这种L的扩张系统被贾戈尔表述为一种受限制的收缩规则的Lambek演算扩张。受贾戈尔的启发，将采用收缩规则来扩张基本的类型语法。收缩规则可以简单的理解为一组类型a1···an在语法分析中可以被多次重复的使用，用逻辑公理的方式表达为：a1···an≤a1···an·a1···an。例如“At his or her request”、“in his or her presence”和“in the presence of each other”均可以由一组类型序列a1···an表示，通过收缩规则可以得到类型a1···an刻画语句“At his or her request and in his or her presence and in the presence of each other”。

其次，另一个法律英文句子的重要特征是wh-词组（如whom、whose）在句子中经常被省略使用。如下面的例子：

在范畴语法中针对wh-词组的语言现象，往往需要引进模态算子如□↓来控制对应类型。含有□↓的类型在某些情况下可以进行位置移动（通过交换律和结合律实现）。which通常会被赋值为(n )/(s/□↓np)，其中(s/□↓np)指一个句子在某个地方缺少了一个名词词组。而对wh-词组被直接省略的句子，如上面的例子，则同样可以使用收缩规则结合算子□↓来处理，在合适的地方使用上面提到的收缩规则增加缺失的名字词组(□↓np)，并利用模态算子□↓控制np位置的变换。

通过对一些法律句子的考察，可以发现法律英文句子还有一重大特征：法律英文句子具有很明显的语法标记特征，这些句子基本是以第三人称的形式来书写。除非在非常特殊的场合，不然不会出现用第一人称和第二人称表达的语句。唯一例外的就只有遗嘱，由于遗嘱本身的特殊性，它多数是以第一人称书写，但为了显示句子的客观性，往往遗嘱中句子会使用被动语态来平衡第一人称的主观性。另外，在每个法律英文文档中都可以发现大量的被动语态被使用，被动语态出现的频率远高于主动语态。

综上所述，为了刻画上面总结的英文法律语篇中语言的句法特征，我们反推出所需的类型逻辑必须包含有收缩规则和模态算子，同时出于计算性方面的考虑结合律可以被放弃，因此我们将使用带有模态算子与收缩规则的非结合Lambek演算扩张来刻画英文法律语句。

3 基于英文法律语言句法特征的类型逻辑

Lambek演算L以及与其类似的类型逻辑演算常常用于自然语言的信息处理中，在这里我们考虑其非结合的形式，即通常所说的非结合Lambek演算NL。我们考虑非结合Lambek演算的模态扩张NL♢。NL♢可以被表达为根岑序列演算的形式。NL♢公式的递归定义如下：公式结构被递归地定义为要么是单一的公式，要么是公式结构的合并：(Γ◦Δ),〈Δ〉，其中◦、〈〉是与·、♢相对应的公式结构算子。最早的根岑序列演算是由兰贝克给出（[9]）。定义序列为如下的结构：Γ⇒A，其中Γ是一个公式结构，A是一个公式。NL♢可以由下面的公理与规则进行表示

公理：

推理规则：

如果序列Γ⇒A在NL♢下是可推演的则将其记为⊢NL♢Γ⇒A。

同时考虑使用带如下收缩规则(C)的NL扩张系统。

该系统被记为NL♢c。下面证明NL♢c是可判定的。首先，需要证明NL♢c具有子公式性质：对于任意序列Γ⇒A如果其在系统NL♢c可证，必然包含一个证明使得所有出现在证明的序列中的公式均为Γ⇒A中公式的子公式。这里将采用[11]中的方法。这里，引入(Mix)规则表示如下：

令NL♢c为用(Mix)规则替换NL♢c中(Cut)规则所得的系统。

此时，先对Γ1⇒A,Γ2⇒B和Γ3[Δ1[A◦B]◦···◦Δ1[A·B]]⇒C分别使用(Mix)规则，那么根据第一重归纳假设，此时的(Mix)公式长度较小，因此可以消除。然后再对Γ1◦Γ2⇒A·B与Γ1[Δ3[Δ[Γ1◦Γ2]◦···◦Δ[A·B]]]⇒C使用(Mix)规则，因为该(Mix)规则的两前提证明总长度比之前小1，那么根据第二重归纳假设该(Mix)规则可被消除。

推论1如果⊢NL♢cΓ⇒A，那么Γ⇒A存在一个在NL♢c中不包含任何(Mix)规则的证明。

推论2NL♢c满足子公式性质。

下面证明另一个重要的定理，称为固定插补定理（fixed interpolation theorem）。

定理2对于任意的(B◦C)，如果⊢NL♢cΓ[B◦C]⇒A，那么存在一个固定的公式D满足：⊢NL♢cB◦C⇒D和⊢NL♢cΓ[D]⇒A，并且D是Γ⇒A中出现的公式的子公式。

证明.由推论2可得，Γ[B◦C]⇒A存在一个不包含(Cut)规则的证明。假设Γ[B◦C]⇒A是由规则R所得，下面分情况讨论：

·(B◦C)不是由R所生成，那么(B◦C)必然存在R规则的前提中，证明可直接由归纳假设与R规则得到。

·(B◦C)是由R所生成。假设R=(L)的前提为B⇒C1和Γ[C2]⇒A。因为⊢NL♢cB◦C1C2⇒C2，所以D=C2。对R=(/L)，同理可证。假设R=(·L)的前提为Γ[B·C]⇒A，那么D=B·C。

·(B◦C)是由R所生成。假设R=(C)的前提为Γ[(B◦C)◦(B◦C)]⇒A.由归纳假设得存在着公式D满足⊢NL♢c(B◦C)⇒D和⊢NL♢cΓ[D◦D]⇒A。再由(C)规则可得⊢NL♢cΓ[D]⇒A。

综上所述，定理得证。

由定理2，可以轻易推导出如下定理：

定理3如果⊢NL♢cΓ[Δ]⇒A，那么存在一个固定公式D满足：⊢NL♢cΔ⇒D和⊢NL♢cΓ[D]⇒A，并且D是Γ⇒A中出现的公式的子公式。

注意定理2对于定理3的证明起到至关重要的作用。我们无法使用归纳假设的办法直接证明定理3。因为当Γ[Δ]⇒A是由Γ[Δ◦Δ]⇒A使用(C)规则得到时，根据归纳假设，将存在两个公式D1D2满足定理的条件。但是因为归纳假设并不保证D1=D2，无法从Γ[D1◦D2]⇒A得到Γ[D1]⇒A或Γ[D2]⇒A，因此无法证明该定理。这个问题最初被描述于[5]。

下面证明NL♢c是可判定的。令Φ为形如A⇒B的序列的有穷集合，布茨考夫斯基（W.Buszkowski）（[1]）证明了如下命题：

命题1对于任意的Γ⇒A,Φ⊢NLΓ⇒A是可判定的。

任给一个序列Γ⇒A,令T为其所有公式的子公式的集合，定义Φ={A⇒A·A|A∈T}。那么：

定理4⊢NL♢cΓ⇒A，当且仅当Φ⊢NLΓ⇒A。

证明.从右到左的方向的证明是显然的，因为Φ中任何序列在NL♢c下显然可证。对于从左到右的证明，由定理3可得，对于Γ⇒A在NL♢c中的证明，都可以被改写成一不包含有(C)规则但仍保持子公式性质的证明。即使用D⇒D·D和(Cut)规则代替(C)规则，并且由于定理3，D∈T通过施归纳假设于Γ⇒A在NL♢c中的证明所使用的(C)规则个数可以轻易证得该结论。而Γ⇒A在NL♢c中的这种证明恰恰就Γ⇒A在NL中从Φ出发的一个推演。

4 英文法律语言的范畴语法

范畴语法的精准定义如下：范畴语法可以被定义为基于一个类型逻辑TL上的三元组G=〈Σ,I,D〉：

·Σ是非空字符串集合；

·I是一个从Σ到TL公式集的映射；

·D是一个特殊的公式。

通常D是一个原子公式，比如s。基于TL逻辑的范畴语法通常称为TL语法。TL语法G=〈Σ,I,D〉所接受的语言可以定义为一个字符串序列a1···an，其中ai∈Σ,1≤i≤n,且n≥1满足：存在A1,...,An和Γ使得对所有1≤i≤n〈ai,Ai〉∈I,使得Φ⊢TLΓ⇒D和st(Γ)=A1···An。st(Γ)表示一个由公式结构去掉所有结构算子产生的公式序列。

下面证明一个结论NL♢c语法等价于上下文无关语法。证明思路如下：证明被NL♢c语法所接受的语言同样能被一个上下文无关语法所接受。首先需要构造一个与NL♢c等价的系统。给定公式集T，令S为如下系统：

·公理：NL♢c中所有可证的形如A◦B⇒C,〈A〉⇒B和A⇒B的序列，其中A,B,C∈T；

·推演规则：切割规则(Cut)。

给定公式集T使得其包含序列Γ⇒A中所有公式的子公式，构造S如上，可证如下引理：

引理1⊢NL♢cΓ⇒A当且仅当⊢SΓ⇒A。

证明.从右到左方向自然成立。现在考虑从左到右方向，证明基于定理2，施归纳假设于Γ中公式的个数即可证得结论。

现在从一个NL♢c语法G=〈Σ,I,D〉来构造一个上下文无关语法。定义公式集T使得其包含所有D,I中出现的公式并对子公式闭包，S定义如上。上下文无关文法构造如下：终结符为Σ中字符串，非终结符为T中公式，开始符号为D，生成规则被定义为：{A→B:⊢SB⇒A}∪{A→B:⊢S〈B〉⇒A}∪{A→BC:⊢SB◦C⇒A}∪{A→v:〈v,A〉∈I}。

结合[1]中结论，任何一个上下文无关语法都是一个范畴语法，可以得到如下定理。

定理5NL♢c语法等价于上下文无关文法。

5 小结

本文从法律英文句子出发，研究分析法律英文句法的特征，在此基础上构建了相应的类型逻辑和范畴语法。对应的范畴语法可以用来模拟法律英文句子检测。从定理5可知基于本文考虑的范畴语法，我们可以通过构造等价的上下文无关语法，并且利用上下文无关语法已知的算法，如CYK算法等对NL♢c语法进行计算模拟实现。

[1]W.Buszkowski,2005,“Lambek calculus with nonlogical axioms”,in C.Casadio,P.J. Scott and R.A.G.Seely(eds.),Language and Grammar,pp.77–93.

[2]W.Buszkowski,2011,“Interpolation and FEP forlogics of residuated algebras”,Logic Journal of IGPL,19(3):437–454.

[3]K.Chvalovsky and R.Horcik,2004,“Full Lambek calculus with contraction is undecidable”,Journal of Symbolic Logic,1(2):1–17.

[4]B.Danet,1985,“Legal discourse”,in T.A.van Dijk(ed.),Handbook of Discourse Analysis,vol.1,pp.273–291,London:Academia Press.

[5]G.Jager,2004,“Residuation,structural rules and context freeness”,Journal of Logic, Language and Information,vol.13,pp.47–59.

[6]G.Jager,2005,Anaphora and Type Logical Grammar,Netherlands:Springer.

[7]W.H.Kwok,2000,Some linguistic devices in legal English that cause problems to the translation of legislative texts from English to Chinese,PhD thesis,Western Sydney University.

[8]J.Lambek,1958,“The mathematics of sentence structure”,American Mathematical Monthly,65(3):154–170.

[9]J.Lambek,1961,“On the calculus ofsyntactic types”,in R.Jakobson(ed.),Structureof Language and Its Mathematical Aspects,pp.168–178,Rhode Island:American Mathematical Society.

[10]M.Moortgat,1996,“Multimodallinguistic inference”,JournalofLogicLanguageand Information,5:349–385.

[11]H.Ono,1998,“Proof-theoretic methods in nonclassical logic–An introduction”,Theories of Types and Proofs,pp.207–254.

（责任编辑：潘琳琦）

A Lambek Calculus of English Legal Language

Yinxiong Guan
School of Criminal Justice,East China University of Political Science and Lawguanyingxiong@ecupl.edu.cn
Xiaojun Kang
School of Philosophy and Sociology，Jilin Universitykxj319@gmail.com

In this paper,we analysis the main syntactic features of English legal discourse on the grammar level.Then we design a extended Nonassociative Lambek calculus and its corresponding categorial grammars for processing of English legal discourse.Finally, we prove that our system is decidable and the corresponding grammars are context-free. The results will provide a theoretical basis for the automatic processing of English legal language.

B81

A

2016-03-07；

2016-08-31

国家社会科学基金青年项目（15CZX045）。

†致谢：感谢匿名审稿人对本文的帮助。本文通讯作者为康孝军。