時序邏輯程序語言XYZ/E的創新性

鄒崇理

(1.四川師范大學 邏輯與信息所， 成都 610068; 2.中國社會科學院， 北京 100732)

一、XYZ/E是邏輯和計算機科學的融合創新

邏輯學跟計算機科學有深刻的淵源關系。自從羅素與懷特海共同撰寫了《數學原理》后，人們期望以邏輯為基礎，構建整個數學乃至科學大廈。這種邏輯主義思想使得人們對計算機科學所依據的“能行可計算”的概念進行探索，數理邏輯學家丘奇和哥德爾、計算機科學家圖靈對“能行可計算”概念分別給出不同且等價的定義。丘奇提出Lambda演算，用來刻畫“能行可計算”的概念；哥德爾提出“一般遞歸函數”作為“能行可計算”的定義；圖靈則通過對“圖靈機”這種裝置來描述“能行可計算”的概念。“圖靈機”是現代計算機的理論模型，現代計算機科學的誕生同現代邏輯的思想密切相關。

唐稚松院士是我國著名的邏輯學家和計算機科學家[注]唐稚松(1925—2007)，大學與研究生就讀于清華大學哲學系，師從我國著名邏輯學家金岳霖先生學習邏輯學，后進入中國科學院計算技術研究所工作，從事邏輯學與計算機科學的交叉研究，于1991年當選為中國科學院院士。，他率領中國科學院的科研團隊從20世紀80年代初開始，歷經3個五年計劃的科研攻關，終于在1995年開發出世界上獨創的軟件工程工具系統XYZ(該系統被稱為系列化語言組，其對應的漢語拼音為Xiliehua Yuyan Zu，簡稱XYZ)。這項創新性成果榮獲1989年國家自然科學獎一等獎和1996年何梁何利科學技術進步獎，它是我國軟件工程領域發展的一個里程碑，同時也是我國為世界軟件工程領域做出的重要貢獻之一。“XYZ系統是將時序邏輯和軟件工程有機結合而成的整體，時序邏輯語言XYZ/E是XYZ系統的核心，它既是一個時序邏輯系統，又是一種程序語言。”[1]42作為XYZ軟件工具系統的核心，XYZ/E是基于時序邏輯的程序語言，是計算機程序的邏輯演算，或者說是用時序邏輯表述的計算機程序。邏輯和計算機科學處于“你中有我”或“我中有你”的關系，XYZ/E就是邏輯和計算機科學融合創新的產物。

XYZ/E是邏輯和計算機科學融合創新的著名案例。融合創新猶如生物學的物種嫁接，生物學可以通過已有物種的嫁接產生新物種：A物種+B物種=C物種，C對A和B進行取長補短，C既比A更實用，又比B更高效，這就是創新。為實現這種創新，需要找準嫁接融合的切入點或突破口。邏輯和程序語言的嫁接融合，切入點在哪里？用什么樣的邏輯去跟程序語言融合？邏輯融合程序語言的什么地方？具有深厚邏輯功底和計算機科學知識的唐院士看到，時態邏輯的模型基礎是時間點由先到后延伸的序列，時間算子的性質依靠時間點的先后關系來定義。而主流的可執行程序語言的核心是對計算機狀態轉換關系(更確切說變項的賦值更新)的描述，時間點的先后關系對應機器狀態的轉換關系。采用時態邏輯時間點的先后順序關系去刻畫程序語言的狀態轉換關系，這就是邏輯融合計算機程序語言的切入點。據此切入點，唐院士構建了基于時序邏輯語義的程序語言XYZ/E。

二、XYZ/E對傳統時態邏輯的創新

更具體地講，XYZ/E依據的時序邏輯跟傳統的時態邏輯是有所區別的。XYZ/E的表達力對于揭示程序設計的動態思想來說更加實用接地氣。XYZ/E依據的時序邏輯是對傳統時態邏輯的應用創新，要明確這點，有必要看看唐院士是怎樣采用時態邏輯的形式語義去刻畫程序語言的狀態轉換機制的。

時序邏輯在邏輯學界也叫時態邏輯，起源于20世紀50年代的普萊爾(A.Prior)的有關研究。在哲學那里，時態邏輯作為一種形式化手段，用來解釋關于時間的哲學問題。在自然語言的形式語義研究中，時態邏輯對時間表達式的語義解釋大有用場。時態邏輯歷來受到計算機科學家的關注，在計算機軟件工程中，時態邏輯可以作為對計算機程序的執行進行規約、形式化分析和驗證的工具。最近20多年，時態邏輯對計算機科學的發展產生了重要的影響，圖靈獎作為“計算機界的諾貝爾獎”，已經成為計算機科學領域的最高榮譽。在1996年至2015年期間接近60項獲獎成果中[注]歷年圖靈獎的獲得者及其獲獎成就的介紹可以參考美國計算機協會的圖靈獎網站：http://amturing.acm.org。，有接近20項的成果與邏輯有著直接的關聯，尤其跟時態邏輯的關聯甚為密切。例如，1996年計算機圖靈獎的獲得者阿米爾·伯努利(Amir Pnueli)的成果就是把時態邏輯方法引入到計算機科學研究中。

時態邏輯的顯著特征是：理論系統性強，形式語義清晰。基本的時態算子有：P，F，G和H。P和F稱為弱時態算子，G和H稱為強時態算子(作為P和F的對偶算子可以通過P和F來定義)。Pφ表示“在過去的某個時間φ是真的”，Fφ表示“在將來的某個時間φ是真的”，其嚴格清晰的形式語義定義分別為[2]32：

在唐院士所處的年代，時態邏輯就計算機程序語言刻畫狀態轉換機制的需求來說，其短處是：沒有針對個體詞項的時態算子，或者說程序語言中基于數值個體詞項顯示出的動態更新思想無法采用已有的時態邏輯算子進行刻畫。時態邏輯不能直接明確地刻畫程序語言的狀態轉換控制機制；其次，時態邏輯提供的算子不夠用，而程序設計的實踐需要更多的時態算子。Pφ只能籠統說“φ在過去某個時間真”，而不能具體表明“φ在現在時間t之前的哪個過去時間點真”的情況，等等。

上例C語言的賦值語句有：sum=sum+i和i=i+1。其動態含義非常明確，等號左邊的sum或i不同于等號右邊的sum或i，右邊的sum或i分別加上i或1后動態地變成了左邊的sum或i。程序開始：sum賦值0，i賦值1；接著執行處理框的任務，第一賦值語句中等號左邊的sum賦值0+1，即1；第二賦值語句中等號左邊的i賦值1+1，即2。然后程序進入判斷框，由于此刻i=2, 即 i≤100為真；于是程序返回處理框，循環往復，……，直到i >100，“1+2+3+… +100”的累加得到結果，程序結束。

可執行程序語言的長處是：對體現狀態轉換控制機制的賦值語句的描述顯得簡潔直觀，明確顯示出程序設計中的動態更新思想。其短處則是：沒有清晰的形式語義描述，不利于程序語言的深入研究，如程序語言的模型驗證。

唐院士的做法是：對時態邏輯和計算機程序語言兩個領域進行跨學科研究。他敏銳地看到一方的長處恰是另一方的短處，取長補短，融合各自的優勢。即，用時態邏輯具有精準形式語義的長處去彌補可執行程序語言缺乏清晰形式語義的短處，用可執行程序語言簡潔的狀態轉換機制去激發時態邏輯提出新的時態算子。這樣獲得的時序邏輯程序語言XYZ/E既有時態邏輯那樣精致的語義理論，又能像可執行程序語言那樣簡明直觀地顯示計算機的狀態轉換機制。

唐院士創新的結果是：在XYZ/E中提出兩種時序算子，通常針對公式的時序算子和特別針對詞項的時序算子，如：“若t是項，則$O t也是項”。同時，進一步區分兩種變量及其賦值：通常全局變量的賦值由β擔任，作為局部變量的時序變量的賦值由ηi負責。帶時序算子的時序變量其形式語義定義為：“對于給定的時序模型〈A, α, β, η0, η1, η2, …〉的任一狀態Si，時序邏輯中的項t在Si下有唯一的值，……，其中項$O t在Si下的值Si($O t)定義為項t在狀態Si+1下的值Si+1(t)”[1]220。時序模型任一狀態Si，即〈A, α, β, ηi〉下Si($O t)的值，即ηi($O t)就是ηi+1(t)。在傳統時態邏輯中，只有Pφ，Fφ，Gφ和Hφ之類的表達式，時態算子的運算對象是公式，而程序語言的賦值語句中顯示動態思想的表達式大都是作為數值變量的個體詞項，對此時態算子無法直接運算。于是，經XYZ/E改造過的時序邏輯便提出了新的技術手段，其時序算子“$O”可以直接針對個體詞項進行運算，賦值語句的動態更新思想一目了然。在XYZ/E的程序表述中，出現狀態轉換等式“$O j=j+1”之類的賦值語句，其中時序邏輯算子$O的作用是：等號左邊的$O j指下一個時刻j 的值，等號右邊的j 指當下時刻j的值，這里ηi+1(j)顯然不同于ηi(j)，因為ηi+1(j)=ηi(j)+1，此時的j不同于彼時的j，從ηi到ηi+1是一種轉換的動態關系。XYZ/E用時序邏輯的語義精準地刻畫了賦值語句的動態特征。對可執行程序語言的狀態轉換機制的表述以及對計算機程序設計來說，XYZ/E的時序邏輯非常接地氣，這是對傳統時態邏輯在計算機科學應用領域的一種創新。

此外，XYZ/E相比傳統的時態邏輯來說，基于程序設計實踐的需求，除“$O”外，還提出了更多的時序算子：“將來時時序算子，如：下一時刻算子(即一目算子‘下一時刻’，表示成‘$O’)，必然算子(即一目算子‘從所指時刻起以后所有時刻’，表示成‘[ ]’，或通常的‘□’)，終于算子(即一目算子‘從所指時刻起某一時刻’，表示成‘〈 〉’，或通常的‘◇’)，直到算子(即二目算子‘左式真直到右式真’，表示成‘$U’)，除非算子(即二目算子‘左式真除非右式真’，表示成‘$W’)。……過去時時序算子，如：上一時刻算子(即一目算子‘上一時刻’，表示成‘(· )’或通常的‘$⊙’)……自從算子(即二目算子‘自從右式真以來左式真’，并假定右式必曾經為真，表示成‘$S’)，回溯算子(即二目算子‘左式真可一直回溯到右式真之后’，表示成‘$B’)，故回溯算子是自從算子去掉右式必曾經為真的假設而成。”[1]44-45唐院士進一步指出：“為了提高表達力，還可擴充一組所謂狹義時序算子，◇,□,,,$U,$W,$S,$B均有其相應的狹義算子，它們分別是◇′,□′,′,′,$U′,$W′,$S′,$B′，……”[1]47這些時序算子的深入討論這里從略。

三、XYZ/E對通常動態邏輯的創新

對計算機程序的動態轉換機制進行專門刻畫的邏輯稱為量化動態邏輯(Quantificational Dynamic Logic, 簡稱QDL)。就程序語言動態思想的表述而言，XYZ/E的解讀比QDL顯得簡明直觀，便于掌握。對于計算機程序設計的實踐來說，XYZ/E關于狀態轉換控制機制的表述顯得更為實用，XYZ/E是動態邏輯關于計算機程序語言應用的一種創新。

φ∷≡R(t1,…,tn)|t1=t2|⊥|(|φ1→φ2|[π]φ

就前文所示C語言的算法例子而言，輸入輸出框中的兩個賦值等式之間是靜態的合取關系：sum=0且i=1。按照QDL，先執行“sum=0”后執行“i=1”，一個賦值函項能夠勝任對兩個變量的分別賦值，對第一合取支中的sum用這個賦值函項賦值0，對第二合取支中的i用這個函項賦值1。這里不是對同一個變量進行兩次不同賦值的情況，因此談不上由這個賦值函項更新為另一個賦值函項。而處理框中的兩個賦值等式之間則是明顯的動態合取關系：sum=sum+i且i=i+1。按照QDL，先執行sum=sum+i后執行i=i+1，針對第一合取支，等號左邊的sum和等號右邊的sum，賦值函項必須更新，設賦值函項a和b，a對等號右邊的sum賦一個值，這個值加上1后成為更新a后獲得的另一賦值函項b對等號左邊的sum的賦值。然后針對第二合取支，需要從賦值函項b更新到另一賦值函項c的操作(過程類似第一合取支)。盡管QDL對程序序列的語義解讀具有普適性，能夠適用于程序語言賦值語句的動態合取，也可以解讀程序語言賦值語句的靜態合取(這里賦值函項的情況是a=b=c)，但是從簡明直觀的角度看，QDL對程序序列的動態特征和靜態特征的區分是不夠明顯的。

XYZ/E是建立在時序邏輯基礎上的程序語言，與QDL相比，XYZ/E更貼近程序語言的實際情況。唐院士多次強調，計算機科學本質上是一種技術科學，一旦面臨理論訴求和技術實用的選擇時，XYZ/E必定傾向技術的實用性。為使XYZ/E更方便服務于廣大程序設計人員，讓他們更容易理解程序賦值語句的動態思想，XYZ/E對QDL的改進有：

其次，XYZ/E從特定的角度對程序的動態特征和靜態特征給予區分。考慮到理解的直觀簡明，XYZ/E通過程序基本構件的外部特征來顯示程序的動態特征和靜態特征，使得二者的區別顯而易見。照唐院士看來，程序的動態特征通過程序構件中包含時序變量不同時刻賦值的條件元的演進推移體現出來，而程序的靜態特征則指程序構件中條件元的依次合取而沒有發生時序變量在不同時刻的賦值。在其構造的XYZ/E中，對基本構件(單元)的表述進行了精巧構思，在程序的外貌上區分程序的動態特征和靜態特征。XYZ/E的基本構件單元的表述為：□[A1, …, An] WHERE B1∧, …,∧Bm。

當基本構件單元中的n≥2，m=0時，單元中時序算子□限制的諸條件元A1, …, An之間體現了一種動態的演進過程。譬如：求階乘0!,1!,…, k!的和，即s=SUM(i=0, …, k)(i!)。XYZ/E的一種表述是：

□ [LB=START_sf∧k≥0 ? $Oi=0∧$Or=0∧$Oj=0∧$OLB=11；

A1

LB=11∧i=k+1 ? $Os=r∧$OLB=STOP；

A2

LB=11∧i≠k+1 ? $Of=1∧$Oj=1∧$OLB=l2；

A3

LB=l2∧j=i+1 ? $OLB=l3；

A4

LB=l2∧j≠i+1 ? $Of=f*j∧$Oj=j+l∧$OLB=12；

A5

LB=l3 ? $Or=r+f∧$Oi=i+l∧$OLB=11]

A6

從A1到A2，…，到A6，顯示出計算機的狀態轉換，每一Ai中都含有時序算子“$O”對時序變量的運算。尤其條件元A5中的“$O j=j+1”，條件元A6中的“$O r=r+f”和“$O i=i+l”均表現出同一時序變量在不同時刻下賦值的情況，這是XYZ/E對程序動態演進特征一種幾乎直白的表述。

當基本構件單元中的n=1，m≥1時，單元中的WHERE部分，其中各條件元B1,…,Bm之間體現的是一種靜態的邏輯合取。因為合取支之間只有單純的毗連，并沒有出現同一時序變量在不同時刻下賦值的情況。對上述例證XYZ/E的另一種表述是：

□[LB=START_sf∧k≥0 ? ◇(s=SUM(i=0,…,k)(i!)∧LB=STOP)]

A1

WHERE(sumfact(s,k) ? s=SUM(i=0,…,k)(i!)∧

B1

(sumfact(1,0)∧(fact(h,m)∧s=r+h∧sumfact(r,m-1) ? sumfact(s,m)))∧

B2

(fact(1,0)∧fact(g,n-1)∧f=g*n ? fact(f,n))

B3

B1—B3皆是有關數學概念的定義。就B3而言，這是一個數學歸納定義，其通俗解讀為：歸納基始：0!=1；歸納：若n-1!=g則n!=g×n。于是有：1!=0!×1，2!=1!×2，3!=2!×3…。這里程序的外部特征是：B1—B3的內部沒有出現時序算子“$O”，皆不涉及時序變量的動態賦值，因而從B1到B2到B3皆是靜態合取，表現了程序的靜態特征。

總之，對計算機編程人員來說，從程序表述的外部特征去領會和掌握其動態思想，XYZ/E顯得簡明直觀，而量化動態邏輯QDL的方式則顯得艱深難懂。對涉及大量人員使用的科學技術來說，把復雜的表述簡單化，這也是一種進步和創新。

四、結語

時序邏輯程序語言XYZ/E是新世紀前的產物，其時序邏輯和計算機程序語言的融合創新，能夠給今天的人們帶來新的啟示和思考：往小處說，我們有必要吸取唐院士的成果，按照當今計算機程序語言的實際需求，探索揭示程序動態更新思想的更為直觀簡明的方式，譬如基于語言邏輯和計算機程序領域的跨學科思考，采用組合范疇語法CCG的方式去分析和表述賦值語句的動態特征；往大處講，我們要發揚唐院士的治學精神，強調交叉融合的跨學科思考。唐院士能夠在計算機軟件領域把西方的邏輯和數學理論同計算機程序語言的動態特征融合起來，這種融合的做法源于他對博大精深的中國古代哲學思想如孔子的中庸哲學和佛教的認識論哲學等具有深刻的領悟。金岳霖先生認為中國哲學非常簡潔，富有暗示性，包容獨創思想。唐院士秉承師訓，在計算機科學領域通過融合創新的方式做出巨大成就。計算機圖靈獎獲得者伯努利(Pnueli)等人評價道：“唐稚松教授使時序邏輯概念超越了任何人的想像，他將之應用于各方面，在以前無人認為是可能的。”[5]日本軟件工程學會主席岸田孝一先生也給予高度贊揚：唐院士的成就是東方文明對于新的21世紀計算機技術發展的一大貢獻。