Práctica 2 (pre 2010, Paradigmas)

De Cuba-Wiki
Saltar a: navegación, buscar
Back.png Volver a la página de la materia

Semantica Operacional[editar]

Ejercicio 05[editar]

Calcular las formas normales de los siguientes términos :

  1. (λx : Bool, y.Bool → Bool.yx)true(λx : Bool.x)
  2. (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
  3. (λx : Bool, y.Bool → Bool.y(yx))false(λx : Bool.x)
  4. S S S S S S S , donde S = λx : Bool → Bool → Bool, y : Bool → Bool, z : Bool.xz (yz )

Rta:

  1. true
  2. false
  3. false, igual a la anterior? no entiendo si está mal el enunciado.

Ejercicio 06[editar]

  1. Supongamos que if M then P else Q → D. ¿Es cierto que D tendrá necesariamente la forma if M′ then P′ else Q′ ?
  2. Supongamos que M →→ M′ , P →→ P′ , Q →→ Q′ . ¿Es cierto que if M then P else Q →→ if M′ then P′ else Q′ ?

Rta:

  1. No,
    if true then P else Q
    se convierte en P.
  2. No, termina siendo P' o Q' en muchos pasos y
    if M' then P else Q
    en un paso.

Ejercicio 07[editar]

Ejercicio 08[editar]

Hallar un término M tal que se cumpla:

  1. M 3 →→ true
  2. M n →→ false si n != 3

Rta:'

  1. M = (\x.true)
  2. 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[editar]

Ejercicio 10[editar]

Ejercicio 11[editar]

Ejercicio 12[editar]

Ejercicio 13[editar]

Ejercicio 14[editar]

Ejercicio 15[editar]

Ejercicio 16[editar]

Tipado[editar]

Ejercicio 17[editar]

Probar que

  1. x : Bool, y : Bool |> if x then x else y : Bool
  2. 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[editar]

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[editar]

Ejercicio 20[editar]

Ejercicio 21[editar]

Ejercicio 22[editar]

Ejercicio 23[editar]

Ejercicio 24[editar]

Ejercicio 25[editar]

Ejercicio 26[editar]

Extensiones[editar]

Ejercicio 27[editar]

Ejercicio 28[editar]

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[editar]

  • 1. if M then P else Q = caseunit,unit,τ MPQ

Ejercicio 30[editar]

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).

  1. Agregar reglas de tipado para las nuevas expresiones.
  2. 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'

Ejercicio 31[editar]