Lambda微积分和教堂数字混淆 [英] Lambda calculus and church numerals confusion

问题描述

我试图理解lambda微积分和教会数字的基础知识。我一直在做大量的阅读和练习，但我似乎一直在试图看看一些函数是如何工作的。

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.

1的教会数字可以表示为：

The Church numeral for 1 can be represented as:

λf. λx. f x

可以给出Church数字（m ）的指数函数as：

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

λm. λn. n m

我想要做的是显示通过将指数函数应用于1和1，回1，因为1 ¹ = 1。我这样做，所以我更好地理解这些函数是如何工作的。我的工作如下，每次都卡住：

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)

在那里我卡住了。我失去了 f 的剩余部分，只剩下 x 的位置，而我还没有回到1。我在哪里错了？

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?

推荐答案

我要去哪里？

Where am I going wrong?

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

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

λf. λx. f x

并且您有

and you have

λx2. (λx1. x2 x1)

重命名 x2 至 f 和 x1 至 x 和voilà！您有

Rename x2 to f and x1 to x and voilà! You have

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

这篇关于Lambda微积分和教堂数字混淆的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！