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

Beta 歸約

編輯

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

 

這裡的   是(可能)涉及變量   的項。

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

 

這裡的   是把項   中變量   替換為項   的結果。

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

  •  , where  .

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

歸約策略

編輯

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

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

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

 
 
 
 
 

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

 
 

參見

編輯