\documentclass[12pt]{article}
\usepackage[spanish]{babel}
\usepackage{amscd,amsfonts,amsmath,amssymb,latexsym}
\usepackage[latin1]{inputenc}

\title{Funcionamiento, en PCF, del Operador de Punto Fijo}
\author{José de Jesús Lavalle Martínez}
\date{Octubre de 2005}

\newcommand{\ed}{\ensuremath{\overset{\text{def}}{=}}}
\newcommand{\rs}[1]{\ensuremath{\overset{#1}{\rightarrow}}}
\newcommand{\su}[2]{\ensuremath{[#1/#2]}}
\newcommand{\eq}[2]{\ensuremath{\textbf{ Eq? } #1 \quad #2}}
\newcommand{\tf}[2]{\ensuremath{#1 \rightarrow #2}}
\newcommand{\ite}[3]{\ensuremath{\textbf{ if } #1 \textbf{ then } #2 \textbf{
else } #3}}
\newcommand{\pr}[3]{\ensuremath{\textbf{ Proj}_#1\langle#2,#3\rangle}}
\newcommand{\la}[3]{\ensuremath{\lambda #1 : #2 . #3}}
\newcommand{\li}[3]{\ensuremath{\textbf{ let } #1 = #2 \textbf{ in } #3}}
\newcommand{\lri}[3]{\ensuremath{\textbf{ letrec } #1 = #2 \textbf{ in } #3}}

\begin{document}
\maketitle

\begin{equation*}
f(y) =
\begin{cases}
1 & \text{cuando } y=0 \\
y * f(y-1) & \text{en otro caso}
\end{cases}
\end{equation*}

\begin{gather*}
\li{f:\tf{nat}{nat}}
{
\la{y}{nat}{\ite{\eq{y}{0}}{1}{y * f(y-1)}}
}
{f \quad 3 } \rs{\text{def}} \\
(\la{f}{\tf{nat}{nat}}{f \quad 3}) 
(\ite{\eq{y}{0}}{1}{y * f(y-1)})
\rs{\beta} \\
(\ite{\eq{y}{0}}{1}{y * f(y-1)}) \quad 3
\rs{\beta} \\
\ite{\eq{3}{0}}{1}{3 * f(3-1)}
\rs{\text{Eq?}} \\
\ite{false}{1}{3 * f(3-1)}
\rs{\text{if}} \\
3 * f(3-1)
\end{gather*}

\begin{equation*}
F = \la{f}{\tf{nat}{nat}}{\la{y}{nat}{\ite{\eq{y}{0}}{1}{y *
f(y-1)}}}
\end{equation*}

\begin{equation}\label{tF}
F: \tf{(\tf{nat}{nat})}{(\tf{nat}{nat})}
\end{equation}

\begin{equation}\label{tfix}
fix_{\sigma}: \tf{(\tf{\sigma}{\sigma})}{\sigma}
\end{equation}

\begin{equation}\label{tfixF}
(fix_{\sigma} F): (\tf{nat}{nat}), \text{ de (\ref{tfix}) y
(\ref{tF})
haciendo } \sigma = (\tf{nat}{nat})
\end{equation}

\begin{equation*}
F (fix_{(\tf{nat}{nat})} F):(\tf{nat}{nat}), \text{ de
(\ref{tF}) y
(\ref{tfixF}})
\end{equation*}

\begin{equation*}
(fix_{(\tf{nat}{nat})} F) = F (fix_{(\tf{nat}{nat})} F)
\end{equation*}

\begin{equation*}
((fix_{(\tf{nat}{nat})} F) n): nat, \text{ de (\ref{tfixF}) si }
n:nat
\end{equation*}

\begin{equation*}
(fix_{\sigma} M): \sigma \text{ y } M (fix_{\sigma} M): \sigma, \text{ de (\ref{tfix})
si } M: (\tf{\sigma}{\sigma})
\end{equation*}

\begin{equation*}
(fix_{\sigma} M) = M (fix_{\sigma} M)
\end{equation*}

\begin{equation*}
fix_{\sigma} = \la{f}{\tf{\sigma}{\sigma}}{f(fix_{\sigma} f)} \qquad
(fix)
\end{equation*}

\begin{equation*}
\lri{f:\sigma}{M}{N} \ed
\li{f:\sigma}{(fix_{\sigma} \la{f}{\sigma}{M})}{N}
\end{equation*}

\pr{1}{M}{N}, \pr{2}{2}{\pr{2}{4}{5}}, \su{(\su{M}{x}N)}{y}

\end{document}
\rightarrow
\longrightarrow
\overrightarrow{}