Β范式

在λ演算中，若一个项不能β归约，则称为β范式（β规范型）；如果既不能β归约，又不能η归约，则称为β-η范式。如果不能在头部β归约，则称为头部范式。

β归约
在λ演算中，β可归约式(redex)是如下形式的项

: ((\mathbf{\lambda} x . A(x)) t)

这里的A(x)是（可能）涉及变量x的项。

“在头部位置的β归约”是把如下重写规则应用于一个β可归约式

: ((\mathbf{\lambda} x . A(x)) t) \rightarrow A(t)

这里的A(t)是把项A(x)中变量x替换为项t的结果。

一个β归约在头部位置，如果它有如下形式：

• \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 i \geq 0, n \geq 1 .

不是这种形式的任何归约都是内部β归约。

归约策略
一般的说，对于给定项有多个不同的可能的β归约。正规序归约是一种求值策略，它始终应用“头部位置的β归约”的规则，直到没有更多的这种归约是可能的。在这一点上，结果的项是“头部范式”。

相反的，在应用序归约中，首先应用内部归约，而只在没有更多的内部归约是可能的时候应用头部归约。

正规序归约是完备的，在如果一个项有头部范式则正规序归约总是能最终达到它的意义上。相反的，应用序归约可能不终止，即使在这个项有规范形式的时候。例如，使用应用序归约，下列归约序列是可能的：

: (\mathbf{\lambda} x . z) ((\lambda w. w w w) (\lambda w. w w w))
: \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))
: \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))
: \rightarrow (\lambda x . z) ((\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w) (\lambda w. w w w))
:\ldots

而使用正规序归约，同样的起点迅速的归约到范式：

: (\mathbf{\lambda} x . z) ((\lambda w. w w w) (\lambda w. w w w))
: \rightarrow z

参见

• λ演算
• 规范化性质