currying - uncurry 和 curry 函数

Question

我对 lambda-calculus 很陌生，我正在尝试做以下练习，但我无法解决它。

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 的归约规则来归约上述项，即使用：

• α-转换：改变绑定变量
• β-reduction：将函数应用于其参数

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