Práctica 2 (pre 2010, Paradigmas)

Generalidades

Ejercicio 01

Para los siguientes términos:

1. ux(yz)(λv.vy)
2. (λxyz.xz(yz))uvw
3. w(λxyz.xz(yz))uv

Se pide:

1. Insertar todos los paréntesis de acuerdo a la convención usual.
2. Indicar cuáles ocurrencias de variables aparecen ligadas y cuáles libres.
3. ¿En cuál de los términos anteriores ocurre (λxyz.xz(yz))u ?
4. ¿Cuáles de los términos anteriores son formas normales?
5. ¿Ocurre x(yz) en ux(yz)?

Rta:

1. Alguien que me explique esto.

2. (negrita ligada, italica libre)

1. ux(yz)(λv.vy)
2. (λxyz.xz(yz))uvw
3. w(λxyz.xz(yz))uv

3. Que quiere decir "ocurre"?

4. Forma normal es que no pueda beta-reducirse más. Creo que el primero.

5. Que quiere decir "ocurre"?

Ejercicio 02

Mostrar un término que no sea tipable y que no tenga variables libres ni abstracciones.

Rta:

if 0 then true else false

Para mi iria algo como este (cumple con la forma M N y no cumple ninguna regla de tipado):

true false

Ejercicio 03

Sean σ, τ , ρ tipos. Según la definición de sustitución, calcular:

1. (λy : σ.x(λx : τ .x)) {x ← (λy : ρ.xy)}
2. (y(λv : σ.xv)) {x ← (λy : τ .vy)}

Renombrar variables en ambos términos para poder evaluarlos con mayor facilidad.

Rta:

1. (λy : σ.(λz : ρ.xz)(λx : τ .x))
2. (y(λv : σ.(λy : τ .zy)v))

Ejercicio 04

Utilizando la definición de substitución usual, la noción de longitud de un término M notada |M|, y la nocion de subtermino, notada con ⊆, probar:

1. M {x ← x} = M
2. |M {x ← y}| = |M |
3. si x ̸∈ F V (M ) entonces M {x ← N } = M
4. si M ⊆ E entonces |M | ≤ |E|
5. |E{x ← M }| ≥ |E|. ¿En que casos vale la igualdad?

Rta:

1. Sale
2. Sale
3. Sale
4. Sale
5. Sale. Cuando M es una variable vale la igualdad.

Semantica Operacional

Ejercicio 05

Calcular las formas normales de los siguientes términos :

1. (λx : Bool, y.Bool → Bool.yx)true(λx : Bool.x)
2. (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
3. (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
4. S S S S S S S , donde S = λx : Bool → Bool → Bool, y : Bool → Bool, z : Bool.xz (yz )

Rta:

1. true
2. false
3. false, igual a la anterior? no entiendo si está mal el enunciado.

Ejercicio 06

1. Supongamos que if M then P else Q → D. ¿Es cierto que D tendrá necesariamente la forma if M′ then P′ else Q′ ?
2. Supongamos que M →→ M′ , P →→ P′ , Q →→ Q′ . ¿Es cierto que if M then P else Q →→ if M′ then P′ else Q′ ?

Rta:

1. No,

   if true then P else Q

   se convierte en P.
2. No, termina siendo P' o Q' en muchos pasos y

   if M' then P else Q

   en un paso.

Ejercicio 08

Hallar un término M tal que se cumpla:

1. M 3 →→ true
2. M n →→ false si n != 3

Rta:'

1. M = (\x.true)
2. M = (\x.false). - notar que no dice que debe pasar cuando n==3 asi que está bien ;)

Tipado

Ejercicio 17

Probar que

1. x : Bool, y : Bool |> if x then x else y : Bool
2. x : Bool -> Bool, y : Bool |> if xy then y else xy : Bool

Item 1

Sea el contexto G = x : Bool, y : Bool

3 x : Bool in G  x : Bool in G  y : Bool in G 
2 G |> x : Bool  G |> x : Bool  G |> y : Bool
1 G |> if x then x else y : Bool
0 x : Bool, y : Bool |> if x then x else y : Bool

Pasos: 1 renombre, 2 T-If, 3 T-Var

Ejercicio 18

Sean s, t y r tipos (en el original, sigma, tau y rho). Definimos los siguientes terminos:

S str = \x : s -> t -> r, y : s -> t, z : s . xz(yz)
K st  = \x : s, y : t . x
id s  = \x : s . x

Usando las definiciones anteriores, probar que valen:

1. |> S str : (s -> t -> r) -> (s -> t) -> (s -> r)
2. |> S str K st : (s -> t) -> s -> s
3. |> K st id s : t -> s -> s

Item 1

5. x : s->t->r in G  z : s in G  y : s->t in G  z : s in G
4. G |> x : s->t->r  G |> z : s  G |> y : s->t  G |> z : s
3. G |> xz : t->r  G |> yz : t
2. G |> xz(yz) : r
1. x : s->t->r, y : s->t, z : s |> xz(yz) : r
0. |> (\x : s -> t -> r, y : s -> t, z : s . xz(yz)) : (s -> t -> r) -> (s -> t) -> (s -> r)

Pasos: 1 T-Abs, 2 Renombre, 3 T-App, 4 T-App, 5 T-Var; vale que G = x : s->t->r, y : s->t, z : s.

Item 2

|> S str K st : (s -> t) -> s -> s

Item 3

2. Como tipa esto? Me daria s = t? Esta ok? Help!
1. |> (\x : s, y : t . x) : s->s->t->s->s  |> (\x : s . x) : s->s
0. |> (\x : s, y : t . x) (\x : s . x) : t -> s -> s

Pasos: 1 T-App

Extensiones

Ejercicio 28

pred(n) = search(λx -> succ(x)>=n)

Ejercicio 29

• 1. if M then P else Q = case_unit,unit,τ MPQ