explicit form for currying

In lambda calculus, we may express Currying functions and their inversesexplicitly using lambda expressions. Suppose that $f$ is a functionof two arguments. Then, if $c_2$ is the currying function which mapsof two arguments to higher order functions, we have, by definition,

$$f(x,y)=((c_2(f))(x))(y).$$

We then have

$$c_2(f)={\lambda }_v({\lambda }_{u}f(u,v)),$$

hence

$$c_2={\lambda }_w({\lambda }_v({\lambda }_{u}w(u,v))).$$

Likewise, from the original equation, we see that

$$c_2^{-1}={\lambda }_w({\lambda }_{ab}(w(x))(y)).$$

We can write similar expressions for any number of arguments:

$c_3$$={\lambda }_w({\lambda }_c({\lambda }_b({\lambda }_{a}w(a,b,c))))$

$c_4$$={\lambda }_w({\lambda }_d({\lambda }_c({\lambda }_b({\lambda }_{a}w(a,b,c,d)))))$

$c_5$$={\lambda }_w({\lambda }_e({\lambda }_d({\lambda }_c({\lambda }_b({\lambda }_{a}w(a,b,c,d)))))),$

etc.

Their inverses look as follows:

$c_3^{-1}$$={\lambda }_w({\lambda }_{abc}((w(a))(b))(c))$

$c_4^{-1}$$={\lambda }_w({\lambda }_{abcd}(((w(a))(b))(c))(d))$

$c_4^{-1}$$={\lambda }_w({\lambda }_{abcde}((((w(a))(b))(c))(d))(e))$