Práctica 3 (pre 2010, Paradigmas)

Ejercicio 02

• a.

λx. λy. λz . (z x) y z 
           |(ABS)
λy. λz . (z x) y z
           |(ABS)
λz . (z x) y z
           |(ABS)
    (z x) y z
    |         |  (APP)
   (z x) y    z:s4
  |      | (APP)
 (z x)   y:s3
 |   | (APP)
z:s1 x:s2

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)

• (APP) S = MGU {s1=s2->s5}={s2->s5/s1} ; Γ = {z:s2->s5,x:s2} |> z x : s5
• (APP) S = MGU {s5=s3->s6}={s3->s6/s5} ; Γ = {z:s2->(s3->s6),x:s2,y:s3} |> (z x) y : s6
• (APP) S = MGU {s6=s4->s7,s4=s2->(s3->s6)}={s2->(s3->s6)/s4,(s2->(s3->s6))->s7/s6}

De lo anterior se puede ver que s6 es un tipo infinito -> FALLA.

• b.

λx. x (w (λy.w y)) 
       |(ABS)
  x (w (λy.w y)) 
 |            |   (APP)
x:s1      (w (λy.w y)) 
           |      |   (APP)
         w:s2  (λy.w y)
                 |  (ABS)
                w y
               |    | (APP)
              w:s3 y:s4

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)

• (APP) S = MGU {s3=s4->s5}={s4->s5/s3} ; Γ = {w:s4->s5,y:s4} |> w y : s5
• (ABS) Γ = {w:s4->s5} |> λy:s4.xy : s4->s5
• (APP) S = MGU {s2=s4->s5,s2=(s4->s5)->s6}={s4->s5=(s4->s5)->s6}={(s4->s5)->s6/(s4->s5)}

De lo anterior se puede ver que (s4->s5) es un tipo infinito -> FALLA.

• c.

( λz. λx. x (z (λy. z)) ) True
     |                      | (APP)
λz. λx. x (z (λy. z))     True:bool
   | (ABS)
λx. x (z (λy. z))
   | (ABS)
x (z (λy. z))
  |    | (APP)
x:s1 (z (λy. z))
       |    | (APP)
     z:s2  (λy. z)
             | (ABS)
            z:s3

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)

• (ABS) Γ = {z:s3} |> λy:s4. z : s4->s3
• (APP) S = MGU {s2=s3,s2=(s4->s3)->s5}={s3=(s4->s3)->s5}={(s4->s3)->s5/s3}

De lo anterior se puede ver que s3 es un tipo infinito -> FALLA.

Ejercicio 09

Extender el algoritmo de inferencia para soportar la inferencia de tipos de arboles binarios. En esta extension del algoritmo solo se consideraran los constructores del arbol.

Respuesta:

Sean 0 el contexto vacio, G el contexto gamma, U la union, _s sub sigma, =:= la unificacion de tipos:

W(nil_s) = 0 |> nil_s : ABs

W(bin_s(M,N,O)) = SG1 U SG2 U SG3 |> S(bin_s(M,N,O)) : ABs donde
 W(M) = G1 |> M : rho
 W(N) = G2 |> N : tau
 W(O) = G3 |> O : phi
 S = MGU {tau =:= s, rho =:= ABs, phi =:= ABs} U
      U {mu1 =:= mu2 | x : mu1 in Gi, x : mu2 in Gj, i != j}

Escribir las reglas de tipado e inferencia para el case de arboles binarios, y la regla analoga en el algoritmo de inferencia.