论类型逻辑语法的多种表述，本文主要内容关键词为：语法论文,逻辑论文,多种论文,类型论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
一、类型逻辑语法的三种基本表述
类型逻辑语法亦称范畴类型逻辑。荷兰逻辑学家和计算语言学家莫特加特（Moortgat）用三个口号概括出要点：认知（cognition）＝计算（computation）；语法（grammar）＝逻辑（logic）；解析（parsing）＝演绎（deduction）（Moorigat，2005a）。这意谓，语言认知可以化归为计算过程；语言的语法解析（句法毗连和语义组合）能够纳入逻辑的框架；语言的句法语义分析就是一种演绎推理。简言之，类型逻辑语法的最大特色就是把自然语言的句法毗连和语义组合转化成运算和推演；这是满足计算机信息处理之需求而制定的自然语言语法，是面向计算机人工智能领域的自然语言语法。
类型逻辑语法的最早形态是上个世纪30—40年代由波兰逻辑学家爱裘凯维茨（Ajduciewicz）提出并在50年代初由美国计算语言学家巴－希勒尔（Bar-Hillel）充实完善的范畴语法。作为范畴语法的形式系统，加拿大数学家兰贝克（J.Lambek）在《句子结构的数学》一文中提出了著名的兰贝克演算。（Lambek）兰贝克以描述英语的一个片段为自己的目标。首先，确立表示句子的范畴s和表示名称的范畴n为初始范畴，形成复合范畴的定义为：
如果x和y是范畴，那么x／y（读作x在y之上）和y＼x（读作y在x之下）是范畴。
这里x／y和y＼x又叫函子范畴，相对而言，y叫主目范畴，x叫结果范畴。
其次，再给英语的若干词类指派范畴，这种指派形成词库，如：
为了强调这种指派服务于句子分析的作用，兰贝克还列出一些实际的英语句配以范畴指派的说明：
（1）Johnworks（约翰工作）
nn\s
（2）John(never works)（约翰从不工作）
n
(n\s)/(n\s) n\s
（3）(John works) (for
Jane)（约翰为简工作）
n n\s(s\s)/n n
（4）(John works) (and (Jane rests))（约翰工作而简歇着）
nn\s(s\s)/s nn\s
对句子的成分指派了范畴后，就需要确立范畴运算的规则：若表达式α对应范畴A／B并且表达式β对应范畴B，则表达式αβ对应范畴A；若表达式α对应范畴A并且表达式β对应范畴A＼B，则表达式αβ对应范畴B。在兰贝克演算中，上述运算规则表现为刻画范畴推演规律的定理，T1：（A／B）B→A，T2：A（A＼B）→B。
对兰贝克构造的英语片段中的合语法句子，根据上述定理，能够给出逻辑上更加清晰的推演过程：
从左到右，一个箭头表明定理的一次运用，符号串的长度依次递减，最后到达范畴s。
兰贝克演算上世纪80年代末被兰贝克和多森（Dose）再次提及，给出其现代表述，即所谓类型逻辑语法的三种基本表述：公理表述（axiomatic presentation）、根岑（Gentzen）表述和ND表述（Natural Deduction Presentation）。
类型逻辑语法的公理表述由一条公理和五条规则构成。非结合的兰贝克演算是这种表述的代表：
第一条是同一公理，其余都是推演规则。生成自然语言句子的范畴推演的工具由公理表述中的定理所提供，参见前例所涉及的定理T1和定理T2。
相应的根岑表述，也称作类型逻辑语法的后承演算（sequent calculus），表现为：
与公理表述不同的是推演规则增加为七条，除第一条公理外，每个后承的前件做出更一般的概括，由公理表述那里的单个公式扩展成公式序列。后承前件中的空心圆“。”相当于逗号的作用。Γ［A］表明包含A作为其子序列的公式序列Γ。根岑表述仍然可以给自然语言的生成提供范畴运算的依据，令Δ＝A＝B，Γ［A］＝B＝C，
，［\L］就是：
加上［Ax］公理的作用，就推出了公理表述中定理T2的对应物：
。
类型逻辑语法基本表述的最后一种是所谓ND表述：
比较根岑表述，ND表述有一条类似同一公理和除cut规则外其他六条推演规则的对应，如［/R］对应［/I］，［/L］对应［/E］。［/R］与［/I］非常形似，［/L］跟［/E］的最大区别是，前者在推演规则的结论中引进左斜线算子，后者则是把前提中的左斜线算子消去。前者的做法（以及cut规则的消除）有利于判定问题的解决，后者则是为了展示联系自然语言的毗连生成而做出的便于直观认知的推演。
二、类型逻辑语法三种表述的功能作用
尽管类型逻辑语法的三种基本表述在推演能力上是等价的（Moortgat，2005b），然而却有各自的功能。公理表述的功能是用于框架语义学基础上的可靠性完全性的元逻辑讨论；根岑表述则便于定理证明的有穷搜索，即判定问题的解决；ND表述有助于联系自然语言而使范畴演算显得直观自然。
为类型逻辑语法公理表述配备的框架语义学是：
公理表述的元逻辑性质：
A→B是可证的，当且仅当对每一框架的每一赋值V来说，
。
从左到右是说公理表述的可靠性，从右到左显示公理表述的完全性。为证明完全性，需要定义典范模型及其真值引理。令典范模型
，其中：
W是公理表述所有公式的集合；
类型逻辑语法的公理表述的作用已说明。那么，根岑表述的功能是什么呢？我们知道，逻辑系统的判定性是指：给定任意的公式，能在有穷步骤内断定它是否是系统中的定理。据此衡量，公理表述中传递规则的使用，由于不清楚“中介”公式B的形式构造，就无法确定其来源。因此传递规则推出的A→C是否是系统的定理，就没有一个能行的判定程序。而在根岑表述这里，对应传递规则的Cut规则是可以消去的。在公式复杂度即所包含的算子数量是有穷的情况下，给定任意根岑后承，每回溯使用一次根岑表述的推演规则，算子就减少一个，最后化归到不含算子的后承，若这些后承都是同一公理，则被判定的根岑后承就是定理。这些化归是有穷的，化归过程就是根岑后承的判定程序。因此在根岑表述系统内，可确定任意根岑后承是否是定理。（Moortgat，1997）
要确立判定定理，先需证明消去Cut规则的根岑定理：如果
是一个根岑后承，则存在一个消除Cut规则的关于的证明。证明的要点有：
●确立构造性的算法，把涉及Cut规则的推演改造成消去Cut规则的推演；
●证明的方法是：施归纳于Cut规则的复杂度，基于其中算子出现的次数；
Cut规则：
其复杂度：α（Cut）＝α（Δ）＋α（Γ）＋α（Γ′）＋α（A）＋α（B）
Cut公式：4
Active公式：指前提中包含算子的公式
●证明的目标是把使用Cut规则的推演置换成一个或两个使用更小复杂度Cut规则的推演。重复这个置换过程，直到Cut规则的使用都被消去。
根据上述思路，施归纳于使用Cut规则的各种情况：
情况1.归纳基始情况：Cut规则的前提之一是公理，另一前提就等同于Cut规则的结论，这时显然就不需要Cut规则的使用。
情况2.Cut规则的左前提或右前提中的Active公式不是Cut公式，这时要证明引进Active公式中算子的推演规则和Cut规则可以交换顺序使用，即把先用引进算子的推演规则后用Cut规则的次序换成先用Cut规则后用推演规则的次序。交换后的Cut规则，其复杂度显然小于原先的Cut规则（六种情况）。
情况3.Cut规则的左前提和右前提中的Active公式就是Cut公式（三种情况）。（J
ger，2005）
判定定理：根岑表述的推演是可判定的。
判定定理之所以成立，是因为：在消除Cut规则后的根岑证明中使用的每个规则那里，前提中的每个公式总是结论中某个公式的子公式，规则使用一次就增添一个算子。反过来说，对给定复杂度的根岑后承来说，我们企图从下到上构造一个树形图的证明，每一步向上回溯都消去算子的一次出现。由于每个根岑后承所包含的算子是有穷的，在有穷多步后总可以消去所有的算子。给定后承关系是可推出的，当且仅当构造的回溯证明树形图是成功的（即这个树形图的所有分支都化归到公理）。
类型逻辑语法的公理表述用于系统可靠性完全性的元逻辑讨论，其根岑表述的功能是解决系统的判定问题。那么，ND表述有什么作用呢？简言之，这种表述有助于联系自然语言而使自然语言的毗连和范畴演算的关系显得直观自然。
添加词库（Lexicon）的内容，ND表述就成为联系自然语言的类型逻辑语法。这里从ND表述的初始符号谈起，ND表述有两大类初始符号（Moot）：
定义基于原子公式集合A和5个范畴算子，所有公式（范畴）的集合为：
定义基于结构变项的可数无穷集合V，结构树的集合为：
这里可以把
看作是自然语言单词的集合，
意谓结构树
属于公式
。在词库中，每一单词对应一个这样的“属于”，这些“属于”意谓对初始的结构变项（单词）配备公式（范畴），意谓把具体的单词抽象成范畴。词库可能包含：
由于词库的作用，一开始就把具体的自然语言单词同抽象的范畴运算联系在一起，而ND表述特定的［/E］和［\E］之类推演规则更能保持这种联系，这就使自然语言的毗连生成和范畴的运算推演始终同步进行，这样很接近人类的认知习惯。例如：
上例表明：“├”左边是自然语言从小到大的生成毗连，右边是相伴随的范畴运算的推演。与根岑表述的［/L］和［\L］规则做比较，ND表述的［/E］和［\E］规则最能体现自然直观的推演特色，展示如下：
根岑表述的［/L］规则关注的是如何在结论中引入斜线算子，体现为结论的后承展示的是从抽象范畴到抽象范畴的“化归”。而ND表述的［/E］规则却在作为结论的断定中消去了斜线算子，结论中的断定可以显示从自然语言到范畴的抽象。根岑表述多用于理论探讨，揭示范畴之间的推演规律。而ND表述擅长于应用关联，突出范畴和自然语言的联系。
三、类型逻辑语法的加标树模式ND表述
最后讨论类型逻辑语法的一种综合表述形式：既是加标的，又是树模式的（tree format）。
“加标的”概念意谓：基于哈里－霍华德对应定理（Curry- Howard Correspondenee），在类型逻辑语法中给范畴推演的每一步配备λ-词项，在范畴推演的同时也让对应的λ-词项进行组合运算。范畴推演属于句法层面，而λ-词项则属于语义层面。二者的并行推演运算体现出句法和语义的接口（interface）。加标的类型逻辑语法表述意谓在对自然语言的处理中引入了语义因素。
我们既可对根岑表述加标，也可对ND表述加标。后者表现为：
如果在联系自然语言的词库中对每个单词指派λ-词项和范畴的序对，类型逻辑语法就表现出句法和语义的并行推演：代表句法规律的范畴在运算的同时，代表语义的λ-词项也在组合运算。一个简单推演为：
类型逻辑语法的加标树模式ND表述是把加标ND表述中语言符号串的横向排列换成纵向排列（Jger，2003）：
可以证明类型逻辑语法的加标ND树模式表述跟加标ND表述乃至加标根岑表述具有同等推演力（Carpenter,pp.67－68）。但是，既然已有加标ND表述，加标树模式ND表述的价值何在？初看起来，加标树模式ND表述比加标ND更直观，更符合自然语言自上而下的生成过程。但在笔者看来，其更重要的价值在于适合描述自然语言那些在语义上互相依赖且有独立性而在句法上是分开的情况，譬如自然语言中的照应回指现象。句子系列的在前句子所包含的先行语大都是名词短语或专名，在语义上先行语和后续句中的回指代词指同一个对象，但在句法上先行语和回指词却是非连续的，其间插有其他成分。如包含宾语子句的复合英语句“John said he walked”，“John”是先行语，“he”是回指词，中间插有“said”。为处理这个现象，耶格（Jger）提出直线算子及其树模式的ND推演规则：
在词库里对作为先行语的专名和回指代词指派特定的加标范畴值后，就可以对上述英语句进行加标的树模式ND推演：
这里回指代词的语义作用是：从先行语那里通过运算获得确切的语义所指，这一点同两个斜线算子的作用类似。另外，直线算子运算的结果可以在自身语境中进行推演，但给先行语指派的类型逻辑语义值并没有消失，仍然独立存在于另一语境中而发挥作用，这一点与斜线算子的情况完全不同，这就是直线算子处理非连续现象的特殊功能。直线算子范畴的运算既要依赖其主目范畴，又要求主目范畴保持一定的独立性。这恰好说明了回指词同先行词之间的语义关系。树模式ND表述的规则展示的纵向推演，其顶端正好表现自然语言符号串中间断开的横向排列。用通常的ND表述难以胜任这个任务。
结论：类型逻辑语法有三种基本的表述方式：公理表述可以配备框架语义学而成为一种多模态逻辑系统；根岑表述是专门为解决判定问题而设计的装置，具有重要的可计算性价值；ND表述便于联系自然语言而体现出“语法=逻辑”的思想；加标的树模式ND表述是类型逻辑语法的综合表述方式，它有利于处理自然语言的复杂现象，值得我们进一步发掘和拓展。