explicit form for currying

In lambda calculusMathworldPlanetmath, we may express Currying functions and their inversesPlanetmathPlanetmathPlanetmathPlanetmath explicitly using lambda expressions. Suppose that f is a function of two arguments. Then, if c2 is the currying function which maps of two arguments to higher order functions, we have, by definition,


We then have




Likewise, from the original equation, we see that


We can write similar expressions for any number of arguments:

c3 =λw(λc(λb(λaw(a,b,c))))
c4 =λw(λd(λc(λb(λaw(a,b,c,d)))))
c5 =λw(λe(λd(λc(λb(λaw(a,b,c,d)))))),


Their inverses look as follows:

c3-1 =λw(λabc((w(a))(b))(c))
c4-1 =λw(λabcd(((w(a))(b))(c))(d))
c4-1 =λw(λ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