Lambda微积分的β-还原

Question

我有以下蓝氏微积分：

1)λx .katze(X)(加菲尔德)

2)λP .λx .P(X)(茶)

3)λy .λx .喜欢(x，y)(米亚)

我如何减少他们与贝塔削减？

我的解决方案：

1) katze (加菲猫)

2)茶

3)喜欢(Mia)

Answer 1

在执行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函数。因为您只有一个输入，所以只需要减少一个函数--第一个函数，留下另一个函数。你可以想一想，把外皮剥掉，露出内心。

在λ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)