范畴类型逻辑：伽罗瓦联络和作用域

§§\·理论计算机科学电子笔记53（2003）网址：http://www.elsevier.nl/locate/entcs/volume53.html18页范畴型逻辑中的伽罗瓦联络卡洛斯·阿雷塞斯a，1，2拉斐尔·贝尔纳迪b，3迈克尔·莫特加特b，4aILLC，阿姆斯特丹大学，荷兰bUiL-OTS，乌得勒支大学，荷兰摘要一元连接词的引入是对范畴词汇的重要补充到目前为止，所考虑的连接符是保序的;在本文中，我们考虑的是加序反转的伽罗瓦连接算子。第二章是模型理论和证明理论的基础。在第3章中，我们利用伽罗瓦连通算子的表达能力来限制广义量化表达式的作用域可能性并描述极性项的类型学1介绍范畴类型逻辑为自然语言的形式和意义的 二元乘积运算符捕获语法部分的组合，剩余含义=和表达关于组合关系的不完整性。 在[11，18]中，范畴词汇表被扩展为一对unaryoperators，3和resiidua2#。这一定义增加了范畴类型语言的分析能力。 与二元连接词相结合，一元运算符可用作增强特征，为结构推理提供词汇锚定控制。但是，在代数逻辑NL（3）中，1我们要感谢Dick Oehrle在乌得勒支大学访问期间就剩余和Galois conctedope rato rs之间的关系进行的有趣讨论，以及RajeevGo re'forhisco nst ant h e n t h e n th e n t endprom ptc lari fic at o ns。2电子邮件地址：carlos@science.uva.nl3电子邮件：Raffaella. let.uu.nl4电邮：迈克尔。莫特加。UU. nl2003年3月由ElsevierScienceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。阿雷塞斯、贝尔纳迪和穆加特20AB≤≤··stants产生类型赋值的精化，这将在使用3;2#deccration的情况下过度生成。3;2~#连续算子是一个关于可导性关系的保序算子。基本逻辑的代数结构也为一对逆序伽罗瓦连通算子提供了空间，在本文中，我们将其写为：0·;·. 要理解这两个概念之间的关系，可能useful有用to emphasize数学them in their其natural自然algebraic代数context上下文. Birkhoff [5]和Ore [20]等人的工作研究了剩余映射和Galois连通映射对。Michael Dunn强调了这一早期工作与当前子结构逻辑研究的相关性，[7]我们从中得出以下定义。定义1.1C：设A=（A;≤A）和B=（B;≤B），以及函数f：A → B; g：B →A。 称对（f; g）是剩余的当且仅当[RES]fa≤Bb当且仅当a≤Agb：称对（f; g）是伽罗瓦连通的当且仅当[GC]b≤Bfa当且仅当a≤Agb：保持偏序集和不同有助于理解剩余映射对和伽罗瓦连通映射对之间的联系。我们来当（≤）={（b;a）|a≤b}，and1 1BB考虑函数h：B→A。在[RES]之后，函数f; h形式如果f个二进制数满足a（≤B）b惠a≤hbholds，则计算d对。But1一现在，通过y≤，我们可以使atb≤fa惠a≤hb，即，e.1B B这一对是用特定顺序B和A连接D的Galoi。Dunn在[7]中指出，Galois连通对是通过翻转不等式y≤B在特征分解中得到的.当我们把这个代数讨论投射到范畴类型对数中时，我们将考虑的对象是类型，按它们的可导性关系排序 伽罗瓦连通算子也在线性逻辑[12，1，9，21]的背景下进行了研究，其中它们旨在表现出类似否定的行为。 这意味着伽罗瓦性质必须与保证双重否定定律0（A0）= A =（0A）0的额外特征混合。在相关的工作中，Jim Lambek [13，14]考虑了他称之为预群的代数结构，其中每个元素a都有一个左伴随和一个右伴随，记为l和r。同样在这些结构中，具有lr=a=rl。 在本文中，我们不考虑这些更强的概念，但我们集中在纯伽罗瓦性质和研究的效果，添加0;0到eb作为elogicNL（3）。 我们之所以对基本逻辑感兴趣，是因为我们认为它为语法构成的不变量打开了一扇窗--基本逻辑的定律是普遍的，因为它们不依赖于结构公设（即非逻辑公理）。B阿雷塞斯、贝尔纳迪和穆加特3§§·我→·M··12本文件的结构如下。在第二章中，我们提供了基本的模型理论和证明理论基础。 我们证明了NL（3）的标准K型经验表示的完备性是如何推广到Galois连通算子上的，以及如何得到一个无割的Gentzen型表示. 在第三章中，我们转向Beghelli和Stowell对作用域选取方式的分析[3]和Giannakidou的极项分布理论[8]，为伽罗瓦连通算子提供语言学上的理据。 我们利用伽罗瓦算子引入的新的可导性模式来约束广义量化器表达式的范围可能性，并描述极性项的类型。这样，我们改进了[4]中用递推算子s3;2#给出的分析。2正式任命2.1公理化表示，完备性本文将NL（3）（se[19]）的标准公理化表示推广到广义代数上。 系统NL（3，0）可以通过用公理（A1），（A2）和定理（R1），（R2）对NL（3）进行扩展而得到. 在这种情况下，很容易证明（GC）是一个派生规则或者，将（GC）转换为NL（3）。证明了（A1），（A2）和定理（R1），（R2）是可导的.（A1）A0（A0）：（A2）A（0A）0：（R1）从AB推断B0A0：（R2）从AB推断B0B0A：(GC)A=0B当且仅当B=A=0：NL（3）是一个K-型的语义空间[10]，它可以直接表示为NL（3，·0）. 对于NL（3，·0）的一个模型，满足M=W;R3;R2;R2;V当W是非空集时，R3R2，R3，R4 W2和V是一个评估V：PROP2W。R3关系超过了该值，则该值=，R2 相对于第3;2#对，R为2 GovernstheGa-1 2lois连接对0;0.为了简单起见，下面我们将把自己限制在模型= W; R;V中，R是控制伽罗瓦算子的关系。给定一个模型M=W; R;V∈W，我们定义：M; mA0当且仅当m0：（Rmm0<$M;m0/A）：00 0 0M;mA当且仅当：（Rm m <$M;m/A）：阿雷塞斯、贝尔纳迪和穆加特4M∪M►⇒∈M∈0给定箭头A<$B，模型M=<$W; R;V<$且m∈W，我们说，M;m|=AB当且仅当M;mA隐含M;mB. M|=AB iff对于所有m∈W，M;m A<$B.我们说AB是有效的（记法|=A<$B），当且仅当对任意模型M，M |= A B.很容易证明公理（A1）和（A2）在所有Kripke模型中都是正确的，并且规则（R1）和（R2）保持有效性，建立可靠性。为了完整性，我们可以将基于公式的canoni-calconn结构扩展为NL（3）（cf. [6，10]）。这是一个很好的模式 =Wc;Rc; Vc具有WC = FORM（语言中所有公式的集合）;<$RcAB当且仅当<$A<$B0;以及A∈Vc（p）当且仅当<$A<$p：注意，我们定义了W的两个元素与R不相关的情况。当然，这也确定了哪些要素是相关的。 但我们可以做得比C更好。 给定一个箭头A B，我们可以将Wc限制为简单的Wc = Sub（A）Sub（B）（A和B的子公式的集合），并证明下面的真值引理。Lemma2.1（TruthLemm a）GivenAB，对于A0;B0 ∈Su b（A）Sub（B）Mc;A0 B0iffA0 B0：有了这个引理，我们可以证明关于一类有限模型的完备性，从而也得到可判定性（实际上，甚至是复杂性的上界证据 证明过程中归纳的复杂性的conse-quent为mula。B组PROP，c; AB当且仅当AVc（B）当且仅当Vc，A B的定义。我们假设作为归纳假设（IH），引理对于比B更低或相等复杂度的公式是正确的。我们考虑0B（B0的情况更简单）。[1]direct cti o n. Mc; A0B，如果f为所有B0 ∈Wc如果RcB0A n Mc;B0 /B。通过对所有B0、Mc;B0的Rc进行比较和定义 B意味着B0 0. B和定义Wc，B0 在Sub（A）中，我们可以应用IH来确定所有B0 ∈Wc，∈B0 B表示 0. 在我的演讲中，B∈Wc且由（REFL）<$B<$B，因此<$B<$A0。通过（GC），A=0B。[10]Direction. 假设A=0B，以提供Mc; A= 0B。TakeB0 如果RcB0A，我们应提供Mc;B0 /B。NoticethatbydefineitionofRc，weehavet/B0 0. 对于一致性，支持Mc;B0 B，在我身边，► b0的 但是新的网络可以提供更多的信息 如图所示，阿雷塞斯、贝尔纳迪和穆加特5► B B► A组B组⇒ ∈· ⇒⇒⇒A► A100B0► 0B0B0 （R2）00（变速箱）（GC）（一个）► b0的 中国02定理2.2（完备性）给定A<$B，则|=AB意味着一个大的。Proof. 我知道了 。 ThenbyLemma2. 1Mc; A/B 。AsMc; AA，我们有Mc|=ABanddhence|=AB.2正如我们已经说过的，引理2.1实际上建立了一个强有限模型p rope rty（arowApB是valid当且仅当B在Mc中满足;A， 一个（pointed）模型，其大小是多项式，|一| ∪ |B|）.由此，对于NL（3，·0）follows，存在一个NP上边界条件。理论2.3GivenABNL（3，0），当rABisvalid可以在非确定性多项式时间内完成。2.2Gentzen演示，剪切消除在 这 一 节 中 ， 我 们 将 [18] 中 NL （ 3 ） 的 广 义 相 对 论 推 广 到 NL（3，·0）。我们如何使Cutrule符合阈值，从而产生可确定的证明搜索。我们的根岑表示有连续项，其中;∈C. 结构被定义为：|[2008年12月20日]|[C，结构连接词[和]与逻辑连接词0·和0，分别。文[9，21]在显示演算的框架下给出了伽罗瓦连通算子的证明理论。[2]展示了如何从显示演算转移到Gentzen演算（一元和二元）剩余和Galois连接算子。 在显示演算中，[and]通过（DGC）（（GC）的结构对应物）[iff]相关，这使得可以为连接词给出以下逻辑规则：（D1）（D2）（D3）[A]（D4） （2）0A[A0]0AA0在Gentzen的演示中，我们希望在逻辑规则中编译掉（DGC）（以及部分Cut规则）。因为伽罗瓦算子是逆序的，所以我们必须在割规则的陈述中区分正上下文和负上下文。我们写[]表示子结构处于等序位置（由偶数个结构连接词支配）的结构，写{}表示子结构处于反序位置的阿雷塞斯、贝尔纳迪和穆加特6·⇒（由奇数个结构连接词支配）。在（3）中，我们给出了我们必须考虑的割规则的四个例子⇒A[A] ⇒0[ ]100中国0 {A}（C1）0[A]A0 []{A} 0（C2）（三）0（C3）（C4）联系我们下面左边的介绍逻辑规则与显示演算表示中一样，右边的介绍规则在（DGC）的应用程序中编译A（0·L）0A[A 0]0AA0（4）中的逻辑规则交换了一个序列的前件和后件. 为了进行切割消除，我们还需要规则的上下文版本，在公理模式（A1）/（A2）中编译（C2）/（C4），并且补充规则（L），（R+）通过它们各自的结构对应物来描述逻辑连接。{A} 单位（0·L+）{A}（·0L+）（5）{]0A}{[A0}[A]（0·R）（·0R）（6）[]0A]我们将调用Seq-NL（3，·0），该Gentz表示NL（3，·0）的集合，以区分它与Hilbe表示Hil-NL（3，·0）的集合。第二个。在Seq-NL（3，0）中，每一个有效的矩阵AB都有一个无割证明.证明过程中归纳的复杂性削减推理。下面，我们介绍割消变换的主要情况：复割公式上的割被其子公式上的割所取代的情况，从而降低了复杂性。 其他案件遵循同样的想法。在（7）和（8）中，复公式A0上的同素割（C1;C3）被反素割（C4;C2）取代对于0A上的切割也是如此。（我们使用双线来实例化使逻辑规则适用的前提。）阿雷塞斯、贝尔纳迪和穆加特7Ab中国A0（·0R）联系我们Γ{b（A0）}0Γ[A0]0（·0L+）（七）Γ[π]π0（C1）Γ{A}0AbΓ{b<$}0;Γ{b<$}0（C4）Ab中国A0（·0R）[A]∆0 [b（A0）]0（·0R）（八）∆0（C3）0∆0⇒;Γ[b]0在（9）和（10）中，反序切割（C4;C2）被同序切割（C1;C3）代替联系我们{A0}（·0L）∆⇒AA0⇒∆（·0L）∆⇒AΓ{A}⇒∆0（九）Γ{}0（C4）;Γ{}0 （C1）[A]0（·0R+）∆⇒AA0⇒∆（·0L）∆⇒A∆0 [A]（十）∆0r[（C3）2.3Seq-NL（3，·0）的声音和互补性我们首先证明以下几点命题2.5设M= <$W; R;V<$是一个模型，且m∈W，则(i) M;m|=[A ][B][C]|=AB然后[B].㈡男; 男|=[A]0，|=B<$A，n[B]<$0。阿雷塞斯、贝尔纳迪和穆加特8(iii) M;m|=0{A}，|=BA然后10{B}。(iv) M;m|={A}0 和|=A<$B则{B}<$0。证据通过对A周围的算子个数的归纳，得到了A.2现在定义下面的遗忘函数。阿雷塞斯、贝尔纳迪和穆加特9→|⇒|⇒············定义2.6我们定义了以下翻译Tr：如下所述Tr（p）= p，其中p∈PROPTr（0（A））=0（ Tr（A）） Tr（[（A））=0（ Tr（A））Tr（A）0）=（ Tr（A））0 Tr（A））=（ Tr（A））0：运算符2.7（Seq-NL（3，· 0）的序列号）逻辑NL（3，·0）的序列号是不存在的。证据给定一个规则A组B组CD我们证明了如果=Tr（A）Tr（B），则=Tr（C）Tr（D），对于有两个前提的规则也是如此。注意命题2.5证明了割规则的合理性 对于规则（0R）、（0R）、（0L）和（ 0L ） ， 使 用 （ GC ） 规 则 是 合 理 的 这 一 事 实 。 对 于 规 则 （ 0R ） 、（0R）、（0L+）和（0L+），使用公式2。5加上公理（A1）和（A2）是有效的。2第二个。8（Seq-NL（3，·0）和Hil-NL（3，·0）的等式）如果A_B是Hil-NL（3，·0）的理论，则A_B在Seq-NL（3，·0）中的结果是正确的。对 于 Seq-NL （3，·0）中的一个方程，Tr（）→Tr（）是Hil-NL（3，·0）的一个定理.3语言运用既然NL（3，0）的语言学原理已经被解释清楚，让我们转向它的语言学应用。 为了探索伽罗瓦一元运算符的可能用途，重要的是要看看它们引入的新属性。正如我们在开始时所指出的，这些新算子不同于剩余算子的地方在于它们的单调性，以及在考虑它们的合成时它们关于它们的自变量的可导性关系（即，当A派生出（0A）0和0（A0）时，它派生出2#3A但不是32#A）。如果我们把复杂类型看作函数的组合，我们就会意识到，有向下单调运算符可以用来修改它们的参数的极性位置例如，如果我们考虑0与二元函数=的复合，它的第一个参数是正的，另一个参数是负的，我们看到它们的单调性是相反的。更具体地说，如果0A与B=组合，给出B=0（A），A将处于正位置，如果它与=B组合，导致0（A）=B，A将处于负位置。由于连接词的单调性决定了阿雷塞斯、贝尔纳迪和穆加特10·−→−→类型，增加了伽罗瓦运算符增加了类型之间的连接，这是范畴类型逻辑的主要特征在本节的下一部分中，我们将展示如何使用NL（3，0）的可导性项来计算广义量化器关于否定的可导性分布，并描述极性项的类型学3.1广义量化器作用域我们从一个例子开始，说明如何使用Galoisoperators和t（0s）0←→2#3s的组合来解释作用域现象，其中A−→B意味着公式是重言式，即A−→B当且仅当|= A ⇒ B.在范畴文献中，广义量化表达式（GQ）的一个众所周知的问题是对GQ的范围可能 性 所 需 的 原 位 绑 定 操 作 的 适 当 表 征 。 在 [17] 中 ， 引 入 了 一 个 “scop-ingconstructor”操作符q（A;B;C）来捕获此对象。 GQ被赋予类型q（np; s; s），因为它在局部表现得像一个名词短语，但在语义上在更高的语义层次上具有范围。控制该运算符的逻辑规则为：[A]B[C]D（qL）：[[q（A; B;C）]]D这个连接词的引入引起了许多模型理论和证明理论的问题，这些问题已经在[16]中得到了解决，其中证明了q连接词可以作为标准范畴类型系统的定义算子获得，并且上面的（qL）规则可以作为推理的这里提出的解决办法可以进一步简化，但由于篇幅的原因，我们不能详细讨论这方面的作用域构造函数q的目的是在多个量化器上下文中提供完整的组合可能作用域关系集-在这个意义上，它可以被视为May的[15]作用域一致性论文的演绎版本。Beghelli和Stowell [3]令人信服地证明了GQ具有非均匀范围的可能性。他们的理论的主要主张是，对于数量类型的某些组合，自然语言语法只是排除了某些逻辑上可能的作用域。在我们的设置中，这需要对q（np; s; s）赋值的子类型进行类型细化。在[4]中提供了遵循这些想法的第一个分析本文用导子关系32# s2#3s区分三个不同的能量水平：负的上界（32#s）、负的上界（s）和高的上界（2#3s）。GQ的不同分布，如每个N，一个N和一些N，相对于这些概率水平编码在它们的类型分配。阿雷塞斯、贝尔纳迪和穆加特11−→（s）/1023s0 0#⇒⇒¬¬然而，由一对剩余算子给出的线性可导性关系不足以解释更复杂的语言现象。例如，在[4]中提出的类型分配不能阻止负极性表达式的出现，如肯定句中的任何N我们将通过一个例子来说明如何使用类型（0）0来解决这个问题，以及如何解释正负极性项的不同范围可能性。让didn' t ∈（（s =（np \ s））\ s）=（np \（0s）0）.任意N∈q（np;（0s）0;（0s）0）.s ∈N∈q（np; 2#3s;2#3s）.在积极的语境中出现任何一个词，例如任何人离开，被阻挡在前面的房间里（as（0s）02#3s不能在微积分中推导出）：np np s（0s）0np·np\s（0s）0（\L）q（np;（0s）0;（0s）0）·np\s2#3s（qL）语法上的不合，例如，任何人现在我们转向极性项相对于否定的非均匀行为。GQ和否定的结合产生了作用域歧义，这在类型逻辑语法中对应于多重证明。在极性项（PI）的情况下，并非所有的逻辑可能性都是允许的。具体地，负PI将仅允许具有宽范围（GQ）的否定的阅读，而正PI将产生具有窄范围（GQ）的否定的阅读图2和图3中的证明图式说明了上面的词典条目如何正确地预测这些语言现象。当用一个像某本书一样的概率项来实例化quanti_r_q（np;s1;s2）时，例如John没有读过某本将类型分类应用于所有的book，q（np; 2#3s;2#3s），数量s1;s2的性质将不会使用h2#3s实例化d。图2中的第二个定义 −→（s）将失败（如23s−→（s））。当你在这里的时候0 0# 0 0图3中的详细说明将是可行的，可见。s−→2#3s，2#3s−→2#3s。另一方面，当考虑推导作为约翰没有读任何书的证明时，分配给负极性的 =s2 =（0s）0，其中hgivecorrectderivations−→（0s）0 和（0s）0 −→（0s）在图2中，并在图3中阿雷塞斯、贝尔纳迪和穆加特12···−→−→6Q3421图3中h（0s）0−→2#3s。这些简单的例子表明，属于同一句法范畴的项目所涵盖的不同范围分布可以通过类型之间的可导性模式来解释更确切地说，unaryoperatos（3;2#;0;0）提供了一种方法来编码表征相同类别的项目的 在上面的例子中，我们只使用了NL（3，0）中丰富的类型模式的一小部分。图中的Figur1总结了我们拥有的关系。注意，这些关系可以进一步扩展到第三层，因为除了导数A（0A）0之外，A0（A0） 在接下来的几页中，我们将使用图1中给出的相应缩写si来引用类型。0：（02#3s）0Q6在在@@0：（02#332#s）02#3sQ0 ：（0s）0Q6@I6@@@@S 4 ：2#332#s@@@@@@sQ0：（q 032#s）0q@@@@ 在S 1 ：32#s图1.一、NL（3，·0）中的一个随机分布SSQ@ SSnpnpss1nps=（np\s）ss1np·（s=（np布雷纳普（s））np·（s=（np\s）=（np\（s））·（（np（s））\s）=（np\（s））·np\s）0 0（=L）10 0\s）=np·np））（=L）1秒速时时彩2#q（np;s1;s2\1⇒⇒2122nn（\L）np·（（np\s）=np·np）s1（=L）%s%s%s%0（qL）np·（（np\s）=np·（0秒）0nps=（np\s） s2#3s（np\s）=np·q（np;s; s）<$np\（0s）0（\R）np·（s=（np\s））\s<$2#3s（L）np·（s=（np\s））\s）=（np\（0s）0）·（（np\s）=np·q（np;s; s）<$2#3s（=L）|{z } |{z}|{z}|{z}主语否定trans. 动词属量化器图二、宽范围否定（<$GQ）s（0s）0np npnp\snp\（0s）0（\R;L）NPnp·（s=（np\s））\ss1（\L）（qL）np·（s=（np\s））\s）=（np\（0s）0）·（（np\s）=np· ））2#3s|{z}主题|{z}否定|{z}译动词|{z}将军量化器图3.第三章。狭义否定q（np;s1;s2阿雷塞斯、贝尔纳迪和穆加特12阿雷塞斯、贝尔纳迪和穆加特13在本文的剩余部分，我们将展示上述推导模式如何提供一种精确的方法：（i）更深入地理解形式语言学文献中提出的极性项类型学;（ii）澄清类型学预测的结果，为进一步的研究开辟道路;（iii）进行跨语言比较。特别是，我们将研究[8]中讨论的希腊极性项目的类型学，并将其与意大利的数据和类型进行比较。3.2NL（3，·0）中概率项的一种类型扩展[23，22]中给出的结果，Giannakidou在[8]中给出了极性项对（非）真实性敏感性的深入分析- 其中，直观地，非真实表达式NV是这样的，当与命题p组合时，它不需要p为真。 除了我们上面介绍的负极性和正极性项目之间的标准区别之外，她还提供了前一组项目之间进一步分类的证据。 出于很快就会变得清晰的原因，她将整个群体称为情感PI（API），留下形容词“消极”来表示特定类型的API。对API不长的极性项被认为是正极性项（PPI）。现在我们粗略地介绍一下这一理论，并简述其类型学解释。要对极性项进行范畴类型逻辑（CTL）分析，需要记住的主要观察结果如下。（1）情节句（E）可以是真实的或非真实的，区别在于真实与非真实的出现。非真实表达（例如，分别是现在和五月）。（b）在非真实表达式中，我们可以区分反真实表达式（AV）的子集，它们是否定类算子（例如，没有，没有）。（c）在情感极性项目中，我们必须区分负极性项目（NPI）和APIs，负极性项目被定义为需要成为AV的论点的项目，APIs也在NV的范围内。在CTL术语中，（a）意味着NV（以及AV）表达式的应用将返回一个情节句;（b）意味着AV的类型必须派生NV的类型;（c）表示API是比NPI弱的类型，因此分配给API的类型必须派生NPI的类型。 让我们通过下面的推导来说明这一点。设NV∈E=P I;AV∈E=NP I且E=NP I−→E=P I，则AV∈E/NPINPI ∈NPIAVNPI∈ENV∈E/PIAPI∈APINVAPI∈EAV∈E/NPINV ∈E/API[编辑]AV∈E/APIPI ∈APIAVAPI∈ENV∈E/NPINV<$NPI∈E阿雷塞斯、贝尔纳迪和穆加特14推导表明，如果我们分配给AV和NV类型由上述关系控制，则反验证表达式将与NPI和API组合，但非验证运算符将不会与NPI（因为[*]中的推理失败）。由于=的逻辑性质，E=AP I−→E=NP I意味着NP I−→AP I，E=NP I−→E=AP I意味着AP I−→NP I。因此，（c）点是（b）点的简单推论更正式地说，这个简单的事实可以使用图1中给出的可导性关系（之一）来表达。但是立方体提供了更丰富的类型层次，这将允许我们在极性项之间进行更细粒度的区分，这实际上是语言数据所需要的我们看了[8]中的希腊语数据和意大利语数据进行跨语言分析。在Giannakidou 我们将把它们包含在我们的数据中。 在下面的示例中，许可操作符被强调，许可项被加下划线。>代表作用域分布，例如Neg> API意味着Neg的作用域超过API。希腊NPI：ipe leksi，API：kanenan，FCI：opudhipote1.我是卡南。阴性>API（tr.我2.Dhenipe leksi oli meraNeg>NPI（tr. 他一3.*Dhen idha opjondhipote *Neg> FCI（tr.我4.Objosdhipotefititisbori na lisi afto provlima.Modal> FCI（tr.任何学生都可以解决这个问题。5.Anthis tin Elena [puthena/opudhipote]，：Cond> API/FCI（tr. 如果你在任何地方看到埃琳娜，：：）6.一个人的生活是这样的。Cond> NPI（tr.如果你说一个字，我会杀了你）由于上面讨论的原因，以下类型将正确预测这些数据。为了完整性，我们还包括PPIkapjos（tr.某人）。阿雷塞斯、贝尔纳迪和穆加特154424414121144441412词典PPI：q（np;s; s），kapjo sNPI：np\s0，ipeleksiAPI：q（np;s0;s0），kanenanFCI：q（np;s0;s0），opudhipote1 1 4 4m 〇dal：（s0=np）\s0）\s）=（np\s0），b 〇rineg. ：（np\s）=（np\s0），dhencond. ：（s=s0）=s0，an11 3我们可以比较希腊的数据和类型与意大利的。意大利NPI：nessuno，API：mai，FCI：chiunque1.Nongiocomai Neg> API（文。我2.Nonho vistonessuno Neg> NPI（tr.我3.*Non ho visto chiunque *Neg> FCI（tr.我4.Chiunquepuor`risolverequuestopro ollemaModal>FCI（tr. 任何人都可以解决这个问题）。5.*请注意 *Modal> API（tr.你可以永远玩6.*Puoi prendere in puoi tonessun libro *Modal> NPI（tr.（可以借任何书）7.如果您使用的是trovarmi，：Cond> API（tr.如果你来看我，：：）词典PPI：q（np;s; s），qualcunoPPI：q（np;s0;s0），nessuno4 42 2API：（np\s）\（np\s0），maiFCI：q（np;s00;s00），chiunquem odal：（s00=np）\s00）\s）=（np\s00），puo`neg. ：（np\s）=（np\s0），noncond：（s=s0）=s0，se11 4读者可以参考[8]对希腊数据的完整分析阿雷塞斯、贝尔纳迪和穆加特16QQQQQQ希腊FCIAPINPI其实的***否定*是的 是的情态动词是的 是的 *条件是的 是的 是的意大利FCIAPINPI其实的***否定*是的 是的情态动词是的 **条件*是的 *我们总结了下表中的结果，并将其与意大利的结果进行了比较。最后，希腊语和意大利语的词汇类型分配可以总结如下：CondFCI/ModalQQ6在@@@NPI/阴性Q QCondQ6在@@@NPI/阴性Q Q6I@6@@6I@@I@6在@@@@@@@@PPIQ@@@@PPIQ@@@@6API@@在在6API@@在在@FCI/Modal？在希腊语意大利语从这一比较中可以得出以下结论：（i）可能存在PPI和API都合适的上下文（例如，条件句和模态算子）;（ii）可能存在不许可极性项的非验证算子（例如，在意大利语中，FCI在条件中是不允许的），（iii）可以存在对这些和对其他种类的非真实表达敏感的其他种类的极性项4结论本文着重讨论了伽罗瓦连通算子在基本逻辑的最小实现，并说明了这种最小加法如何提高文法逻辑的精确性进一步研究的一个明显的主题是伽罗瓦算子与一元和二元剩余族之间的通信@@QQ阿雷塞斯、贝尔纳迪和穆加特17·0;另一个有趣的方向是研究在范畴类型中添加逆序运算符在第3节的主要语言应用中，我们只使用了Galois运算符（0）0运营商0（（·）0），它们本身是保序的此外，我们对正确词汇类型分配的研究表明，非判定性和（0··）与真实性之间的可能联系和（2#;3）. 当用于与语言资源进行推理时，这可能会对这些运算符的语义引用[1] Abrusci，V.，Phase Semantics and Phase Calculus for Pure NoncommutativeClassical Linear Propositional Logic ， The Journal of Symbolic Logic56（1991），pp.1403-1451。[2] 阿雷塞斯角和R. Bernardi，分析范畴语法的核心，在：P. Blackburn和M.Kohlhase，editors，Proceedings of ICoS-3，2001，pp.7比28[3] Beghelli，F.和T.Stowell，Distributivity and Negation：The Syntax of Eachand Every，in：A.Szabolcsi，editor，Ways of Scope Taking，Kluwer，1997 pp.72比107[4] 贝尔纳迪河和R. Moot，Generalized quantifiers in declarative and interrogativesentences，in：Proceedings of ICoS-2，Dagstuhl，2000，pp.1-15。[5] Birkhoff，G.，“格理论”，美国数学学会，普罗维登斯，1940年，1948年，1967年。[6] DosEscheren ， K. ，AbriefsurveyoframesforrtheLambekcalculuss ，Zeitschriftfur？rmathematischen Logik und Grundlagen der Mathematik 38（1992），pp. 179比187[7] 邓恩，J.，伽罗瓦连接和剩余的抽象，应用于否定和各种逻辑运算，在：JELIA 1990。Proceedings of the European Workshop on Logics in Arti FicialIntelligence，1991，pp. 31比51[8] Giannakidou，A.， 论文，格罗宁根大学（1997年）。[9] G或e' ，R.，Substructurallogicsondisplay，LogicJournalofeIGPL6（1998），pp.451-504[10] Kurtonina，N.， 范畴推理的模态分析论文，OTS乌得勒支大学，ILLC阿姆斯特丹大学（1995年）。[11] Kurtonina，N.和M. Moortgat，结构控制，在：P. Blackburn和M. de Rijke，editors，《语法结构》（阿姆斯特丹，1994年），CSLIPublications，Stanford，CA，1997 pp.75比113;阿雷塞斯、贝尔纳迪和穆加特18[12] L AMBek，J.， 从范畴到双线性逻辑，n：K。 D osenanddP. Schr？der-Heister，editors，Substructural Logics，Oxford University Press，1993 pp.207- 237[13] Lambek，J.，类型语法重新审视，在：计算语言学的逻辑方面（南希，1997年），施普林格，柏林，1999年页。1-27号。[14] Lambek，J.，Type grammars as pregroups，Grammars4（2001）.[15] 梅河， 麻省理工学院（1977）。[16] Moortgat，M.，原位结合：模态分析，在：P。Dekker和M.Stokhof，editors ， Proceedings of the Tenth Amsterdam Colloqium ， ILLC ， 1995 ，pp.539- 549[17] Moortgat，M.，广义量化和不连续类型构造函数，在：H。Bunt和A.vanHorck ， editors ， Discontinuous Constituency ， MoutondeGruyter，Berlin，1996 pp.181-207.[18] Moortgat，M.，多模态语言推理，逻辑，语言和信息杂志5（1996），pp。349-385[19] Moortgat，M.，范畴类型逻辑，在：J。van Benthemand A.《逻辑与语言手册》，麻省理工学院出版社，剑桥，马萨诸塞州，1997年。93比178[20] 奥 尔 岛 ， Galoisconnections ， TransactionsoftheAmericanMathematical Society55（1944），pp.493-513.[21] Restall，G.，[22] van der Wouden，T.，“消极语境”博士论文，格罗宁根大学（1994年）。[23] Zwarts，F.，非真实语境，语言分析25（1995），pp。286-312