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

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

(新疆財經大學 信息管理學院，新疆 烏魯木齊 830012)

0 引 言

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

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

1 HyperLMNtal

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

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

init.

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

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

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

從L出發遍歷G；

僅遍歷普通邊并訪問結點，而不遍歷超級邊；

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

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

init.

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

圖1 子圖的復制與刪除

2 λ-演算及其超圖表示

2.1 λ-演算

無類型λ-表達式的語法如下

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

2.2 λ-表達式的超圖表示

用超圖表示λ-表達式既簡單又自然。通過應用以下規則可以寫出任何一個λ-表達式的超圖表達式。

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

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

應用表達式：結點app(T,U,L) 表示tu，其中T和U分別是t和u的超圖表達式，L是普通邊。

新時代背景下，城市化的發展也進入了一個新的階段，新時期對于城市規劃的要求自然也進一步提高。自然環境保護力度加大，人性化的規劃需求的加強以及其他方面的綜合因素，要求必須從我國實際情況出發來對城市進行綜合、科學和可持續的規劃建設。

備注：普通邊僅用于通過表示結點之間的父子關系，以形成λ-表達式的框架，而不用于表示變量。

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

init.

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

圖2 超圖λ-表達式

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

3 歸約策略的建模

3.1 完全歸約

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

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

ground(T,1) | R=Y.

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

subs(S,X,U)).

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

3.2 按名稱調用

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

id(id(λz.id z))

→id(λz.id z)

→λz.idz

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

為了實現這種按一定順序進行的歸約方式，將引入兩個節點。結點eval包裝一個輸入表達式，并開始對該表達式進行歸約。結點value將抽象表達式標記為值，它防止在抽象表達式之內進行歸約。下面的一組重寫規則實現按名稱調用歸約方式

init.

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

其中，第二行中的規則產生一個將丘奇數1應用到丘奇數2的應用表達式，該表達式通過最后三行實現按名稱調用方式進行歸約。如在第六行規則所示，當eval遇到一個應用表達式時首先嘗試歸約其左側。如在第七行規則所示，當eval遇到一個抽象表達式時，將用value將該抽象表達式標記為值，因此不會在抽象表達式內進行歸約。當一個可歸約表達式的左側參數已標記為value時，最后一行的規則觸發β-歸約并產生代換表達式，該代換表達式將由3.1節中實現的代換操作的4條規則來計算。

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

3.3 按值調用

大多數編程語言使用按值調用歸約。與按名稱調用不同，按值調用計算右側已成為值的可歸約表達式，如以下示例所示

id(id(λz.id z))

→id(λz.id z)

→λz.idz

為了歸約第一行中最外面的可歸約表達式，首先應該歸約其右側(下劃線的表達式)。在第二行中可以歸約最外面的可歸約表達式，因為其右側已經歸約為值。簡而言之，按值調用歸約一個可歸約表達式之前，首先需要歸約其左側和右側部分。以下重寫規則實現按值調用

第一條規則將抽象表達式標記為值。第二和第三條規則按從左到右的順序歸約一個可歸約表達式的左側和右側。當一個可歸約表達式的兩側部分都歸約為值時，第四條規則觸發β-歸約并產生代換表達式，其由3.1節中實現的代換操作的4條規則來計算。按這些規則所計算的輸入表達式的構造方法在3.2節中已經給出。

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

以上規則的作用是將自由變量的不可歸約表達式標識為值。例如，第一條規則將一個自由變量標識為值。第二條規則將一個左側為值的應用表達式標識為值，其中左側本來是一個自由變量。第三條規則中將左側已標識為值的應用表達式標識為值，其中左側是一個應用表達式。

3.4 模型分析

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

4 結束語

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