#LyX 2.3 created this file. For more info see http://www.lyx.org/ \lyxformat 544 \begin_document \begin_header \save_transient_properties true \origin unavailable \textclass book \begin_preamble \input{../defs} \end_preamble \use_default_options true \maintain_unincluded_children false \language spanish \language_package default \inputencoding auto \fontencoding global \font_roman "default" "default" \font_sans "default" "default" \font_typewriter "default" "default" \font_math "auto" "auto" \font_default_family default \use_non_tex_fonts false \font_sc false \font_osf false \font_sf_scale 100 100 \font_tt_scale 100 100 \use_microtype false \use_dash_ligatures true \graphics default \default_output_format default \output_sync 0 \bibtex_command default \index_command default \paperfontsize default \spacing single \use_hyperref false \papersize default \use_geometry false \use_package amsmath 1 \use_package amssymb 1 \use_package cancel 1 \use_package esint 1 \use_package mathdots 1 \use_package mathtools 1 \use_package mhchem 1 \use_package stackrel 1 \use_package stmaryrd 1 \use_package undertilde 1 \cite_engine basic \cite_engine_type default \biblio_style plain \use_bibtopic false \use_indices false \paperorientation portrait \suppress_date false \justification true \use_refstyle 1 \use_minted 0 \index Index \shortcut idx \color #008000 \end_index \secnumdepth 3 \tocdepth 3 \paragraph_separation indent \paragraph_indentation default \is_math_indent 0 \math_numbering_side default \quotes_style french \dynamic_quotes 0 \papercolumns 1 \papersides 1 \paperpagestyle default \tracking_changes false \output_changes false \html_math_output 0 \html_css_as_file 0 \html_be_strict false \end_header \begin_body \begin_layout Standard Un \series bold sistema formal \series default está formado por: \end_layout \begin_layout Enumerate Un \series bold lenguaje formal \series default , con una serie de \series bold símbolos \series default y \series bold reglas sintácticas \series default para combinarlos obteniendo \series bold fórmulas \series default . \end_layout \begin_layout Enumerate Una serie de \series bold reglas de inferencia \series default , formadas por 0 o más juicios en el antecedente (arriba) y uno en el precedente (abajo). Los juicios son expresiones de la forma \begin_inset Formula $\Gamma\vdash f$ \end_inset , que indican que la fórmula \begin_inset Formula $f$ \end_inset se deriva de las fórmulas en \begin_inset Formula $\Gamma$ \end_inset , donde \begin_inset Formula $f$ \end_inset puede contener símbolos que indican entidades de cierto tipo en el lenguaje (subcadenas con ciertas restricciones) y el mismo símbolo representa la misma entidad en toda la regla. \end_layout \begin_layout Standard Un \series bold teorema \series default es una fórmula \begin_inset Formula $f$ \end_inset tal que \begin_inset Formula $\vdash f$ \end_inset se puede obtener aplicando una cantidad finita de reglas de inferencia. Un \series bold axioma \series default es un teorema que se obtiene aplicando una sola regla de inferencia. \end_layout \begin_layout Standard El \series bold cálculo lambda \series default es un sistema formal diseñado por Alonzo Church y Stephen Kleen en los años 30 \begin_inset Foot status open \begin_layout Plain Layout Los del siglo XX. \end_layout \end_inset para investigar la definición de funciones computables, aplicación de funciones y recursividad. Es el precursor de lenguajes funcionales como Lisp, ML y Haskell, y puede expresar cualquier función computable. \end_layout \begin_layout Standard El alfabeto del lenguaje está formado por la \series bold igualdad \series default \begin_inset Formula $=$ \end_inset , la \series bold reducción \series default \begin_inset Formula $\to$ \end_inset , los \series bold símbolos impropios \series default \begin_inset Formula $\lambda$ \end_inset , \begin_inset Formula $.$ \end_inset , \begin_inset Formula $($ \end_inset y \begin_inset Formula $)$ \end_inset , y símbolos para representar una cantidad infinita de variables. Un \series bold término \series default es una variable, una \series bold aplicación \series default \begin_inset Formula $(M\,N)$ \end_inset , donde \begin_inset Formula $M$ \end_inset y \begin_inset Formula $N$ \end_inset son términos, o una \series bold abstracción \series default \begin_inset Formula $(\lambda x.M)$ \end_inset , donde \begin_inset Formula $x$ \end_inset es una variable llamada \series bold variable ligada \series default y \begin_inset Formula $M$ \end_inset es un término llamado \series bold cuerpo \series default . Una fórmula es una expresión \begin_inset Formula $M=N$ \end_inset o \begin_inset Formula $M\to N$ \end_inset , donde \begin_inset Formula $M$ \end_inset y \begin_inset Formula $N$ \end_inset son términos. Dos términos \begin_inset Formula $M$ \end_inset y \begin_inset Formula $N$ \end_inset son \series bold idénticos \series default , \begin_inset Formula $M\equiv N$ \end_inset , si tienen la misma expresión. \end_layout \begin_layout Standard Para reducir el uso de paréntesis, consideramos que la aplicación tiene máxima prioridad y es asociativa por la izquierda, la abstracción se extiende lo más lejos posible y \begin_inset Formula $\to$ \end_inset y \begin_inset Formula $=$ \end_inset tienen el máximo alcance. Además, si \begin_inset Formula $x_{1},\dots,x_{n}$ \end_inset son variables y \begin_inset Formula $M$ \end_inset es un término, la sintaxis \begin_inset Formula $\lambda x_{1}\,x_{2}\,\dots\,x_{n}.M$ \end_inset equivale a \begin_inset Formula $\lambda x_{1}.\lambda x_{2}.\dots\lambda x_{n}.M$ \end_inset . \end_layout \begin_layout Standard Si \begin_inset Formula $x$ \end_inset es una variable y \begin_inset Formula $M$ \end_inset y \begin_inset Formula $N$ \end_inset son términos, definimos el conjunto de \series bold variables libres \series default de un término como \begin_inset Formula \begin{align*} \text{FV}(x) & \coloneqq\{x\}, & \text{FV}(M\,N) & \coloneqq\text{FV}(M)\cup\text{FV}(N), & \text{FV}(\lambda x.M) & \coloneqq\text{FV}(M)\setminus\{x\}, \end{align*} \end_inset y el conjunto de \series bold variables ligadas \series default como \begin_inset Formula \begin{align*} \text{BV}(x) & \coloneqq\emptyset, & \text{BV}(M\,N) & \coloneqq\text{BV}(M)\cup\text{BV}(N), & \text{BV}(\lambda x.M) & \coloneqq\text{BV}(M)\cup\{x\}. \end{align*} \end_inset Estos conjuntos no contienen variables sino apariciones de variables en la expresión, y en sus definiciones para una abstracción, el término \begin_inset Formula $\{x\}$ \end_inset se refiere a todas las apariciones de \begin_inset Formula $x$ \end_inset en \begin_inset Formula $M$ \end_inset . \end_layout \begin_layout Standard Sean \begin_inset Formula $M$ \end_inset , \begin_inset Formula $N$ \end_inset y \begin_inset Formula $P$ \end_inset términos y \begin_inset Formula $x$ \end_inset e \begin_inset Formula $y$ \end_inset variables distintas, definimos la \series bold sustitución \series default de un término en otro como \begin_inset Formula \begin{align*} x[N/x] & \coloneqq N,\\ y[N/x] & \coloneqq y,\\ (M\,P)[N/x] & \coloneqq(M[N/x])(P[N/x]),\\ (\lambda x.M)[N/x] & \coloneqq\lambda x.M,\\ (\lambda y.M)[N/x] & \coloneqq\lambda z.(M[z/y][N/x]), \end{align*} \end_inset donde \begin_inset Formula $z$ \end_inset es una variable cualquiera que no está en \begin_inset Formula $\text{FV}(M)\cup\text{FV}(N)$ \end_inset . Si \begin_inset Formula $y\notin\text{FV}(N)$ \end_inset o \begin_inset Formula $x\notin\text{FV}(M)$ \end_inset , en la última regla se puede omitir \begin_inset Formula $[z/y]$ \end_inset y la sustitución es \series bold válida \series default o \series bold segura \series default , pero si no es así, al aplicar la versión simplificada se dice que se produce \series bold captura de variables \series default , en la que una variable libre en \begin_inset Formula $N$ \end_inset pasa a estar ligada en \begin_inset Formula $(\lambda y.M)[N/x]$ \end_inset . \end_layout \begin_layout Standard Las reglas de inferencia son las siguientes, donde \begin_inset Formula $M$ \end_inset , \begin_inset Formula $N$ \end_inset , \begin_inset Formula $S$ \end_inset , \begin_inset Formula $T$ \end_inset y \begin_inset Formula $U$ \end_inset son términos y \begin_inset Formula $x$ \end_inset e \begin_inset Formula $y$ \end_inset son variables. \begin_inset Formula \begin{align*} \alpha\text{-conversión: } & \frac{\{y\notin\text{FV}(M)\}}{\Gamma\vdash(\lambda x.M)\to(\lambda y.M[y/x])} & & & & \frac{\Gamma\vdash S\to T}{\Gamma\vdash(U\,S)\to(U\,T)}\\ \beta\text{-conversión: } & \frac{}{\Gamma\vdash((\lambda x.M)\,N)\to M[N/x]} & & & & \frac{\Gamma\vdash S\to T}{\Gamma\vdash\lambda x.S\to\lambda x.T}\\ \eta\text{-conversión: } & \frac{\{x\notin\text{FV}(M)\}}{\Gamma\vdash(\lambda x.(M\,x))\to M} & & & & \frac{\Gamma\vdash S\to T}{\Gamma\vdash S=T}\\ & \frac{}{\Gamma\vdash T\to T} & & & & \frac{\Gamma\vdash S=T}{\Gamma\vdash T=S}\\ & \frac{\Gamma\vdash S\to T\ \ \Gamma\vdash T\to U}{S\to U} & & & & \frac{\Gamma\vdash S=T\ \ \Gamma\vdash T=U}{\Gamma\vdash S=U}\\ & \frac{\Gamma\vdash S\to T}{\Gamma\vdash(S\,U)\to(T\,U)} \end{align*} \end_inset Las \series bold conversiones \series default \begin_inset Formula $\alpha$ \end_inset , \begin_inset Formula $\beta$ \end_inset y \begin_inset Formula $\eta$ \end_inset también se llaman \series bold reducciones \series default . El resto de reglas dicen que las reducciones se pueden aplicar a subtérminos, que la reducibilidad es reflexiva y transitiva, y que dos términos son iguales si se pueden conectar por una cadena finita de reducciones hacia un lado u otro. La igualdad es \series bold extensional \series default , de modo que si dos funciones son iguales, al aplicarlas a los mismos parámetro s se obtienen resultados iguales. \end_layout \begin_layout Standard El \series bold cálculo lambda puro \series default es el que se ha descrito, pudiendo definir términos comunes para abreviar pero sin constantes predefinidas. El \series bold cálculo lambda impuro \series default permite también constantes predefinidas sin definir estas como términos, como números o funciones sobre estos. Se añaden \series bold \begin_inset Formula $\delta$ \end_inset -reducciones \series default , en las que una expresión en que intervienen constantes se sustituye por su valor según reglas específicas a dichas constantes. \end_layout \begin_layout Standard Un \series bold radical \series default o \series bold \emph on redex \series default \emph default es un término de la forma \begin_inset Formula $(\lambda x.U)T$ \end_inset , y su \series bold contrato \series default es \begin_inset Formula $U[T/x]$ \end_inset . Un término \begin_inset Formula $M$ \end_inset es \series bold normal \series default si no contiene ningún radical, y es \series bold normalizable \series default si existe un término normal \begin_inset Formula $N$ \end_inset tal que \begin_inset Formula $M\to N$ \end_inset , en cuyo caso se puede llegar a una por una cadena de \begin_inset Formula $\beta$ \end_inset -reducciones en el término o subtérminos. El objetivo principal al manipular una expresión lambda es reducirla a su forma normal, lo que corresponde a la idea de fin de cálculo en la programac ión convencional. Hay expresiones no normalizables, como \begin_inset Formula $(\lambda x.xx)\lambda x.xx$ \end_inset . \end_layout \begin_layout Standard Una \series bold estrategia de evaluación \series default indica el orden en que aplicar \begin_inset Formula $\beta$ \end_inset -reducciones para tratar de llegar a la forma normal. Algunas son: \end_layout \begin_layout Enumerate \series bold Orden normal: \series default Se reduce primero el radical más exterior más a la izquierda, que para un término \begin_inset Formula $(\lambda x.S)T$ \end_inset es el propio término, para otra aplicación \begin_inset Formula $S\,T$ \end_inset es el de \begin_inset Formula $S$ \end_inset si tiene alguno o el de \begin_inset Formula $T$ \end_inset en otro caso, y para \begin_inset Formula $\lambda x.S$ \end_inset es el de \begin_inset Formula $S$ \end_inset . \begin_inset Foot status open \begin_layout Plain Layout Es lo que usan los lenguajes perezosos como Haskell, aunque con optimizaciones. \end_layout \end_inset \end_layout \begin_layout Enumerate \series bold Orden aplicativo: \series default Se reduce primero el radical más interior más a la izquierda, que se define como el radical exterior más a la izquierda salvo que, para un término \begin_inset Formula $(\lambda x.S)T$ \end_inset , primero se reduce el primero de \begin_inset Formula $S$ \end_inset si tiene alguno, o el primero de \begin_inset Formula $T$ \end_inset si tiene alguno y \begin_inset Formula $S$ \end_inset no. \begin_inset Foot status open \begin_layout Plain Layout Es lo que usan la mayoría de lenguajes de programación, salvo que no se reduce el interior de una expresión lambda y en algunos no se garantiza que la evaluación de parámetros se haga de izquierda a derecha. \end_layout \end_inset \end_layout \begin_layout Standard \series bold Teoremas de Church-Rosser: \end_layout \begin_layout Enumerate \series bold Propiedad del diamante: \series default Si \begin_inset Formula $S\to T_{1}$ \end_inset y \begin_inset Formula $S\to T_{2}$ \end_inset , existe \begin_inset Formula $U$ \end_inset tal que \begin_inset Formula $T_{1}\to U$ \end_inset y \begin_inset Formula $T_{2}\to U$ \end_inset . Además, la forma normal de un término a la que se llega por \begin_inset Formula $\beta$ \end_inset -reducciones es única salvo \begin_inset Formula $\alpha$ \end_inset -conversiones. \end_layout \begin_layout Enumerate Si un término es normalizable, se puede llevar a su forma normal por el orden de reducción normal. \end_layout \begin_layout Standard Un \series bold combinador \series default o \series bold término cerrado \series default es un término sin variables libres. Los más simples son \begin_inset Formula ${\bf I}\coloneqq\lambda x.x$ \end_inset , \begin_inset Formula ${\bf K}\coloneqq\lambda x\,y.x$ \end_inset y \begin_inset Formula ${\bf S}\coloneqq\lambda f\,g\,x.f\,x\,(g\,x)$ \end_inset . Todo término tiene un equivalente con las mismas variables libres y sin abstracciones usando solo estos 3 combinadores. \end_layout \end_body \end_document