问题标签 [lambda-calculus]

我正在研究The Lambda calculus书的练习题。我被困的一个问题是证明以下几点：表明应用程序不是关联的；事实上，x(yz) 不等于 (xy)z

这是我到目前为止所做的工作：

它是否正确？请帮我理解。

继续Lambda Calculus书中的练习，问题如下：

假设 λ-演算字母表的符号总是 0.5 厘米宽。写下长度小于 20 厘米的 λ 项，其范式长度至少为 (10^10)^10 光年。光速为 c = 3 * (10^10) 厘米/秒。

我完全不知道在这个问题上需要做什么。谁能给我一些指示以帮助理解这个问题以及这里需要做什么？请不要解决或提及最终答案。

希望得到答复。

问候，小黑

对于一个lambda表达式(x (λx y. x y) z h)，我不明白怎么自由变量x (outer x)，z并且h可以在C代码中转换？

问候，小黑

我试图弄清楚如何在这个最终无标签 EDSL 中表达 Y-Combitor：

我不确定，但我认为 Y-Combinator 的默认实现应该可以使用“lam”和“app”。

有人知道怎么做吗？我的第一次尝试失败是因为“无法构造无限类型”的东西。

干杯，Günther

全部，

下面是我发现难以减少的 lambda 表达式，即我无法理解如何解决这个问题。

(λm λn λa λb . m (nab) b) (λ f x. x) (λ f x. fx)

这是我尝试过的，但我被卡住了：

将上述表达式视为： (λm.E) M 等于
E= (λn λa λb. m (nab) b)
M = (λf x. x)(λ f x. fx)

=> (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

将上述表达式视为 (λn. E)M 等于
E = (λa λb. (λ f x. x) (λ f x. fx) (nab) b)
M = ??

..我迷路了！！

谁能帮我理解，对于任何 lambda 演算表达式，执行归约的步骤应该是什么？

我可以理解如何创建和思考 SKI 和 BCKW 微积分，但我永远无法找到实际用途。也许我看的不够深入？也就是说，我想知道（仅举一个例子，我并不是暗示这是真的）Java Servlet 广泛使用 S，而 Python 生成器是 BCW 的一个例子，而我只是无法看穿森林吗？

http://muaddibspace.blogspot.com/2008/01/type-in ​​ference-for-simply-typed-lambda.html 是 Prolog 中简单类型 lambda 演算的简明定义。

看起来不错，但随后他声称将类型分配给 Y 组合器......而在非常真实的意义上，将类型添加到 lambda 演算的全部目的是拒绝为 Y 组合器之类的东西分配类型。

谁能确切地看到他的错误或 - 更有可能 - 我的误解在哪里？

我正在通过 SICP 工作，问题 2.6让我陷入了困境。在处理 Church 数字时，将零和 1 编码为满足某些公理的任意函数的概念似乎是有意义的。此外，使用零的定义和 add-1 函数推导出单个数字的直接公式是有意义的。我不明白如何形成加号运算符。

到目前为止，我有这个。

查看lambda calculus的维基百科条目，我发现 plus 的定义是 PLUS := λmnfx.mf (nfx)。使用该定义，我能够制定以下程序。

我不明白的是，如何仅使用先前派生过程提供的信息直接派生该过程。谁能以某种严格的类似证明的形式回答这个问题？直觉上，我想我明白发生了什么，但正如理查德·费曼曾经说过的，“如果我不能建造它，我就无法理解它……”

我正在用 F# 编写 lambda 演算，但我坚持执行 beta-reduction（用实际参数替换形式参数）。

用法示例：

所以我很想听听一些关于其他人如何解决这个问题的建议。任何想法将不胜感激。

谢谢！

我正在使用 F# 创建 lambda 演算。我目前正试图弄清楚如何实现定点运算符（也称为 Y 组合器）。

我认为其他一切都井然有序。表达式由以下可区分联合表示：

我的eval功能似乎有效。以下示例都产生了预期的结果。
示例 1：
> eval (Fun("x",Plus(Const 7,Var("x"))));;
val it : Expr = Fun ("x",Plus (Const 7,Var "x"))
示例 2：
> eval (App(Fun("x",Plus(Const 7,Var("x"))),Const 3));;
val it : Expr = Const 10
示例 3：
> eval (If(Const 0,Const 3,Const 4));;
val it : Expr = Const 4

但正如我所提到的，我很难在我的 lambda 演算中实现定点运算符。这里定义为：
Y = lambda G. (lambda g. G(g g)) (lambda g. G(g g))

有没有人有什么建议？我查看了有关 Y 组合器的其他问题，但找不到任何我能够成功采用的东西。

感谢所有帮助。

编辑：修正了代码中的错字......以前我有Mult而不是Minus在受歧视的工会中。有趣的是我才注意到这一点！