uncurry和curry函数

Question

我是λ演算的新手，我正在尝试做下面的练习，但我不能解决它。

uncurry(curry E) = E

有人能帮帮我吗？

Answer 1

假设以下定义(您需要检查这些定义是否与您的定义匹配)

// creates a pair of two values
pair    := λx.λy.λf. fxy
// selects the first element of the pair     
first   := λp. p(λx.λy. x)
// selects the second element of the pair                     
second  := λp. p(λx.λy. y)
// currys f
curry   := λf.λx.λy . f (pair x y)
// uncurrys f
uncurry := λf.λp . f (first p) (second p)

你展示

uncurry(curry E) = E

通过将上面的定义插入到curry和uncurry中

uncurry(curry E)

这导致了

(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (pair x y)) E)

然后使用lambda-caluclus的缩减规则减少上面的项，即使用：

• conversion-conversion:更改绑定变量并将函数应用于其参数

http://en.wikipedia.org/wiki/Lambda_calculus http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf

这应该会导致

E

如果你写下每一个减少步骤，你已经证明了

uncurry(curry E) = E

下面是它应该是什么样子的草图：

uncurry(curry E) = // by curry-, uncurry-definion
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (pair x y)) E) = // by pair-definiton
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λx.λy.λf. fxy x y)) E) = // 2 alpha-conversions
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λa.λb.λf. fab x y)) E) = // 2 beta-reductions
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (λf. fxy)) E) = // ...

...
...
... = // β-reduction
E