Lambda 演算问题答案

【问题标题】：Lambda calculus problemLambda 演算问题
【发布时间】：2026-01-06 19:20:03
【问题描述】：

我要解决一个 lambda 演算问题。我达到了某个点，但我不知道如何继续：

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> g::a5 (f::a2 x::a3 g::a5)::a6)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a4

a1 = (a3 -> a5 -> a4) -> a3 -> a4
a1 = (a3 -> (a6->a4) -> a4) -> a3 -> a4

有什么方法可以完成吗？我使用“a1,a2,a3...”来表示元素或函数的类型。例如，1::Int、2.4::Float、f::a1、x::a3 等等。不知道够不够清楚...

非常感谢！！

【问题讨论】：

我很确定大多数人不理解您在这里使用的符号。由于他们无法掌握问题所在（以及到目前为止您的解决方案是什么），因此他们无法帮助您。
好的，我稍微解释一下以防万一。我希望，人们可以更好地理解它:)
您使用:: 用于类型注释，\x -> ... 用于 lambda，据我所知，它们的组合是 Haskell 以及与之密切相关的事物所独有的。鉴于此，为什么不直接在 GHCi 中输入 :t \f x -> \g -> g (f x g) 看看它会告诉你什么？
大概是因为整个练习都是在考验他理解和计算类型的能力，显然是值得的。
另一个提醒接受下面的答案。点击绿色勾号。

标签： functional-programming lambda-calculus

【解决方案1】：

你犯了一个错误。 g=a5: a6 -/-> a4.你的括号在第 2 行是错误的。

h f x = \g -> g (f x g)

(h::a1 f::a2 x::a3)::a4 = (\g -> (g::a5 (f::a2 x::a3 g::a5)::a6)::a7)::a4

a1 = a2 -> a3 -> a4
a2 = a3 -> a5 -> a6
a5 = a6 -> a7
a4 = a5 -> a7

a1 = (a3 -> a5 -> a6) -> a3 -> a4
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> a5 -> a7
a1 = (a3 -> (a6->a7) -> a6) -> a3 -> (a6 -> a7) -> a7

因此，这是 h 的正确类型（您可以通过在 SML 提示符中键入 fun h f x = (fn g => g (f x g) ) 并获得完全相同的结果来检查您是否偏执；使用适当语法的 Haskell 也是如此）。 h是一个多态函数，所以所有的a都是任意的，但是表达了h的参数类型和应用h的结果的参数之间的关系等等。

【讨论】：

太棒了！！无论如何，你是如何得到 a4 = a5 -> a7 的？我在任何地方都找不到这种关系。非常感谢！！
定义 h 时，您看到返回的值了吗？这是\g->g(f x g)。这是一个函数，它接受一个参数（我们称他为 g），并返回 g(f x h)。这正是语句所说的：a4 是一个函数，它接受一个类型为 a5 的参数（我们称之为 g 的类型），并返回一个类型为 a7 的函数（我用它标记了 g 的输出；那是你忘记的那个标记）。
顺便说一句，最后剩下的三种类型，a3,a6,a7是唯一剩下的，因为它们是唯一适用于任何东西的函数，所以我们不能说什么更多关于他们的类型。这就是我们知道何时完成的方式。
附言。最好返回并单击以“接受”已回答的问题的答案。减少未回答问题的数量并让回答者满意。
单击大勾号使其变为绿色。 See here