Encuentro 5 - 29/7/2012 - Cálculo Lambda 2

TALLER DE LENGUAJES: 05 (29/07/12)

Repaso de la clase pasada:

Calculo Lambda:

Un lenguaje de programación que no sirve para programar.

SINTAXIS

t ::= x | \x.t | t t <- variable | abstracción | aplicación
v ::= \x.t

Un ejemplo de programa:

(\x.x) (\y.y z)

Acá vemos que las ocurrencias de x e y están ligadas y la de z está libre.

En un programa bien fundado no hay variables libres, pero en un pedacito de programa sí podría (estaría ligada más afuera).

EVALUACION

[BETA] (\x.t) u -> t{x:=u}

x{x:=u} := u
y{x:=u} := y con y!=x
(t1 t2){x:=u} := t1{x:=u} t2{x:=u}
(\y.t){x:=u} := \y.t{x:=u} con x!=y & y no pertence a FV(t) <- FV: Free Variables
FV(x)     = {x}
FV(t1 t2) = FV(t1) U FV(t2)
FV(\x.t)  = FV(t) - {x}
Ojo:

(\x.(\y.x)) y

Si no me avivo, podría reducir esto a:

(\y.y)

Esto sería un error... y no debería quedar ligada.

CONVENCION DE VARIABLES: En todos los contextos los nombres de las variables ligadas son distintos entre si y con cada una de las variables de ocurrencia libres


Ahora, guarda. Si solo tengo BETA para reducir, un programa como:

(\x.(\y.y) x)

NO sería un Redex.

Entonces se agregan otras reglas, para poder reducir.

[MU] t1->t1'
_______________

t1 t2 -> t1' t2


[NU] t2->t2'
_______________

t1 t2 -> t1 t2'


[PSI]   t->t'
 _______________

  \x.t -> \x.t'


_()_ = (\x.x x) (\x.x x) <- OMEGÓN!: Un término muy puto que reduce a si mismo.


(\x.\y.x) z _()_ <- Esto puede reducir a z o a _()_ . Esto pasa porque hay más de un Redex. Depende de como juego con las reglas.


Cómo cambiamos las reglas para tener otras estratégias de evaluación?

* Una forma es dejarlo así, no deterministico y fumartelo todo. Probablemente no puedas programarlo en una computadora...

* Otra es decidir otras reglas para garantizar que NUNCA le paso a una aplicación un parámetro que no esté totalmente evaluado.

[BETA CBV] (\x.t) v -> t{x:=v} CVB: Call By Value
[MU CBV] t1->t1'
_______________
t1 t2 -> t1' t2


[NU CBV]   t2->t2'
_______________

 v t2 -> v t2'


Para que estas reglas terminen de servir, hay que volver a las variables valores.

Notar que NO PUEDO reducir el parámetro hasta que la función no sea un valor; y no puedo aplicar [BETA CVB] hasta no llegar a que ambos son valores.
Este conjunto es el que usan los lenguajes clásicos como Java.

Ej:

((\x.\y.x) z) ((\w.w) v)

[MU CVB] (\x.\y.x) z -> \y.z
____________________________________________

((\x.\y.x) z) ((\w.w) v) -> (\y.z) ((\w.w)v)

[NU CVB] (\y.z) ((\w.w)v) -> (\y.z) v

[BETA CVB] (\y.z) v -> z


--------------------------------------------------------------------------------------------------------------------
TAREA:

* Tratar de definir reglas que permitan una estrategia de evaluación parecida a la de Haskell (Call By Name).
* Probar por inducción que en la estrategia CBV solo una regla aplica para cada posible término (Que es deterministico).
* Implementar el cálculo lambda en algún lenguaje.
* Bajarse el código en Scala con la implementación del BoolNat y...
- Usarlo de base para implementar el Lambda
- Extraer un Trait de BoolNatSyntax SOLO para los Bool y hacer que BoolNatSyntax lo extienda
- Extraer un Trait de BoolNatSyntax SOLO para los Bool y otro SOLO para los Nat y hacer que BoolNatSyntax los extienda
- Y bueno, seguir partiendo los traits y ver que funcionan por separado y juntandolos, etc. Práctica de Scala.

Comments