Encuentro 6 - 11/8/2012 - Calculo Lambda Tipado

TALLER DE LENGUAJES: 06 (11/08/12)

Repaso de la clase pasada:

  Calculo Lambda básico:

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

      [MU] t1->t1'
_______________

t1 t2 -> t1' t2


      [NU] t2->t2'
_______________

t1 t2 -> t1 t2'


      [XI]   t->t'
_______________

 \x.t -> \x.t'

      [ETA]  (\x.t) x -> t


    Call by Value:

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

t1 t2 -> t1' t2


      [NU CBV]   t2->t2'
_______________

v t2 -> v t2'

    -----------------------------------------------------

    Call by Name:

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

      [MU CBN]    t1->t1'
_______________

t1 t2 -> t1' t2


    Veamos el ejemplo de la otra vez:

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


    Hagamos la reducción usando Call by Value:

      [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


    Ahora, hagamoslo por Call by Name:

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

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

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

    Hay que notar que ambos llegan a z!

    
    Pensemos en las representaciones de los valores:

      zero  = \s.\z.z
      false = \t.\f.f

    Que loco, son el mismo término!

    Se pueden representar estos tipos tanto definiendolos como lambdas como agregandolos a los términos del lenguaje, así:

      t ::= x | \x:T.t | t t | true | false | if t then t else t | 0 | succ t | pred t | isZero t <- Notar que metimos el tipo en el lambda

      v  ::= \x:T.t | true | false | vn
      vn ::= 0 | succ vn

    Usar esta forma me permite diferenciar tipos (o sea, el zero es numerico y el false no. Pero si están representados por lo mismo no puedo distinguirlos).


  A Tiparla...:

    T ::= T -> T | Bool | Num

    [VAR]  x:T perteneceA G
 _________________

    G |- x : T


    [ABS]  G,x : T1 |- t : T2 <- G es un conjunto de suposiciones. acá estoy diciendo: "Si supongo que x es de tipo T1, entre otras cosas..."
 _______________________

 G + (\x:T1.t): T1 -> T2


    G ::= vacío | G , x : T


      Ej: (\y:Num.(\x:Bool.if x then 0 else y))


x:Bool c- G    y:Bool c- G
____________            ____________

G |- x:Bool    G |- 0:Num    G |-y:Num
__________________________________________

G = y:Num, x:Bool |- if x then 0 else y : Num <- voy a decirle G a {y:Num, x:Bool} para no repetir tanto...
_________________________________________________

y:Num |- \x:Bool.if x then 0 else y : Bool -> Num
_______________________________________________________________
  
|- \y:Num.\x:Bool.if x then 0 else y : Num -> Bool -> Num <- no pongo el contexto porque es vacío


    [APP] G |- t1:S->T G |- t2:S
 ________________________________

 G |- t1 t2 : T

      Ej:
 
x:Num      |- isZero x:Bool
______________________________

|- (\x:Num.isZero x):Num->Bool |- 0:Num
___________________________________________________

(\x:Num.isZero x) 0 : Bool


      Ej2:

      ______________________________[VAR]     __________________________[VAR] <- pongo así para no escribirlo, se aplica VAR.

      x:Num->Bool, y:Num |- x:Num->Bool   x:Num->Bool, y:Num |- y:Num 
      ______________________________________________________________________

      x:Num->Bool, y:Num |- x y : Bool
      __________________________________________

      x:Num->Bool |-(\y:Num.x y):Num->Bool
      _____________________________________________________

      |- (\x:Num->Bool.\y:Num.x y) : (Num->Bool)->Num->Bool



  EJERCICIO:

    Hacer la función:

      f(x,y) = x == 0 && y == 0

    Y demostrar que tipa.


    SOLUCION:

      and := \x.:Bool\y:Bool.if x then y else false

      f := \a:Num.\b:Num.and (isZero a) (isZero b)

      Tipo de and:

 ... ... ...
_______[VAR] _______[VAR]  ____________________[TFALSE]

x:Bool, y:Bool |- if x then y else false : Bool
_____________________________________________________________[ABS]

x:Bool |- \y:Bool.if x then y else false : Bool -> Bool
_____________________________________________________________[ABS]

\x.:Bool\y:Bool.if x then y else false : Bool -> Bool -> Bool


      Tipo de f:

... ...
___________________________[ABS] ______________[ISZERO]

G |- and : Bool->Bool->Bool isZero x : Bool ...
_________________________________________________[APP] _____________________[ISZERO]

G |- and (isZero x) : Bool->Bool G |- isZero y : Bool
______________________________________________________________________________[APP]

x:Num, y:Num |- (and (isZero x)) (isZero y): Bool
________________________________________________________[ABS]

x:Num |- \y:Num.(and (isZero x)) (isZero y): Num -> Bool
__________________________________________________________________[ABS]

\x:Num.\y:Num.(and (isZero x)) (isZero y) : Num -> Num -> Bool



 -------------------------------------------------------------------------------------------------------------------

  Tarea:

    * Demostrar que esto es verdad:

      G |-t:T => (-V-G'.G c G' => G'|-t:T)

      "Si sigo agregando variables al contexto de un programa que tipa, sigue tipando"


    * Chequear el tipo y adivinar que es T:

      ((\x:T.x 2) (\y:Num.\z:Bool.if z then 3 else y)) false
Comments