uncurry和咖喱的功能

Question

我对lambda微积分相当陌生，我正在尝试做下面的练习，但我无法解决它。

uncurry(curry E) = E

任何人都可以帮助我吗？

Answer 1

假设以下definions（您需要检查那些符合你定义）

// 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 

通过将以上的定义为咖喱和在uncurry

uncurry(curry E) 

这导致

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

然后就减少术语以上使用λ-caluclus的缩减规则，即使用：

• α转换：改变约束变量
• β - 还原：在应用功能，他们的论据

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