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 演算
• 规范化性质