1958年,Joachim Lambek提出了Lambek演算,进一步推动了逻辑学、语苦学、计算机科学等学界的纵深和交叉发展。然而存语法分析方面,Lambek演算与范畴语法的结合仍存在不足,就传统的Lambek演算而言,由于其过于刚性,因此所能处理的语法问题还有限。本文重点论述了传统Lambek演算不能处理的时态句型问题,并基于此设计了模态Lambek演算系统(Lambek Calculus with Temporal Modality,LTM系统)。LTM系统在相应关系框架上是可靠的和完全的,同时在证明论方面也具有良好的性质,其不仅具有切割消除性,还具有判定性。鉴于Lambek演算与Montague内涵语义理论的对应衔接,使得语法和语义的衔接采用了同样的文法(Lambek演算),这为计算机界研发自然语言的编译工具提供了有力支撑。由此,我们希望所设计出相应的LTM演算系统,也终将能推动计算机编译系统对时态问题进行处理。
In 1958, Joachim Lambek presented the so-called Lambek Calculus, which had since then promoted the research in logic, linguistics and computer science and their interaction. But in the field of syntactic parse, classical Lambek Calculus has some insufficiency, such as it fails to deal with more syntactic problems. In this paper, we mainly discuss temporal syntactics that classical Lambek Calculus cannot deal with. Based on it, we design a logic system that can parse temporal sentences. According to its characteristics, we name it Lambek Calculus with Temporal Modality (LTM System). LTM System is sound and complete with respect to Kripke frame, and is cut-free and decidable. Based on the connection between Lambek Calculus and Montague Grammar, this work can help researches in computer compliers of natural language. We hope that our work in this paper and the LTM System can promote computer compliers to deal with temporalities of sentence in the future.