lambda-calculus - 带教会数字的 1 后继的缩减步骤

Question

我试图了解在正常订单减少之后执行以下减少的正确步骤。我不明白在这个表达式中我应该执行减少的正确顺序是什么，以及为什么：

(λn.λs.λz.n s (sz)) (λs.λz.s z)

你能帮帮我吗？

注意：这个减少也可以看作是函数的后继

(λn.λs.λz.n s (sz))

应用于教会数字 1

(λs.λz.s z)

知道数字零表示为：

(λs.λz.z)

Answer 1

正常的，AKA 最左边的，减少顺序尝试首先减少最左边的最外面的子项。

由于您正在寻找最外层的术语，因此您需要确定术语的主要构建块，记住每个术语都是变量、术语的抽象或术语的应用：

(λn.λs.λz.n s (s z)) (λs.λz.s z)
---------LHS-------- ----RHS----
----------APPLICATION-----------

主项的左边( LHS) 是最左边的最外边，所以它是归约的起点。它的最外层抽象是λn并且在该术语中有一个绑定变量n，因此它将被右边的术语替换：

λn.λs.λz.n s (s z)
--       -

但是，由于两者都LHS包含RHS和s变量z，因此您需要先在其中一个中重命名它们；我选择重命名RHS：

λs.λz.s z -> λa.λb.a b

现在您可以删除λn抽象并将n变量替换为λa.λb.a b：

λn.λs.λz.n s (s z) -> λs.λz.(λa.λb.a b) s (s z)
--       -                  -----n-----

是时候寻找下一个还原点了：

λs.λz.(λa.λb.a b) s (s z)

由于 lambda 演算是左结合的，这与以下内容相同：

λs.λz.(((λa.λb.a b) s) (s z))

下一个最左边的最外可约项是(λa.λb.a b) s减少为(λb.s b)：

λs.λz.(((λa.λb.a b) s) (s z)) -> λs.λz.((λb.s b) (s z))
         --    -    -                       -

最后一个可约项是(λb.s b) (s z)，其中b替换为(s z)：

λs.λz.((λb.s b) (s z)) -> λs.λz.(s (s z))
        --   -  -----              -----

这导致正常形式的最终状态：

λs.λz.s (s z)