λ-演算歸約策略的簡(jiǎn)易建模

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

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

0 引 言

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

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

1 HyperLMNtal

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

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

init.

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

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

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

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

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

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

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

init.

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

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

2 λ-演算及其超圖表示

2.1 λ-演算

無(wú)類(lèi)型λ-表達(dá)式的語(yǔ)法如下

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

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

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

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

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

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

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

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

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

init.

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

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

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

3 歸約策略的建模

3.1 完全歸約

本節(jié)介紹超圖λ-表達(dá)式完全歸約的超圖重寫(xiě)規(guī)則實(shí)現(xiàn)。完全規(guī)約在任何時(shí)間對(duì)任何位置的可歸約表達(dá)式都可以進(jìn)行歸約，該過(guò)程一直進(jìn)行到?jīng)]有余下的可歸約表達(dá)式為止。例如，令id=λx.x， 則λ-表達(dá)式id(id(λz.idz)) 有3個(gè)可歸約表達(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ì)算過(guò)程中絕不發(fā)生變量捕獲并輸出正確的計(jì)算結(jié)果。第一，第一條規(guī)則將自動(dòng)應(yīng)用于輸入表達(dá)式中的任意一個(gè)可歸約表達(dá)式，不存在可歸約表達(dá)式時(shí)停止，這正是完全歸約。第二，第五條規(guī)則將一個(gè)超圖λ-表達(dá)式復(fù)制到它的兩個(gè)等價(jià)并且不同的副本中，從而使所有表示綁定變量的超級(jí)邊在計(jì)算過(guò)程中保持不同。在此過(guò)程中，表示自由變量的超級(jí)邊在副本之間共享，這正是λ-演算中自由變量從不更名的情況。第三， ground(L,1) 是一個(gè)子圖，它由普通邊、結(jié)點(diǎn)和局部超級(jí)邊組成，其中普通邊和結(jié)點(diǎn)組成基本框架。不難發(fā)現(xiàn)，ground子圖的結(jié)構(gòu)特性與超圖λ-表達(dá)式的結(jié)構(gòu)特性完全相同。這意味著，在第三條規(guī)則中通過(guò)ground刪除的超圖λ-表達(dá)式T正是對(duì)應(yīng)于表1中的第二條規(guī)則中被刪除的λ-表達(dá)式t。類(lèi)似地，在第五條規(guī)則中通過(guò)ground復(fù)制的超圖λ-表達(dá)式U正是對(duì)應(yīng)于在表1中的第四條規(guī)則中被復(fù)制的λ-表達(dá)式u。

3.2 按名稱(chēng)調(diào)用

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

id(id(λz.id z))

→id(λz.id z)

→λz.idz

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

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

init.

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

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

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

3.3 按值調(diào)用

大多數(shù)編程語(yǔ)言使用按值調(diào)用歸約。與按名稱(chēng)調(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)歸約為值。簡(jiǎn)而言之，按值調(diào)用歸約一個(gè)可歸約表達(dá)式之前，首先需要?dú)w約其左側(cè)和右側(cè)部分。以下重寫(xiě)規(guī)則實(shí)現(xiàn)按值調(diào)用

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

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

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

3.4 模型分析

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

4 結(jié)束語(yǔ)

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