提问人：zell 提问时间：3/24/2023 最后编辑：zell 更新时间：3/24/2023 访问量：67
lambda 演算中的编码对
Encoding pair in lambda calculus
问：
我对 lambda 演算如何编码对数据结构背后的逻辑感到困惑。
在 lambda 演算中，PAIR 编码为
对 ：= λx.λy.λf.f x y
.
为什么我不能直接将其编码为
对 ：= λx.λy。x、y、
或
对 ：= λf.λx.λy。f x y
?
进行此类编码时的设计选择是什么？
答：
1赞
flawr
3/24/2023
#1
给定两个参数，该函数应该接受一个新函数并将其应用于“一对”参数。我将尝试给出一个直观的观点，现在让我们看看您的示例是做什么的：x, ypairf
λx.λy. x y
此函数接受两个参数，并将第二个 （） 作为参数传递给第一个 （）。所以这只是函数应用。yx
λf.λx.λy. f x y
从表面上看，这看起来与原版相似，但它有一个问题。在这里，我们得到两个参数将作为第一个参数提供给的函数。这意味着实际上不可能存储这两个参数，这就是为什么原始版本是有意义的版本。x,y
1赞
Orace
3/24/2023
#2
这被称为教会对。
人们应该记住，它们不是一回事。pairPAIR
PAIR构建一对：给定两个参数，返回PAIRpairpair允许检索 Pair 元素
要检索成对元素，您需要能够使用回调函数为其提供信息，这就是您需要的原因。f
表示为接受函数参数的函数。当给定其参数时，它会将参数应用于该对的两个组件。
pair
评论