In lambda calculus, we may express Currying functions and their inverses explicitly using lambda expressions. Suppose that $f$ is a function of two arguments. Then, if $c_2$ is the currying function which maps of 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:

Their inverses look as follows: