λ-演算歸約策略的簡易建模

阿力木江·亞森，阿布都克力木·阿布力孜，朱義鑫，哈里旦木·阿布都克里木

(新疆財經(jīng)大學(xué) 信息管理學(xué)院，新疆 烏魯木齊 830012)

0 引 言

編程語言理論中的計(jì)算過程主要包括函數(shù)定義、函數(shù)調(diào)用以及函數(shù)調(diào)用的歸約。幾十年來，研究人員一直在研究如何定義函數(shù)以及對其調(diào)用。以提高效率為目標(biāo)的計(jì)算技術(shù)可用于開發(fā)函數(shù)式編程語言或邏輯編程語言，具有簡單推理特點(diǎn)的計(jì)算技術(shù)可用于建模原型語言。已有的基于圖形的計(jì)算技術(shù)不適用于對形式系統(tǒng)進(jìn)行推理證明。無類型λ-演算被認(rèn)為是最小的編程語言，因此以無類型λ-演算為例回顧基于圖形的計(jì)算技術(shù)。

本文以經(jīng)典λ-演算為例實(shí)現(xiàn)函數(shù)式編程語言和邏輯編程語言中常用的歸約策略的建模。其中λ-表達(dá)式以超圖表示，超圖由結(jié)點(diǎn)、普通邊和超級邊組成的超圖。使用超圖表示λ-表達(dá)式的想法提出在文獻(xiàn)[12]中，但其在HyperLMNtal里并沒有實(shí)現(xiàn)相關(guān)開發(fā)。文獻(xiàn)[13]的圖形類型在HyperLMNtal里實(shí)現(xiàn)。用超圖表示的λ-表達(dá)式極為相似于理論上的λ-表達(dá)式。該技術(shù)使用超圖重寫的建模語言HyperLMNtal，其中的重寫規(guī)則能夠通過圖形類型處理任意大小的子圖。

1 HyperLMNtal

HyperLMNtal是基于超圖重寫的建模語言。程序中的超圖按以下語法表達(dá)

其中，0是空的超圖，p(X1,…,Xm) 是一個名稱為p并且具有m個邊的結(jié)點(diǎn)，P,P是超圖的并行組成。Xi可以是最多能連接兩個結(jié)點(diǎn)的普通邊，也可以是連結(jié)任意數(shù)量的結(jié)點(diǎn)的超級邊。在程序中，結(jié)點(diǎn)名以小寫字母開頭，邊名以大寫字母開頭。一個超級邊被創(chuàng)建時，一個自然數(shù)可以作為屬性提供給它。特殊結(jié)點(diǎn)“=”稱為連機(jī)結(jié)點(diǎn)，用于連接兩條邊。例如，X=Y連接X的一個端點(diǎn)和Y的一個端點(diǎn)：如果X是普通邊而Y是超級邊，則X將成為超級邊Y的一部分。為了方便地編寫程序，該語言提供一種術(shù)語表示法，它允許將q(…,Y,…)，p(…,Y) 寫為q(…,p(…),…)， 其中Y必須是普通邊。對于兩條普通邊X和Y而言，X=Y，p(…,Y) 相當(dāng)于p(…,X)， 也可以寫為X=p(…)。 利用該術(shù)語表達(dá)法可編寫具有良好可讀性的程序。

init.

第一行中給出的結(jié)點(diǎn)init將被第二行中的重寫規(guī)則轉(zhuǎn)換為由3個結(jié)點(diǎn)a,b,c以及一條屬性為1的超級邊K組成的一個超圖。一條邊在規(guī)則左側(cè)和右側(cè)出現(xiàn)的數(shù)目可能表示該條邊代表的子圖正在被刪除或復(fù)制，如下所述。

邊L在第一條規(guī)則中被復(fù)制，因?yàn)長在該規(guī)則的左側(cè)出現(xiàn)一次，而在右側(cè)出現(xiàn)兩次。顯然，邊L在第二條規(guī)則中被刪除。不過這些規(guī)則沒指出邊L代表什么，因此這些規(guī)則是無法運(yùn)行。需要在規(guī)則中使用圖形類型來說明被復(fù)制或刪除的每一條邊代表什么。圖形類型檢查給定參數(shù)是否具有該圖形類型所預(yù)期的屬性。例如，hlink(L,1)檢查L是否為具有屬性1的超級邊，int(K)檢查K是否連接到包含一個整數(shù)的結(jié)點(diǎn)。除了檢查單個圖形元素之外，有些圖形類型，如ground可用于定義子圖。

圖形類型ground(L,a1,…,an) 表示通過下面的方法從超圖G中獲得的子圖P={N,E,H}：

從L出發(fā)遍歷G；

僅遍歷普通邊并訪問結(jié)點(diǎn)，而不遍歷超級邊；

從而獲得已被遍歷的普通邊集合E，已被訪問的結(jié)點(diǎn)集合N，以及所有端點(diǎn)都在N中并且屬性在 {a1,…,an} 中的超級邊集合H。

一條超級邊K∈H稱為P的局部超級邊，只有部分端點(diǎn)在P中出現(xiàn)的超級邊稱為P的全局超級邊。簡而言之，一個ground是一個由一組普通邊、一組結(jié)點(diǎn)和一組完全包含在這些普通邊和結(jié)點(diǎn)之內(nèi)并且具有指定屬性的超級邊組成的子圖。在重寫規(guī)則中使用ground可以復(fù)制或刪除子圖，如下所示

init.

第一行給出結(jié)點(diǎn)init。第二行中的規(guī)則將init重寫為r(abs(X,app(X,Y)))，其中r,abs和app是由屬性為1和2的超級邊X和Y以及一些普通邊連接的結(jié)點(diǎn)，如圖1(a)所示。根據(jù)術(shù)語表示法，普通邊在程序中隱式的，例如r和abs之間是普通邊，還有abs和app之間的也是普通邊。在圖中直線表示普通邊，帶曲線的黑點(diǎn)表示超級邊，箭頭指向結(jié)點(diǎn)的第一條邊表示結(jié)點(diǎn)中邊的順序。當(dāng)在第三行的規(guī)則應(yīng)用于圖1(a)中的超圖時，ground(L,1)先找到一個子圖(圖1(a)中的虛線區(qū)域)，然后將該子圖復(fù)制到兩個位置，從而獲得圖1(b)所示的超圖。當(dāng)?shù)谒男械囊?guī)則應(yīng)用于圖1(a)中的超圖時ground(L,1)子圖將被刪除，結(jié)果為圖1(c)。復(fù)制ground子圖時，其局部超級邊將被復(fù)制到新的超級邊中，并且全局超級邊將在復(fù)制后的子圖之間共享，例如圖1(b)所示圖1(a)中的X1被復(fù)制到F1和K1，而Y2被共享。刪除ground子圖時，其局部超級邊將被完全刪除，并且全局超級邊中連結(jié)到子圖的部分被刪除，如圖1(c)所示。復(fù)制或者刪除ground子圖時，其中的普通邊將被復(fù)制到新的普通邊中或被完全刪除。

圖1 子圖的復(fù)制與刪除

2 λ-演算及其超圖表示

2.1 λ-演算

無類型λ-表達(dá)式的語法如下

其中x是變量，λx.t是抽象表達(dá)式，tu表示將t應(yīng)用于u的應(yīng)用表達(dá)式。在λx.t中，λx是綁定機(jī)制，并稱t為λx的轄域，x稱為綁定變量，一個未收到綁定并出現(xiàn)在t中的變量稱為自由變量。例如，λx.xy中x是一個綁定變量，y是一個自由變量。綁定變量的名稱并不重要，λx.x和λy.y是等價的，稱為α-等價性。形式為(λx.t)u的表達(dá)式稱為可歸約表達(dá)式，通過以下的β-歸約法進(jìn)行歸約

2.2 λ-表達(dá)式的超圖表示

用超圖表示λ-表達(dá)式既簡單又自然。通過應(yīng)用以下規(guī)則可以寫出任何一個λ-表達(dá)式的超圖表達(dá)式。

變量：屬性為1的超級邊表示綁定變量，屬性為2的超級邊表示自由變量。

抽象表達(dá)式：結(jié)點(diǎn)abs(X,T,L) 表示λx.t，其中X是表示綁定變量的超級邊，T是t的超圖表達(dá)式，L是普通邊。

應(yīng)用表達(dá)式：結(jié)點(diǎn)app(T,U,L) 表示tu，其中T和U分別是t和u的超圖表達(dá)式，L是普通邊。

新時代背景下，城市化的發(fā)展也進(jìn)入了一個新的階段，新時期對于城市規(guī)劃的要求自然也進(jìn)一步提高。自然環(huán)境保護(hù)力度加大，人性化的規(guī)劃需求的加強(qiáng)以及其他方面的綜合因素，要求必須從我國實(shí)際情況出發(fā)來對城市進(jìn)行綜合、科學(xué)和可持續(xù)的規(guī)劃建設(shè)。

備注：普通邊僅用于通過表示結(jié)點(diǎn)之間的父子關(guān)系，以形成λ-表達(dá)式的框架，而不用于表示變量。

λ-表達(dá)式的這種超圖表示稱為超圖λ-表達(dá)式。以下程序說明如何使用超圖λ-表達(dá)式

init.

第二行生成λx.xx的超圖λ-表達(dá)式，第三行生成λx.x的超圖λ-表達(dá)式。第四行生成一個將第二行生成的超圖λ-表達(dá)式應(yīng)用到第三行生成的超圖λ-表達(dá)式上所得到的超圖λ-表達(dá)式。在程序的最后三行中生成的超圖λ-表達(dá)式分別在圖2(a)～2(c)所示。

圖2 超圖λ-表達(dá)式

在圖形中只要兩個不同的名稱標(biāo)記兩個不同的邊即可，邊的名稱并不重要。邊的這種特性與λ-表達(dá)式中的綁定變量的特性完全相同：一個綁定變量可以有任何名稱，只要該名稱不與其它變量名稱發(fā)生沖突即可。根據(jù)在2.1節(jié)中的λ-表達(dá)式的語法，可能會有一些令人困惑的λ-表達(dá)式如λx.λx.x。在λx.λx.x中，兩個綁定變量x不是相同的變量，該表達(dá)式實(shí)際上相當(dāng)于λy.λx.x。對于這種不同綁定變量具有相同名稱的λ-表達(dá)式應(yīng)轉(zhuǎn)換為不同綁定變量具有不同名稱的等價λ-表達(dá)式，然后將其轉(zhuǎn)換為對應(yīng)的超圖λ-表達(dá)式。此條件也適用于基于圖形的其它技術(shù)。

3 歸約策略的建模

3.1 完全歸約

本節(jié)介紹超圖λ-表達(dá)式完全歸約的超圖重寫規(guī)則實(shí)現(xiàn)。完全規(guī)約在任何時間對任何位置的可歸約表達(dá)式都可以進(jìn)行歸約，該過程一直進(jìn)行到?jīng)]有余下的可歸約表達(dá)式為止。例如，令id=λx.x， 則λ-表達(dá)式id(id(λz.idz)) 有3個可歸約表達(dá)式，它們按任何順序計(jì)算都有相同的結(jié)果λz.z，其不包含任何可歸約表達(dá)式。

表1 避免變量捕獲的代換操作定義

ground(T,1) | R=Y.

|R=app(subs(T,X,U),

subs(S,X,U)).

這些規(guī)則實(shí)現(xiàn)超圖λ-表達(dá)式的完全歸約，由于以下原因其計(jì)算過程中絕不發(fā)生變量捕獲并輸出正確的計(jì)算結(jié)果。第一，第一條規(guī)則將自動應(yīng)用于輸入表達(dá)式中的任意一個可歸約表達(dá)式，不存在可歸約表達(dá)式時停止，這正是完全歸約。第二，第五條規(guī)則將一個超圖λ-表達(dá)式復(fù)制到它的兩個等價并且不同的副本中，從而使所有表示綁定變量的超級邊在計(jì)算過程中保持不同。在此過程中，表示自由變量的超級邊在副本之間共享，這正是λ-演算中自由變量從不更名的情況。第三， ground(L,1) 是一個子圖，它由普通邊、結(jié)點(diǎn)和局部超級邊組成，其中普通邊和結(jié)點(diǎn)組成基本框架。不難發(fā)現(xiàn)，ground子圖的結(jié)構(gòu)特性與超圖λ-表達(dá)式的結(jié)構(gòu)特性完全相同。這意味著，在第三條規(guī)則中通過ground刪除的超圖λ-表達(dá)式T正是對應(yīng)于表1中的第二條規(guī)則中被刪除的λ-表達(dá)式t。類似地，在第五條規(guī)則中通過ground復(fù)制的超圖λ-表達(dá)式U正是對應(yīng)于在表1中的第四條規(guī)則中被復(fù)制的λ-表達(dá)式u。

3.2 按名稱調(diào)用

在完全歸約中不存在計(jì)算策略，隨時可以歸約任何一個可歸約表達(dá)式。完全歸約的時間效率低，因此實(shí)際編程語言采用其它的歸約方式，例如按名稱調(diào)用歸約方式。下面的示例說明如何根據(jù)按名稱調(diào)用進(jìn)行歸約

id(id(λz.id z))

→id(λz.id z)

→λz.idz

按名稱調(diào)用總是試圖歸約最左最外面的可歸約表達(dá)式(歸約下劃線的表達(dá)式)，并且不允許在抽象表達(dá)式內(nèi)部進(jìn)行歸約。例如，在上面第三行不計(jì)算λz的轄域里面的可歸約表達(dá)式，最終結(jié)果為λz.idz。

為了實(shí)現(xiàn)這種按一定順序進(jìn)行的歸約方式，將引入兩個節(jié)點(diǎn)。結(jié)點(diǎn)eval包裝一個輸入表達(dá)式，并開始對該表達(dá)式進(jìn)行歸約。結(jié)點(diǎn)value將抽象表達(dá)式標(biāo)記為值，它防止在抽象表達(dá)式之內(nèi)進(jìn)行歸約。下面的一組重寫規(guī)則實(shí)現(xiàn)按名稱調(diào)用歸約方式

init.

|R=abs(X, abs(Y, app(X,app(X,Y)))).

其中，第二行中的規(guī)則產(chǎn)生一個將丘奇數(shù)1應(yīng)用到丘奇數(shù)2的應(yīng)用表達(dá)式，該表達(dá)式通過最后三行實(shí)現(xiàn)按名稱調(diào)用方式進(jìn)行歸約。如在第六行規(guī)則所示，當(dāng)eval遇到一個應(yīng)用表達(dá)式時首先嘗試歸約其左側(cè)。如在第七行規(guī)則所示，當(dāng)eval遇到一個抽象表達(dá)式時，將用value將該抽象表達(dá)式標(biāo)記為值，因此不會在抽象表達(dá)式內(nèi)進(jìn)行歸約。當(dāng)一個可歸約表達(dá)式的左側(cè)參數(shù)已標(biāo)記為value時，最后一行的規(guī)則觸發(fā)β-歸約并產(chǎn)生代換表達(dá)式，該代換表達(dá)式將由3.1節(jié)中實(shí)現(xiàn)的代換操作的4條規(guī)則來計(jì)算。

在3.1節(jié)中的完全歸約的重寫規(guī)則中只要存在可歸約表達(dá)式就將觸發(fā)β-歸約，沒有特定的歸約順序。只要存在可歸約表達(dá)式，HyperLMNtal自動調(diào)用β-歸約法的重寫規(guī)則。在按名稱調(diào)用的歸約方式中，3個規(guī)則利用eval和value遍歷一個表達(dá)式并根據(jù)按名稱調(diào)用的原理控制歸約順序。

3.3 按值調(diào)用

大多數(shù)編程語言使用按值調(diào)用歸約。與按名稱調(diào)用不同，按值調(diào)用計(jì)算右側(cè)已成為值的可歸約表達(dá)式，如以下示例所示

id(id(λz.id z))

→id(λz.id z)

→λz.idz

為了歸約第一行中最外面的可歸約表達(dá)式，首先應(yīng)該歸約其右側(cè)(下劃線的表達(dá)式)。在第二行中可以歸約最外面的可歸約表達(dá)式，因?yàn)槠溆覀?cè)已經(jīng)歸約為值。簡而言之，按值調(diào)用歸約一個可歸約表達(dá)式之前，首先需要?dú)w約其左側(cè)和右側(cè)部分。以下重寫規(guī)則實(shí)現(xiàn)按值調(diào)用

第一條規(guī)則將抽象表達(dá)式標(biāo)記為值。第二和第三條規(guī)則按從左到右的順序歸約一個可歸約表達(dá)式的左側(cè)和右側(cè)。當(dāng)一個可歸約表達(dá)式的兩側(cè)部分都?xì)w約為值時，第四條規(guī)則觸發(fā)β-歸約并產(chǎn)生代換表達(dá)式，其由3.1節(jié)中實(shí)現(xiàn)的代換操作的4條規(guī)則來計(jì)算。按這些規(guī)則所計(jì)算的輸入表達(dá)式的構(gòu)造方法在3.2節(jié)中已經(jīng)給出。

上述介紹的按名稱調(diào)用和按值調(diào)用的重寫規(guī)則不能計(jì)算包含自由變量的表達(dá)式。通過在按名稱調(diào)用和按值調(diào)用的重寫規(guī)則中添加以下處理自由變量的重寫規(guī)則，使它們能夠計(jì)算包含自由變量的表達(dá)式

以上規(guī)則的作用是將自由變量的不可歸約表達(dá)式標(biāo)識為值。例如，第一條規(guī)則將一個自由變量標(biāo)識為值。第二條規(guī)則將一個左側(cè)為值的應(yīng)用表達(dá)式標(biāo)識為值，其中左側(cè)本來是一個自由變量。第三條規(guī)則中將左側(cè)已標(biāo)識為值的應(yīng)用表達(dá)式標(biāo)識為值，其中左側(cè)是一個應(yīng)用表達(dá)式。

3.4 模型分析

本文所提出的技術(shù)與其它基于圖形的技術(shù)不同之處在于以下幾點(diǎn)。第一，已有的基于圖形的技術(shù)使用普通邊和某些輔助結(jié)點(diǎn)來表示變量。在本文所給出的技術(shù)中，超級邊能夠表示任何變量，并不需要額外的結(jié)點(diǎn)來表示出現(xiàn)次數(shù)多于2的變量。第二，大多數(shù)基于圖形的技術(shù)都是用Interaction Nets，其中重寫規(guī)則每一次只能更改幾個基本圖形元素，不能處理任意大小的子圖。本文所給出的技術(shù)中，重寫規(guī)則使用圖形類型可以重寫任意大小的超圖λ-表達(dá)式，因此各種歸約策略的重寫規(guī)則實(shí)現(xiàn)簡單而緊湊，幾乎與理論完全一致。第三，在大多數(shù)基于圖形的技術(shù)中，對λ-表達(dá)式歸約策略建模時需要一組專門的重寫規(guī)則來實(shí)現(xiàn)資源管理。本文所給出的技術(shù)不需要在計(jì)算過程中專門清理不再需要的表達(dá)式的重寫規(guī)則，不再需要的表達(dá)式在實(shí)現(xiàn)代換操作的重寫規(guī)則中由ground立即刪除即可。第四，文獻(xiàn)[14]提出使用輔助結(jié)點(diǎn)來遍歷圖并限制歸約順序的方法，并將該方法用在普通圖形重寫中。本文提出的技術(shù)將使用輔助結(jié)點(diǎn)來遍歷圖的思路引入到超圖重寫中。

4 結(jié)束語

本文介紹了一種基于超圖重寫的實(shí)現(xiàn)各種歸約策略的技術(shù)。在該技術(shù)中，超圖λ-表達(dá)式在形式上相似于理論中的λ-表達(dá)式并且具有良好的可讀性。歸約策略用超圖重寫規(guī)則實(shí)現(xiàn)，其中使用的圖形類型ground執(zhí)行顯式α-轉(zhuǎn)換。完全歸約、按名稱調(diào)用和按值調(diào)用的重寫規(guī)則易于理解，并且對計(jì)算過程的描述完全對應(yīng)于理論上的描述。該技術(shù)中，限制歸約順序的方法被融入到超圖重寫中，因此能夠直觀地實(shí)現(xiàn)各種歸約策略。如在引言中指出，大多數(shù)基于圖形的技術(shù)是為了高效計(jì)算。本研究沒有優(yōu)先考慮計(jì)算效率，而認(rèn)為與理論相似程度的高低和是否能獲得直觀的計(jì)算模型才是優(yōu)先考慮。該技術(shù)可用于快速建模和演示。例如，如果在實(shí)際開發(fā)某一個形式系統(tǒng)之前想要測試或者演示它，那么該技術(shù)可用于建立它的可執(zhí)行模型。另外，由于使用該技術(shù)時理論和實(shí)踐幾乎保持一致，因此，這種建模過程將是比較簡單的。將來的研究方向是進(jìn)一步提高該技術(shù)的計(jì)算效率，以期能應(yīng)用到更復(fù)雜的大型形式系統(tǒng)中。