# 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:

 $\displaystyle c_{3}$ $\displaystyle=\lambda_{w}(\lambda_{c}(\lambda_{b}(\lambda_{a}w(a,b,c))))$ $\displaystyle c_{4}$ $\displaystyle=\lambda_{w}(\lambda_{d}(\lambda_{c}(\lambda_{b}(\lambda_{a}w(a,b% ,c,d)))))$ $\displaystyle c_{5}$ $\displaystyle=\lambda_{w}(\lambda_{e}(\lambda_{d}(\lambda_{c}(\lambda_{b}(% \lambda_{a}w(a,b,c,d)))))),$

etc.

Their inverses look as follows:

 $\displaystyle c_{3}^{-1}$ $\displaystyle=\lambda_{w}(\lambda_{abc}((w(a))(b))(c))$ $\displaystyle c_{4}^{-1}$ $\displaystyle=\lambda_{w}(\lambda_{abcd}(((w(a))(b))(c))(d))$ $\displaystyle c_{4}^{-1}$ $\displaystyle=\lambda_{w}(\lambda_{abcde}((((w(a))(b))(c))(d))(e))$
Title explicit form for currying ExplicitFormForCurrying 2013-03-22 17:03:57 2013-03-22 17:03:57 rspuzio (6075) rspuzio (6075) 5 rspuzio (6075) Derivation msc 68Q01