assuming the following definions (you need to check if those match you definitions)
// 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)
you show
uncurry(curry E) = E
by inserting the definitions above into curry and uncurry in
uncurry(curry E)
which leads to
(λf.λp . f (first p) (second p)) ( (λf.λx.λy . f (pair x y)) E)
Then you reduce the term above using the reduction rules of the lambda-caluclus, namely using:
- α-conversion: changing bound variables
- β-reduction: applying functions to their arguments
http://en.wikipedia.org/wiki/Lambda_calculus http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf
which should lead to
E
if you write down each reduction step, you have proven that
uncurry(curry E) = E
here a sketch how it should look like:
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