第3期 刘冬宁，等：时态查询语言的并发Lambek演算及范畴语法 ·247. 动的.下面以表1举一个简单的例子 规则： 表1人员工作覆历表 X上AY,A,Z上B(Cut)； Table 1 Personnel employment Record Y,X,Z-B Works XHA.B YA.B,ZC (E); Y,X,ZB Valid Name Company [1997,2001] John DEC X上AX上B(·D: XFA·B [2003,forever] John HP [1999,2005] Marry HP X上AY上A→B(+E); X,Y-B [2005,forever Marry Microsoft 0: 在表1中，希望查询没有失业过的人员名单，该 查询语句如下所示： X上A←BY上B(←E): X,Y-A Select rl.Name from works rl,works r2 ←n: where rl.Name r2.Name X上A-B Y BIC(IE'); and Valid (rl)meets Valid (2) X,YFA·C 这里Valid(rl)和Valid(2)表示有效时间，这 X上A1BY上B→C(IE'); X,YFA·C 是基于时态查询结构化语言(ATSQL2)和TempDB 语法习惯的叨.作为时间属性，Vaid(rl)和Valid X上AX上B(I0. XFAI B (r2)的类型分别为：a←1和t→a,其中：l表示时间 除(IE)、(IE)、(II)3条规则外，其余规则 类型，α表示属性类型，属性类型是由时间类型驱动 是经典Lambek演算L系统的全部规则，它们组成 的.meets是Allen提出的l3种时态区间运算之 原L系统6.(IE)、(1E)、(I)3条规则是为新 一1)，也是AT$QL2规定的时态运算.在这里它的 添加的连接符“1”加入的消去和引入规则。在消去 类型为l(a→(s←a)1,其中：仍然表示时间 规则中，(1E)为左消去规则，(1E)为右消去规 类型；a→(s←a)表示关系运算类型，对于时态关 则，(1)为引入规则. 系运算而言，2种类型应是并发处理的. 定义1如果矢列T→A在L演算中是可推 句法分析的主要目标是根据初始类型，通过相 导的，则写作T卜m→A. 应演算系统，得出终止类型.据此，新连接词“”的 2.2代数模型 引入及词项的类型赋值变化，要对上述例子做句法 与经典Lambek演算的L系统大致相同，Lcro系 分析，必须设计相应的Lambek演算系统，作者称之 统的模型也为剩余代数(residuated algebra)模型3]， 为并发的Lambek演算系统，即Lcm演算系统(Lamr 对于LcrQ系统的剩余半群(residuated semigroup)和 bek caculus with concurrence for temporal querying). 剩余运算(re3 iduated operation)描述如下. 在下文中，先讨论Lm演算系统的相关性质，并最后 定义2Lro的剩余半群的结构为M=(M,·, 将其应用于上例中 →，←-，I,≤)，使得(M,·)是1个半群，≤是M上 偏序关系，且+、←-、丨是M上的二元运算，并对所 2LcQ演算系统 有a,b,c,d∈M满足以下关系： 1)b≤a+cfa·b≤cfa≤c←-b; 2.1类型与自然演绎系统 2)a≤bl cif(a≤b&a≤c); Lc心系统的类型由原子类型P1P2…等构成，所 3)a←-b·(cld)≤a·df(b≤c&c≤b): 有原子类型的集合表示为T。类型的有穷非空矢列 4)(alb)·c→d≤a·df(b≤c&c≤b) 个二元连接词·、一→、一和+。 Lcm系统的可满足性和有效性定义如下： 集合写作T.Lcm演算的矢列形如T卜A,并包含4 定义3Lm系统的代数模型为一序对(M, 该演算系统的自然演绎系统如下所示： u),使得M是1个剩余半群，4为M上的类型赋值. 公理：AFA 如果(A1)·…·(An)≤u(A),则序列A1,…