[科普中國(guó)]-Beta范式

在lambda演算中，一個(gè)項(xiàng)是beta范式（規(guī)范型），如果沒(méi)有“beta歸約”是可能的。一個(gè)項(xiàng)是beta-eta范式，如果既沒(méi)有beta歸約又沒(méi)有“eta 歸約”是可能的。一個(gè)項(xiàng)是頭部范式，如果沒(méi)有“在頭部位置的 beta-可規(guī)約式”。1

Beta 歸約在lambda演算中，beta可歸約式(redex)是如下形式的項(xiàng)

這里的是（可能）涉及變量的項(xiàng)。

“在頭部位置的beta歸約”是把如下重寫(xiě)規(guī)則應(yīng)用于一個(gè)beta可歸約式

這里的是把項(xiàng)中變量替換為項(xiàng)的結(jié)果。

一個(gè)beta歸約在頭部位置，如果它有如下形式：

不是這種形式的任何歸約都是內(nèi)部beta歸約。

歸約策略一般的說(shuō)，對(duì)于給定項(xiàng)有多個(gè)不同的可能的 beta 歸約。正規(guī)序歸約是一種求值策略，它始終應(yīng)用“頭部位置的 beta 歸約”的規(guī)則，直到?jīng)]有更多的這種歸約是可能的。在這一點(diǎn)上，結(jié)果的項(xiàng)是“頭部范式”。

相反的，在應(yīng)用序歸約中，首先應(yīng)用內(nèi)部歸約，而只在沒(méi)有更多的內(nèi)部歸約是可能的時(shí)候應(yīng)用頭部歸約。

正規(guī)序歸約是完備的，在如果一個(gè)項(xiàng)有頭部范式則正規(guī)序歸約總是能最終達(dá)到它的意義上。相反的，應(yīng)用序歸約可能不終止，即使在這個(gè)項(xiàng)有規(guī)范形式的時(shí)候。例如，使用應(yīng)用序歸約，下列歸約序列是可能的：

而使用正規(guī)序歸約，同樣的起點(diǎn)迅速的歸約到范式：

本詞條內(nèi)容貢獻(xiàn)者為:

王沛 - 副教授、副研究員 - 中國(guó)科學(xué)院工程熱物理研究所