slides.tex

\documentclass[spanish, a4paper, 12pt, final, slideColor, nototal, colorBG, pdf, noaccumulate, darkblue] {beamer}
\usepackage[spanish]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{latexsym}
\usepackage{mathtools}
\usepackage{anysize}
%\marginsize{2cm}{2cm}{2cm}{3cm}
\usepackage{soul}
\usepackage{mathtools}
\DeclarePairedDelimiter{\ceil}{\lceil}{\rceil}
\newcommand\eqdef{\stackrel{\mathclap{\mbox{\tiny{def}}}}{=}}
\newcommand\eqac{\stackrel{\mathclap{\mbox{*}}}{=}}

\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{float}
\usepackage{verbatim}
\DeclareGraphicsExtensions{.pdf,.png,.jpg}

\usetheme{Madrid}

\title{Introducción al $\lambda$-cálculo}
\subtitle{Otro camino en la resolución de problemas}
\author{Marco Antonio Garrido Rojo\thanks{\url{https://github.com/MaSteve/lambda-calculo}}}
\date{4 de julio de 2016}

\begin{document}
\maketitle
\begin{frame}
    \frametitle{Un poco de historia}
    \begin{itemize}
        \item Desde los tiempos de Leibniz se intentó conseguir la creación de un lenguaje universal para formular todos los problemas posibles y un método de decisíon para resolverlos (en caso de existir).
        \item Lo primero se consiguió con la lógica de primer orden, mientras que para lo segundo tuvimos que esperar hasta el año 1936 para obtener como respuesta un no.
        \item Alan Turing inventó las máquinas de Turing mientras que Alonzo Church inventó un sistema formal llamado $\lambda$-cálculo. Posteriormente, Turing demostró que ambos métodos definían la misma noción de computabilidad.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Un poco de historia}
    \begin{itemize}
        \item Las máquinas de Turing inspiraron el diseño de nuestros actuales ordenadores con arquitectura Von Neumann y los lenguajes de programación imperativos.
        \item Los lenguajes funcionales, por otro lado, se basan en el $\lambda$-cálculo, al igual que lo hacen las máquinas de reducción, diseñadas para la ejecución de este tipo de programas.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{¿Qué es esto del $\lambda$-cálculo?}
    Es un sistema formal basado en funciones que expresan los datos y los algoritmos que se aplican sobre estos. Se apoya en los principios de:
    \begin{itemize}
        \item {\textbf{Reducción: } reemplazar una parte $P$ de $E$ por otra expresión $P'$ con el fin de simplificar. Cuando no puede aplicarse más veces este proceso a una expresión se dice que se ha alcanzado la forma normal $E^*$ de $E$.}
        \item {\textbf{Aplicación: } $F\cdot A$. Emplear $A$ como entrada del algoritmo $F$. Al no existir tipos en esta noción una función puede aplicarse a sí misma.}
        \item {\textbf{Abstracción: } Dada una expresión $M[x]$, $\lambda x.M[x]$ denota una función en la que a cada $N$ le asigna el resultado de $(\lambda x.M[x])N = M[x := N]$.} %OJO Variables libres
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{¿Qué es esto del $\lambda$-cálculo?}
    Definimos el conjunto de los $\lambda$-términos ($\Lambda$) de forma recursiva sobre un conjunto $V$ de variables infinito:
    \begin{itemize}
        \item $x \in V \Rightarrow x \in \Lambda$
        \item $M, N \in \Lambda \Rightarrow (MN)\in \Lambda$
        \item $M \in \Lambda, x \in V \Rightarrow \lambda x.M \in \Lambda$
    \end{itemize}
    De forma similar se puede definir el conjunto de variables libres de una expresión $M$ ($FV(M)$) como:
    \begin{itemize}
        \item $FV(x) = \{x\}$
        \item $FV(MN) = FV(M) \cup FV(N)$
        \item $FV(\lambda x.M) = FV(M) - \{x\}$
    \end{itemize}%OJO: Convenio de variables
    Una expresión sin variables libres es una \textbf{expresión cerrada}.
\end{frame}
\begin{frame}
    \frametitle{¿Qué es esto del $\lambda$-cálculo?}
    Algunos axiomas y reglas:
    \begin{itemize}
        \item \textbf{Axioma principal del $\lambda$-cálculo (regla $\beta$): }$(\lambda x.M[x])N = M[x := N]$
        \item \textbf{Regla $\alpha$: }$\lambda x.M = \lambda y.M[x := y]$ donde $y$ no aparece en $M$.
        \item \textbf{Regla $\eta$: }$\lambda x.Mx = M$ donde $x$ no aparece en $M$.
        \item \textbf{Igualdad: }
        \begin{itemize}
            \item $M = M$
            \item $M = N \Rightarrow N = M$
            \item $M = N, N = L \Rightarrow M = L$
        \end{itemize}
        \item \textbf{Reglas de compatibilidad: } Si $M = M'$ tenemos que:
        \begin{itemize}
            \item $MZ = M'Z$
            \item $ZM = ZM'$
            \item $\lambda x.M = \lambda x.M'$
        \end{itemize}
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{¿Qué podemos hacer con el $\lambda$-cálculo?}
    \textbf{Algunos operadores conocidos:}
    \begin{itemize}
        \item $I \equiv \lambda x.x$
        \item $K \equiv \lambda xy.x$
        \item $K_* \equiv \lambda xy.y$
        \item $S \equiv \lambda xyz.xz(yz)$
    \end{itemize}
    \textbf{Teorema del punto fijo: }$\forall F, \exists X / FX = X$, en concreto tenemos que $F(YF) = YF$ donde $Y = \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$
\end{frame}
\begin{frame}
    \frametitle{¿Qué podemos hacer con el $\lambda$-cálculo?}
    \textbf{Numerales de Church:}
    Definiendo $F^n(M)$ de forma recursiva como:
    \begin{itemize}
        \item $F^0(M) \equiv M$
        \item $F^{n+1}(M) \equiv F(F^n(M))$
    \end{itemize}
    definimos los numerales de Church como $c_n = \lambda fx.f^n(x)$ y los operadores
    \begin{itemize}
        \item $A_+ \equiv \lambda xypq.xp(ypq)$ con $A_+ c_n c_m = c_{n+m}$
        \item $A_* \equiv \lambda xyz.x(yz)$ con $A_* c_n c_m = c_{n*m}$
        \item $A_{exp} \equiv \lambda xy.yx$ con $A_{exp} c_n c_m = c_{n^m}$
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{¿Qué podemos hacer con el $\lambda$-cálculo?}
    ¿Qué hay de los booleanos? Definámoslos:
    \begin{itemize}
        \item $True \equiv K$
        \item $False \equiv K_*$
    \end{itemize}
    La expresión if $B$ then $P$ else $Q$ queda ahora de la forma $BPQ$.
    Utilizaremos por comodidad la notación $[M,N] = \lambda z.zMN$ de modo que:
    \begin{itemize}
        \item $[M,N]True = M$
        \item $[M,N]False = N$
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{¿Qué podemos hacer con el $\lambda$-cálculo?}
    Una alternativa a los numerales de Church:
    \begin{itemize}
        \item $\ceil{0} \equiv I$
        \item $\ceil{n+1} \equiv [False, \ceil{n}]$
    \end{itemize}
    Con los siguientes operadores:
    \begin{itemize}
        \item $S^{+} \equiv \lambda x.[False, x]$
        \item $P^{-} \equiv \lambda x.xFalse$
        \item $Zero \equiv \lambda x.xTrue$
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Hablemos de computación}
    Una función $\varphi$ es $\lambda$-definible si existe un operador $F$ tal que $F\ceil{n_1}\ldots\ceil{n_p} = \ceil{\varphi(n_1\ldots n_p)}$. Las funciones anteriores junto con las proyecciones son $\lambda$-definibles.\\
    Decimos que una clase de funciones $\mathcal{A}$ es:
    \begin{itemize}
        \item \textbf{Cerrada bajo composición} si dada $\varphi(\vec{n}^{\,}) = \chi(\psi_1(\vec{n}^{\,}),\ldots, \psi_m(\vec{n}^{\,}))$ donde $\chi, \psi_i \in \cal{A}$, se tiene que $\varphi \in \cal{A}$.
        \item \textbf{Cerrada bajo recursión} si dada $\varphi(0, \vec{n}^{\,}) = \chi(\vec{n}^{\,})$ y $\varphi(k+1, \vec{n}^{\,}) = \psi(\varphi(k, \vec{n}^{\,}), k, n)$ donde $\chi, \psi \in \cal{A}$, se tiene $\varphi \in \cal{A}$.
        \item \textbf{Cerrada bajo la condición de mínimo} si dada $\varphi(\vec{n}^{\,}) = \mu m[\chi(\vec{n}^{\,}, m) = 0]$ con $\chi \in \cal{A}$ tal que $\forall \vec{n}^{\,} \exists m \chi(\vec{n}^{\,}, m) = 0$, se tiene $\varphi \in \cal{A}$.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Hablemos de computación}
    La clase $\mathcal{R}$ de las funciones recursivas es la clase más pequeña que contiene a los operadores iniciales y que es cerrada bajo composición, recursión y la condición de mínimo. Teniendo que las funciones iniciales son $\lambda$-definibles y que toda función $\lambda$-definible es cerrada respecto a las condiciones anteriores se tiene que toda función recursiva es $\lambda$-definible por construcción.
\end{frame}
\begin{frame}
    \frametitle{Hablemos de computación}
    ¿Qué pasa con los numerales de Church?\\
    \begin{itemize}
        \item Previamente los hemos definido como un método de numeración pero en la definición de $\lambda$-definible no se emplean.
        \item Es conveniente ver que ambas notaciones son equivalentes y para ello se emplean las funciones
        \begin{itemize}
            \item $T \equiv \lambda x.xS^{+}\ceil{0}$
            \item $T^{-1} \equiv \lambda x.[c_0, S^{+}_c (T^{-1}(P^{-}x))]Zero \ceil{x}$
        \end{itemize}
        que definimos junto con los operadores
        \begin{itemize}
            \item $S^{+}_c \equiv \lambda xyz.y(xyz)$
            \item $P^{-}_c \equiv \lambda xyz.x(\lambda pq.q(py))(Kz)I$
            \item $Zero_c \equiv \lambda x.x(K False)True$
        \end{itemize}
        De este modo se puede replantear la definición de $\lambda$-definible con los numerales de Church.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Alguna curiosidad más}
    \begin{itemize}
        \item Originalmente, la teoría del $\lambda$-cálculo no contaba con tipos. Una ampliación al respecto se debe a Curry que incorporó la noción de tipo a la teoría.
        \item Aunque ya sepamos que toda función computable se puede expresar con $\lambda$-términos, existe una versión extendida que admite constantes para facilitar el manejo de ciertas operaciones. Mediante una nueva regla de reducción ($\delta$) aportamos significado a dichas constantes.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Alguna curiosidad más sobre el $\lambda$-cálculo con tipos}
    \begin{itemize}


    \item Definimos el conjunto $\mathbb{T}$ de tipos sobre el conjunto $\mathbb{V}$ de variables de tipo y $\mathbb{B}$ con ``tipos constantes'' como:
    \begin{itemize}
        \item $\alpha \in \mathbb{V} \Rightarrow \alpha \in \mathbb{T}$
        \item $B \in \mathbb{B} \Rightarrow B \in \mathbb{T}$
        \item $\sigma, \tau \in \mathbb{T} \Rightarrow (\sigma \rightarrow \tau) \in \mathbb{T}$
    \end{itemize}
    \item Usaremos la notación $M:\sigma$ para asignar $M$ al tipo $\sigma$. Una base $\Gamma$ será un conjunto de asignaciones.
    \item La derivación de un tipo se sigue de las siguientes reglas, asumiendo $x:\sigma$:
    \begin{itemize}
        \item $M:\sigma \rightarrow \tau, N:\sigma \Rightarrow MN:\tau$
        \item \textst{$x:\sigma$}$, M:\tau \Rightarrow \lambda x.M:\sigma \rightarrow \tau$
    \end{itemize}
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Alguna curiosidad más sobre el $\lambda$-cálculo con tipos}
    \begin{itemize}
        \item A partir de un $\Gamma$ (que puede ser vacio) decimos que $\Gamma \vdash M:\sigma$ si hay una derivación en la que toda asignación no cancelada está en $\Gamma$.
        \item Lema de generación:
        \begin{itemize}
            \item $\Gamma \vdash x:\sigma \Rightarrow (x:\sigma)\in \Gamma$
            \item $\Gamma \vdash MN:\tau \Rightarrow \exists \sigma /\Gamma \vdash M:(\sigma \rightarrow \tau) \wedge \Gamma \vdash N : \sigma$
            \item $\Gamma \vdash \lambda x.M:\rho \Rightarrow \exists \sigma, \tau / \Gamma \cup \{x:\sigma \} \vdash M:\tau \wedge \rho \equiv (\sigma \rightarrow \tau)$
        \end{itemize}
        \item Lema de substitución:
        \begin{itemize}
            \item $\Gamma \vdash M:\sigma \Rightarrow \Gamma[\alpha:=\tau] \vdash M:\sigma[\alpha:=\tau]$
            \item Si $\Gamma \cup \{x:\sigma \} \vdash M:\tau$ y $\Gamma \vdash N:\sigma$, entonces $\Gamma \vdash M[x:=N]:\tau$
        \end{itemize}
        \item Tipado de los subtérminos: Si $M$ tiene un tipo, todo subtérmino de $M$ también tiene un tipo.
        \item Teorema de reducción: Si $M$ es reducible a $M'$ mediante la aplicación de la regla $\beta$, ambos términos tienen el mismo tipo.
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Alguna curiosidad más sobre la normalización}
    \begin{itemize}
        \item A partir de las herramientas antes discutidas podemos llegar a un resultado importante de la teoría del $\lambda$-cálculo.
        \item Mientras que en el $\lambda$-cálculo sin tipos podemos encontrar expresiones del estilo $(\lambda x.xx)(\lambda x.xx)$, estas resultan imposibles de concebir en la teoría con tipos.
        \item El $\lambda$-cálculo con tipos resulta fuertemente normalizable, lo que quiere decir que toda expresión tiene una forma normal alcanzable en un número finito de pasos sea cual sea el camino escogido. (¿Alguien ve el problema que tenemos con la Turing completitud?)
    \end{itemize}
\end{frame}
\begin{frame}
    \frametitle{Alguna curiosidad más sobre la normalización}
    \begin{itemize}
        \item Al menos podemos conformarnos con que el $\lambda$-cálculo cumple el teorema de Church–Rosser que nos dice que el orden en que tomemos las transformaciones no afecta al resultado final, es decir, se da el resultado de confluencia.
    \end{itemize}
\end{frame}
\end{document}