Diferencia entre revisiones de «Práctica 2 (pre 2010, Paradigmas)»
(Sin diferencias)
|
Revisión del 21:08 17 feb 2009
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 ;)
Edit: Me parece que lo que se pide es un M que verifique AMBAS cosas a la vez. Suponiendo eso, una solución posible es:
M = (\x:Nat. if (isZero(pred(pred(x)))) then false else (if (isZero(pred(pred(pred(x))))) then true else false))
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
Considerar la siguiente definicion:
search = \p : nat -> bool .letrec f(x : nat) : nat = if (p x) then x else f(x + 1) in f0
Definir la funcion predecesor pred usando search. En el caso de 0 definir pred de manera que pred 0 ->> 0.
Respuesta:
pred(n) = search(λx -> succ(x)>=n)
Ejercicio 29
- 1. if M then P else Q = caseunit,unit,τ MPQ
Ejercicio 30
Este ejercicio extiende el Calculo Lambda tipado con listas. Comenzamos ampliando el conjunto de tipos:
donde representa el tipo de las listas cuyas componentes son de tipo . El conjunto de terminos ahora incluye:
donde es la lista vacia cuyos elementos son de tipo , agrega M a la lista N y es el observador de listas (h y t son variables que se ligan en Q).
- Agregar reglas de tipado para las nuevas expresiones.
- Agregar los (dos) axiomas de reduccion asociados a las nuevas expresiones.
Reglas de tipado
En las siguientes reglas, reemplazar s por sigma. Gamma o G representa el contexto, y tau un tipo generico.
T-Nil
---------------------- Gamma |> nil_s : [s]
T-Cons
Gamma |> M : s Gamma |> N : [s] -------------------------------- Gamma |> M :: N : [s]
T-Case
G |> M : [s] G |> P : tau G union {h : s, t : [s]} |> Q : tau --------------------------------------------------------------- Gamma |> case_s M of (nil -> P | h::t -> Q) : tau
Axiomas de reduccion
Case
M -> M' -------------------------------------------------------------------------- case_s M of (nil -> P | h::t -> Q) -> case_s M' of (nil -> P | h::t -> Q)
-------------------------------------------- case_s nil_s of (nil -> P | h::t -> Q) -> P
----------------------------------------------------------- case_s A::B of (nil -> P | h::t -> Q) -> Q [h <- A, t <- B]
Constructores
H -> H' ------------- H::T -> H'::T
T -> T' ------------- H::T -> H::T'