((f f)(g g))在应用阶降阶和正态阶降阶中是如何降阶的？两者以相同的方式减少陈述吗？
假设"减少"；是指"；β还原">
我不会严格介绍形式定义，因为这不是问题所在。之前，我需要澄清一些术语：
beta-contraction(此处写入~>)表示评估的单个步骤
例如(λx.λy.xy)(a)(b) ~> (λy.ay)(b) forall terms a, b- 一个
beta-reduction(这里写=>)意味着一个完整的评估
例如(λx.λy.xy)(a)(b) => ab forall atoms a, b - 如果一个术语不包含redex，则它在
beta-normal form中
例如，λx.x是一个beta-normal form，但(λx.x)y具有beta-normal form(y)，当y有的beta-normal form时。另一个重要的观点是：无论我们采用什么策略来减少A，术语A都有一个唯一的beta-normal form - 如果两个项的
beta-normal forms是alpha-equivalent，则它们是beta-equals(此处写入==)例如(λx.λy.xy)(a)(b) == (λy.ay)(b)
在AOR strategy的情况下，为了减少项A，我们beta-contract是最右边最里面的redex，直到我们得到beta-normal form
更直观：
>> (λx.x)((λy.y)((λz.z)a))~> (λx.x)((λy.y)a)~> (λx.x)a~> a
在NOR strategy的情况下，为了减少项A，我们beta-contract是最左边的redex，直到我们得到beta-normal form更直观：
>> (λx.x)((λy.y)((λz.z)a))~> (λy.y)((λz.z)a)~> (λz.z)a~> a
因此，在您的情况下，使用f f => A、g g => B
AOR：
>> (f f)(g g)~> (f f)B~> AB
NOR：
>> (f f)(g g)~> A(g g)~> AB
这不是很严格，但想法很清楚。当然还有(f f)(g g) == (f f)(g g)