關(guān)穎雄 康孝軍 華東政法大學(xué)刑事司法學(xué)院 吉林大學(xué)哲學(xué)社會(huì)學(xué)院

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

基于英文法律語(yǔ)言的Lambek演算*,?

關(guān)穎雄 康孝軍 華東政法大學(xué)刑事司法學(xué)院 吉林大學(xué)哲學(xué)社會(huì)學(xué)院

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

本文的主要研究對(duì)象是服務(wù)于英文法律語(yǔ)言處理的類型邏輯與范疇語(yǔ)法。首先，分析并總結(jié)英文法律語(yǔ)言主要的句法特征，由此提出刻畫這些特征的類型邏輯與對(duì)應(yīng)的范疇語(yǔ)法。同時(shí)，證明了本文所關(guān)注的類型邏輯是可判定的且其對(duì)應(yīng)的范疇語(yǔ)法是上下文無(wú)關(guān)的。本文研究結(jié)果為英文法律語(yǔ)言自動(dòng)處理提供了理論基礎(chǔ)。

英文法律語(yǔ)言；類型邏輯；范疇語(yǔ)法

1 引言

法律語(yǔ)言學(xué)的研究可以追溯到威廉·布萊克斯通（Sir William Blackstone, 1758）。法律語(yǔ)言學(xué)的研究主要分為法醫(yī)語(yǔ)言與法律語(yǔ)篇（legal discourse）研究。語(yǔ)篇是描述書面和口頭交流的術(shù)語(yǔ)。法律語(yǔ)篇分析側(cè)重于法律文本、代碼和記錄的調(diào)查分析。法律文件（合同、許可證等）、法庭訴狀（傳票、判決等）、法律報(bào)告和法律信函等構(gòu)成其研究的語(yǔ)言材料來源。英文法律語(yǔ)篇中的句子包含有許多一般英語(yǔ)表達(dá)中不常見的詞語(yǔ)、語(yǔ)言結(jié)構(gòu)、語(yǔ)言規(guī)則和標(biāo)點(diǎn)符號(hào)的特殊使用方式。英文法律語(yǔ)篇中的句法分析引起不少學(xué)者的關(guān)注，許多相關(guān)研究成果可參考B.Danet的文章（[4]）。

自然語(yǔ)言處理在日常生活或?qū)I(yè)工作中都扮演著重要的角色，像法律語(yǔ)言這種特征明顯的半結(jié)構(gòu)化的語(yǔ)言在計(jì)算機(jī)處理中有更廣泛的應(yīng)用。隨著大數(shù)據(jù)的發(fā)展，人們需要更快速、有效、準(zhǔn)確的地處理大量的法律語(yǔ)篇數(shù)據(jù)。但傳統(tǒng)的基于概率模型的方法難以勝任這一工作，一些傳統(tǒng)的語(yǔ)法工具需要極其繁瑣的構(gòu)造，會(huì)使計(jì)算機(jī)處理時(shí)間復(fù)雜度提高?；陬愋瓦壿嫷姆懂犝Z(yǔ)法，有著許多優(yōu)點(diǎn)。簡(jiǎn)單而言，范疇語(yǔ)法由一個(gè)詞庫(kù)和一個(gè)推理核心邏輯組成。大多數(shù)類型邏輯在自然語(yǔ)言處理中是可判定的，例如Lambek演算與pregroup語(yǔ)法演算。同時(shí)，范疇語(yǔ)法是易于修改的，在改變一個(gè)范疇語(yǔ)法時(shí)，并不需要改變其核心推理邏輯，只需要對(duì)詞庫(kù)進(jìn)行修改即可。Lambek演算由著名的加拿大學(xué)者蘭貝克（J.Lambek）于1958年提出，用于自然語(yǔ)言處理中的句法分析（[8]）。其核心思想就是：語(yǔ)言認(rèn)知是數(shù)學(xué)計(jì)算，語(yǔ)法分析是邏輯推演。Lambek演算是自然語(yǔ)言處理一個(gè)重要的分支，很多學(xué)者都致力于這方面的研究。

本文從英文法律語(yǔ)篇材料和過往研究出發(fā)，分析總結(jié)了英文法律語(yǔ)篇中語(yǔ)言的句法特征，并根據(jù)這些特征反推出適合刻畫英文法律語(yǔ)篇的類型邏輯及其對(duì)應(yīng)的范疇語(yǔ)法，同時(shí)證明了本文考慮的類型邏輯是可判定的，并且基于該類型邏輯的范疇語(yǔ)法等價(jià)于上下文無(wú)關(guān)語(yǔ)法。值得注意的是本文第一次證明了帶收縮（contraction）規(guī)則的非結(jié)合Lambek演算是可判定的。賈戈?duì)枺℅.Jager）論證了收縮規(guī)則在處理語(yǔ)法上的照應(yīng)問題有重要的用途（[6]）。這種語(yǔ)言現(xiàn)象在法律英語(yǔ)中也相當(dāng)普遍。然而，因?yàn)橛懈F地使用的結(jié)合律可被假設(shè)集所模擬，所以在Lambek演算上添加收縮規(guī)則會(huì)導(dǎo)致所得到的邏輯是不可判定的（[3]）。因此，本文所考慮的帶假設(shè)集的非結(jié)合收縮的模態(tài)Lambek演算可以被看成該不可判定邏輯的可判定部分。同時(shí)，通過對(duì)[2]中插補(bǔ)性質(zhì)的研究，得到一個(gè)更進(jìn)一步的固定插補(bǔ)（fixed Interpolation）性質(zhì)，該性質(zhì)即為本文的定理2。

2 英文法律語(yǔ)言的句法特征分析

本文主要關(guān)注英文法律語(yǔ)篇中語(yǔ)言的句法特征，并且在此基礎(chǔ)上研究使用運(yùn)算和推演的手段描述法律英語(yǔ)語(yǔ)言的形式化工具。沃克（W.H.Kwok）對(duì)大量法律英文句子進(jìn)行了分析，提出了法律英文句子大量使用了四種語(yǔ)言工具（[7]）：

1.帶有非常規(guī)意思的常用詞，比如“shall”在法律英文句子中更多的是表示一種義務(wù)，而不單純是時(shí)態(tài)或意愿；

2.二項(xiàng)式表達(dá)或多項(xiàng)式表達(dá)；

3.名詞化；

4.量詞化。

這四種語(yǔ)法工具的大量使用通常會(huì)帶來詞法和句法上分析的一些困難。這里，我們將著重分析英文法律句子在句法上大量使用二項(xiàng)式或多項(xiàng)表達(dá)式時(shí)的特點(diǎn)，并通過構(gòu)造合適類型邏輯，在范疇語(yǔ)法層面上對(duì)這種語(yǔ)言現(xiàn)象進(jìn)行分析。法律英文句子的一個(gè)顯著的語(yǔ)言特點(diǎn)就是句子長(zhǎng)而且相當(dāng)復(fù)雜。在法律英文句子中有大量的排列式短語(yǔ)存在，有各種短語(yǔ)的互相嵌套等。一般來說，在日常語(yǔ)言中，人們甚少大量使用二項(xiàng)式表達(dá)或多項(xiàng)式表達(dá)：即兩個(gè)或多個(gè)形式相同的單詞序列放在同一語(yǔ)法層次并通常由某種詞匯鏈接。而在法律英文文獻(xiàn)中，這種用法卻被大量地使用。比如下面的例子：

對(duì)簡(jiǎn)單的二項(xiàng)表達(dá)式，如“in life and death”，可以通過在類型語(yǔ)法中對(duì)一些詞語(yǔ)賦予特別的類型來解決。比如令“and”→(n p)/n，“l(fā)ife,death”→n。那么在經(jīng)典的Lambek演算中，可以得到“l(fā)ife and death”→np，而在處理類似上面這個(gè)復(fù)雜例子的時(shí)候就無(wú)法通過簡(jiǎn)單更改類型語(yǔ)法詞庫(kù)的賦值來解決問題。賈戈?duì)枺℅.Jager）在2004年提出“語(yǔ)言資源的多次使用應(yīng)該是在句法層面而不應(yīng)該在詞匯層面上進(jìn)行；在類型邏輯語(yǔ)法下進(jìn)行的分析應(yīng)該在Lambek演算L的一個(gè)擴(kuò)張系統(tǒng)中進(jìn)行表述”（[5]）。這種L的擴(kuò)張系統(tǒng)被賈戈?duì)柋硎鰹橐环N受限制的收縮規(guī)則的Lambek演算擴(kuò)張。受賈戈?duì)柕膯l(fā)，將采用收縮規(guī)則來擴(kuò)張基本的類型語(yǔ)法。收縮規(guī)則可以簡(jiǎn)單的理解為一組類型a1···an在語(yǔ)法分析中可以被多次重復(fù)的使用，用邏輯公理的方式表達(dá)為：a1···an≤a1···an·a1···an。例如“At his or her request”、“in his or her presence”和“in the presence of each other”均可以由一組類型序列a1···an表示，通過收縮規(guī)則可以得到類型a1···an刻畫語(yǔ)句“At his or her request and in his or her presence and in the presence of each other”。

其次，另一個(gè)法律英文句子的重要特征是wh-詞組（如whom、whose）在句子中經(jīng)常被省略使用。如下面的例子：

在范疇語(yǔ)法中針對(duì)wh-詞組的語(yǔ)言現(xiàn)象，往往需要引進(jìn)模態(tài)算子如□↓來控制對(duì)應(yīng)類型。含有□↓的類型在某些情況下可以進(jìn)行位置移動(dòng)（通過交換律和結(jié)合律實(shí)現(xiàn)）。which通常會(huì)被賦值為(n )/(s/□↓np)，其中(s/□↓np)指一個(gè)句子在某個(gè)地方缺少了一個(gè)名詞詞組。而對(duì)wh-詞組被直接省略的句子，如上面的例子，則同樣可以使用收縮規(guī)則結(jié)合算子□↓來處理，在合適的地方使用上面提到的收縮規(guī)則增加缺失的名字詞組(□↓np)，并利用模態(tài)算子□↓控制np位置的變換。

通過對(duì)一些法律句子的考察，可以發(fā)現(xiàn)法律英文句子還有一重大特征：法律英文句子具有很明顯的語(yǔ)法標(biāo)記特征，這些句子基本是以第三人稱的形式來書寫。除非在非常特殊的場(chǎng)合，不然不會(huì)出現(xiàn)用第一人稱和第二人稱表達(dá)的語(yǔ)句。唯一例外的就只有遺囑，由于遺囑本身的特殊性，它多數(shù)是以第一人稱書寫，但為了顯示句子的客觀性，往往遺囑中句子會(huì)使用被動(dòng)語(yǔ)態(tài)來平衡第一人稱的主觀性。另外，在每個(gè)法律英文文檔中都可以發(fā)現(xiàn)大量的被動(dòng)語(yǔ)態(tài)被使用，被動(dòng)語(yǔ)態(tài)出現(xiàn)的頻率遠(yuǎn)高于主動(dòng)語(yǔ)態(tài)。

綜上所述，為了刻畫上面總結(jié)的英文法律語(yǔ)篇中語(yǔ)言的句法特征，我們反推出所需的類型邏輯必須包含有收縮規(guī)則和模態(tài)算子，同時(shí)出于計(jì)算性方面的考慮結(jié)合律可以被放棄，因此我們將使用帶有模態(tài)算子與收縮規(guī)則的非結(jié)合Lambek演算擴(kuò)張來刻畫英文法律語(yǔ)句。

3 基于英文法律語(yǔ)言句法特征的類型邏輯

Lambek演算L以及與其類似的類型邏輯演算常常用于自然語(yǔ)言的信息處理中，在這里我們考慮其非結(jié)合的形式，即通常所說的非結(jié)合Lambek演算NL。我們考慮非結(jié)合Lambek演算的模態(tài)擴(kuò)張NL?。NL?可以被表達(dá)為根岑序列演算的形式。NL?公式的遞歸定義如下：公式結(jié)構(gòu)被遞歸地定義為要么是單一的公式，要么是公式結(jié)構(gòu)的合并：(Γ?Δ),〈Δ〉，其中?、〈〉是與·、?相對(duì)應(yīng)的公式結(jié)構(gòu)算子。最早的根岑序列演算是由蘭貝克給出（[9]）。定義序列為如下的結(jié)構(gòu)：Γ?A，其中Γ是一個(gè)公式結(jié)構(gòu)，A是一個(gè)公式。NL?可以由下面的公理與規(guī)則進(jìn)行表示

公理：

推理規(guī)則：

如果序列Γ?A在NL?下是可推演的則將其記為?NL?Γ?A。

同時(shí)考慮使用帶如下收縮規(guī)則(C)的NL擴(kuò)張系統(tǒng)。

該系統(tǒng)被記為NL?c。下面證明NL?c是可判定的。首先，需要證明NL?c具有子公式性質(zhì)：對(duì)于任意序列Γ?A如果其在系統(tǒng)NL?c可證，必然包含一個(gè)證明使得所有出現(xiàn)在證明的序列中的公式均為Γ?A中公式的子公式。這里將采用[11]中的方法。這里，引入(Mix)規(guī)則表示如下：

令NL?c為用(Mix)規(guī)則替換NL?c中(Cut)規(guī)則所得的系統(tǒng)。

此時(shí)，先對(duì)Γ1?A,Γ2?B和Γ3[Δ1[A?B]?···?Δ1[A·B]]?C分別使用(Mix)規(guī)則，那么根據(jù)第一重歸納假設(shè)，此時(shí)的(Mix)公式長(zhǎng)度較小，因此可以消除。然后再對(duì)Γ1?Γ2?A·B與Γ1[Δ3[Δ[Γ1?Γ2]?···?Δ[A·B]]]?C使用(Mix)規(guī)則，因?yàn)樵?Mix)規(guī)則的兩前提證明總長(zhǎng)度比之前小1，那么根據(jù)第二重歸納假設(shè)該(Mix)規(guī)則可被消除。

推論1如果?NL?cΓ?A，那么Γ?A存在一個(gè)在NL?c中不包含任何(Mix)規(guī)則的證明。

推論2NL?c滿足子公式性質(zhì)。

下面證明另一個(gè)重要的定理，稱為固定插補(bǔ)定理（fixed interpolation theorem）。

定理2對(duì)于任意的(B?C)，如果?NL?cΓ[B?C]?A，那么存在一個(gè)固定的公式D滿足：?NL?cB?C?D和?NL?cΓ[D]?A，并且D是Γ?A中出現(xiàn)的公式的子公式。

證明.由推論2可得，Γ[B?C]?A存在一個(gè)不包含(Cut)規(guī)則的證明。假設(shè)Γ[B?C]?A是由規(guī)則R所得，下面分情況討論：

·(B?C)不是由R所生成，那么(B?C)必然存在R規(guī)則的前提中，證明可直接由歸納假設(shè)與R規(guī)則得到。

·(B?C)是由R所生成。假設(shè)R=(L)的前提為B?C1和Γ[C2]?A。因?yàn)?NL?cB?C1C2?C2，所以D=C2。對(duì)R=(/L)，同理可證。假設(shè)R=(·L)的前提為Γ[B·C]?A，那么D=B·C。

·(B?C)是由R所生成。假設(shè)R=(C)的前提為Γ[(B?C)?(B?C)]?A.由歸納假設(shè)得存在著公式D滿足?NL?c(B?C)?D和?NL?cΓ[D?D]?A。再由(C)規(guī)則可得?NL?cΓ[D]?A。

綜上所述，定理得證。

由定理2，可以輕易推導(dǎo)出如下定理：

定理3如果?NL?cΓ[Δ]?A，那么存在一個(gè)固定公式D滿足：?NL?cΔ?D和?NL?cΓ[D]?A，并且D是Γ?A中出現(xiàn)的公式的子公式。

注意定理2對(duì)于定理3的證明起到至關(guān)重要的作用。我們無(wú)法使用歸納假設(shè)的辦法直接證明定理3。因?yàn)楫?dāng)Γ[Δ]?A是由Γ[Δ?Δ]?A使用(C)規(guī)則得到時(shí)，根據(jù)歸納假設(shè)，將存在兩個(gè)公式D1D2滿足定理的條件。但是因?yàn)闅w納假設(shè)并不保證D1=D2，無(wú)法從Γ[D1?D2]?A得到Γ[D1]?A或Γ[D2]?A，因此無(wú)法證明該定理。這個(gè)問題最初被描述于[5]。

下面證明NL?c是可判定的。令Φ為形如A?B的序列的有窮集合，布茨考夫斯基（W.Buszkowski）（[1]）證明了如下命題：

命題1對(duì)于任意的Γ?A,Φ?NLΓ?A是可判定的。

任給一個(gè)序列Γ?A,令T為其所有公式的子公式的集合，定義Φ={A?A·A|A∈T}。那么：

定理4?NL?cΓ?A，當(dāng)且僅當(dāng)Φ?NLΓ?A。

證明.從右到左的方向的證明是顯然的，因?yàn)棣抵腥魏涡蛄性贜L?c下顯然可證。對(duì)于從左到右的證明，由定理3可得，對(duì)于Γ?A在NL?c中的證明，都可以被改寫成一不包含有(C)規(guī)則但仍保持子公式性質(zhì)的證明。即使用D?D·D和(Cut)規(guī)則代替(C)規(guī)則，并且由于定理3，D∈T通過施歸納假設(shè)于Γ?A在NL?c中的證明所使用的(C)規(guī)則個(gè)數(shù)可以輕易證得該結(jié)論。而Γ?A在NL?c中的這種證明恰恰就Γ?A在NL中從Φ出發(fā)的一個(gè)推演。

4 英文法律語(yǔ)言的范疇語(yǔ)法

范疇語(yǔ)法的精準(zhǔn)定義如下：范疇語(yǔ)法可以被定義為基于一個(gè)類型邏輯TL上的三元組G=〈Σ,I,D〉：

·Σ是非空字符串集合；

·I是一個(gè)從Σ到TL公式集的映射；

·D是一個(gè)特殊的公式。

通常D是一個(gè)原子公式，比如s。基于TL邏輯的范疇語(yǔ)法通常稱為TL語(yǔ)法。TL語(yǔ)法G=〈Σ,I,D〉所接受的語(yǔ)言可以定義為一個(gè)字符串序列a1···an，其中ai∈Σ,1≤i≤n,且n≥1滿足：存在A1,...,An和Γ使得對(duì)所有1≤i≤n〈ai,Ai〉∈I,使得Φ?TLΓ?D和st(Γ)=A1···An。st(Γ)表示一個(gè)由公式結(jié)構(gòu)去掉所有結(jié)構(gòu)算子產(chǎn)生的公式序列。

下面證明一個(gè)結(jié)論NL?c語(yǔ)法等價(jià)于上下文無(wú)關(guān)語(yǔ)法。證明思路如下：證明被NL?c語(yǔ)法所接受的語(yǔ)言同樣能被一個(gè)上下文無(wú)關(guān)語(yǔ)法所接受。首先需要構(gòu)造一個(gè)與NL?c等價(jià)的系統(tǒng)。給定公式集T，令S為如下系統(tǒng)：

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

·推演規(guī)則：切割規(guī)則(Cut)。

給定公式集T使得其包含序列Γ?A中所有公式的子公式，構(gòu)造S如上，可證如下引理：

引理1?NL?cΓ?A當(dāng)且僅當(dāng)?SΓ?A。

證明.從右到左方向自然成立。現(xiàn)在考慮從左到右方向，證明基于定理2，施歸納假設(shè)于Γ中公式的個(gè)數(shù)即可證得結(jié)論。

現(xiàn)在從一個(gè)NL?c語(yǔ)法G=〈Σ,I,D〉來構(gòu)造一個(gè)上下文無(wú)關(guān)語(yǔ)法。定義公式集T使得其包含所有D,I中出現(xiàn)的公式并對(duì)子公式閉包，S定義如上。上下文無(wú)關(guān)文法構(gòu)造如下：終結(jié)符為Σ中字符串，非終結(jié)符為T中公式，開始符號(hào)為D，生成規(guī)則被定義為：{A→B:?SB?A}∪{A→B:?S〈B〉?A}∪{A→BC:?SB?C?A}∪{A→v:〈v,A〉∈I}。

結(jié)合[1]中結(jié)論，任何一個(gè)上下文無(wú)關(guān)語(yǔ)法都是一個(gè)范疇語(yǔ)法，可以得到如下定理。

定理5NL?c語(yǔ)法等價(jià)于上下文無(wú)關(guān)文法。

5 小結(jié)

本文從法律英文句子出發(fā)，研究分析法律英文句法的特征，在此基礎(chǔ)上構(gòu)建了相應(yīng)的類型邏輯和范疇語(yǔ)法。對(duì)應(yīng)的范疇語(yǔ)法可以用來模擬法律英文句子檢測(cè)。從定理5可知基于本文考慮的范疇語(yǔ)法，我們可以通過構(gòu)造等價(jià)的上下文無(wú)關(guān)語(yǔ)法，并且利用上下文無(wú)關(guān)語(yǔ)法已知的算法，如CYK算法等對(duì)NL?c語(yǔ)法進(jìn)行計(jì)算模擬實(shí)現(xiàn)。

[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.

（責(zé)任編輯：潘琳琦）

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

國(guó)家社會(huì)科學(xué)基金青年項(xiàng)目（15CZX045）。

?致謝：感謝匿名審稿人對(duì)本文的幫助。本文通訊作者為康孝軍。