lambda-calculus - Beta 约简 Lambda 演算示例

Question

(λw. w) (λu. λv. u) (λu. λv. v) (λu. λv. u)

谁能给我这个例子的逐步Beta缩减？我真的很困惑

标签： lambda-calculus

Answer 1

(λw. w) (λu. λv. u) (λu. λv. v) (λu. λv. u)

将 (λw. w) 应用于 (λu. λv. u)。由于这是身份功能，因此没有任何变化。

(λu. λv. u) (λu. λv. v) (λu. λv. u)

将 (λu. λv. u) 应用于 (λu. λv. v)。它在表达式中替换了 u。由于我们现在可能对第一个表达式中的多个 v 感到困惑，我们可以将内部表达式中的 v 重命名为另一个变量 x。

(λv. (λu. λx. x)) (λu. λv. u)

将 (λv. (λu. λx. x)) 应用于 (λu. λv. u)。由于 v 没有出现在 lambda 的主体中，因此该参数被有效地丢弃。

(λu. λx. x)

我们现在可以（可选地）再次 alpha 重命名以恢复原始变量名称。

(λu. λv. v)