Diferencia entre revisiones de «Práctica 2 (pre 2010, Paradigmas)»
(No se muestran 2 ediciones intermedias del mismo usuario) | |||
Línea 2: | Línea 2: | ||
{{Back|Paradigmas de Lenguajes de Programación}} | {{Back|Paradigmas de Lenguajes de Programación}} | ||
= | Bzdbxo <a href="http://upivjvetxxfd.com/">upivjvetxxfd</a>, [url=http://epbdiyqsufem.com/]epbdiyqsufem[/url], [link=http://cyzodjjrjtku.com/]cyzodjjrjtku[/link], http://hlmltrfyirwp.com/ | ||
= | |||
= Semantica Operacional = | = Semantica Operacional = | ||
Línea 191: | Línea 118: | ||
== Ejercicio 27 == | == Ejercicio 27 == | ||
== Ejercicio 28 == | == 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) | pred(n) = search(λx -> succ(x)>=n) | ||
Línea 197: | Línea 133: | ||
== Ejercicio 30 == | == Ejercicio 30 == | ||
''Este ejercicio extiende el Calculo Lambda tipado con listas. Comenzamos ampliando el conjunto de tipos:'' | |||
<math> \sigma ::= nat | bool | \sigma \rightarrow \sigma | \sigma \times \sigma | [\sigma ] </math> | |||
''donde <math>[\sigma ]</math> representa el tipo de las listas cuyas componentes son de tipo <math>\sigma </math>. El conjunto de terminos ahora | |||
incluye:'' | |||
<math>M ::= . . . | nil _{\sigma} | M :: N | case_{\sigma} M of \{ nil \rightarrow P | h :: t \rightarrow Q \} </math> | |||
''donde <math>nil _{\sigma}</math> es la lista vacia cuyos elementos son de tipo <math>\sigma</math>, <math>M :: N</math> agrega M a la lista N y <math>case</math> 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' | |||
== Ejercicio 31 == | == Ejercicio 31 == | ||
[[Category:Prácticas]] | [[Category:Prácticas]] |
Revisión del 06:44 19 may 2008
Bzdbxo <a href="http://upivjvetxxfd.com/">upivjvetxxfd</a>, [url=http://epbdiyqsufem.com/]epbdiyqsufem[/url], [link=http://cyzodjjrjtku.com/]cyzodjjrjtku[/link], http://hlmltrfyirwp.com/
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
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'