lambda-calculus - 正常顺序的步骤比应用顺序少的示例？

Question

我似乎想不出这样的例子，想知道是否有这样的例子？我知道如果我有一个表达式，其中应用顺序不会终止，那么正常顺序可能仍会终止。我想知道是否有两个订单都终止但正常订单的步骤更少的示例。

Answer 1

(λ p. λ q. q) ((λ x. λ y. λ z. ((x y) z)) (λ w. λ v. w))

有一些空格:

(λ p. 
   λ q.
     q
)
(
  (λ x.
     λ y.
       λ z.
         ((x y) z)
   )
   (λ w.
      λ v.
        w
   )
)

按正常顺序，最外层的归约可以先进行，一步直接归约到恒等组合子。应用顺序也会到达那里，但它需要更长的时间，因为需要首先评估 x-y-z-w-v 表达式。

请注意，x-y-z-w-v 表达式甚至未被使用。您可以将正常顺序视为一种惰性求值:表达式仅在使用时才求值或归约。因此，您只需构建一个不使用其中一个参数的公式，您就会立即获得这种效率取胜的示例。