函項(xiàng)分層思想及其在語言學(xué)研究中的應(yīng)用

滿海霞

(北京科技大學(xué)外國語學(xué)院，北京 100083)

函項(xiàng)分層思想及其在語言學(xué)研究中的應(yīng)用

滿海霞

(北京科技大學(xué)外國語學(xué)院，北京 100083)

基于現(xiàn)代邏輯思想的形式語義學(xué)理論，離不開類型和范疇的分層思想。它的理論源泉之一是邏輯學(xué)家弗雷格區(qū)分“完全”、“不完全”表達(dá)式的討論，其影響主要為兩方面:邏輯類型論和范疇理論。通過對比分析邏輯類型論和范疇理論在語言學(xué)領(lǐng)域的兩個(gè)綜合應(yīng)用模式:蒙太格語法和類型邏輯語法可知，形式語義學(xué)總體來講具有兩種發(fā)展趨勢，即偏向自然語言與偏向邏輯兩種風(fēng)格。

函項(xiàng)分層;邏輯類型論;范疇理論;蒙太格語法;類型邏輯語法

一、背景介紹

現(xiàn)代邏輯之父弗雷格發(fā)現(xiàn)，用自然語言表達(dá)邏輯概念，很難達(dá)到期望的精準(zhǔn)程度。于是從《概念文字》(Begriffsschrifi)開始嘗試提供一套檢驗(yàn)系列推理有效性的可靠工具，并在《算術(shù)基礎(chǔ)》(Grundgesetze der Arithmetik)中，試圖將數(shù)學(xué)構(gòu)造為邏輯的分支。在此過程中，弗雷格為函項(xiàng)給出具有一般性的定義。其區(qū)分完全(complete)和不完全(incomplete)表達(dá)式的做法，對形式語義學(xué)的發(fā)展有兩方面重要的影響:

(1)弗雷格區(qū)分完全、不完全表達(dá)式的思想以及胡塞爾(Husserl)將思維對象分為若干層的想法在哲學(xué)界誘發(fā)了化學(xué)反應(yīng)。列斯尼維斯基和愛裘凱維茨(Ajdukiewicz)將范疇分層思想形式化，發(fā)展出以判斷語詞句法行為為目的的范疇理論。在幾代邏輯學(xué)家和語言學(xué)家的努力下，范疇語法逐步發(fā)展出當(dāng)今形式語義學(xué)的一個(gè)重要分支——類型邏輯語法。

(2)1901年，羅素指出《算術(shù)基礎(chǔ)》存在悖論(即著名的羅素悖論)，核心問題是，謂詞是否可以做其自身的謂詞?不管答案為是為否，都存在矛盾。①羅素悖論具體地說，是一個(gè)謂詞是否可以做其自身的謂詞?假設(shè)函項(xiàng)f(x)是所有不具備可做其自身謂詞的元素的集合A，A={x|﹁x(x)}。那么，若承認(rèn)謂詞f可以做其自身的謂詞，則將f作用在f上，根據(jù)集合A的定義，f(f)的值就是﹁f(f)，矛盾;若不承認(rèn)謂詞f可以做其自身的謂詞，則f具有性質(zhì)﹁f(f)，是集合A中的一個(gè)元素，根據(jù)定義，有f(f)為前提，亦矛盾。這個(gè)悖論的癥結(jié)在于系統(tǒng)允許函項(xiàng)自指(self－reference)。羅素和懷特海(Whitehead)在《數(shù)學(xué)原理》中提出一種解決方案，主要思想是:通過構(gòu)造基于類型的層級，為每種數(shù)學(xué)對象都配以相應(yīng)的類型，具有給定類型的對象只能從更高一級類型的對象構(gòu)造來，避免了函項(xiàng)自指造成的惡性循環(huán)。這是邏輯類型論的雛形［1］15。而后，憑借類型概念在 λ－演算(typed lambda calculus)中的重要地位，受到形式語言學(xué)家的關(guān)注，成為計(jì)算自然語言形式語義的經(jīng)典依據(jù)。

范疇理論與邏輯類型論之間具有微妙而密切的聯(lián)系，在現(xiàn)代形式語義學(xué)的研究中缺一不可。以下首先簡要介紹兩種理論的基礎(chǔ)——范疇與類型之間的對應(yīng)，給出兩種理論之間的對應(yīng)基礎(chǔ)，然后對比二者在語言學(xué)研究中的兩個(gè)綜合應(yīng)用模型——蒙太格語法和類型邏輯語法，說明兩種應(yīng)用分別代表了形式語義學(xué)偏向自然語言和偏向邏輯的兩種研究風(fēng)格

二、范疇與類型的對應(yīng)

范疇語法所謂的“范疇”，就是將自然語言中的表達(dá)式按照句法行為特征分成若干大類，將每個(gè)大類共有的特征抽象出來，即為范疇。以最早的范疇演算系統(tǒng)蘭貝克演算L為例［2］，L的句法系統(tǒng)包括兩個(gè)基本范疇:np和s，分別為代表名稱的范疇和代表語句的范疇。①蘭貝克演算L本身使用的是n，本文為與目前主要的范疇使用標(biāo)記保持一致，統(tǒng)一使用np。復(fù)合范疇按照定義1遞歸得到。

定義1 范疇形成定義

(i)np和s是范疇;

(ii)如果A和B是范疇，則A/B，BA，A·B也是范疇;

(iii)除了由(i)和(ii)生成的范疇之外，其他的都不是范疇。

其中，右斜線算子“/”、左斜線算子“”和積算子“·”為作用在相鄰范疇上的范疇構(gòu)造算子。積算子表示相鄰范疇的直接毗連。斜線算子的情況稍微復(fù)雜，其傾斜方向表示需要結(jié)合論元范疇的方向，斜線下方和上方分別表示需要結(jié)合的論元范疇和所得的值范疇。

類型論的基本想法類似。為避免悖論，羅素將模型論中的對象置于不同的層級上，這種區(qū)分反映在類型論語言中，就是分屬不同類型的表達(dá)式。假設(shè)存在一個(gè)有窮的初始語義類型集，語義類型集依據(jù)定義2遞歸得到。

定義2 語義類型的形成定義

令BTYPE為初始語義類型的有窮集合。TYPE是包含語義類型的最小集合，使得:

(i)BTYPE?TYPE;

(ii)如果 a，b∈TYPE，那么〈a，b〉∈TYPE［3］11。

類型為〈a，b〉的表達(dá)式與類型為a的表達(dá)式嚴(yán)格遵守函項(xiàng)貼合原則做貼合運(yùn)算，得到類型為b的表達(dá)式。

從范疇和類型的語義定義中我們也可以看出二者的相似與對應(yīng)關(guān)系。

如果將范疇“A/B”設(shè)為函項(xiàng)f1，把〈a，b〉設(shè)為一個(gè)函項(xiàng)f2，則有:

①復(fù)合范疇運(yùn)算規(guī)則A/B+B→A對應(yīng)函項(xiàng)表達(dá)式:f1(B)=A

②復(fù)合類型〈a，b〉與b的貼合運(yùn)算對應(yīng)函項(xiàng)表達(dá)式:f2(a)=b

從函項(xiàng)的角度看，復(fù)合范疇/類型總是比它的組成范疇/類型高一階。換言之，函項(xiàng)分層思想已經(jīng)編碼在范疇/類型的定義中。f1和f2相似，但不相等。主要原因在于，范疇的斜線構(gòu)造算子區(qū)分方向，f1不但可以對應(yīng)“A/B”，同時(shí)也可做復(fù)合范疇“BA”的對應(yīng)函項(xiàng);而類型不需要區(qū)分論元的結(jié)合方向，所以f2相當(dāng)于f1不區(qū)分方向的版本。這體現(xiàn)了句法范疇與語義類型之間具有一定的對應(yīng)關(guān)系(定義3)，也從宏觀上保證了范疇理論與邏輯類型論的對應(yīng)，保證形式語義學(xué)句法和語義兩方面理論的同步發(fā)展。

定義3 范疇到類型的對應(yīng)

令τ是一個(gè)從范疇集到類型集的函項(xiàng)。τ是對應(yīng)函項(xiàng)，當(dāng)且僅當(dāng)

定義3說明，給定一個(gè)范疇，就可以從這個(gè)范疇的內(nèi)部結(jié)構(gòu)預(yù)測出它所對應(yīng)的語義類型。從邏輯的角度看，即一個(gè)語言符號串的語義類型是其句法范疇的同態(tài)像(homomorphic image)。換個(gè)角度考慮，類型和范疇只不過是函項(xiàng)分層思想對自然語言語詞在語義和句法上的兩種標(biāo)記。不過，句法范疇到語義類型的對應(yīng)關(guān)系不是一對一，而是多對一。以蒙太格語法(Montague Grammar)為例，其初始類型有兩個(gè):e(entity)和t(truth)，語義上分別對應(yīng)個(gè)體和真值，通常情況下，分別被映射到個(gè)體集合E和真值集合{0，1}上［4］。以語句“John walks”為例，在語義上看，“walks”是所有具有走路性質(zhì)的個(gè)體組成的集合，如定義4所給“walk”在模型M1中的語義定義。這里單詞的全小寫字母表示它在模型論域中對應(yīng)的個(gè)體，單詞大寫表明它所對應(yīng)的邏輯式，〖〗表示自然語言表達(dá)式在模型中對應(yīng)的語義值。

定義4 “walk”在M1模型內(nèi)的語義定義

從圖1可以看到，“walk”的語義值是將e類型個(gè)體映射到t類型真值的集合上的函數(shù)，即fWALK(e)=t。因此，WALK對應(yīng)類型，〈e，t〉。②此處為簡化問題，不討論專名的類型提升。只強(qiáng)調(diào)一點(diǎn)，在蒙太格語法中，為保證專名與量詞能夠做一致處理，專名的類型被提升為〈〈e，t〉，t〉，而非e。沒有類型為e的自然語言表達(dá)式，類型為e的只是模型論中的個(gè)體。詳細(xì)討論參見參考文獻(xiàn)［5］。如果已知它的句法范疇，依據(jù)定義3，從它到語義類型的映射結(jié)果是唯一的，為〈e，t〉。反過來，如果已知“walks”的語義類型，往回推溯則只能推斷“walks”句法范疇的2種可能情況:nps或者s/np。

圖1 ?WALK?M1，g的特征函項(xiàng)直觀圖

需要說明的是，在對語言學(xué)的應(yīng)用中，執(zhí)行語義運(yùn)算工作的是基于類型的λ－演算，參與運(yùn)算的基本單位是自然語言符號串在λ－演算中的翻譯，即語義表達(dá)式。雖然參與運(yùn)算的不是類型本身，但是語義表達(dá)式的運(yùn)算基礎(chǔ)是他們對應(yīng)的類型，要求類型之間能夠依據(jù)λ－演算做應(yīng)用或者抽象運(yùn)算。基本想法如定義5。

定義5 λ－演算的兩條運(yùn)算規(guī)則［6］

對于每個(gè)類型，都允許(i)和(ii)中λ－項(xiàng)的構(gòu)造:

(i)如果t1的類型為〈a，b〉，t2類型為a，則t1(t2)是類型為b的項(xiàng);(λ－應(yīng)用)

(ii)如果t的類型為b，x是類型為a的變元，則(λx.t)的類型為〈a，b〉。(λ－抽象)

三、語言學(xué)應(yīng)用:蒙太格語法與類型邏輯語法

總之，從宏觀上看，正是邏輯類型論與范疇理論之間的相似和對應(yīng)，使蒙太格給自然語言的句法找到遵循組合原則的語義解釋，開創(chuàng)了用形式方法研究自然語言語義的先河;也正是這種相似和對應(yīng)，使范·本瑟姆(van Benthem)為范疇語法配備了基于類型的語義解釋，從而推進(jìn)了范疇語法的當(dāng)代形式——類型邏輯語法的產(chǎn)生和發(fā)展。

20世紀(jì)60年代末70年代初，美國杰出數(shù)理語言學(xué)家蒙太格以其特有的邏輯高度，發(fā)現(xiàn)范疇語法在結(jié)構(gòu)上同表現(xiàn)自然語言語義的邏輯類型論間有著驚人的相似，并看到自然語言與形式語言在本質(zhì)上是相同的。因此，蒙太格嘗試以類型為基礎(chǔ)，依據(jù)組合原則構(gòu)建一套通用的語法(Universal Grammar)，來描述邏輯人工語言和自然語言間的某些共同規(guī)律，由此開始了用形式方法研究自然語言語義的思路［7］32。80年代初，范·本瑟姆［8］受蒙太格語法的啟發(fā)，為范疇語法配上了語義系統(tǒng)(即Lvb演算)，彌補(bǔ)了范疇語法在語義組合方面的欠缺，孕育出范疇語法的一個(gè)當(dāng)代形式—類型邏輯語法。幾個(gè)理論之間的關(guān)系可用圖2表示。

圖2中的箭頭表示“啟發(fā)”與“促進(jìn)”，其中蒙太格語法和范疇語法之間的關(guān)系很有意思，大有互相幫助、共同進(jìn)步的意味。一方面，范疇語法是蒙太格語法的理論基礎(chǔ)之一，另一方面，蒙太格語法在語義構(gòu)造上的獨(dú)特視角又啟發(fā)了范疇語法語義系統(tǒng)的產(chǎn)生，間接促進(jìn)了范疇語法后繼理論——類型邏輯語法的出現(xiàn)。

(一)蒙太格語法

蒙太格語法的具體做法是:首先，確立句法范疇和語義類型之間的對應(yīng)關(guān)系。其描述自然語言句法生成的句法規(guī)則以范疇語法為基礎(chǔ)，依據(jù)規(guī)則對規(guī)則假設(shè)，令一條句法規(guī)則有一條語義規(guī)則相對應(yīng)，語義規(guī)則的基本單位λ－項(xiàng)之間以λ－演算為基礎(chǔ)，從而使得用形式化方法研究自然語言語義成為可能。在蒙太格語法中，句法和語義運(yùn)算展示的是類似自然語言句法和高階謂詞函項(xiàng)的操作。以蒙太格構(gòu)造的英語部分語句系統(tǒng)PTQ為例，一共包含17條句法規(guī)則和對應(yīng)配備的17條語義規(guī)則。比如從及物動(dòng)詞生成不及物動(dòng)詞的句法規(guī)則S7:

S7:如果δ∈PTV，且α∈PT，則F6(δ，α)∈PIV，且F6(δ，α)=δα'。其中，如果α是句法變元，則α'是α的賓格形式，否則α'=α。［8］166

S7中，δ、α為自然語言符號串，PA指示由所有范疇為A的語言符號串組成的集合，下標(biāo)IV、TV分別代表不及物動(dòng)詞和及物動(dòng)詞的范疇，T為函項(xiàng)范疇S/IV，F(xiàn)6是對自然語言符號串做句法操作的函項(xiàng)。從S7可以看出，蒙太格語法中的詞表是按范疇分類的若干集合，如:PTV={love，like，play}，PT={Mary，John}。那么，依據(jù)S7，“l(fā)ove Mary”的句法生成過程就是:

δ=love∈PTV，α=Mary∈ PT，love和Mary毗連之后屬于范疇為IV的語言符號串集合，二者的毗連結(jié)果F6(love，Mary)=loveMary。如果把Mary換成句法變元he，那么依據(jù)F6，運(yùn)算的結(jié)果就是lovehim，因?yàn)楦鶕?jù)S7的最后一句注解規(guī)定，要把he換成其賓格形式。

可以看出，蒙太格語法中句法系統(tǒng)類似自然語言語法。它將自然語言按照范疇分為不同的大類，抽象出具有相同或不同范疇的語言符號串之間進(jìn)行毗連的規(guī)律，制定成系統(tǒng)的句法規(guī)則。這個(gè)句法系統(tǒng)是一個(gè)開系統(tǒng)，可以根據(jù)所選自然語言語句系統(tǒng)的句法要求增加規(guī)則，如鄒崇理構(gòu)造的處理漢語時(shí)態(tài)結(jié)構(gòu)的部分語句系統(tǒng)，就包含21條句法規(guī)則［9］400－422。

同時(shí)，在語義方面，蒙太格給自然語言表達(dá)式指派相應(yīng)的邏輯式，這個(gè)邏輯式是以類型為語義載體的，或者說，是以圖2中提到的“基于類型的λ－演算”的運(yùn)算單位—λ－項(xiàng)為語義載體。然后，要對應(yīng)相應(yīng)的句法規(guī)則，制定從自然語言表達(dá)式到邏輯表達(dá)式的翻譯。以S7對應(yīng)的翻譯規(guī)則T7(如下)為例(其中α|→β意味:自然語言表達(dá)式α被翻譯成邏輯式β):

T7:如果δ∈PTV，α∈PT，且α|→α'，β|→β'，則F6(δ，α)|→ δ'(α')。［8］167

因此短語“l(fā)ove Mary”的語義組合過程為:love |→λxλyLOVE'(x)(y)，Mary|→MARY'，所以love和Mary進(jìn)行句法毗連之后，語義上的組合結(jié)果是λyLOVE'(MARY')(y)(定義5中的λ－應(yīng)用規(guī)則)。這里，在運(yùn)算過程中看到的，都是從自然語言語詞出發(fā)進(jìn)行的形式計(jì)算，相比之下，另一種語言學(xué)應(yīng)用—類型邏輯語法—?jiǎng)t顯得更加抽象，邏輯味道更加濃重。

(二)類型邏輯語法

基本的類型邏輯語法也包括句法系統(tǒng)和語義系統(tǒng)，前者是蘭貝克演算L，后者則是定義5提到的λ－演算。不嚴(yán)格地說，對于類型邏輯語法，蘭貝克演算說明了什么結(jié)構(gòu)是可能的，λ－項(xiàng)則描述了這些結(jié)構(gòu)如何進(jìn)行運(yùn)算。

在類型邏輯語法的詞庫中，每個(gè)詞條都對應(yīng)一個(gè)序?qū)?，它包含兩方面信息，一是它所對?yīng)的句法范疇，一是代表其語義的λ－項(xiàng)。仍以“John walks”為例，它們在詞庫中對應(yīng)的詞條分別為: John:〈np，JOHN'〉;walks:〈nps，WALK'〉，該句在類型邏輯語法中的生成過程如圖3所示。

圖3 “John walks”的類型邏輯生成圖①圖3的類型邏輯生成并不嚴(yán)格。在類型邏輯生成過程中，一般來說，語詞的邏輯式都經(jīng)過范式化，計(jì)算中使用的都是最簡的形式。如這里面“walk”的邏輯式還可以再做η－劃歸，變成“WALK'”。

如果不做深層次考慮，單看詞條之間的運(yùn)算關(guān)系，至少能得到這樣的可行性信息:每個(gè)范疇對應(yīng)一個(gè)語義類型，而λ－運(yùn)算是基于類型的，這為類型邏輯語法提供了一個(gè)很好的句法 －語義接口，保證句法運(yùn)算和語義組合有實(shí)現(xiàn)并行推演的基礎(chǔ)。

四、形式語義學(xué)的兩個(gè)發(fā)展方向

形式語義學(xué)又稱邏輯語義學(xué)，顧名思義，是關(guān)于邏輯學(xué)和語言學(xué)交叉領(lǐng)域的研究。事實(shí)上，蒙太格語法與類型邏輯語法之間的差異和特色恰好反映了形式語義學(xué)研究的兩大方向。蒙太格語法屬于語言學(xué)意味較濃的形式語義研究，類型邏輯語法屬于突出對自然語言做形式分析的邏輯風(fēng)格研究。

對比考察表1可以看出:(1)在范疇的應(yīng)用上，類型邏輯語法將自然語言的毗連規(guī)則抽象為范疇間的貼合規(guī)則，以范疇為基本單位參與句法運(yùn)算;而對于蒙太格語法來說，范疇表面上的功能只不過是自然語言表達(dá)式分類的標(biāo)準(zhǔn)和標(biāo)簽，參與句法運(yùn)算的，是屬于這一范疇集合的自然語言表達(dá)式。蒙太格改變了強(qiáng)調(diào)范疇運(yùn)算甚于語言生成的做法，把范疇的運(yùn)算置于幕后的次要地位。(2)在對自然語言詞條的使用上，蒙太格語法不管是對句法規(guī)則還是語義規(guī)則，都是從自然語言詞條開始，或做句法毗連，或賦以語義翻譯;而在類型邏輯語法中，這些工作都轉(zhuǎn)給了詞庫，從詞庫出來便不見自然語言表達(dá)式的蹤影，運(yùn)算過程中看到的都是句法范疇和語義λ－項(xiàng)。

從表1中“詞庫”一橫欄開始對比兩種語法，可以得出以下結(jié)論:類型邏輯語法幾乎總是更加抽象一層;反過來，蒙太格語法總要更貼近自然語言一些，在其中看到的自然語言表達(dá)式的影子要多些。以句法系統(tǒng)為例，二者的句法系統(tǒng)都由一系列句法規(guī)則構(gòu)成，但是蒙太格語法的句法規(guī)則表現(xiàn)的是對自然語言表達(dá)式之間如何結(jié)合的規(guī)定，說明它們之間是什么貼合順序、句法上有什么轉(zhuǎn)化等，句法規(guī)則的增加與語句系統(tǒng)中語詞之間的毗連情況有關(guān)。至于類型邏輯語法，它的句法系統(tǒng)則是一個(gè)邏輯系統(tǒng)，表現(xiàn)的是抽象的范疇之間的毗連規(guī)律，每增加一條規(guī)則或者聯(lián)接詞，都要經(jīng)過嚴(yán)格的證明和推導(dǎo)。

表1 蒙太格語法與類型邏輯語法基本機(jī)制對比

見微知著，從函項(xiàng)分層理論在語言學(xué)領(lǐng)域的兩個(gè)應(yīng)用，可以看出形式語義學(xué)的主體發(fā)展趨勢:偏向自然語言與偏向邏輯兩種風(fēng)格。前者以蒙太格語法為代表，其分析更接近自然語言，抽象程度不高;后者以類型邏輯語法為代表，其分析更接近邏輯的風(fēng)格，對形式化的構(gòu)造也要求有更高的抽象度和精準(zhǔn)度。兩種力量之間相互影響、互相促進(jìn)，如圖2所示。但是，無論蒙太格語法還是類型邏輯語法，都是函項(xiàng)分層思想的兩個(gè)后繼理論——類型論和范疇語法在語言學(xué)領(lǐng)域的綜合應(yīng)用模式，是語言學(xué)與邏輯學(xué)交叉領(lǐng)域研究的縮影。目前，類型論和范疇理論已成為計(jì)算機(jī)領(lǐng)域重要的基礎(chǔ)理論［10］，并在計(jì)算科學(xué)界取得了廣泛的應(yīng)用［11－12］。從對二者的綜合分析與對比，我們可以看出，邏輯類型和句法范疇的結(jié)合將為形式語義學(xué)的發(fā)展提供更多的研究成果、更廣闊的研究空間，也將為自然語言程序化提供更成熟更有指導(dǎo)意義的元理論思想和依據(jù)。

［1］Kamareddine，F(xiàn)airouz，Laan Twan，Nederpelt Rob.A Modern Perspective on Type Theory:From its origins until today［M］.New York，Boston，Dordrecht，London，Mos－cow:Kluwer Academic Publishers，2005.

［2］Lambek Joachim.The Mathematics of Sentence Structure［J］.The American Mathematical Monthly，1958(3):154－170.

［3］J?ger Gerhard.Anaphora and Type Logical Grammar［M］.Dordrecht:Springer，2005.

［4］Montague，Richard.Formal Philosophy［M］.New Haven: Yale University Press，1974.

［5］滿海霞.形式語義學(xué)兩題［J］.畢節(jié)學(xué)院學(xué)報(bào)，2010 (2):37－41.

［6］van Benthem，Johan.The semantics of variety in categorial grammar［C］//Categorial Grammar.Amsterdam:Benjamin，1988.

［7］鄒崇理.范疇類型邏輯［M］.北京:中國社會科學(xué)出版社，2008.

［8］GAMUT L T F.Logic，Language and Meaning(II)—Intentional Logic and Logical Grammar［M］.Chicago and London:The University of Chicago Press，1991.

［9］鄒崇理.自然語言邏輯研究［M］.北京:北京大學(xué)出版社，2000.

［10］Asperti Andrea，Longo Giuseppe.Categories，Types and Structures:An Introduction to Category Theory for the Working Computer Scientist(Foundations of Computing Series)［M］.Cambridge:The MIT press，1991.

［11］高東平.申請專利:一種基于類型論的漢語分詞方法［S］.專利申請?zhí)?200910078879.0，2009.

［12］Moot，Richard.Proof Nets for Linguistic Analysis［D］.Dutch:Utrecht University，2002.

Function Stratification and Its Application in Linguisitics

MAN Hai－xia
(Foreign Language Department，University of Science＆Technology Beijing，Beijing 10083，China)

Formal Semantics，originated from Modern Logics，is inseparable from the concept of function stratification.One of its theoretical sources is the classification over complete and incomplete expressions by Frege，the influences of which mainly reflected in two aspects:Type theory and Categorial Grammars.In addition，the present paper compares two integrated models that Type theory and Categorial grammars applied to—Montague Grammar and Type Logical Grammar，in order to demonstrate two major trends during the development of Formal Semantics，namely，pro－Linguistics and pro－Logics.

Function stratification;Type theory;Categorial grammars;Montague Grammar;Type Logical Grammar

B81

A

1674－8425(2011)08－0083－06

2011－06－30

國家社會科學(xué)基金項(xiàng)目“面向自然語言信息處理的范疇類型邏輯研究”(09BZX046)。

滿海霞(1983—)，女，內(nèi)蒙古自治區(qū)烏蘭浩特人，博士，講師，研究方向:形式語義學(xué)、語言邏輯。

(責(zé)任編輯 鄺坦勵(lì))