问题描述
((f f) (g g)) 在应用级减少和正常级减少中是如何减少的？两者都以相同的方式减少语句吗？
解决方法
假设“reduce”的意思是“Beta-Reduce”。
我不会严格地介绍形式定义，因为这不是问题。
之前，我需要澄清一些术语：
- A
beta-contraction（在此处写入~>）表示评估的单个步骤。
例如(λx.λy.xy)(a)(b) ~> (λy.ay)(b) forall terms a,b - A
beta-reduction（此处写=>）表示完整评估。
例如(λx.λy.xy)(a)(b) => ab forall atoms a,b - 一个词在
beta-normal form中，如果它不包含 redexes。
例如λx.xis 是beta-normal form，但是(λx.x)yhas 是beta-normal form(y) iffy有一个beta-normal form。 另一个重点：无论我们采用哪种策略来减少 A，术语A都有一个独特的beta-normal form。 - 如果它们的
beta-equals是==，则两个术语是beta-normal forms（在此处写alpha-equivalent） 例如(λ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)