Diferencia entre revisiones de «Práctica 2 (pre 2010, Paradigmas)»
Línea 142: | Línea 142: | ||
== Ejercicio 18 == | == 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 | |||
== Ejercicio 19 == | == Ejercicio 19 == | ||
== Ejercicio 20 == | == Ejercicio 20 == |
Revisión del 19:02 27 abr 2008
Generalidades
Ejercicio 01
Para los siguientes términos:
- ux(yz)(λv.vy)
- (λxyz.xz(yz))uvw
- w(λxyz.xz(yz))uv
Se pide:
- Insertar todos los paréntesis de acuerdo a la convención usual.
- Indicar cuáles ocurrencias de variables aparecen ligadas y cuáles libres.
- ¿En cuál de los términos anteriores ocurre (λxyz.xz(yz))u ?
- ¿Cuáles de los términos anteriores son formas normales?
- ¿Ocurre x(yz) en ux(yz)?
Rta:
1. Alguien que me explique esto.
2. (negrita ligada, italica libre)
- ux(yz)(λv.vy)
- (λxyz.xz(yz))uvw
- 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:
- (λy : σ.x(λx : τ .x)) {x ← (λy : ρ.xy)}
- (y(λv : σ.xv)) {x ← (λy : τ .vy)}
Renombrar variables en ambos términos para poder evaluarlos con mayor facilidad.
Rta:
- (λy : σ.(λz : ρ.xz)(λx : τ .x))
- (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:
- M {x ← x} = M
- |M {x ← y}| = |M |
- si x ̸∈ F V (M ) entonces M {x ← N } = M
- si M ⊆ E entonces |M | ≤ |E|
- |E{x ← M }| ≥ |E|. ¿En que casos vale la igualdad?
Rta:
- Sale
- Sale
- Sale
- Sale
- Sale. Cuando M es una variable vale la igualdad.
Semantica Operacional
Ejercicio 05
Calcular las formas normales de los siguientes términos :
- (λx : Bool, y.Bool → Bool.yx)true(λx : Bool.x)
- (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
- (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
- S S S S S S S , donde S = λx : Bool → Bool → Bool, y : Bool → Bool, z : Bool.xz (yz )
Rta:
- true
- false
- false, igual a la anterior? no entiendo si está mal el enunciado.
Ejercicio 06
- Supongamos que if M then P else Q → D. ¿Es cierto que D tendrá necesariamente la forma if M′ then P′ else Q′ ?
- Supongamos que M →→ M′ , P →→ P′ , Q →→ Q′ . ¿Es cierto que if M then P else Q →→ if M′ then P′ else Q′ ?
Rta:
- No,
if true then P else Q
se convierte en P. - No, termina siendo P' o Q' en muchos pasos y
if M' then P else Q
en un paso.
Ejercicio 07
Ejercicio 08
Hallar un término M tal que se cumpla:
- M 3 →→ true
- M n →→ false si n != 3
Rta:'
- M = (\x.true)
- M = (\x.false). - notar que no dice que debe pasar cuando n==3 asi que está bien ;)
Ejercicio 09
Ejercicio 10
Ejercicio 11
Ejercicio 12
Ejercicio 13
Ejercicio 14
Ejercicio 15
Ejercicio 16
Tipado
Ejercicio 17
Probar que
- x : Bool, y : Bool |> if x then x else y : Bool
- 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
Ejercicio 19
Ejercicio 20
Ejercicio 21
Ejercicio 22
Ejercicio 23
Ejercicio 24
Ejercicio 25
Ejercicio 26
Extensiones
Ejercicio 27
Ejercicio 28
pred(n) = search(λx -> succ(x)>=n)
Ejercicio 29
- 1. if M then P else Q = caseunit,unit,τ MPQ