在 lambda 演算中,一個項是beta 範式(規範型),如果沒有「beta 歸約」是可能的。一個項是 beta-eta 範式,如果既沒有 beta 歸約又沒有「eta 歸約」是可能的。一個項是頭部範式,如果沒有「在頭部位置的 beta-可規約式」。
Beta 歸約
在 lambda 演算中,beta 可歸約式(redex)是如下形式的項
![{\displaystyle ((\mathbf {\lambda } x.A(x))t)}](//wikimedia.org/api/rest_v1/media/math/render/svg/39e996b4c4f78582d0a3f4dcf83bb805abb4960a)
這裡的
是(可能)涉及變量
的項。
「在頭部位置的 beta 歸約」是把如下重寫規則應用於一個 beta 可歸約式
![{\displaystyle ((\mathbf {\lambda } x.A(x))t)\rightarrow A(t)}](//wikimedia.org/api/rest_v1/media/math/render/svg/ba30b6b8f120c89d3d7507af510604e2dc6cb10e)
這裡的
是把項
中變量
替換為項
的結果。
一個 beta 歸約在頭部位置,如果它有如下形式:
, where
.
不是這種形式的任何歸約都是內部 beta 歸約。
歸約策略
一般的說,對於給定項有多個不同的可能的 beta 歸約。正規序歸約是一種求值策略,它始終應用「頭部位置的 beta 歸約」的規則,直到沒有更多的這種歸約是可能的。在這一點上,結果的項是「頭部範式」。
相反的,在應用序歸約中,首先應用內部歸約,而只在沒有更多的內部歸約是可能的時候應用頭部歸約。
正規序歸約是完備的,在如果一個項有頭部範式則正規序歸約總是能最終達到它的意義上。相反的,應用序歸約可能不終止,即使在這個項有規範形式的時候。例如,使用應用序歸約,下列歸約序列是可能的:
![{\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}](//wikimedia.org/api/rest_v1/media/math/render/svg/afdb10500a9dc5a7711b04f3f5f3886d5116321d)
![{\displaystyle \rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))}](//wikimedia.org/api/rest_v1/media/math/render/svg/1f2446d58cf1f7c5802419a6288561293358e6bf)
![{\displaystyle \rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))}](//wikimedia.org/api/rest_v1/media/math/render/svg/dcea266b8c16fdd8a655673ce2621d15fdb99335)
![{\displaystyle \rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))}](//wikimedia.org/api/rest_v1/media/math/render/svg/559104d02faaa172e69daefa9b51633aeda4d078)
![{\displaystyle \ldots }](//wikimedia.org/api/rest_v1/media/math/render/svg/3b8619532e44ee1ccae3ab03405a6885260d09ed)
而使用正規序歸約,同樣的起點迅速的歸約到範式:
![{\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}](//wikimedia.org/api/rest_v1/media/math/render/svg/afdb10500a9dc5a7711b04f3f5f3886d5116321d)
![{\displaystyle \rightarrow z}](//wikimedia.org/api/rest_v1/media/math/render/svg/a1be1c090869a35daa32611cef6af9bdd73fdc53)
參見