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