劉冬寧, 湯 庸

(1．中山大學(xué)計算機科學(xué)系，廣東 廣州 510275; 2．中山大學(xué)數(shù)學(xué)系，廣東 廣州 510275)

關(guān)于時間的表達、推理與查詢一直是時態(tài)數(shù)據(jù)庫中最為關(guān)鍵的研究點。目前許多的時態(tài)查詢語言已經(jīng)使用于時態(tài)數(shù)據(jù)庫，其理論基礎(chǔ)也相對繁雜，但其中最為直接關(guān)聯(lián)并得到廣泛應(yīng)用的就是基于時態(tài)邏輯的查詢語言[1]。這主要是由于時態(tài)邏輯能充分體現(xiàn)時間的特性。然而，1994年Gabby等論證了時態(tài)邏輯是不可遞歸公理化的，由此它的公理化系統(tǒng)和證明論方法不適于時態(tài)數(shù)據(jù)庫查詢語言的句法分析和語義分析[2]。這使得相關(guān)形式化研究工作存在較大的遺憾，時態(tài)邏輯無法利用公理化系統(tǒng)的良好性質(zhì)及相關(guān)證明論方法對時態(tài)數(shù)據(jù)庫的推理和查詢做更為嚴(yán)謹(jǐn)和細致的刻畫。因此，目前用于時態(tài)數(shù)據(jù)庫查詢語言的時態(tài)邏輯都是非公理化的，無論其適用與否，對于計算性語言這都是一個不足。

時態(tài)邏輯之所以與時態(tài)查詢密切相關(guān)，主要是因為其體現(xiàn)了時間的特性，在句法分析和語義分析方面都對時間的處理給予極大支持。因此，要取代時態(tài)邏輯在時態(tài)查詢語言中的地位，替代者也必須能恰如其分的體現(xiàn)時態(tài)屬性、時態(tài)關(guān)系之間的運算，并最終用于時態(tài)查詢語言的句法分析和語義分析。針對此，我們曾提出：以Lambek演算[3]為核心的范疇語法系統(tǒng)作為句法分析工具，類型演算(λ-演算[4]作為語義分析工具，從而取代時態(tài)邏輯在時態(tài)查詢中的地位。

據(jù)此，我們構(gòu)建了并發(fā)的Lambek演算(LCTQ)及其范疇語法用以作時態(tài)查詢的句法分析，本文將據(jù)LCTQ演算構(gòu)造相應(yīng)的LCTQ標(biāo)號自然演繹系統(tǒng)，從而提供句法演算到語義計算的轉(zhuǎn)換方式，為時態(tài)查詢的語義分析提供相關(guān)接口。

1 LCTQ的自然演繹系統(tǒng)

LCTQ系統(tǒng)系統(tǒng)的類型由原子類型p1、p2…等構(gòu)成，所有原子類型的集合表示為Tp。類型的有窮非空矢列集合寫作Tp+。LCTQ演算的矢列形如ГA，并包含4個二元連接詞·、→、←(和|。

該演算系統(tǒng)的自然演繹系統(tǒng)如下所示：

規(guī)則：

除(|El)、(|Er)、(|I)三條規(guī)則外，其余規(guī)則是經(jīng)典Lambek演算L系統(tǒng)的全部規(guī)則，它們組成原L系統(tǒng)[3]。(|El)、(|Er)、(|I)三條規(guī)則是為新添加的連接符“|”加入的消去和引入規(guī)則。在消去規(guī)則中，(|El)為左消去規(guī)則，(|Er)為右消去規(guī)則。(|I)為引入規(guī)則。

定義1 如果矢列ГA在LCTQ演算中是可推導(dǎo)的，則寫作ГLCTQ→A。

2 LCTQ的句法分析

至此，根據(jù)LCTQ，我們可以時態(tài)查詢語句做相應(yīng)句法分析。舉例如下：

表1 人員工作履歷表

我們希望查詢表1中沒有失業(yè)過的人員名單，該查詢語句如下所示：

Select r1.Name

from works r1, works r2

where r1.Name = r2.Name

and Valid (r1) meets Valid (r2)

在這里Valid (r1)和Valid (r2)表示有效時間，這是基于ATSQL2和TempDB語法習(xí)慣的[5]。

對上例，我們可建立詞匯表(LEX)，如表2所示。

表2 詞匯表

在這里，相關(guān)詞匯類型的設(shè)置是根據(jù)范疇語法對自然語言的處理相應(yīng)轉(zhuǎn)換至半結(jié)構(gòu)SQL語言進行處理的，我們額外添加的類型主要體現(xiàn)在時態(tài)類型、時態(tài)關(guān)系運算以及系統(tǒng)公設(shè)(即System)上。

各部分類型演算步驟分列如下：

1) “System”：系統(tǒng)公設(shè)，類型為n；

2) “Select r1.Name”類型演算為：((n→s)←a)·an→s；

3) “from works r1, works r2 ”類型演算為：((s→s)←f)·((f←f)·(f)·(f→(f←f))·((f←f)· f)s→s ；

4) “where r1.Name = r2.Name”類型演算為：((s→s)←s)·a·(a→(s←a))·as→s；

5) “and Valid (r1) meets Valid (r2)” 類型演算為：((s→s)←s)·(a←t)·(t|(a→(s←a))|t)·(t→a)s→s ；

6) 全句最終類型演算為：n·(n→s)·(s→s)·(s→s)·(s→s)s 。

據(jù)LCTQ演算，上述句型的類型演算最終能推出終止符類型s，使得句法分析演算停止并得到正確結(jié)果。而對于不符合句法的查詢，則不能得到終止符類型s，這是由系統(tǒng)的可靠性和完全性保證的，限于文章篇幅，在此不做介紹。

3 LCTQ標(biāo)號自然演繹系統(tǒng)與語義轉(zhuǎn)換

Lambek演算一個最重要的優(yōu)點，就是可以利用“Curry-Howard”對應(yīng)理論[6-7]，將處理句法分析的演算與應(yīng)用于語義計算(-lambda演算對應(yīng)銜接起來，其對應(yīng)的公理系統(tǒng)為標(biāo)號自然演繹系統(tǒng)。

根據(jù)“Curry-Howard”對應(yīng)理論，我們給出LCTQ演算對應(yīng)的語義演算系統(tǒng)的LCTQ標(biāo)號自然演繹系統(tǒng)如下所示：

公理：

規(guī)則：

特殊地，在這里我們只對時態(tài)屬性和時態(tài)關(guān)系運算做闡述和說明，其余仍和經(jīng)典Lambek演算的標(biāo)號系統(tǒng)一致[4]。

針對r1.Year和r2.Year的類型，我們可用標(biāo)號系統(tǒng)的(←I)規(guī)則和(→I)將其λ抽象為λxM:a←t和λyN:t→a。而before的標(biāo)號系統(tǒng)類型為P: t|(a(→s←a))t，再據(jù)(|El)和(|Er)規(guī)則，r1.Year before r2.Year的句法分析類型為：<λxM, >:a·((a→(s←a))·a)或<<(xM,P>,λyN>:(a·(a→(s←a)))·a(由于·是可結(jié)合的，實際上兩者等價)，從語義上看，這是一個時態(tài)關(guān)系代數(shù)綁定了兩個時間屬性的λ函數(shù)，并由此轉(zhuǎn)入相應(yīng)λ語義計算，將對時間值的處理轉(zhuǎn)入相關(guān)λ抽象處理。

λ語義的抽象處理實際上是函數(shù)化和參數(shù)化的[4]，其與SQL的bag語義處理方式相似程度較高，由此可以作為句法分析和語義分析的良好接口。在國際上(-演算和Lambek演算及線性邏輯的許多交叉研究成果已融入到語義網(wǎng)(Semantic Web)[8]、數(shù)據(jù)流程序[9](Dataflow Programming)和模糊分析信息系統(tǒng)[10]等人工計算語言的語義分析工作上，證明了其是有效的分析方法，值得借鑒。

4 結(jié) 語

在本文中，我們據(jù)Curry-Howard對應(yīng)理論為LCTQ演算構(gòu)造了相應(yīng)的LCTQ標(biāo)號自然演繹系統(tǒng)，從而提供了句法演算到語義計算的轉(zhuǎn)換方式，為時態(tài)查詢語句的語義分析提供相關(guān)接口。在下一步工作中，將主要研究類型演算λ-演算在時態(tài)查詢中的語義演算和推理，并將其作為時態(tài)查詢的語義機理論基礎(chǔ)，建立相應(yīng)的原型系統(tǒng)或直接在TempDB[5]上進行驗證。

參考文獻：

[1] CHOMICKI J, SAAKE G. Logics for databases and information systems: Temporal logic information system [M]. Boston/Dordrecht/London:Kluwer Academic Publishers, 1998.

[2] GABBAY D M, HODKINSON I , REYNOLDS M. Temporal logic: Mathematical foundations and computational aspects [M]. Oxford :Oxford University Press, 1994.

[3] LAMBEK J. The mathematics of sentence structure [J].Amer Math Monthly , 1958,65:154-170.

[4] BARENDEGT H P. The lambda calculus its syntax and semantics [J]. Studies in Logic and The foundations of Mathematics, 2004,103(6).

[5] http://www.cosoft.sysu.edu.cn/TempDB/index.htm, [2008].

[6] CURRY H B. Some logic aspects of grammatical structure [C]// JAKOBSON R. Stucture of language and its mathematical aspects. AMS, Providence, RI.

[7] HOWARD W.The formulae-as-types notion of construction [M].Manuscript, Published in Seldin and Hindley , 1980.

[8] RAO J H, KüNGAS P. Logic-based web services composition from service description to process model [C]//In 2ndIntl. Conference on Web Services,2004.

[9] UUSTALU T, VENE V, The essence of dataflow programming [C]// In 3rd Asian Symp. on Programming Languages and Systems, APLAS’05, Number 3780 in Lect. Notes Comp Sci, 2005.

[10] HAJEK P. Metamathematics of fuzzy logic [C]//Trends in Logic 4. Kluwer, 1998.