Primer Parcial 2do Cuat 2007 (Paradigmas)

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 defincion 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 finitas. 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 define 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. Definir 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 definida 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 infinitos, con lo cual el GrafoBip que los represente tendr´a listas infinitas (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 currificadas 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 definir 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 $(\mu x_{1},...,x_{n}.M)$ y de aplicacion $(M\#_{i}\;N)$. Estos cambios tambien introducen un cambio en el sistema de tipos: en lugar de tener σ → τ tendremos $\{\sigma _{1},...,\sigma _{n}\}$ → τ . Notar que $\{\sigma _{1},...,\sigma _{n}\}$ 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:

$M::=...\;|\;\mu x_{1},...,x_{n}.M\;|\;M\#_{i}\;N$

$\sigma ::=...\;|\;\{\sigma _{1},...,\sigma _{n}\}\rightarrow \tau$

El termino $\mu x_{1},...,x_{n}.M$ sirve para construir una nueva funcion de n parametros ordenados y el operador $\#_{i}$ 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

${\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)$

con n = 1

${\frac {\Gamma \triangleright M:\{\sigma \}\rightarrow \tau \;\;\Gamma \triangleright N:\sigma }{\Gamma \triangleright M\#_{1}\;N:\tau }}(T-\mu APP_{1})$

con n > 1

${\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})$

Punto B

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

Respuesta

$V::=...\;|\;\mu x_{1},...,x_{n}.M$

${\frac {M_{1}\rightarrow M_{1}'}{M_{1}\;\#_{i}\;M_{2}\rightarrow M_{1}'\;\#_{i}\;M_{2}}}(E-\mu APP_{1})$

${\frac {M_{2}\rightarrow M_{2}'}{V_{1}\;\#_{i}\;M_{2}\rightarrow V_{1}\;\#_{i}\;M_{2}'}}(E-\mu APP_{2})$

${\frac {}{(\mu x.M)\;\#_{1}\;V\rightarrow M\{x\leftarrow V\}}}(E-\mu AppAbs_{1})$

${\frac {}{(\mu x_{1},...,x_{n}.M)\;\#_{i}\;V\rightarrow (\mu x_{1},...,x_{n-1}.M')}}(E-\mu AppAbs_{i})$

donde $n>1,1\leq i\leq n$ y

$M'=M\{x_{i}\leftarrow V,x_{j}\leftarrow x_{j-1}{\textrm {\ para\ }}j>i\}$

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

$\lambda x:\sigma .M::=\mu x.M$

$MN::=M\;\#_{1}\;N$

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 unificacion, mostrar el conjunto de ecuaciones a unificar 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} ; Γ = {z:s2->s5,x:s2} |> z x : s5
• (APP) S = MGU {s5=s3->s6}={s3->s6/s5} ; Γ = {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} ; Γ = {x:s4->s5,y:s4} |> x y : s5
• (ABS) Γ = {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) Γ = {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 finita, la cantidad de tipos distintos que contiene sera finita). Por ejemplo, la lista:

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

es de tipo

$list_{\{Nat,Bool,Nat\rightarrow Nat\}}$

En general el tipo $list_{\Sigma }$ 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 $list_{\{\}}$.

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

$M::=...\;|\;M:N\;|\;[]$

$\sigma ::=...\;|\;list_{\Sigma }$

y las reglas de tipado las siguientes:

${\frac {}{\Gamma \triangleright []:list_{\{\}}}}$

${\frac {\Gamma \triangleright M:\sigma \;\;\Gamma \triangleright N:list_{\Sigma }}{\Gamma \triangleright M:N:list_{\Sigma \;\cup \;\{\sigma \}}}}$

Respuesta

$\mathbb {W} ([])=\emptyset \triangleright []:list_{\{\}}$

$\mathbb {W} (M)=\Gamma \triangleright M:\alpha$

$\mathbb {W} (N)=\Gamma '\triangleright N:\beta$

Sea $S=MGU\{\beta =list_{\Sigma }\}$

$\mathbb {W} (M:N)=_{\textrm {def}}S\Gamma \;\cup \;S\Gamma '\triangleright S(M:N):list_{\Sigma '}$

donde $\Sigma '=S\Sigma \cup \{\alpha \}$