姚從軍，陳寶愛

（湘潭大學(xué)碧泉書院，湖南 湘潭 411105）

1 XYZ的程序語言及其孕育的邏輯動態(tài)化發(fā)展思想

中國科學(xué)院的唐稚松院士是我國著名的邏輯學(xué)家和計算機科學(xué)家。①唐稚松院士科研團隊從20世紀(jì)80年代初開始，歷經(jīng)3個五年計劃的科研攻關(guān)，終于在1995年開發(fā)了世界上獨創(chuàng)的大型軟件工程工具系統(tǒng)XYZ。XYZ系統(tǒng)被稱為系列化語言組，其對應(yīng)的漢語拼音為Xiliehua Yuyan Zu，因此簡稱XYZ。這項創(chuàng)新性成果榮獲1989年國家自然科學(xué)獎一等獎和1996年何梁何利科學(xué)技術(shù)進步獎，它是我國軟件工程領(lǐng)域發(fā)展的一個里程碑，同時也是我國為世界軟件工程領(lǐng)域所做的重要貢獻之一。

唐院士提出了世界上第一個可執(zhí)行時序邏輯語言XYZ/E，該語言在邏輯系統(tǒng)中引入狀態(tài)轉(zhuǎn)換的控制機制，是時序邏輯形式化理論與最新軟件技術(shù)交叉研究的創(chuàng)新案例。XYZ系統(tǒng)由時序邏輯語言XYZ/E及一組基于該語言的CASE工具集組成?！癤YZ系統(tǒng)是將時序邏輯和軟件工程有機結(jié)合而成的整體，時序邏輯語言XYZ/E是XYZ系統(tǒng)的核心，它既是一個時序邏輯系統(tǒng)，又是一種程序語言?！盵1]42

在時序邏輯語言XYZ/E和C語言的賦值語句那里，出現(xiàn)“一表達式一范疇多語義”的情況，這里顯示出動態(tài)邏輯的思想；另一方面，計算機程序C語言的賦值語句直接就是量化動態(tài)邏輯的研究對象，可以對此進行更加精細的刻畫；XYZ/E之后出現(xiàn)的動態(tài)邏輯主要關(guān)注程序語言的動態(tài)特征，然而XYZ/E的基本構(gòu)件，即單元的表述既有動態(tài)的特征也兼具靜態(tài)的性質(zhì)，可以設(shè)想擴大標(biāo)準(zhǔn)動態(tài)邏輯的表達能力，全面刻畫XYZ/E的兼容功能；XYZ/E的子語言XYZ/BE所描述的并發(fā)通訊進程語義的組合性問題是：踏步語句的靜態(tài)組合和非踏步語句的動態(tài)組合，靜態(tài)組合原則已有一般性的概括表述，尚需要給出動態(tài)組合原則的一般邏輯表述；XYZ/E是建立在時序邏輯基礎(chǔ)上的程序語言，時序邏輯的語義是靜態(tài)的，但XYZ/E卻可表現(xiàn)可執(zhí)行命令式編程語言的動態(tài)特征——狀態(tài)轉(zhuǎn)換的控制機制，況且XYZ/E依據(jù)的一階時序邏輯還是一種擴展的多體的時序邏輯，可以設(shè)想更精準(zhǔn)的方案，來確立XYZ/E的邏輯基礎(chǔ)。

2 從XYZ的程序語言看邏輯動態(tài)化發(fā)展的可能性、必要性及路徑

2.1 應(yīng)用CCG分析方式于時序邏輯語言XYZ/E，構(gòu)建動態(tài)CCG

XYZ的基礎(chǔ)和核心是基于時序邏輯的程序語言XYZ/E。計算機程序語言的任務(wù)是刻畫機器狀態(tài)轉(zhuǎn)換的控制機制，而狀態(tài)轉(zhuǎn)換機制則通過賦值語句體現(xiàn)出來，XYZ/E用時序邏輯的語義刻畫賦值語句的動態(tài)特征。

XYZ/E的賦值語句表述，如：求階乘0!,1!,…,k!的和，即s=SUM(i=0,…,k)(i!)。[1]53XYZ/E的表述是：

古希臘辯證法思想家赫拉克利特的名言：

一個人不能兩次踏進同一條河流

XYZ/E的賦值語句：

時序邏輯算子$O的作用使得左邊的j和右邊的j不能賦予同一個數(shù)值(否則將導(dǎo)致矛盾)，但其類型（范疇）卻是一樣的，其類型都是e。被賦予的兩個不同的數(shù)值就是兩個j的不同語義所指（見下圖紅色符號串）。具體分析推演如下：

上例可見，可以創(chuàng)立受限的描述個例的CCG函項應(yīng)用規(guī)則：

對XYZ/E中類似的賦值語句進行研究，可以看出動態(tài)視角的CCG研究的必要性。組合范疇語法CCG的自然語言研究，采納結(jié)合語用語境的經(jīng)驗主義方法，遵循“一詞多范疇多語義”和“多詞一范疇多語義”的原則構(gòu)建CCG處理自然語言的詞庫。CCG的研究角度也適合于計算機程序語言的研究。在時序邏輯語言XYZ/E和C語言的賦值語句那里，出現(xiàn)“一表達式一范疇多語義”的情況，這里顯示出動態(tài)邏輯的思想。因此，可以把CCG分析方式應(yīng)用于時序邏輯語言XYZ/E，嘗試構(gòu)建具有動態(tài)邏輯思想的CCG研究模式，提出基于個案個例的CCG函項組合的新規(guī)則，這是一種新的CCG研究方式，即動態(tài)CCG。

2.2 計算機程序C語言的賦值語句本身是量化動態(tài)邏輯的研究對象

上例看到C語言的賦值語句：

CCG對自然語言的分析，參照語用語境的情況是：一詞多范疇。按照CCG的方式對C語言的賦值語句進行分析，(在沒有時序算子$O的條件下)參照不同語境，左邊的i和右邊的i不能賦予同一個數(shù)值，但其類型（范疇）卻是一樣的，其類型都是e。被賦予的兩個不同的數(shù)值就是兩個i的不同語義所指。

對程序語言賦值語句的分析結(jié)果是：一變項一類型（范疇），但一類型多語義，最終是：一變項多語義。變項的語義隨語境而改變，這也體現(xiàn)出動態(tài)的邏輯思想，如量化動態(tài)邏輯QDL關(guān)于賦值等式的語義定義針對的就是這種情況：

這里“x”是被賦值變項，“t”是賦值詞項，它可以是包含變項而經(jīng)過函子運算而產(chǎn)生的項，例如“x+1”。這里賦值語句的動態(tài)特征通過賦值函項a到b的擴展體現(xiàn)出來，b對“x”的賦值可能不同于a。就上例而言，如a把個體2賦給“x+1”中的“x”，b給“x”賦的值就是個體3。

動態(tài)邏輯是上個世紀(jì)90年代才出現(xiàn)的邏輯新品種，直接受計算機程序語言動態(tài)特征的影響，結(jié)合當(dāng)今上千種程序語言的多樣特征，動態(tài)邏輯可以進一步拓展。

2.3 XYZ/E的單元兼顧動靜，呼喚具有兼容功能的動態(tài)邏輯

在唐院士構(gòu)造的XYZ/E中：基本構(gòu)件(單元)的一般表述兼顧動靜，既體現(xiàn)了程序的動態(tài)語義，還顯示了程序的靜態(tài)語義。XYZ/E的基本構(gòu)件，即單元的一般表述為：

XYZ/E的動態(tài)描述：從Ai到Ai+1機器的狀態(tài)轉(zhuǎn)換 變項的賦值更新

XYZ/E的靜態(tài)描述: 從Bi到Bi+1靜態(tài)的邏輯合取 沒有變項的賦值更新

當(dāng)單元中的nF2，m=0時，單元中時序算子＊限制的諸條件元之間體現(xiàn)的是動態(tài)的程序語義。例證：求階乘0!,1!,…,k!的和，即s=SUM(i=0,…,k)(i!)。用純粹可執(zhí)行語言的風(fēng)格表述，即是：

就變項i而言，從A1到A2、A3和A6，被賦予的值不斷更新變化；就變項j而言，從A1到A3、A4和A5，被賦予的值也不斷更新變化?？傊?，A1---A6的合取表現(xiàn)的是動態(tài)的程序語義。

當(dāng)n=1，mF1時，單元中的WHERE部分各合取支之間體現(xiàn)的是一種靜態(tài)的邏輯語義。

沿用上述，其表述為：

WHERE后是單元的約束部分，由三個條件句的合取構(gòu)成，合取支之間沒有變項的賦值更新，因而是一種靜態(tài)的合取。最后一個條件句是“階乘和”的數(shù)學(xué)歸納定義，根據(jù)定義，可依次獲得：1!=0!×1，2!=1!×2，3!=2! × 3，……。

當(dāng)nF2，mF1時，單元中既有＊限制部分中諸條件元之間體現(xiàn)的動態(tài)思想，也有WHERE部分各合取支之間體現(xiàn)的靜態(tài)思想，即整個單元是動態(tài)和靜態(tài)的融合。其價值有：

用混合的形式來表示中間程度的抽象性。表述為：

其動態(tài)合取和靜態(tài)合取的說明同上。

動態(tài)謂詞邏輯DPL對邏輯連接詞尤其是對合取連接詞的定義如下：[3]

由上可知，否定、析取和蘊涵連接詞的定義都是靜態(tài)的，a=a，不存在從賦值a到賦值a的更新。而合取連接詞的定義卻是動態(tài)的，a并非等同c，從賦值a由于賦值b的關(guān)聯(lián)更新到賦值c，因為合取支φ中的變項賦值可能不同于合取支ψ中的變項賦值，猶如XYZ/E單元中從Ai到Ai+1的賦值更新。量化動態(tài)邏輯QDL中對合取連接詞也有類似的動態(tài)處理。

XYZ/E之后出現(xiàn)的動態(tài)邏輯主要關(guān)注程序語言的動態(tài)特征，比如DPL和QDL等動態(tài)邏輯刻畫的是計算機程序語言的動態(tài)機制，其合取連接詞的語義定義是動態(tài)的，但XYZ/E的單元表述中既有動態(tài)的合取，在其受限部分那里還有靜態(tài)的合取。DPL和QDL等動態(tài)邏輯對蘊涵連接詞的定義是靜態(tài)的，但XYZ/E中的條件元后件中可能出現(xiàn)時序算子，就是說這樣的條件元的語義可能是動態(tài)的。因此，可以考慮擴大標(biāo)準(zhǔn)動態(tài)邏輯的表達能力或構(gòu)建新的動態(tài)邏輯來表述XYZ/E的單元中關(guān)于合取和蘊涵的動靜混合的語義，從而全面刻畫XYZ/E的兼容功能。

2.4 子語言XYZ/BE描述并發(fā)通訊進程語義需要最一般地表述動態(tài)組合原則

XYZ/BE中處理并發(fā)通訊進程時：當(dāng)可同步的進程P1和P2中的同步語句α1和α2有一個是踏步語句時，P1，P2的并發(fā)[P1||P2]中的是靜態(tài)組合的產(chǎn)物；當(dāng)可同步的進程P1和P2中的同步語句α1和α2都不是踏步語句時，P1，P2的并發(fā)[P1||P2]中的是動態(tài)組合的產(chǎn)物。[1]229-230踏步語句是一種等待指令，就是等待某個條件成立，它才會繼續(xù)，不然就在原地等待。關(guān)于踏步語句和同步語句的定義參見唐稚松2002。[1]227-228

例證：用XYZ/BE表示出兩進程：

P1中的紅色條件元和P2中的紅色條件元動態(tài)組合成[P1||P2]中藍色條件元，P1中的藍色條件元和P2中的藍色條件元動態(tài)組合成[P1||P2]中藍色條件元。P1中的其他條件元和P2中的其他條件元保持不變直接延續(xù)到[P1||P2]中去，這些組合是通常的靜態(tài)組合。

靜態(tài)組合的定義：設(shè)有復(fù)合表達式的句法運算F(α1,…, αn)，復(fù)合表達式的語義G(α1′,…, αn′)意味由α1′,…, αn′定義的組合語義。

例證：MG（蒙太格語法）中的量化復(fù)合表達式F(α)=every α，這里對應(yīng)的語義運算G(α′)=λP?x[α′(x)→P(x)]

組合前的表達式α′仍然出現(xiàn)在組合后的表達式中，保持不變。

動態(tài)組合就不一樣了。P1藍色條件元和P2藍色條件元中的動作部分的動態(tài)組合：

這里獲得了[P1||P2]藍色條件元的動作部分中的$O j=k，組合前的$Oc?(j)和c!(k)已不在組合后的表達式中出現(xiàn)，組合改變了原有表達式，這就是動態(tài)的組合。我們需要對這類個案個例的程序并發(fā)組合進行搜集，期望獲得規(guī)律性的動態(tài)組合表述。

總之，XYZ/E的子語言XYZ/BE所描述的并發(fā)通訊進程語義的組合性問題是：踏步語句的靜態(tài)組合和非踏步語句的動態(tài)組合，靜態(tài)組合原則已有一般性的概括表述，怎樣概括動態(tài)組合原則的一般表述？值得研究。

2.5 XYZ/E具有的動態(tài)精神預(yù)示了時序邏輯的動態(tài)化發(fā)展方向

XYZ/E是建立在時序邏輯基礎(chǔ)上的程序語言，時序邏輯的語義是靜態(tài)的，而XYZ/E所關(guān)注的是計算機程序中狀態(tài)轉(zhuǎn)換的控制機制，它可表現(xiàn)可執(zhí)行命令式編程語言的動態(tài)特征——狀態(tài)轉(zhuǎn)換的控制機制，這顯示出動態(tài)的精神，可以設(shè)想更精準(zhǔn)的方案，來確立XYZ/E的邏輯基礎(chǔ)。

XYZ/E定義了10個時序算子，比通常時間邏輯定義的算子要多，多出來的算子必要性在哪里？可以嘗試對XYZ/E依據(jù)的時序邏輯進行改造，使其語義直接顯示動態(tài)的觀念，據(jù)此構(gòu)建的動態(tài)時序邏輯顯得更加精致。況且XYZ/E依據(jù)的一階時序邏輯還是一種擴展的多體的時序邏輯，從邏輯系統(tǒng)的精準(zhǔn)性角度調(diào)整XYZ/E的時序邏輯，是有進一步的研究空間。

3 XYZ的程序語言視域下動態(tài)邏輯的構(gòu)建方法

3.1 理論聯(lián)系實際的方法

從邏輯理論出發(fā)，譬如采用組合范疇語法CCG的范疇邏輯分析方式，去剖析計算機程序語言的特性，分析XYZ/E表現(xiàn)出的狀態(tài)轉(zhuǎn)換的控制機制。具體而言，依據(jù)范疇邏輯原理上建立的CCG，把對自然語言的句法構(gòu)造和語義組合進行處理的套路，搬到計算機程序語言的領(lǐng)域：確定原子表達式和初始算子符號的范疇類型，確定對應(yīng)的語義所指；再依據(jù)通常范疇類型運算的規(guī)則對計算機程序語言的復(fù)合表達式乃至語句進行推演，在推演過程中結(jié)合計算機程序語言的實際特征，尤其要捕捉到XYZ/E非常獨特的表述方式，透過時序算子的作用感受到動態(tài)的思想，這樣反過來對CCG已有的推演規(guī)則進行修正或調(diào)整。進而探討新的CCG理論。

3.2 從實際出發(fā)的經(jīng)驗主義方法和理論概括方法

對計算機程序語言XYZ/E進行詳細和持續(xù)的觀察和學(xué)習(xí)，進而上升到動態(tài)邏輯的理論高度。XYZ/E是上個世紀(jì)末由中國科學(xué)家唐稚松院士獨創(chuàng)的計算機程序語言，唐院士非常關(guān)注該語言中的動態(tài)語義和靜態(tài)語義，為了增強XYZ/E的表達力，接近可執(zhí)行命令式程序語言的表述風(fēng)格，并被廣大計算機編程人員所接受，唐院士提出了XYZ/E的基本構(gòu)件——單元的表述方式，單元能夠兼容動態(tài)的程序語義和靜態(tài)的程序語義。通常邏輯的研究范式往往分而治之，根據(jù)XYZ/E的實際情況，在邏輯領(lǐng)域?qū)討B(tài)語義和靜態(tài)語義進行融合表述，構(gòu)建新的解釋力更強大的動態(tài)靜態(tài)交融的邏輯工具，這是基于XYZ/E這樣的程序語言的實際情況實際特征進行的研究。

3.3 個案個例的實證方法和中等程度的抽象方法

“大數(shù)據(jù)”的精神要求我們在處理問題時盡最大可能搜集相關(guān)數(shù)據(jù)例證。可以采用對有限范圍的個案個例進行考證的方法，如通訊進程的并發(fā)程序具有很多復(fù)雜多樣的例證，涉及的語義組合問題是計算機軟件領(lǐng)域的著名難題，涉及許許多多計算機程序的技術(shù)細節(jié)。企圖從理論層面系統(tǒng)解決這樣的問題談何容易！因此可以降低目標(biāo)，從有限的個例出發(fā)，逐步推進求精，實現(xiàn)中等程度的抽象，對于眾多難題解決一點是一點。

注釋：

①著名學(xué)者唐稚松大學(xué)與研究生就讀于清華大學(xué)哲學(xué)系，師從我國著名邏輯學(xué)家金岳霖先生學(xué)習(xí)邏輯學(xué)，先后進入中國科學(xué)院計算技術(shù)研究所和軟件所工作，從事邏輯學(xué)與計算機科學(xué)的交叉研究，1991年當(dāng)選中國科學(xué)院院士。