Ver el código de «Primer Parcial 2do Cuat 2007 (Paradigmas)»

__NOTOC__
{{Back|Paradigmas de Lenguajes de Programación}}

== Ejercicio 1: Programación funcional ==
Durante todo este ejercicio no se puede usar recursion explıcita. Para resolver un ıtem pueden 
utilizarse como existentes las soluciones a todos los anteriores, mas alla de si fueron resueltos 
correctamente o no. Tambien pueden usarse las funciones de la practica de programacion 
funcional, y de los modulos Prelude, List y Maybe de Haskell.

Durante este ejercicio traba jaremos con grafos bipartitos. Un grafo bipartito esta representa- 
do por 2 conjuntos de nodos A y B, que permitiremos que sean de distinto tipo, y un conjunto 
de ejes, donde cada eje es una asociacion entre dos nodos, uno de cada conjunto. Para re- 
presentarlos en Haskell usaremos el tipo GrafoBip con un unico constructor, cuya deﬁncion 
es: 

 data GrafoBip a b = GB [a] [b] (a → [b]) 

donde los primeros dos argumentos representan los conjuntos de nodos y el tercero la funcion 
vecinos, que dado un nodo a del conjunto A devuelve un subconjunto de B con los vecinos 
de a (o sea, por cada b ∈ vecinos(a) hay un eje a − b en el grafo). 

A menos que se aclare explıcitamente, puede asumirse que todas las listas son ﬁnitas. En 
cambio, no puede asumirse nada del comportamiento de la funci´on vecinos cuando a no 
pertenece al conjunto A. 

Diremos que un GrafoBip representa un grafo bipartito valido si 
Las listas representan conjuntos (i.e., no tienen elementos repetidos). Esto vale tanto 
para los conjuntos A y B como para las listas devueltas por la funcion vecinos. 
Los conjuntos devueltos por vecinos estan incluidos en el conjunto B. 
Se proveen las siguientes funciones auxiliares para mayor comodidad: 

 nodosA :: GrafoBip a b → [a] 
 nodosA (GB x _ _) = x 
 nodosB :: GrafoBip a b → [b] 
 nodosB (GB _ x _) = x 
 ejes :: GrafoBip a b →(a [b]) 
 ejes (GB _ _ x) = x 

==== Punto A ====
Escribir una funcion valido que dado un GrafoBip determine si representa 
un grafo bipartito valido. 

 valido :: Eq a, Eq b ⇒ GrafoBip a b → Bool

A partir de aqui se puede asumir que los argumentos de todas las funciones seran GrafoBips validos. Asimismo, las funciones que devuelven un GrafoBip siempre deben devolver uno valido.

'''Respuesta'''

 -- valido
 valido :: (Eq a, Eq b) => GrafoBip a b -> Bool
 valido g = (sinRepetir (nodosA g)) && (sinRepetir (nodosB g)) && vecinosOk
         where vecinos x = ejes g x
               sinRepetir xs = all (\x -> length (filter (==x) xs) == 1) xs
               vecinosOk = (all id [(sinRepetir (vecinos a)) && all (\x -> elem x (nodosB g)) (vecinos a) | a <- (nodosA g)])
 
 -- testvalido
 v1 = GB [1, 3, 5] [2, 4, 6] (\x -> [x + 1])
 v2 = GB [1, 2] [3, 4] (\x -> [x])
 v3 = GB [1, 1] [2, 3] (\x -> [x]

Otra version:

 -- valido
 valido :: (Eq a, Eq b) => GrafoBip a b -> Bool
 valido (GB a b v) = (sinRepetir a) && (sinRepetir b) && vecinosOk
         where sinRepetir xs = all (\x -> length (filter (==x) xs) == 1) xs
               subset z w = all (\e -> elem e w) z
               vecinosOk = all (\x -> subset (v x) b && sinRepetir (v x))

==== Punto B ====
Escribir una funcion invertir que dado un grafo bipartito devuelve uno 
isomorfo (con los mismos ejes) y los conjuntos A y B invertidos. 

 invertir :: Eq a, Eq b ⇒ GrafoBip a b → GrafoBip b a

'''Respuesta'''

 -- invertir
 invertir :: (Eq a, Eq b) => GrafoBip a b -> GrafoBip b a
 invertir (GB a b v) = (GB b a f)
         where f x = filter (\y -> elem x (v y)) a

==== Punto C ====
La union de un grafo bipartito de conjuntos A y B y ejes E y otro de conjuntos 
A′ y B′ y ejes E′ se deﬁne como el grafo bipartito de conjuntos A ∪ A′ y B ∪ B′ , y ejes 
E ∪ E′ . Notar que ninguno de estos conjuntos es necesariamente disjunto con el otro. 
Deﬁnir la funcion unionG, que compute la uni´on de dos grafos bipartitos. 

 unionG :: Eq a, Eq b ⇒ GrafoBip a b → GrafoBip a b → GrafoBip a b

'''Respuesta'''

 -- unionG
 unionG :: (Eq a, Eq b) => GrafoBip a b -> GrafoBip a b -> GrafoBip a b 
 unionG (GB a1 b1 v1) (GB a2 b2 v2) = (GB (unionD a1 a2) (unionD b1 b2) f)
         where unionD x y = x ++ (filter (\z -> not (elem z x)) y)
               f x = unionD (v1 x) (v2 x)

==== Punto D ====
Un matching de un grafo bipartito es una asociacion biyectiva entre los 
conjuntos A y B de manera que cada nodo a ∈ A est´a asociado a exactamente un nodo b ∈ B tal que b ∈ vecinos(a). Notar que todo nodo b debe estar a su vez asociado a exactamente un nodo de A. 

Representaremos un matching utilizando una funcion a -> b que indica con que nodo de 
B esta asociado cada nodo de A. Escribir una funci´on match que dado un grafo bipartito 
devuelva un matching, si existe uno. 

 match :: Eq a, Eq b ⇒ GrafoBip a b → Maybe (a → b) 

Si el matching existe, match debe devolver Just m donde m es un matching posible (si 
hay mas de uno se puede devolver cualquiera). Si el matching no existe, la funcion debe 
devolver Nothing. 

Sugerencia: Utilizar la funcion perms de la practica, que dada una lista devuelve la lista 
con todas sus permutaciones. 

perms :: [a] → [[a]]

'''Respuesta'''

La solucion es algo asi no tuve tiempo de verificar en hugs:

 match:: Eq a , Eq d => GrafoBip a b -> Maybe (a->b)
 match (GB as bs f) | length as /= length bs = Nothing
                   | otherwise =  buscarMatch as (perms bs) f

 buscarMatch:: eq a, Eq b =>[a] → [[b]]-> (a->[b])->Maybe(a->b)
 buscarMatch as pbs f = foldr g Nothing pbs
 where g rr pb | rr== Just m = Just m
               | hayMatch (zip as pb) f = Just (/a->pb!!(lugarDe a as))
               | otherwise= Nothing

 hayMatch::eq a, eqb=> [(a,b)]->(a->[b])->Bool
 hayMatch abs f = foldr (/rr (a,b) -> rr && b elem (f a)) True abs

==== Punto E ====
Escribir la expresion grafoDeNumeros deﬁnida como el grafo bipartito donde 
A son los numeros enteros positivos, B los pares ordenados de enteros positivos y existe 
un eje a − (b1 , b2 ) si y solamente si a · b1 ≥ b2 . 

Notar que tanto los nodos como los ejes de este grafo son inﬁnitos, con lo cual el GrafoBip 
que los represente tendr´a listas inﬁnitas (correspondientes a A, B y los conjuntos del 
codominio de vecinos). Las mismas pueden estar en cualquier orden, pero deben ser tales 
que todo elemento del conjunto aparezca eventualmente en la lista que lo representa. 

 grafoDeNumeros :: GrafoBip Int (Int,Int) 

Sugerencia: Utilizar listas por comprension.

== Ejercicio 2: Lámbda cálculo tipado ==
La aplicacion parcial sobre funciones curriﬁcadas es una de las ventajas de los lenguajes 
funcionales, como el calculo lambda tipado. Sin embargo, el mecanismo del calculo lambda 
(que se repite en la mayorıa de los lenguajes funcionales como Haskell) es limitado, ya que la 
aplicacion parcial debe hacerse siempre en el orden de los argumentos. Por ejemplo, si tenemos 
la funcion potencia, podemos usarla con aplicacion parcial para deﬁnir la funcion cuadrado, si 
su primer parametro es el exponente, o la funci´on dosALa si su primer parametro es la base, 
pero no podemos hacer ambas cosas con la misma funci´on potencia.

Para solucionar este problema introduciremos el mu calculo, que es igual al calculo lambda 
en todo, excepto en que el mecanismo para construir funciones (λx.M) y el mecanismo para 
aplicarlas (M N) seran sustituidos por un nuevo mecanismo de construccion <math>(\mu x_1,..., x_n.M)</math> y de aplicacion <math>(M \#_i\; N)</math>. Estos cambios tambien introducen un cambio en el sistema de tipos: en lugar de tener σ → τ tendremos <math>\{\sigma_1 ,..., \sigma_n\}</math> → τ . Notar que <math>\{\sigma_1 ,..., \sigma_n\}</math> no es un nuevo tipo, sino solo una parte del nuevo tipo para funciones. 

La sintaxis del mu calculo y su sistema de tipos, entonces, seran los siguientes: 

<math>M ::= ... \;|\; \mu x_1 , ..., x_n.M \;|\; M \#_i \; N</math>

<math>\sigma ::= ... \;|\; \{\sigma_1 , ..., \sigma_n\} \rightarrow \tau</math> 

El termino <math>\mu x_1 ,..., x_n.M</math> sirve para construir una nueva funcion de n parametros ordenados y el operador <math>\#_i</math> sirve para aplicar el i-esimo parametro. Notar que si la cantidad de parametros de una funcion es mayor a 1, al aplicarla se obtiene una nueva funcion con un parametro menos, pero si la cantidad de parametros es exactamente 1, al aplicarla se obtiene su valor de retorno. 

Notar ademas que que el orden de los tipos de los argumentos es importante: por ejemplo, 
{nat, nat, bool} → nat y {bool, nat, nat} → nat no son el mismo tipo.

==== Punto A ====
Introducir las reglas de tipado para la extension propuesta. 

'''Respuesta'''

<math>\frac{\Gamma, x_1:\sigma_1,...,x_n:\sigma_n \triangleright M : \tau}{\Gamma \triangleright \mu x_1,...,x_n.M : \{\sigma_1,...,\sigma_n\} \rightarrow \tau}(T-\mu ABS)</math>

con n = 1

<math>\frac{\Gamma \triangleright M : \{\sigma\} \rightarrow \tau \;\; \Gamma \triangleright N : \sigma}{\Gamma \triangleright M \#_1\; N : \tau}(T-\mu APP_1)</math>

con n > 1

<math>\frac{\Gamma \triangleright M : \{\sigma_1,...,\sigma_n\} \rightarrow \tau \;\; \Gamma \triangleright N : \sigma_i}{\Gamma \triangleright M \#_i\; N : \{\sigma_1,...,\sigma_n\} - \sigma_i \rightarrow \tau}(T-\mu APP_2)</math>

==== Punto B ====
Dar formalmente la extension de los valores e introducir las reglas de semantica para la extension propuesta.

'''Respuesta'''

<math>V ::= ... \;|\; \mu x_1,...,x_n.M</math>

<math>\frac{M_1 \rightarrow M_1'}{M_1\; \#_i\; M_2 \rightarrow M_1'\; \#_i\; M_2} (E-\mu APP_1)</math>

<math>\frac{M_2 \rightarrow M_2'}{V_1\; \#_i\; M_2 \rightarrow V_1\; \#_i\; M_2'} (E-\mu APP_2)</math>

<math>\frac{}{(\mu x.M)\; \#_1\; V \rightarrow M\{x \leftarrow V\}}(E-\mu AppAbs_1)</math>

<math>\frac{}{(\mu x_1,...,x_n.M)\; \#_i\; V \rightarrow (\mu x_1,...,x_{n-1}.M')} (E-\mu AppAbs_i)</math>

donde <math>n > 1, 1 \le i \le n</math> y

<math>M' = M\{x_i \leftarrow V, x_j \leftarrow x_{j-1} \textrm{\ para\ } j > i\}</math>

==== Punto C ====
Escribir las construcciones basicas del calculo lambda (λ y aplicacion) como syntactic sugar del mu calculo para mostrar que este ultimo puede emularlo. 

'''Respuesta'''

<math>\lambda x : \sigma.M ::= \mu x.M</math>

<math>M N ::= M\; \#_1\; N</math>

== Ejercicio 3: Inferencia de tipos ==
Utilizando el arbol de inferencia, inferir el tipo de las siguientes expresiones o demostrar 
que no son tipables. En cada paso donde se realice una uniﬁcacion, mostrar el conjunto de 
ecuaciones a uniﬁcar y la sustitucion obtenida como resultado de la misma. 

*(5 puntos) λx. λy. λz . (z x) y z 
*(5 puntos) λx. x (x (λy.x y)) 
*(5 puntos) λx. x (x (λy. x))

'''Respuesta'''

(Disculpen lo burdo de los "dibujos")

==== Ejercicio A ====
 λx. λy. λz . (z x) y z 
        |(ABS)
 λy. λz . (z x) y z
        |(ABS)
 λz . (z x) y z
        |(ABS)
     (z x) y z
       /     \  (APP)
    (z x) y   z:s4
     /    \ (APP)
  (z x)   y:s3
   /  \ (APP)
z:s1  x:s2

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)
* (APP) S = MGU {s1=s2->'''s5'''}={s2->s5/s1} ; &Gamma; = {z:s2->s5,x:s2} |> z x : s5
* (APP) S = MGU {s5=s3->'''s6'''}={s3->s6/s5} ; &Gamma; = {z:s2->(s3->s6),x:s2,y:s3} |> (z x) y : s6
* (APP) S = MGU {s6=s4->'''s7''',s4=s2->(s3->s6)}={s2->(s3->s6)/s4,(s2->(s3->s6))->s7/s6}
De lo anterior se puede ver que s6 es un tipo infinito -> FALLA.

==== Ejercicio B ====
 λx. x (x (λy.x y)) 
        |(ABS)
   x (x (λy.x y)) 
  /            \   (APP)
 x:s1      (x (λy.x y)) 
            /      \   (APP)
          x:s2    (λy.x y)
                     |  (ABS)
                    x y
                   /    \ (APP)
                 x:s3   y:s4

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)
* (APP) S = MGU {s3=s4->'''s5'''}={s4->s5/s3} ; &Gamma; = {x:s4->s5,y:s4} |> x y : s5
* (ABS) &Gamma; = {x:s4->s5} |> λy:s4.xy : s4->s5
* (APP) S = MGU {s2=s4->s5,s2=(s4->s5)->'''s6'''}={s4->s5=(s4->s5)->s6}={(s4->s5)->s6/(s4->s5)}
De lo anterior se puede ver que (s4->s5) es un tipo infinito -> FALLA.

==== Ejercicio C ====
 λx. x (x (λy. x))
    | (ABS)
 x (x (λy. x))
   /        \ (APP)
 x:s1   (x (λy. x))
          /      \ (APP)
        x:s2   (λy. x)
                 | (ABS)
                x:s3

Partiendo de abajo hacia arriba: (donde dice =, lease igual con puntito)
* (ABS) &Gamma; = {x:s3} |> λy:'''s4'''. x : s4->s3
* (APP) S = MGU {s2=s3,s2=(s4->s3)->'''s5'''}={s3=(s4->s3)->s5}={(s4->s3)->s5/s3}
De lo anterior se puede ver que s3 es un tipo infinito -> FALLA.

== Ejercicio 4: Inferencia de tipos ==
Extender el algoritmo de inferencia visto en clase para que soporte el tipado de listas multiti- 
padas. Las listas multitipadas son listas que pueden contener elementos de cualquier cantidad 
de tipos (aunque, como la longitud de la lista es ﬁnita, la cantidad de tipos distintos que 
contiene sera ﬁnita). Por ejemplo, la lista: 

 0 : True : (λx : Nat.x) : False : [ ] 

es de tipo

<math>list_{\{Nat,Bool,Nat \rightarrow Nat\}}</math> 

En general el tipo <math>list_\Sigma</math> denotara el tipo de las listas que contienen elementos de tipo t con t ∈ Σ, o sea, Σ es el conjunto de tipos que contiene la lista. Notar para todo elemento del 
conjunto Σ debe haber en la lista al menos un elemento de ese tipo, por eso la lista vacıa [ ] 
sera siempre de tipo <math>list_{\{\}}</math>. 

La extension de la sintaxis y el sistema de tipos es la siguiente: 

<math>M ::= ... \;|\; M : N \;|\; [ ]</math>

<math>\sigma ::= ... \;|\; list_\Sigma</math> 

y las reglas de tipado las siguientes:

<math>\frac{}{\Gamma \triangleright [ ] : list_{\{\}}}</math> 

<math>\frac{\Gamma \triangleright M : \sigma \;\; \Gamma \triangleright N : list_\Sigma}{\Gamma \triangleright M : N : list_{\Sigma \;\cup\; \{\sigma\}}}</math>

'''Respuesta'''

<math>\mathbb{W}([]) = \emptyset \triangleright [] : list_{\{\}}</math>

<math>\mathbb{W}(U) = \Gamma \triangleright M : \alpha</math>

<math>\mathbb{W}(V) = \Gamma' \triangleright N : \beta</math>

Sea <math>S = MGU\{\beta = list_\Sigma\} \cup \{\sigma_1 = \sigma_2  |  x:\sigma_1 \in \Gamma, x:\sigma_2 \in \Gamma'\}</math>

<math>\mathbb{W}(U:V) =_{\textrm{def}} S\Gamma \;\cup\; S\Gamma' \triangleright S(M:N) : list_{\Sigma'}</math>

donde <math>\Sigma' = S\Sigma \cup \{\alpha\}</math>

[[Category:Parciales]]