explicit form for currying

Primary tabs

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

Type of Math Object:

Derivation

Major Section:

Reference

Parent:

Groups audience:

68Q01 General