2

有没有一种明确的方法可以在 lambda 演算中找到术语?例如假设我们有一个pair构造函数

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),

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

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

4

1 回答 1

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

我认为这很清楚。“给定一个选择器程序,一对aand将首先输入它,然后再输入它。” bab等等

我们可以通过简单的句法转换在两种风格之间来回切换,例如:

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

一厢情愿的原则通常很有帮助:我们使用一些函数,就好像它们已经编写好了;那么它们的用途决定了我们必须如何定义它们。就像我们对上面的first_argument_selectorand所做的那样second_argument_selector

好名字有帮助。视觉上对齐代码会有所帮助。此外,使用完整的括号(就像我在帖子顶部所做的那样)。

于 2018-08-29T19:11:53.173 回答