Práctica 2 (pre 2010, Paradigmas)

Semantica Operacional

Ejercicio 05

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

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 08

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

Tipado

Ejercicio 17

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

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

Extensiones

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 = case_unit,unit,τ MPQ

Ejercicio 30

Este ejercicio extiende el Calculo Lambda tipado con listas. Comenzamos ampliando el conjunto de tipos:

$\sigma ::=nat|bool|\sigma \rightarrow \sigma |\sigma \times \sigma |[\sigma ]$

donde $[\sigma ]$ representa el tipo de las listas cuyas componentes son de tipo $\sigma$. El conjunto de terminos ahora incluye:

$M::=...|nil_{\sigma }|M::N|case_{\sigma }Mof\{nil\rightarrow P|h::t\rightarrow Q\}$

donde $nil_{\sigma }$ es la lista vacia cuyos elementos son de tipo $\sigma$, $M::N$ agrega M a la lista N y $case$ 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'