正确定义lambda-calculus构造函数的方法

Question

有没有明确的方法来找到lambda演算中的术语？例如，假设我们有一对构造函数

pair = λa. λb. λf. f a b

我们有fst构造函数

fst = λp. p (λa. λb. a)

返回该对的第一个元素，我们现在要定义snd构造函数，它返回该对的第二个项目。我已经到了这样来定义它

snd = λp. p (λa. λb. b)与snd (pair a b) = b。

snd也可以定义为

snd = λp. p (λb. λa. b)，

问题是，有没有明确的方法来定义新的构造函数？

当我必须定义构造函数时，人们应该如何思考，当我被要求定义新构造函数时，如何测试我的答案是否正确。

Answer 1

(λa. (λb. b)) x y = (λb. b) y = y

但

(λb. (λa. b)) x y = (λa. x) y = x

，所以不，两者不等价：第一个定义返回第二个参数，但第二个定义返回第一个参数。

除了与参数建立对应关系外，名称不计算在内。争论的立场很重要。

至于如何思考它，我经常发现以组合方式编写定义更容易遵循：

pair a b selector = selector a b

fst apair = apair first_argument_selector

snd apair = apair second_argument_selector

first_argument_selector  a b = a

second_argument_selector a b = b

我认为这很清楚。 “一对a和b，根据选择程序，首先喂它a，然后喂b。”等等

我们可以通过简单的句法转换在两种样式之间来回转换，例如：

second_argument_selector     a     b = b       =>
second_argument_selector     a = (λb . b)      =>
second_argument_selector = (λa . (λb . b))

一厢情愿的原则通常非常有用：我们使用一些功能就像它们已经写好;然后他们的用途决定了我们如何定义它们。就像我们在上面用first_argument_selector和second_argument_selector做的那样。

好名字有帮助。在视觉上对齐代码有帮助。另外，使用完整的括号（就像我在帖子顶部所做的那样）。