第3期 刘冬宁，等：时态查询语言的并发Lambek演算及范畴语法 ·249 行处理的，额外添加的类型主要体现在时态类型、时 一类既没有收缩规则，又没有弱化规则的逻辑系统 态关系运算以及系统公设上.由于添加了系统公设， 称为资源敏感逻辑(uc-enaitive)),它能使得 第1节例子的查询语句的转换如下. 参与演算的资源都“用到且仅用到一次”，满足了计 System 算性资源的特点，由此在计算语言学中得到广泛应 Select rl.Name 用.因此，使得在此基础上建立的LcQ演算和Lcm范 from works rl,works r2 畴语法能更好地用于时态查询语言的句法分析.从 where rl.Name r2.Name 证明论性质上，由于计算性资源的保障，也使得系统 and Valid (rl)meets Valid (r2) 更为严谨和完善。 各部分类型演算步骤分列如下： 5结束语 1)“System”:系统公设，类型为n; 2)“Select rl..Name”类型演算为：（(n+s)← 由于时态类型区别于语言学中诸如动词、名词、 a)·a上n→s; 副词等语言结构类型，针对时态查询，文章提出了并 3)“from work8rl,work82”类型演算为： 发的Lambek演算，证明了其可靠性和完全性，并通 ((ss)-f)·((←f)·月·f→Uf←f))· 过实例进行了阐述与演算，文中提出的并发的Lam- ((f←f)f)s+s； bck演算(LQ),从证明论角度上，保障了计算性资 4)“whererl.Name=2.Name”类型演算为： 源，避免了蕴含怪论等问题，使得系统更为严谨和完 (s+s)←-s)·a·(a→(s←a)·as→s; 善.在下一步工作中，将主要研究句法分析和语义分 5)“and Valid(rl)meets Valid(r2)”类型演算 析的衔接问题以及语义分析，其基本思路是通过 为：((s+s)←-s)·(a←)·(t1(a+ Curry-Howard对应理论和类型演算入-演算将句法演 (s←a))lt)·(t+a)上s→s; 算过渡到语义演算，对相关语义进行分析，并建立原 6)全句最终类型演算为：n·(n+s)·(s→s)· 型系统或直接在TempDB上进行验证， (s+s)·(s+s)3 参考文献： 据Lm演算，上述句型的类型演算最终能推出 终止符类型：，使得句法分析演算停止并得到正确 [1]CHOMICKI J,TOMAN D.Temporal logic information sys- 结果.而对于不符合句法的查询，则不能得到终止符 tems[M]//CHOMICKI J,SAAKE G.Logics for databases and information systems.Norwell,USA:Kluwer Academic 类型s,这是由可靠性和完全性保证的， Publishers,1998:31-70. 4 证明论性质 [2]GABBAY D M,HODKINSON I,REYNOLDS M.Temporal logic:mathematical foundations and computational aspects 文中根据时态查询语言需要表现时态性的特 [M].New York,USA:Oxford University Press,1994. 点，修改了Lambek演算，在其基础上添加了并发连 [3]BUSZKOWSKI W.Categorial grammars and substructural 接词“1”和相关规则，新的系统称为L灬演算.事实 logics[C]//Proceedings of the 5th International Conference 上，如果在系统中添加了收缩律(contraction),如下 on Logic and Cognition.Guangzhou,China,2006 所示： [4]RESTALL G.An introduction to substructural logics M]. X,A,A,Y上B New York,USA:Routledge,2000. X,A,YB (contraction), [5]JAGER G.Anaphora and type logical grammar[M ]Dor- 则并发连接词“1”将与经典的连接词“八”等价.但 drecht,the Netherlands:Springer,2005. [6]LAMBEK J.The mathematics of sentence structure J]. 这不是所希望得到的，因为收缩律的缺失，使得每一 The American Mathematical Monthly,1958,65:154-170 个演算的资源都至多只能使用1次，保证了句法分 [7]BARENDEGT H P.The lambda calculus:its syntax and se- 析的词项不能重复使用.同时，系统由于没有弱化规 mantics:volume 103 of studies in logic and the foundations 则(weakening),如下所示： of mathematics[M].Amsterdam,the Netherlands:Elsevi- a(（abeni). er,1984. [8 ]PENTUS M.Lambek grammars are context-free[C]//Pro- 使得每一个演算的资源都至少要使用1次.这样的 ceedings of the 8th Annual IEEE Symposium on Logic in