在 lambda 演算中,一个项是beta 范式(规范型),如果没有“beta 归约”是可能的。一个项是 beta-eta 范式,如果既没有 beta 归约又没有“eta 归约”是可能的。一个项是头部范式,如果没有“在头部位置的 beta-可规约式”。
Beta 归约
在 lambda 演算中,beta 可归约式(redex)是如下形式的项
![{\displaystyle ((\mathbf {\lambda } x.A(x))t)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39e996b4c4f78582d0a3f4dcf83bb805abb4960a)
这里的
是(可能)涉及变量
的项。
“在头部位置的 beta 归约”是把如下重写规则应用于一个 beta 可归约式
![{\displaystyle ((\mathbf {\lambda } x.A(x))t)\rightarrow A(t)}](https://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))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/afdb10500a9dc5a7711b04f3f5f3886d5116321d)
![{\displaystyle \rightarrow (\lambda x.z)((\lambda w.www)(\lambda w.www)(\lambda w.www))}](https://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))}](https://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))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/559104d02faaa172e69daefa9b51633aeda4d078)
![{\displaystyle \ldots }](https://wikimedia.org/api/rest_v1/media/math/render/svg/3b8619532e44ee1ccae3ab03405a6885260d09ed)
而使用正规序归约,同样的起点迅速的归约到范式:
![{\displaystyle (\mathbf {\lambda } x.z)((\lambda w.www)(\lambda w.www))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/afdb10500a9dc5a7711b04f3f5f3886d5116321d)
![{\displaystyle \rightarrow z}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1be1c090869a35daa32611cef6af9bdd73fdc53)
参见