Calculo Lambda

Lambda-C´lculo a
Mauro Jaskelioff

6/9/2011

Origen del λ-c´lculo a

El λ-c´lculo fue inventado por Alonzo Church en a la d´cada de 1930. e Originalmente fue inventado como parte de un sistema formal para modelar la m´tematica. a
¡Pero es inconsistente!

Es utilizado para estudiar la computabilidad.
En paralelo, Turing presenta su m´quina. a

En los 1960s, Peter Landin muestra que sepuede usar para dar sem´ntica a los lenguajes de a programaci´n (imperativos). o Los lenguajes funcionales est´n basados en el a λ-c´lculo. a

SINTAXIS

Sintaxis

Suponemos la existencia de un conjunto infinito de identificadores
x, y ,z, . . . , x0 , x1 denotan elementos de X

El conjunto Λ de λ-t´rminos se define inductivamente por las e siguientes reglas: x ∈X x ∈Λ Ejemplos: x (x y )(λx.x) t∈Λ u∈Λ (t u) ∈ Λ x ∈X t∈Λ (λx.t) ∈ Λ

(λx.(λy .((x y ) y )))

¿Esto es todo?

Con este peque˜o lenguaje se pueden representar todas las n funciones computables!
(Tesis de Church)

Esta simpleza hace que:
Se facilite la prueba de propiedades. Se use para dar sem´ntica a lenguajes imperativos y a funcionales. Su use como metalenguaje para definir otras teor´ y c´lculos. ıas a

Laelegancia hace que sea m´s pr´ctico! a a

Convenciones

Las may´sculas indican λ-t´rminos arbitrarios (ej: M,N,P) u e Escribimos: M N P λx.P Q λx1 x2 . . . xn .M en lugar de ((M N) P) en lugar de (λx.P Q) en lugar de (λx1 .(λx2 .(. . . (λxn .M) . . . ))

Ejercicio
Insertar todos los par´ntesis y λs en los sig. t´rminos abreviados: e e x y z (y x) (λx.v u u) z y (λx y z.x z (y z)) u v w u x(y z) (λv .v y )

Ocurrencias
La identidad sint´ctica se denota con ≡ a
M ≡ N iff M es exactamente el mismo t´rmino que N. e

Definici´n (Ocurrencia) o
La relaci´n P ocurre en Q (o P es un subt´rmino de Q) se define o e inductivamente sobre la estructura de Q P ocurre en P; si P ocurre en M o en N, entonces P ocurre en (M N); si P ocurre en M o P ≡ x, entonces P ocurre en (λx.M).

EjercicioEncontrar las ocurrencias de (x y ) en los t´rminos e (λx y .x y ) (z (x y ) (λx.y (x y )) x y )

Variables libre y ligadas

para una ocurrencia de λx.M en P, M es el alcance de la abstracci´n λx. o Hay 3 tipos de ocurrencia de una variable x en un t´rmino P e
1. ocurrencia de ligadura (si es la x en un λx) 2. ocurrencia ligada (si es una x en el alcance de un λx en P). 3. ocurrencia libre(en cualquier otro caso).

Llamamos FV (P) al conjunto de las variables libres en P. Un t´rmino cerrado es un t´rmino sin variables libres. e e

Ejemplos

(λx.x y ) Observamos que

(λx.x (λx.x)) x

una misma variable puede ocurrir libre y ligada distintas ocurrencias pueden ligarse a distintas ocurrencias de ligadura la ligadura depende de toda la expresi´n o (una ocurrencia cambia de”status” de una subexpresi´n a la o expresi´n final; ej: x vs. (λx.x)) o

Ejercicio
Dar las variables libres y las ligaduras y sus alcances en el t´rmino e (λy .y x (λx.y (λy .z) x)) v w

Substituci´n o
Definici´n (Substituci´n) o o
Para todo M, N, x se define M[N/x] como el resultado de substituir N por toda ocurrencia libre de x en M. M´s a precisamente, por inducci´n sobre la estructura deM. o x[N/x] ≡N a[N/x] ≡a (P Q)[N/x] ≡ (P[N/x] Q[N/x]) (λx.P)[N/x] ≡ λx.P (λy .P)[N/x] ≡ λy .P (λy .P)[N/x] ≡ λy .P[N/x] (λy .P)[N/x] ≡ λz.(P[z/y ])[N/x]

(a ≡ x)

if x ∈ FV (P) ∧ y ≡ x if x ∈ FV (P) ∧ y ∈ FV (N) if x ∈ FV (P) ∧ y ∈ FV (N)

Asumimos que y ≡ x y que z es la 1er variable ∈ FV (N P)

α-equivalencia

Dado una ocurrencia de λx.M en un t´rmino P, si y no e ocurre en M podemosreemplazar λx.M por: λy .(M[y /x]) Esta operaci´n se llama cambio de variable ligada o o α-conversi´n. o Si P puede cambiarse a Q por una serie finita de cambios de variable ligada decimos que P es congruente con Q, o que P α-convierte a Q, o P ≡α Q Ejemplo: λx y .x (x y ) ≡α λu v .u (u v ) (Probarlo!)

Propiedades de la α-conversi´n o
Lema
a) Si P ≡α Q entonces FV (P) = FV (Q) b) La...