P3

/*
* Ej 1
*/
a) No, falta .
b) Sí, (((x y) z) (y x))
c) Sí, (λx.((u x) y))
d) Sí, (λu.(u (λx.y)))
e) No, falta t ∈ Λ
f) Sí, (((λu.((v u) u)) z) y)
g) Sí, (λx.(y (λz.z)))
h) Sí, (((u x) (y z)) (λv.(v y)))
i) Sí, ((((λx.(λy.(λz.((x z) (y z))))) u) v) w)

/*
* Ej 2
* Mayus -> Ocurrencia
*/
a) λx y.X Y
b) x (U V) (λu.v (U V)) u v
c) λu.u v

/*
* Ej 3
* L -> Ligadura
* l -> Ligada
* F -> Free
*/
a) (λy.y (λx.x) z)
 x:        L←l
 y:  L←l
 z:             F

b) (λy.x (λx.x) z)
 x:    F   L←l
 y:  L
 z:             F

c) (λy.y (λy.y) y x)
 x:               F
 y:  L←l   L←l  l
     ↑          ↓
     ↖←←←←←←←←←←↙

d) (λy.y (λx.y)) y x
 x:        L       F
 y:  L←l     l   F
     ↑       ↓
     ↖←←←←←←←↙

e) (λx y z.x (λy.y z) w) (λx.x y) w z
 x:  L←←←←←l               L←l
 y:    L       L←l             F
 z:      L←←←←←←←←←l                F
 w:                   F           F

f) (λx x.x y (λy y.x y)) x
 x:  L L←l         l     F
       ↑           ↓
       ↖←←←←←←←←←←←↙
 y:        F   L L←←←l

/*
* Ej 4
*/
a) (λy.y (λx.x) z) [(λw.w t)/z] =
   (λy.y (λx.x) (λw.w t))

b) ((λy.y (λx.x)) z) [(λw.w t)/z] =
   ((λy.y (λx.x)) (λw.w t))

c) (λy.x (λx.x) z) [(λw.w t)/z] =
   (λy.x (λx.x) (λw.w t))

d) (λy.x (λx.x) z) [(λw.w y)/z] =
   (λv.x (λx.x) (λw.w y))

e) (λy.y z) [z/y] =
   (λy.y z)

f) (λy.y z) [y/z] =
   (λw.(y z)[w/y]) [y/z] =
   (λw.w z) [y/z] =
   (λw.w y)

/*
* Ej 5
*/
a) No, están asociados de forma distinta
b) No, cambió la variable libre w
c) No, están asociados de forma distinta
d) No, cambia la relación de ligadura entre la primer
ocurrencia λz y la siguiente variable z asociada a esta
e) (λx y z.x (λy.y z) w) α=
                         z←t
   (λx y t.x (λy.y t) w) α=
                         x←v
   (λv y t.v (λy.y t) w) α=
                         y←u
   (λv u t.v (λu.u t) w) α=
                         u←v en (λu.u t)
   (λv u t.v (λv.v t) w)

/*
* Ej 6
*/
a) (λx. λy. x y) (λy. y z)   β=
        ---M---- ----N----
                            M[N/x]

   (λy. (λy. y z) y)         β=
       ----M1--- N1
                            M1[N1/y]

   (λy.y z)

b) (λx.λy.x y) (λz.y z) z    β=
               ----M--- N
                            M[N/z]

   (λx.λy.x y) (λz.y z)      β=
       --M1--- ---N1---
                            M1[N1/x]

   (λy.(λz.y z) y)           β=
       ---M2--- N2
                            M2[N2/y]
   (λz.y z)

c) (λx.(λy.x) y λz.z) (λy.y z) β=
   (λy.(λy.y z)) y λz.z β=
   (λy.y z) λz.z β=
   (λz.z) z β=
   z