68Q01-ExplicitFormForCurrying.tex

\documentclass[12pt]{article}
\usepackage{pmmeta}
\pmcanonicalname{ExplicitFormForCurrying}
\pmcreated{2013-03-22 17:03:57}
\pmmodified{2013-03-22 17:03:57}
\pmowner{rspuzio}{6075}
\pmmodifier{rspuzio}{6075}
\pmtitle{explicit form for currying}
\pmrecord{5}{39358}
\pmprivacy{1}
\pmauthor{rspuzio}{6075}
\pmtype{Derivation}
\pmcomment{trigger rebuild}
\pmclassification{msc}{68Q01}

\endmetadata

% 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

\begin{document}
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*}
%%%%%
%%%%%
\end{document}