Proving curried and uncurried functions

32 Views Asked by At

We are given

$$ \underline{add} \ \underline{m} \ \underline{n} = \underline{m+n} $$ $$ \underline{mult} \ \underline{m} \ \underline{n} = \underline{m \times n} $$

and

$$ \underline{sum} \ (\underline{m}, \underline{n}) = \underline{m+n} $$ $$ \underline{prod} \ (\underline{m}, \underline{n}) = \underline{m \times n} $$

where $\underline{sum}$ is said to be an uncurried version of $\underline{add}$ and similarly $\underline{prod}$ is an uncurried version of $\underline{mult}$ such that

$$ \underline{sum} = \underline{uncurry} \ \underline{add} $$ $$ \underline{prod} = \underline{uncurry} \ \underline{mult} $$

where

$$ \underline{curry} = \lambda fx_1 x_2. f (x_1, x_2) $$ $$ \underline{uncurry} = \lambda fp. f (\underline{fst} \ p) (\underline{snd} \ p) $$

The question

The question starts by giving properties that

$$ \underline{curry} (\underline{uncurry} \ E) = E $$ $$ \underline{uncurry} (\underline{curry} \ E) = E $$

And I am to use this to show that:

$$ \underline{add} = \underline{curry} \ \underline{sum} $$ $$ \underline{mult} = \underline{curry} \ \underline{prod} $$

My answer

(i) It would be sufficient to show that $(\underline{curry} \ \underline{sum})\underline{m} \ \underline{n} = \underline{m+n}$.

But $\underline{add} = \underline{curry} (\underline{uncurry} \ \underline{add}) = \underline{curry} \ \underline{sum}$.

So we need to show that $(\underline{curry} (\underline{uncurry} \ \underline{add})) \underline{m} \ \underline{n} = \underline{m+n}$.

Let's go!

$((\lambda f x_1 x_2. f (x_1, x_2)) ( (\lambda fp. f (\underline{fst} \ p)(\underline{snd} \ p)) \ \underline{add} )) \underline{m} \ \underline{n} = ((\lambda fx_1 x_2. f(x_1, x_2)) (\lambda p. \underline{add} (\underline{fst} \ p)(\underline{snd} \ p)) \underline{m} \ \underline{n} = (\lambda x_1 x_2. (\lambda p. \underline{add} (\underline{fst} \ p)(\underline{snd} \ p))(x_1, x_2)) \underline{m} \ \underline{n} = (\lambda x_1 x_2. \underline{add} \ x_1 \ x_2) \underline{m} \ \underline{n} = \underline{add} \ \underline{m} \ \underline{n} = \underline{m+n}$

(ii) It would be sufficient to show that $(\underline{curry} \ \underline{prod}) \underline{m} \ \underline{n} = \underline{m \times n}$.

But $\underline{mult} = \underline{curry} (\underline{uncurry} \ \underline{mult}) = \underline{curry} \ \underline{prod}$.

So we need to show that $(\underline{curry} (\underline{uncurry} \ \underline{mult})) \underline{m} \ \underline{n} = \underline{m \times n}$.

Let's do it!

$((\lambda f x_1 x_2. f(x_1, x_2)) ((\lambda fp. f(\underline{fst} \ p)(\underline{snd} \ p)) \underline{mult})) \underline{m} \ \underline{n} = ((\lambda fx_1 x_2. f(x_1, x_2)) (\lambda p. \underline{mult} (\underline{fst} \ p)(\underline{snd} \ p))) \underline{m} \ \underline{n} = (\lambda x_1 x_2. (\lambda p. \underline{mult} (\underline{fst} \ p)(\underline{snd} \ p)) (x_1, x_2)) \underline{m} \ \underline{n} = (\lambda x_1 x_2. \underline{mult} \ x_1 x_2) \underline{m} \ \underline{n} = \underline{mult} \ \underline{m} \ \underline{n} = \underline{m \times n}$

$\square$

Are the steps correct and reasonable? Thanks a bunch!