如何在 Haskell 的 Lambda 微积分中转换整数列表生成器 [m ...]

How to turn Integer-List Generator [m ...] in Lambda Calculus in Haskell

我给了一个任务,在 lambda 演算中制作整数列表生成器 [m...]。 所以它应该满足这个定义。

Y F m ≡ : m (Y F (+ m 1))

因此需要 lambda 演算 F。 我不知道如何找到应该是哪个 lambda 演算 F。 有没有人对F有什么建议?

等式推理让你到达你需要去的地方。我们有这两个等式:

Y F = F (Y F) -- the basic useful property of Y
Y F m = : m (Y F (+ m 1))

所以现在我们解决。我们将 Y F m = ... 中的 Y F 替换为它等于的东西:

F (Y F) m = : m (Y F (+ m 1))

这个等式的一个解法是从 Y F 泛化到任意变量 g 处处:

F g m = : m (g (+ m 1))

完成。现在这是 F 的一个很好的定义方程。如果你不喜欢语法糖,你可以把它写成 lambda:

F = \g m -> : m (g (+ m 1))

当然,当你自己在其他问题上练习这个时,请善待自己:在每一步重写东西的方式有很多不同的选择,在你之前你可能需要尝试几种不同的方式偶然发现一个可以让你到达你想去的地方,而不是沿着我在这里概述的直线路径走,我已经尝试过并消除了一堆错误的方法。坚持下去,你就能学会。

我想就 [m..]y f m = m : (y f (+ m 1)) 的关系提供一些注释。从观察开始

[m..] = m : [m+1..]

并使用 g m = [m..] 替换 [m..],我们得到

g m = m : (g (m+1))

作为g的定义,观察这是一个递归定义。递归定义可以分为通用递归部分y(由y f = f (y f)给出)和非递归部分f

g = y f

这用非递归 f 替换了递归 g,我们仍然需要 determine/solve。将 g 代入前面的等式中得到

y f m = m : (y f (m+1))

要点是递归函数 (g) 可以重构为非递归函数 (f)。您只需要一个递归函数 (y),您可以将其重复用于其他递归 functions/problems.