((f f) (g g)) 在 AOR 和 NOR 中的减少方式不同吗？

如何解决((f f) (g g)) 在 AOR 和 NOR 中的减少方式不同吗？

((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.x is 是 beta-normal form，但是 (λx.x)y has 是 beta-normal form (y) iff y 有一个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)