Download el cálculo lambda - paradigmas

EL CÁLCULO LAMBDA
λ
EL CÁLCULO LAMBDA λ
 El cálculo λ fue desarrollado por el matemático
Alonzo Church en la década del 30, a fin de
establecer una teoría general de funciones y
extenderla a modo de proveer fundamentos para la
lógica y matemática.
 Propiedades generales de las funciones
independiente del área particular de problemas.
EL CÁLCULO LAMBDA λ
 El cálculo λ puro, es una gramática para términos:
𝑀 ∷ 𝑥 𝑀1 𝑀2 𝜆𝑥. 𝑀
𝑉𝑎𝑟𝑖𝑎𝑏𝑙𝑒 = 𝑥, 𝑦, 𝑧, …
𝑇é𝑟𝑚𝑖𝑛𝑜 = 𝑀, 𝑁, 𝑃, 𝑄 (Un término puedeser una
variable, una aplicación (M N) o una bstracció𝑛 𝜆𝑥. 𝑀
EL CÁLCULO LAMBDA λ
 El cálculo λ no tiene tipos (tomar en cuenta ámbito -
paso de parámetros - estrategia de evaluación).
 Programación funcional es esencialmente cálculo λ
con constantes apropiadas.
 El cálculo λ con tipos asocia un tipo con cada
término.
APORTE CONCEPTUAL A LOS LENGUAJES DE
PROGRAMACIÓN
 Sintaxis de base.
 Una semántica para el concepto de función como
proceso de transformación de argumentos en
resultados.
 Medios para definir primitivas de programación.
< Termino >≔ < Variable >:
λ < 𝑉𝑎𝑟𝑖𝑎𝑏𝑙𝑒 >. < 𝑇𝑒𝑟𝑚𝑖𝑛𝑜 >:
(< 𝑇𝑒𝑟𝑚𝑖𝑛𝑜 >< 𝑇𝑒𝑟𝑚𝑖𝑛𝑜 >)
REGLAS DEL CÁLCULO λ
 El cálculo debe proveer mecanismo por el cual se
obtiene el resultado de aplicar una función a
argumentos dados:
𝑀=𝑁
M y N son terminos = es una relación de equivalencia
 Los axiomas y reglas de inferencia fijarán
condiciones para términos equivalentes
REGLAS DEL CÁLCULO λ
 Para que relación = sea efectivamente de
equivalencia se consigue imponiendo las
propiedades de:

Reflexividad M. = M

Simetría M=N
N=M
Transitividad
M=N
N = P por lo tanto
M=P

IGUALDAD EN CÁLCULOS λ PUROS
 Igualdad Beta 𝑀 = 𝛽𝑁 si M y N son iguales - deben
tener el mismo valor.
 Se relaciona con el resultado de abstracción(𝜆𝑥. 𝑀) a
un argumento N.
Ej.: fun cuadrado 𝑥 = (𝑥 ∗ 𝑥)
La invocación de cuadrado (5)n sustituye en el cuerpo
a x por 5
𝐶𝑢𝑎𝑑𝑟𝑎𝑑𝑜 5 = 𝛽5 ∗ 5
IGUALDAD EN CÁLCULOS λ PUROS
 El aspecto central del cálculo consiste en establecer el
mecanismo por el cual se obtiene el resultado de
aplicar una función (representada por una
abstracción) a un argumento (representado por un
término cualquiera).
Ej.:
𝑎𝑏𝑠𝑡𝑟𝑎𝑐𝑐𝑖ó𝑛 𝑓𝑢𝑛𝑐𝑖𝑜𝑛𝑎𝑙 = 𝑥 𝑠𝑞𝑟𝑡 2 ∗ 𝑥 + 1
𝑎𝑝𝑙𝑖𝑐𝑎𝑑𝑜 𝑎 𝑢𝑛 𝑣𝑎𝑙𝑜𝑟 = 𝑥 𝑠𝑞𝑟𝑡 2 ∗ 𝑥 + 1 4
𝑠𝑒 𝑝𝑢𝑒𝑑𝑒 𝑟𝑒𝑑𝑢𝑐𝑖𝑟 𝑎 = 𝑥 𝑠𝑞𝑟𝑡 2 ∗ 4 + 1
IGUALDAD EN CÁLCULOS λ PUROS
 Por convención sintáctica pueden eliminarse los paréntesis, en
su ausencia la aplicación se agrupa de izquierda a derecha,
aunque deba conservarse para asegurar las aplicaciones.
Ej.: Ocurrencia
𝑂𝑐𝑢𝑟𝑟𝑒𝑛𝑐𝑖𝑎 𝑑𝑒 𝑃 𝑒𝑛 𝑄
𝐼𝑛𝑑𝑢𝑐𝑐𝑖ó𝑛 𝑒𝑛 𝑙𝑎 𝑓𝑜𝑟𝑚𝑎 𝑑𝑒 𝑄
𝐵𝐴𝑆𝐸 𝑃 𝑜𝑐𝑢𝑟𝑟𝑒 𝑒𝑛 𝑃
𝐼𝑛𝑑𝑢𝑐𝑐𝑖ó𝑛 𝑠𝑖 𝑃 𝑜𝑐𝑢𝑟𝑟𝑒 𝑒𝑛 𝑀 𝑜 𝑒𝑛 𝑁 𝑒𝑛𝑡𝑜𝑛𝑐𝑒𝑠 𝑃 𝑜𝑐𝑢𝑟𝑟𝑒 𝑒𝑛 𝑀𝑁 .
𝑠𝑖 𝑃 𝑜𝑐𝑢𝑟𝑟𝑒 𝑒𝑛 𝑀. 𝑃 ≔: 𝑥, 𝑒𝑛𝑡𝑜𝑛𝑐𝑒𝑠 𝑃 𝑜𝑐𝑢𝑟𝑟𝑒 𝑒𝑛 𝜆𝑥. 𝑚
VARIABLES LIBRES Y ACOTADAS
 Definición (Ocurrencia Libres y Ligadas de variables)
 Una ocurrencia de la variable x en un término P es ligada si y
solo si aparece en un subtérmino de P de la forma λx.M.
 Cualquier otra ocurrencia de x en P es llamada libre.
Ej.:
( 𝑥 𝑣 𝜆𝑦. 𝑦 𝑣 𝑤)
 Las dos ocurrencias de y son ligadas.
 Todas las ocurrencias de x, v y w son libres.
VARIABLES LIBRES Y ACOTADAS
 Abstracciones 𝜆𝑥. 𝑀 llamado asociaciones restringen
a x en 𝜆𝑥. 𝑀 o sea:


Variable x acotada en 𝜆𝑥. 𝑀.
El conjunto libre (m) formado por variables libres de M.
 Reglas de sintaxis:
Libre(x) = {x}
Libre (MN) = libre (M) ∪ libre(N)
Libre 𝜆𝑥. 𝑀 = libre (M) − {x}
SUSTITUCIÓN
La sustitución por un término N de una variable x en M se
escribe (N/x) M y se define:
 Suponga que las variables libres de N no tienen
apariciones acotadas en M, entones el término (N/x) M
se forma reemplazando con N todas las apariciones.
libres de x en M.
 Otro caso suponga que la variable y es libre en N y
acotada en M. La asociación y las apariciones acotadas
correspondiente de y en M se reemplazan de manera
consistente por una variable nueva z. Se sigue de nuevo
las variables acotadas en M hasta que se pueda aplicar el
caso anterior.
SUSTITUCIÓN
 En lo sigo casos M no tiene apariciones acotadas, así
N reemplaza todas las apariciones de x en M para
formar (N/x) M:
(𝑢/𝑥) 𝑥 = 𝑢
(𝑢/𝑥) (𝑥 𝑥) = (𝑢 𝑢)
(𝑢/𝑥) (𝑥 𝑦) = (𝑢 𝑦)
(𝑢/𝑥) (𝑥 𝑢) = (𝑢 𝑢)
((𝜆𝑥. 𝑥)/𝑥)𝑥 = (𝜆𝑋. 𝑥)
SUSTITUCIÓN
 En lo sig. casos M no tiene apariciones libres de x ,
así que (N/x) M es M mismo:
(𝑢/𝑥) 𝑦 = 𝑦
(𝑢/𝑥) (𝑦 𝑧) = (𝑦 𝑧)
(𝑢/𝑥) (𝐴𝑦 𝑦) = (𝐴𝑦 𝑦)
(𝑢/𝑥) (𝐴𝑋 𝑥) = (𝐴𝑋 𝑥)
((𝜆𝑥. 𝑥)/𝑥)𝑦 = 𝑦
SUSTITUCIÓN
 En lo sig. casos la variable u en M tiene apariciones
acotadas en M de modo que (N/x) M se forma
primero asignando nuevo nombre, a las apariciones
acotadas de u en M:
{𝑢/𝑥} (𝜆𝑢. 𝑥) = {𝑢/𝑥} (𝜆𝑧. 𝑥) = (𝜆𝑧. 𝑢)
{𝑢/𝑥} (𝜆𝑢. 𝑢) = {𝑢/𝑥} (𝜆𝑧. 𝑧) = (𝜆𝑧. 𝑧)
SUSTITUCIÓN
 Ejemplos:
 [N/x]x :=: N
 [N/x]V :=: V




[N/x](PQ) :=: ([N/x] P
[N/x]Q)
[N/x] λx. M :=: λx. M
[N/x] λy. P :=: λy. [N/x] P


si V:≠ x
Si y no ocurre libre en N o x no ocurre libre en P
[N/x] λy. P :=: λz. [N/x] [z/y] P

Si Y no ocurre libre en N y X ocurre libre en P y Z no ocurre libre
en P
AXIOMAS Y REGLAS DE LA IGUALDAD BETA
 Axioma fundamental: (λx.M)N =β {N/x} M (axioma β)
Así (λx.x) u = β u y
(λx.y) u = β y.
(λx. M) = β λz.{z/x}M suponiendo que z no es libre en M
(axioma α)
𝑀 =𝛽 𝑀
𝑟𝑒𝑔𝑙𝑎 𝑑𝑒 𝑟𝑒𝑓𝑙𝑒𝑥𝑖𝑣𝑖𝑑𝑎𝑑
𝑀 =𝛽 𝑁
(𝑟𝑒𝑔𝑙𝑎 𝑑𝑒 𝑐𝑜𝑛𝑚𝑢𝑡𝑎𝑡𝑖𝑣𝑖𝑑𝑎𝑑)
𝑁 =𝛽 𝑀
AXIOMAS Y REGLAS DE LA IGUALDAD BETA
𝑀 =𝛽 𝑁 𝑁 =𝛽 𝑃
𝑟𝑒𝑔𝑙𝑎 𝑑𝑒 𝑇𝑟𝑎𝑛𝑠𝑖𝑡𝑖𝑣𝑖𝑑𝑎𝑑
𝑁 =𝛽 𝑃
𝑀 =𝛽 𝑀′ 𝑁 =𝛽 𝑁′
(𝑟𝑒𝑔𝑙𝑎 𝑑𝑒 𝑐𝑜𝑛𝑔𝑟𝑢𝑒𝑛𝑐𝑖𝑎)
′
𝑀𝑁 =𝛽 𝑀 𝑁′
𝑀 =𝛽 𝑀′
(𝑟𝑒𝑔𝑙𝑎 𝑑𝑒 𝑐𝑜𝑛𝑔𝑟𝑢𝑒𝑛𝑐𝑖𝑎)
𝜆𝑥. 𝑀 =𝛽 𝜆𝑥. 𝑀′
 El efecto de un programa funcional es el cómputo de un valor,
imagen en la función representada por el programa de un
cierto valor dado.
REDUCCIONES (redex)
 Redex representa la idea de un computo que esta por
realizarse.
 Un redex representaría el hecho de aplicar un
programa a cierto dato y su forma normal.
 El proceso por el cual se obtiene esta forma normal
será llamado reducción y podría verse como la
«Ejecución» del «Programa» para el «Dato» en
cuestión.
REDUCCIONES (redex)
 Los cálculos lambda son simbólicos. Los términos se
reducen a la forma simple posible.
𝑁
𝑥
(𝜆𝑥. 𝑀) 𝑁 =𝛽
𝑀 el lado derecho es más simple
 Esto sugiere reglas e rescritura llamada reducción
𝑁
𝑥
(𝜆𝑥. 𝑀) 𝑁 =𝛽
𝜆𝑥. 𝑀 =𝛼 𝜆 𝑦.
𝑦
𝑥
𝑀
(β-reducción)
𝑀 y no es libre en M (α-conversión)
REDUCCIONES (redex)
 Si 𝑃 ⇒𝛽 𝑄 - Subtérmino de P se reduce (p-reducción)
para crear Q Un sub término 𝜆𝑥. 𝑀 𝑁 se denomina
exred (redex = reduction expression) de P que se
𝑁
reemplaza por
𝑀 para crear Q.
𝑥
 Un término que no puede tener reducción se encuentra
en forma normal
REDUCCIONES (redex)
 Ej.:
𝑆𝐼𝐼 = (𝜆𝑥𝑦𝑧. 𝑥𝑧(𝑦𝑧)(𝜆𝑥. 𝑥)(𝜆𝑥. 𝑥)
(𝜆𝑦𝑧. 𝜆𝑥. 𝑥 𝑧 𝑦𝑧 )(𝜆𝑥. 𝑥)
𝜆𝑦𝑧. 𝑍 𝑦𝑧
𝜆𝑥. 𝑥
𝜆𝑧. (𝜆𝑥. 𝑥)𝑧 ((𝜆𝑥. 𝑥) 𝑧)
𝜆𝑧. 𝑧 𝜆𝑥. 𝑥 𝑧
𝜆𝑧. 𝜆𝑥. 𝑥 𝑧𝑧
𝜆𝑧. 𝑧𝑧
TEOREMA DE CHURCH-ROSSER
 Para todos los términos A puros M, P Y Q, si 𝑀 ⇒ 𝑃 y
𝑀 ⇒∗ 𝑄, entonces debe existir un término R tal que
P ⇒∗ 𝑅 Y que 𝑄 ⇒∗ 𝑅
Notación para 0 o
más conversiones α
y reducciones β
TEOREMA DE CHURCH-ROSSER
M
*
*
P
Q
*
*
R
 Si M se reduce a P y a Q, entonces ambos pueden
llegar a algún R común.
REGLAS DE CÁLCULO
 En los lenguajes de programación las aplicaciones M
N de funciones, se dice que se invocan por valor.
 Para cálculo lambda estrategia de reducción es una
regla para escoger redex. Hace corresponder a cada
término P (que no esté en forma normal), con un
término Q tal que 𝑃 ⇒𝛽 𝑄.


Reducción para las invocaciones por valor elige la exred del
extremo izquierdo y más interna de un término.
Reducción para las invocaciones por nombre elige la exred del
extremo izquierdo y más externa.
REGLAS DE CÁLCULO
 A pesar de que ocurra una evaluación sin final, los
lenguajes funcionales utilizan la invocación por valor
debido a que es posible implantarla eficientemente y
alcanza la forma normal con la frecuencia necesaria.
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
 Constantes: están pensadas para representar una
función específica y no una genérica como las
variables - cada cálculo lambda tiene su propio
conjunto de constantes.
Sintaxis
<término> ::= <constante>
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
Ej.: true, false, if, O, iszero, pred, succ, fix, ...
𝑇 ∶: = 𝜆𝑥𝑦. 𝑥
𝐹 ∶: = 𝜆𝑥𝑦. 𝑦
O definir 𝑖𝑓_𝑡ℎ𝑒𝑛_𝑒𝑙𝑠𝑒 ∷= 𝜆𝑏. 𝜆𝑚. 𝜆𝑛((𝑏 𝑚)𝑛) (valor
arbitrario)
Y a partir de allí
((𝑖𝑓_𝑡ℎ𝑒𝑛_𝑒𝑙𝑠𝑒 𝑇) 𝑀 𝑁) = 𝑀
((𝑖𝑓_𝑡ℎ𝑒𝑛_𝑒𝑙𝑠𝑒 𝐹) 𝑀 𝑁) = 𝑁
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
 Par ordenado:
Definir término constructor de pares - Ej.: aplicado
sobre dos términos M N devuelva par (M N)
𝐶𝑜𝑛𝑠 ∷= 𝜆𝑥𝑦. 𝜆𝑧. 𝑧 𝑥 𝑦
𝜆𝑧. ((𝑧 𝑀) 𝑁)
𝑀 𝑁 ∷= (𝐶𝑜𝑛𝑠 𝑀 𝑁)
si aplicamos a M N
útil para representar listas
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
 Ejemplo para construir serie numérica:
 Para el O
0 ∷= 𝜆𝑥. 𝑥
 Para el sucesor 𝑠𝑢𝑐𝑒𝑠𝑜𝑟 ∷= 𝜆𝑥. (𝐶𝑜𝑛𝑠 𝐹 𝑥)
1 ∷= 𝑠𝑢𝑐𝑒𝑠𝑜𝑟 0 = (𝐶𝑜𝑛𝑠 𝐹 0)
2 ∷= 𝑠𝑢𝑐𝑒𝑠𝑜𝑟 1 = 𝐶𝑜𝑛𝑠 𝐹 1 = (𝐶𝑜𝑛𝑠 𝐹 (𝐶𝑜𝑛𝑠 𝐹 0))
Y así sucesivamente.
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
 Reglas de reducción para algunas constantes:
𝐼𝑓 𝑡𝑟𝑢𝑒 𝑀 𝑁 ⇒𝛿 𝑀
𝐼𝑓 𝑓𝑎𝑙𝑠𝑒 𝑀 𝑁 ⇒𝛿 𝑁
𝑓𝑖𝑥 𝑀 ⇒𝛿 𝑀
𝑖𝑠𝑧𝑒𝑟𝑜 ⇒𝛿 𝑡𝑟𝑢𝑒
𝑖𝑠𝑧𝑒𝑟𝑜 (𝑠𝑢𝑐𝑐 𝐾 𝑂) ⇒𝛿 𝑓𝑎𝑙𝑠𝑒
𝑖𝑠𝑧𝑒𝑟𝑜 𝑝𝑟𝑒𝑑𝑘 𝑂 ⇒𝛿 𝑓𝑎𝑙𝑠𝑒
𝑠𝑢𝑐𝑐(𝑝𝑟𝑒𝑑 𝑀) ⇒𝛿 𝑀
𝑝𝑟𝑒𝑑(𝑠𝑢𝑐𝑐 𝑀) ⇒𝛿 𝑀
𝑑𝑜𝑛𝑑𝑒 𝑘 ≥ 1
𝑑𝑜𝑛𝑑𝑒 𝑘 ≥ 1
CONSTANTES Y PRIMITIVAS DE LENGUAJES
DE PROGRAMACIÓN
 Elementos sintácticos para un cálculo lambda aplicado
CONSTRUCTOR
CÁLCULO LAMBDA
Variable
X
Constante
C
Aplicación
MN
Abstracción
𝜆𝑥. 𝑀
Entero
𝑆𝑢𝑐𝑐 𝑘 0, 𝑓𝑜𝑟 𝑘 > 0
Entero
𝑃𝑟𝑒𝑑 𝑘 0, 𝑓𝑜𝑟 𝑘 > 0
Condicional
𝐼𝑓 𝑃 𝑀 𝑁
Asignación
𝜆𝑥. 𝑀 N
Función recursiva
(𝜆𝑥. 𝑀)(𝑓𝑖𝑥 (𝜆𝑓. 𝜆𝑥. 𝑁))