Diferencia entre revisiones de «Práctica 2 (pre 2010, Paradigmas)»
Sin resumen de edición |
|||
(No se muestran 7 ediciones intermedias del mismo usuario) | |||
Línea 5: | Línea 5: | ||
== Ejercicio 01 == | == 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.'''v'''''y'') | |||
# (λ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 == | == 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 == | == 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 == | == 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 = | = Semantica Operacional = | ||
== Ejercicio 05 == | == 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 == | == 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, <pre>if true then P else Q</pre> se convierte en P. | |||
# No, termina siendo P' o Q' en muchos pasos y <pre>if M' then P else Q</pre>en un paso. | |||
== Ejercicio 07 == | == Ejercicio 07 == | ||
== Ejercicio 08 == | == 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 09 == | ||
== Ejercicio 10 == | == Ejercicio 10 == |
Revisión del 23:15 12 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 ;)