uncurry and curry functions [closed]

Question

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.

Closed 9 years ago.

I´m quite new to lambda-calculus and I´m trying to do the following exercise, but I´m not able to resolve it.

uncurry(curry E) = E

Could anyone help me?

Answer 1

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