第一章 预备知识
为了使本书做到“自足”,特给出预备知识,供读者参阅。简单类型论、范畴语法、话语表现理论和λ-演算是理解后续组合性方案的基础,预先熟悉将有助于读者理解范畴语法和话语表现理论两大语义框架的联结。话语表现理论遭遇的组合性问题,其解决方案多涉及类型论相关知识,本章将分别介绍简单类型论、范畴语法、话语表现理论和λ-演算。每一节开头部分会说明该预备知识适用于后面哪一章及文献出处。
第一节 简单类型论
类型论是联结两大语义框架的纽带,话语表现理论组合性方案的很多内容涉及类型论相关知识,本节主要介绍简单类型论,内容依据Gamut(1991a,1991b),以及Stergios Chatzikyriakidis和Luo(2020)的研究进行整理。
类型论自产生起,便受到逻辑学、哲学、计算科学、数学等诸多领域学者的关注。在当今人工智能日盛的大背景下,类型论的计算科学意义得以彰显。对计算科学家而言,类型论是桥梁,联结逻辑和程序语言。本节从类型论的产生背景讲起,扼要介绍罗素悖论的产生及如何避免。值得一提的是,简单类型论中有一个非常著名且强大的系统,称为“construction”,译作“构造”。20世纪40年代,开始出现“带类型”的λ-演算。也是在这个时期,逻辑系统与类型论结合起来。逻辑系统被纳入类型论源于这样一个思想:逻辑蕴含可被看作一个函数。具体来说,一个形如A→B式命题的证明可被看作这样一个函数,它的输入是A的证明,它的输出是B的证明。这样,命题A→B可被视为所有那些以A的证明为论元,以B的证明为输出的函数所构成的类,正是由于这个理念,有人总结出“命题作为类”(propositions as types,PAT)的口号。20世纪60年代,一种非常重要的系统—“纯粹类型系统”(pure type systems,PTSs)出现了,影响非常大。这个时期还出现了二阶类型论,允许变元遍历(ranging over)类,而不像简单类型论那样,变元遍历函数。
现在类型论被广泛用于不同学科,即使与类型论*贴近的逻辑学和数学,也存在几种不同的类型论系统。类型论用途不同,表述形式也不同。但在罗素创立类型论时期,即1903年之前,不存在别的形式或版本的类型论。到了20世纪中叶以后,类型论的探索使得相关成果丰富起来。
类型论*早是用来避免产生悖论的。19世纪末、20世纪初,在数学和逻辑学中出现了悖论,当时,区分出不同类型或者说分层思想是解决悖论的方案之一。这里说的悖论是指罗素悖论,其构造思想是这样的。在朴素集合论中,有一条“概括公理”(the axiom of comprehension),说的是任意一个开放的、构造良好的表达式(well-formed expression)确定了一个概念,这个概念的外延存在且外延就是满足这个概念的所有元素构成的集合。简单来说,就是对于任何性质G,{x|G(x)}都是一个集合。如果这样假设,那么我们就陷入了罗素悖论,它在19世纪末、20世纪初曾引起数学界的巨大恐慌。以下简要回顾该悖论。根据前面的假设,我们必须承认{x|x = x}是集合。因为每个个体都等于它本身,所以设V是包含所有事物的全集。现在,如果V包含所有事物,则有V V;所以像V这样的一些特殊集合具有性质x x,但大多数集合不具有这一特征;比如,0 0,因为0不是集合;{0} {0},因为{0}只含有一个元素0,且0≠{0};N N,因为只有整数才是N中的元素,而整数的集合不是N中的元素;等等。再考虑由所有这样的对象组成的集合R,根据我们的假设,R = {x|x x}。那么,R是不是它自身的一个元素呢?这正是悖论所在。如果假设R R,那么R必须具有决定R中构成元素的性质,即R R,这样从R R推出R R。但是如果R R,那么说明R具有决定R中元素的成员资格,所以必须有R R。因此,从R R可以推出R R。两个方向的推导结果是建立矛盾等价式,悖论也就出现了。
在现代集合论中,有一组公理用来决定哪些集合可以由其他集合定义出来。这样,许多集合可以用{x|G(x)}的方式定义,同时又避免了罗素悖论,代价就是:V = {x|x = x}这类情况不再是集合:因为它的范围太大了。这也是我们在进行谓词逻辑翻译时,不能简单地在论域中放入所有东西的一个原因。
要避免罗素悖论,可以对概括公理进行限制。先从分离公理(separation axiom)(模式)说起,它的一个实例包含自由变元x, w1, , wn, A等。B不在φ中自由出现。借用集合论语言,该公理模式表述如下:
用自然语言表述如下:
给定任意一个集合A,存在一个集合B满足,给定任意集合x,x是B中的一个元素当且仅当x是A中的一个元素,并且φ对x来说成立。
注意,这是一个公理模式,对于任意一个谓词φ,都存在一个具体的公理实例。
集合B一定是集合A的一个子集。因此,这个公理模式真正想说的是,给定任意集合A和谓词P,我们可以找到A的一个子集B,B的y元素恰好是A中具有P属性的那些元素。根据外延公理,确定集合B是唯一的。通常记作:{C A:P(C)}。由此可知,这条公理的本质是说,一个集合的每个由一个谓词定义的子类本身是一个集合。这样就不会出现罗素悖论产生的“大全集”,悖论也就避免了。用集合论的方法避免悖论,还有其他相关内容,这里不多涉及。
一、简单类型论的起源
避免悖论产生的类型论方法完全不同于集合论方法。
首先,在类型论方案中,是通过改变语言而不是改变公理来避免悖论出现。*先提出用限制语言的方法避免悖论的是罗素和庞加莱(Poincaré)。他们都不承认非直谓(impredicative) 的分类方式,而只允许出现直谓(predicative)的分类方式。庞加莱指出,非直谓的定义会导致恶性循环,一个定义是非直谓的是说,定义项包含或涉及一个大全集,其中,被定义项是该大全集的一部分。从集合论角度简单来说就是,一个类本身不能作为这个类的一个元素。对于一个集合A = {x:Φ(x)}来说,它是直谓的,当且仅当不包含变元可取A为值。这对于避免悖论产生有帮助,因为如果允许函数本身(或集合本身)充当自己的论元(或集合的元素)便会出现罗素所谓的恶性循环。罗素和庞加莱的方案用直谓式概括公理(或直谓式概括原则),从个体出发,生成集合,然后再生成新的集合,依次类推。例如,0处于0层,{0}处于第1层,{0, {0}}处于第2层,依次类推 。罗素在《数学原理》里提出的分支类型论(ramified type theory,cf. Whitehead and Russell,1925)使用了(禁止)恶性循环原则,即由一个性质或条件(语言单位上即一个谓词)确定的实体若需要借助于某个整体来定义,则该整体不能包含这样的实体,假定集合的所有元素在构建集合之前便存在。这种思路明显避免了悖论问题,因为?(y y)这个句子不是直谓的。
其次,自从丘奇的λ-演算被扩充为带有类型的演算以来,类型论在逻辑学和数学领域的相关研究一直关注函数概念,将其作为主要研究对象。类型和函数的演变和扩充也是类型论的研究重点。
从弗雷格开始,很多学者研究过类型论系统,如罗素、拉姆齐(Ramsey)、丘奇(Church)等。这些学者研究类型论系统经常以现代类型论框架描述,但现代的描述与原初的系统之间的关系一直没有说清楚。原初的类型论系统在记法上、形式化程度和建立系统的动机或意图上都与现代类型论系统差距很大,如何介绍那些略带时代感的系统是一件具有挑战性的事情。当然,还是要在现代类型论框架内介绍那些初期有关类型论的工作,但会尊重学者当初的研究动机和哲学思想;并采用当代学者熟悉的记法描述原来的系统。
Kamareddine等(2004)介绍了带类型的λ-演算,确切地说是纯粹类型系统(PTSs)所论述的框架,囊括了许多类型论系统,比较接近现代类型论所要求的形式化,也强调类型论的核心:函数抽象和应用。这使得在该框架内比较不同的类型论系统成为一件易事。文献中存在许多PTSs的扩充,包括对PTSs基本定义方面的扩充,也包括对带有П-化归的PTSs所做的扩展,感兴趣的读者可以进行扩展阅读。
本章结合Gamut(1991b:第四章)的研究整理出适用于表征或刻画自然语言语义的简单类型论,以便本书后续章节的阅读,类型论的其他版本会在别的专著里另做研究。
二、简单类型论简介
这里的“简单类型论”源于罗素等人提出的分支类型论,旨在解决罗素悖论等悖论所导致的对数学基础的信任危机。拉姆齐(1925)指出,分支类型论可“简化”为简单类型论,并由丘奇用?-演算将其形式化且被广泛应用。例如,在形式语义学界一直占有统治地位的蒙太格语义学的基础便是简单类型论及其模型理论。
(一)自然语言中类型的划分
下面从自然语言分层开始讲起,逐渐引出简单类型论,其中示例和表述主要援引自Gamut(1991b:第四章)的研究内容,有不清楚的地方可以参阅原著第75~91页。
在联结词和量词(有时还含有等词和函项符号)之外,还有两类符号出现在一阶逻辑的语言中。其中一类是表达某一给定论域中个体的个体常项和个体变项;另一类是谓词常项。谓词常项又分为一阶谓词常项—指称个体的集合和n阶谓词常项—指称由n个个体组成的有序组的集合。
这表明一阶逻辑能对个体的性质和个体所处的关系进行分析。而相对于这些人工语言,人们所使用的“自然语言”,能谈及的对象超出了上述范围。如果要讨论比一阶逻辑面对的对象更复杂的现象,那么需要内容更丰富、功能更强大的工具才行。先考虑一些无法直接翻译成谓词逻辑的语句,然后考虑如何借助表达力更强的逻辑手段将它们充分表达出来。
下面的例句涉及对性质的量化。一般来说,一个句子表达某个或某类个体具有某一性质。当然,还存在其他句子,比如,有的句子能够表达两个个体共有某一性质,同时不必明确指出这一共有的性质是什么。思考:
①If John is self-satisfied,then there is at least one thing he has in common with Peter.
(如果约翰自满,那么他至少在这一点上与彼得相同。)
①含有对性质的量化。②属于另外一种,它断言某一特殊个体具有某一类特殊事物的典型性质:
②Santa Claus has all the attributes of a sadist.
(圣诞老人具备虐待狂的所有性质。)
②说明对任一性质而言,若该性质是虐待狂所具有的一种典型性质,则该性质也是圣诞老人所具有的一种性质。如果量化不仅针对个体,还针对个体的性质,我们就需要引入新的变项,以便对个体以外的变项进行约束,从而对谓词逻辑进行扩展。除了谓词字母,我们还需要谓词变项使得能够对句法中的该类型变项进行量化。令X是这样的一个变项,①和②可以被表示为③和④。
③
④
(注:s代表圣诞老人,X量化了虐待狂所具有的性质)
能够对个体和个体的性质两者进行量化的逻辑系统是二阶谓词逻辑。经典谓词逻辑有时也被称为一阶谓词逻辑。由于二阶谓词逻辑缺乏完全性定理,逻辑学家们对它的研究并不那么热衷。然而,这并不影响它在语言学方面的应用。
在处理自然语言方面,二阶谓词逻辑和一阶谓词逻辑一样表达力不够强大。因为自然语言既有对个体的性质进行量化的语句,也有反过来对个体性质的性质进行描述的语句。例如,谓词“red”(红)表明个体具有的一种性质,因此谓词“color”(颜色)就表明个体性质的一种性质。因此句子“Red is a color”(红是一种颜色)可以表示为(R),二阶谓词“color”用来断定一阶谓词“red”。我们还可以对这些性质的性质进行量化,如“Red
展开