【发布时间】：2020-01-21 11:52:44
【问题描述】：
我有以下 lambda 演算：
1) λx 。 katze(x)(加菲猫)
2) λP 。 λx 。 P(x)(茶)
3) λy 。 λx 。喜欢（x，y）（米娅）
如何使用 Beta Reduction 来减少它们？
我的解决方案：
1) 卡兹（加菲猫）
2) 茶
3) 喜欢（米娅）
【问题讨论】：
标签： math lambda lambda-calculus
【发布时间】：2020-01-21 11:52:44
【问题描述】：
执行 beta 缩减时，您可以将绑定变量替换为 lambda 函数，并使用提供的值。其表示法是[param := value]，您选择给出的第一个变量。
在这种情况下
λx . katze(x)(Garfield) -> katze (Garfield) 减少是正确的。我们已将x 变量替换为Garfield，并在此过程中删除了λx，只保留了表达式。以下是将要采取的步骤：
λx . katze(x)(Garfield)
= katze(x)[x := Garfield]
= katze(Garfield)
但是，另外两个是不正确的。你忘记了你有一个 lambda 函数，其中的表达式是另一个 lambda 函数。由于您有一个 single 输入，因此您只需减少 one 功能 - 第一个，留下另一个。可以想成是剥掉外面的，露出里面的。
在λP . λx . P(x)(tea) 的情况下，这可以更好地表示为(λP . (λx . P(x)))(tea)，现在每个 lambda 函数都用括号括起来。由于我们提供单个输入 tea，因此我们仅使用参数 P 解析外部函数（为了清楚起见，保留括号）：
(λP . (λx . P(x)))(tea)
= (λx . P(x))[P := tea]
= (λx . P(x))
= λx . tea(x)
或者不带括号：
λP . λx . P(x)(tea)
= λx . P(x)[P := tea]
= λx . tea(x)
至于最后一个函数，当只给出一个输入时，它仍然存在删除两个函数的相同问题。正确的归约步骤是：
λy . λx . likes(x, y)(Mia)
= λx . likes(x, y)[y := Mia]
= λx . likes(x, Mia)
【讨论】：
-
谢谢。现在我可以为自己执行 Beta-Reduction。