Práctica 3 (pre 2010, Paradigmas)

De Cuba-Wiki
Saltar a: navegación, buscar
Back.png Volver a la página de la materia

Ejercicio 01[editar]

Ejercicio 02[editar]

  • 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 03[editar]

Ejercicio 04[editar]

Ejercicio 05[editar]

Ejercicio 06[editar]

Ejercicio 07[editar]

Ejercicio 08[editar]

Ejercicio 09[editar]

Item A[editar]

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[editar]

donde

Item B[editar]

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

Respuesta[editar]

donde

Ejercicio 10[editar]