Diferencia entre revisiones de «Práctica 2 (pre 2010, Paradigmas)»
Línea 142: | Línea 142: | ||
== Ejercicio 29 == | == Ejercicio 29 == | ||
*1. if M then P else Q = case(unit,unit,τ) MPQ | |||
== Ejercicio 30 == | == Ejercicio 30 == | ||
== Ejercicio 31 == | == Ejercicio 31 == | ||
[[Category:Prácticas]] | [[Category:Prácticas]] |
Revisión del 19:13 25 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
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 = case(unit,unit,τ) MPQ