Beta範式

在 lambda 演算中，若一個項不能β-歸約，則稱為beta 範式（beta 規範型）；如果既不能β-歸約，又不能η-歸約，則稱為 beta-eta 範式。如果不能在頭部β-歸約，則稱為頭部範式。

Beta 歸約

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

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

這裡的 ${\displaystyle A(x)}$ 是（可能）涉及變量 ${\displaystyle x}$ 的項。

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

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

這裡的 ${\displaystyle A(t)}$ 是把項 ${\displaystyle A(x)}$ 中變量 ${\displaystyle x}$ 替換為項 ${\displaystyle t}$ 的結果。

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

• ${\displaystyle \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 ${\displaystyle i\geq 0,n\geq 1}$.

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

歸約策略

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

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

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

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

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

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

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

${\displaystyle \ldots }$

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

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

${\displaystyle \rightarrow z}$

參見

• lambda 演算
• 規範化性質