Lambda 演算和教会数字混淆

发布于 2024-07-25 09:33:58 字数 736 浏览 8 评论 0原文

我正在尝试了解 lambda 演算和丘奇数字的基础知识。我已经进行了大量的阅读和练习，但我似乎一直试图了解某些函数是如何工作的。

我坚持的例子如下。也许有人可以解释我哪里出了问题。

1 的丘奇数可以表示为：

λf. λx. f x

丘奇数 (mⁿ) 的幂函数可以表示为：

λm. λn. n m

我想要做的就是表明，通过将幂函数应用于 1 和 1，我返回 1，因为 1¹ = 1。我这样做是为了更好地理解这些函数是如何工作的。我的工作如下，每次我都会陷入困境：

// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)

我就陷入困境了。我丢失了两个 f，只剩下 x，而且还没有找回 1 个。我哪里出错了？

原文

I'm trying to understand the basics of lambda calculus and Church numerals. I have been doing a lot of reading and practising, but I seem to keep getting stuck with trying to see how some functions work.

The example I am stuck on is as follows. Perhaps someone can explain where I have gone wrong.

The Church numeral for 1 can be represented as:

λf. λx. f x

The exponentiation function on Church numerals (mⁿ) can be given as:

λm. λn. n m

All I want to do is show that by applying the exponentiation function to 1 and 1, I get back 1, since 1¹ = 1. I am doing this, so I understand better how these functions work. My working is as follows and I get stuck every time:

// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)

And there I am stuck. I have lost both f's, left with x's only, and I haven't got 1 back. Where am I going wrong?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

臻嫒无言 2024-08-01 09:33:59

我哪里出错了？

无处！你完成了。请记住，变量名称并不重要；重要的是变量名称。重要的是结构。名称 f 或 x2 没有意义。重要的是如何使用它们。 1 的教堂数字是

λf. λx. f x

，您可以

λx2. (λx1. x2 x1)

将 x2 重命名为 f，将 x1 重命名为 x，瞧！你有

λf. (λx. f x)
= λf. λx. f x

Where am I going wrong?

Nowhere! You're done. Remember, the variable names aren't important; it's the structure that is important. The names f or x2 aren't meaningful. It only matters how they are used. The Church numeral for 1 is