Beta範式
在 lambda 演算中,一個項是beta 範式(規範型),如果沒有「beta 歸約」是可能的。一個項是 beta-eta 範式,如果既沒有 beta 歸約又沒有「eta 歸約」是可能的。一個項是頭部範式,如果沒有「在頭部位置的 beta-可規約式」。
Beta 歸約
在 lambda 演算中,beta 可歸約式(redex)是如下形式的項
這裡的 是(可能)涉及變量 的項。
「在頭部位置的 beta 歸約」是把如下重寫規則應用於一個 beta 可歸約式
這裡的 是把項 中變量 替換為項 的結果。
一個 beta 歸約在頭部位置,如果它有如下形式:
- , where .
不是這種形式的任何歸約都是內部 beta 歸約。
歸約策略
一般的說,對於給定項有多個不同的可能的 beta 歸約。正規序歸約是一種求值策略,它始終應用「頭部位置的 beta 歸約」的規則,直到沒有更多的這種歸約是可能的。在這一點上,結果的項是「頭部範式」。
相反的,在應用序歸約中,首先應用內部歸約,而只在沒有更多的內部歸約是可能的時候應用頭部歸約。
正規序歸約是完備的,在如果一個項有頭部範式則正規序歸約總是能最終達到它的意義上。相反的,應用序歸約可能不終止,即使在這個項有規範形式的時候。例如,使用應用序歸約,下列歸約序列是可能的:
而使用正規序歸約,同樣的起點迅速的歸約到範式: