Práctica 2 (pre 2010, Paradigmas)
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
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