explicit form for currying

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:

$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))$

Title	explicit form for currying
Canonical name	ExplicitFormForCurrying
Date of creation	2013-03-22 17:03:57
Last modified on	2013-03-22 17:03:57
Owner	rspuzio (6075)
Last modified by	rspuzio (6075)
Numerical id	5
Author	rspuzio (6075)
Entry type	Derivation
Classification	msc 68Q01