Beta範式

在 lambda 演算中，一個項是beta 範式（規範型），如果沒有「beta 歸約」是可能的。一個項是 beta-eta 範式，如果既沒有 beta 歸約又沒有「eta 歸約」是可能的。一個項是頭部範式，如果沒有「在頭部位置的 beta-可規約式」。

Beta 歸約

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

$((\mathbf {\lambda } x.A(x))t)$

這裏的 $A(x)$ 是（可能）涉及變量 $x$ 的項。

「在頭部位置的 beta 歸約」是把如下重寫規則應用於一個 beta 可歸約式

$((\mathbf {\lambda } x.A(x))t)\rightarrow A(t)$

這裏的 $A(t)$ 是把項 $A(x)$ 中變量 $x$ 替換為項 $t$ 的結果。

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

• $\lambda x_{0}\ldots \lambda x_{i-1}.(\lambda x_{i}.A(x_{i}))M_{1}M_{2}\ldots M_{n}\rightarrow \lambda x_{0}\ldots \lambda x_{i-1}.A(M_{1})M_{2}\ldots M_{n}$, where $i\geq 0,n\geq 1$.

不是這種形式的任何歸約都是內部 beta 歸約。

歸約策略

一般的說，對於給定項有多個不同的可能的 beta 歸約。正規序歸約是一種求值策略，它始終應用「頭部位置的 beta 歸約」的規則，直到沒有更多的這種歸約是可能的。在這一點上，結果的項是「頭部範式」。

相反的，在應用序歸約中，首先應用內部歸約，而只在沒有更多的內部歸約是可能的時候應用頭部歸約。

正規序歸約是完備的，在如果一個項有頭部範式則正規序歸約總是能最終達到它的意義上。相反的，應用序歸約可能不終止，即使在這個項有規範形式的時候。例如，使用應用序歸約，下列歸約序列是可能的：

$(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))$

$\rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))$

$\rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))$

$\rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))$

$\ldots$

而使用正規序歸約，同樣的起點迅速的歸約到範式：

$(\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))$

$\rightarrow z$

參見

• lambda 演算
• 規範化性質