nose

Cálculo-λ

Antonio Almazán Faura
Lidia Quintana Pancorbo

Índice
Cálculo- λ
Sintaxis
Notación: paréntesis y macros
Conversiones
Igualdades
Ejemplos: lógica booleana y aritmética
Conclusiones
Cálculo-λ

2

Cálculo-λ
Autor: Alonzo Church
Objetivo:
Formalizar el modo de escribir funciones.
A partir del concepto de función-λ será
posible generar cualquier función
computable.Cálculo-λ

3

Cálculo-λ
Método:
Generar funciones que tomarán datos de
entrada de un problema y proporcionarán
datos de salida.
Todo sin salirse de la definición de este
lenguaje, de su estructura y sintaxis.

Este nueva notación derivó en distintos
lenguajes de programación (como LISP)
Cálculo-λ

4

Sintaxis
Clases de
expresiones-λ
Variables
Aplicación de
funciónAbstracción con
variable ligada y
cuerpo de función
Cálculo-λ


::=
::=
::= λ.

5

Sintaxis
Ejemplos
Aplicación de función:
representa el resultado de
aplicar la función E1 sobre la
función E2
Abstracción: representa el
resultado de evaluar E donde
la variable V tomará el valor
al que se ligue por
argumentos
Cálculo-λ

E1 E2
x(y)
m(n(y))
λV.E
λx.x
λab.(a(b))

6Sintaxis
Variables ligadas
dentro del cuerpo

Valor de
argumento1

(λxy. x(λab.a)y)

Valor de
argumento2

(λcd.c) (λef.e)

Cuerpo de función
Si observamos ambos argumentos, son iguales excepto
por el renombramiento. ES NECESARIO RENOMBRAR,
para no confundirnos al realizar las vinculaciones y
sustituciones.
Cálculo-λ

7

Sintaxis
Expresión-λ de partida
(λxy. x(λab.a)y)(λcd.c) (λef.e)
Expresión-λ de resultado parcial
(λcd.c) ( λab.a ) (λef.e)
Expresión-λ de resultado final
λab.a
Todo son EXPRESIONES-λ, y sólo intervienen
“letras”, paréntesis y puntos.
Cálculo-λ

8

Notación
Una expresión-λ “auténtica”
SIEMPRE contiene TODOS los PARENTESIS
NUNCA contiene MACROS

Pero por comodidad, admitimos una
notación que omite paréntesis y emplea
macros.Cálculo-λ

9

Notación: paréntesis
Al omitir paréntesis debemos tener en
cuenta:
1) Asociación
E1 E2 E3 ... En ≡ (...((E1 E2)E3)...En)
2) Ámbito de variable
λV. E1 E2 E3...En ≡ λV.(E1 E2 E3...En)
3) Orden de variable
λV1 V2 V3... Vn ≡ λV1(λV2(...(λVn.E)...))

La aparición de una variable V en una
expresión-λ es libre si no aparece en el
alcance de λV
Cálculo-λ

10

Notación:macros
Admitimos macros por una cuestión de
comprensión y comodidad al operar,
pero no forman parte del cálculo-λ
Ejemplo
macro:
muchasX = xxxxxxxxxx
uso:
(λx.muchasX) (a)
resultado: aaaaaaaaaa
Cálculo-λ

11

Conversiones
El cálculo-λ está formado por:
Una SINTAXIS específica
Unas CONVERSIONES (o reducciones)
entre expresiones
Cualquier conversión se puede efectuar,
si lassustituciones son válidas
Cálculo-λ

12

Conversiones
Una sustitución E[V:=E’] es válida sii ninguna
de las variables libre de E’ se convierte en
una variable ligada en E[V:=E’]
α-redex: renombramiento de variables
β-redex: vinculaciones de variables
(“bindings”)
η-redex: dos funciones son iguales si al
aplicarles los mismos argumentos dan los
mismos resultados
Cálculo-λ

13Conversiones
Las reglas de conversión son las que nos van
a permitir “jugar” con las expresiones-λ
La reducción-α es “intuitiva” y nos ayuda a
manipular las expresiones; y la reducción-η
puede ser necesaria, aunque nosotros no la
vamos a ver en los ejemplos.
Por otro lado, la reducción-β es la más
importante.
Cálculo-λ

14

Conversiones
[sustitución]

α-redex
λV.E

α

λV’.E [V:=V’][binding]

β-redex
(λV.E1) E2

Cálculo-λ

β

E1 [V:=E2]

15

Conversiones
Ejemplo de α-redex
[sustitución]
λV.E α λV’.E [V:=V’]
(λx.x)
(λxy.xy)
(λxy.xy)

Cálculo-λ

α
x=y
α
x=a, y=b
α
x=a

(λy.y)
(λab.ab)
(λay.ay)

16

Conversiones
Ejemplo de β-redex
[binding]
β E1 [V:=E2]
(λV.E1) E2
(λx.x)
(a)
(λxy.xy) (a) (b)
(λxy.xy) (b)

Cálculo-λ

β
β
β...