lambda 演算如何与以下表达式一起使用：(Ly.Lt.yt)zx？答案

【问题标题】：How lambda calculus works with an expression like: (Ly.Lt.yt)zx?lambda 演算如何与以下表达式一起使用：(Ly.Lt.yt)zx？
【发布时间】：2014-06-15 15:55:04
【问题描述】：

我不明白如何解决这个 lambda 演算表达式：

(Lx.yx)((Ly.Lt.yt)zx)

我不明白zx 是如何传递和评估的。它是否传递给 Ly 或 Lt ？你能帮帮我吗？

编辑：这就是我试图解决它的方法：

(Lx.yx)((Ly.Lt.yt)zx)我首先将zx视为2个参数，并将Ly应用于z：

->(Lx.yx)((Lt.zt)x) 然后我将 Lt 应用于 x，我得到：

->(Lx.yx)(zx) 现在我将 Lx 应用于 (zx)：

->(y(zx))

应该是对的，但我不太明白这种情况下的 rools 是什么：((Ly.Lt.yt)zx)。申请什么，何时申请以及如何申请。你能帮帮我吗？

【问题讨论】：

我检查了您的解决方案。没错。
谢谢。我想问你（Ly.Lt.yt）代表什么？是不是像 Lt(Ly(x)) ??
扩展为(Ly.(Lt.yt))。

标签： lambda-calculus

【解决方案1】：

您总是对最左边的 Beta 减少进行 Beta 减少，而您正在做正确的事情。应用时，将整个 lambda 项替换为函数体，但函数变量的所有出现都必须替换为参数。

例子：

(Lx.Ly.x)(La.Lb.ab)(La.Lb.ba)
[^left most redex^]
(Ly.(La.Lb.ab))(La.Lb.ba)
[^^^^left most redex^^^^]
(Ly.(La.Lb.ab))

(no more beta redexes, done evaluating)

【讨论】：

【解决方案2】：

规则是：

Lx.Ly.M 表示(Lx.(Ly.M))。
MNP 表示((MN)P)。

所以((Ly.Lt.yt)zx) 是(((Ly.(Lt.yt))z)x)。因此，这里第一个可用的 redex 是(Ly.(Lt.yt))z，并且您的所有步骤都是正确的。干得好！

【讨论】：