explicit form for currying
ExplicitFormForCurrying
2007-05-10 01:22:40
2007-05-10 02:10:53
Derivation
currying
% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands here
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:
\begin{align*}
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)))))) ,
\end{align*}
etc.
Their inverses look as follows:
\begin{align*}
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))
\end{align*}