Recuperatorio Primer Parcial 2do Cuat 2007 (Paradigmas)

Ejercicio 1: Programación Funcional

Durante todo este ejercicio no se puede usar recursion explıcita, a menos que se especifique explıcitamente lo contrario. Para resolver un ıtem pueden utilizarse como existentes las soluciones a todos los anteriores, mas alla de si fueron resueltos correctamente o no.

Este ejercicio esta basado en un esquema particular de recursion que representa la tecnica algorıtmica divide and conquer aplicada a problemas de listas. El esquema dac, entonces, tendra el siguiente tipo e implementaci´on:

dac :: b -> (a -> b) -> ([a] -> ([a],[a])) -> ([a] -> b -> b -> b) -> [a] -> b
dac base base1 divide combine [] = base
dac base base1 divide combine [x] = base1 x
dac base base1 divide combine input = combine input (rec leftSide) (rec rightSide)
where rec = dac base base1 divide combine
leftSide = fst (divide input)
rightSide = snd (divide input)

Aquı base representa el caso base del problema para listas vacıas, base1 el caso base cuando la lista tiene exactamente un elemento, divide la funcion que divide el problema en exactamente 2 partes mas chicas.

Pediremos que la union (como conjunto) del par de salida al aplicar divide sea exactamente igual a su entrada y que ninguno de los componentes de su salida sea vacıo (para que sea efectivamente una funcion de division y no genere una recursi´on infinita). Por ultimo, combine combina los resultados recursivos (pudiendo utilizar informacion de la lista original).

Respuesta

Dejo esto para que hagan copy-paste:

-- esquema divide and conquer
dac base base1 divide combine [] = base
dac base base1 divide combine [x] = base1 x
dac base base1 divide combine input = combine input (rec leftSide) (rec rightSide)
        where rec = dac base base1 divide combine
              leftSide = fst (divide input)
              rightSide = snd (divide input)

Punto A

Sin recursion explıcita ni folds utilizar dac para reimplementar map y filter.

map :: (a -> b) -> [a] -> [b]
filter :: (a -> Bool) -> [a] -> [a]

Respuesta

-- parte por la mitad una lista
partirPorLaMitad ys = (primera, segunda)
        where primera = [ys !! i | i <- [0..(div (length ys) 2)-1]]
              segunda = [ys !! i | i <- [(div (length ys) 2)..(length ys)-1]]

-- map usando divide and conquer
dacmap f xs = dac [] (\x -> [f x]) partirPorLaMitad (\_ i d -> i ++ d) xs

-- filter usando divide and conquer
dacfilter p xs = dac [] (\x -> if (p x) then [x] else []) partirPorLaMitad (\_ i d -> i ++ d) xs

Otra manera (que viene en el preludio) de partir por la mitad sería:

partirPorLaMitad xs = splitAt ((length xs) `div` 2) xs

Punto B

Mostrar que foldr es un algoritmo de divide and conquer reescribiendolo en terminos de dac. Se sugiere ser muy cuidadoso con los tipos.

foldr :: (a -> b -> b) -> b -> [a] -> b

Respuesta

-- Foldr
dfoldr :: (a -> b -> b) -> b -> [a] -> b
dfoldr f b = dac b (\x -> f x b) (\xs -> ([(head xs)], (tail xs))) (\xs l r -> f (head xs) r)

Punto C

Usar dac para implementar el algoritmo de ordenamiento merge-sort. Dicho algoritmo se comporta de la siguiente manera: se divide a la lista a ordernar a la mitad (si es impar, en 2 partes lo mas iguales posibles), se ordenan esas partes y luego se fusionan (“merge”) en orden lineal tomando iterativamente el mas chico de las dos cabezas hasta que una lista se vac´ıa, momento en el cual agrega al final todo lo que queda de la otra y devuelve eso como resultado.

mergeSort :: Ord a => [a] -> [a]

Respuesta

-- une linealmente dos listas
merge xs [] = xs
merge [] xy = xy
merge (x:xs) (y:ys)
      | x <= y = x:(merge xs (y:ys))
      | otherwise = y:(merge (x:xs) ys)

-- mergesort usando dac
mergeSort :: Ord a => [a] -> [a]
mergeSort xs = dac [] (\x -> [x]) partirPorLaMitad (\_ x y -> merge x y) xs

Punto D

Usar dac para implementar el algoritmo de ordenamiento quick-sort. Dicho algoritmo se comporta de la siguiente manera: Se elige un elemento como pivote (en nuestro caso sera siempre el primero de la lista) y se parte el resto eligiendo todos los menores o iguales para un lado y todos los estrictamente mayores para el otro. El pivote se incluye en la lista de ambas que haya quedado m´as corta (para evitar que alguna quede vacıa). Ambas listas ya estan ordenadas entre si, por lo cual luego de ordenar cada una es simple obtener el resultado final.

quickSort :: Ord a => [a] -> [a]

Respuesta

import List(delete)

-- elijo el primero como pivote y creo dos listas una de menores y otra de mayores
partirPorPivote xs
        | mayores == [] = (delete pivote menores, pivote:mayores)
        | otherwise = (menores, mayores)
        where pivote = head xs
              menores = filter (<= pivote) xs
              mayores = filter (> pivote) xs

-- quicksort usando dac
quickSort :: Ord a => [a] -> [a]
quickSort xs = dac [] (\x -> [x]) partirPorPivote (\_ i d -> i ++ d) xs

Punto E

Dados los arboles binarios representados por el tipo ArbolBin:

data ArbolBin a = Nil | Bin (ArbolBin a) a (ArbolBin a)

escribir usando dac una funcion indexed que, dada una lista de longitud 2^k −1 para algun k natural, devuelva un arbol binario completo, tal que cada elemento de la lista aparezca en exactamente un nodo del arbol. Se puede asumir que la lista tiene todos elementos distintos.

indexed :: [a] -> ArbolBin a

Respuesta

-- arbol binario
data ArbolBin a = Nil | Bin (ArbolBin a) a (ArbolBin a)

-- dada una lista de longitud impar me devuelve la tripla
-- (hasta el del medio, el del medio, desde el medio)
partirEnTres :: [a] -> ([a], a, [a])
partirEnTres xs = (principio, elem, final)
        where mitadabajo = (div (length xs) 2)
              principio = take mitadabajo xs
              elem = xs !! (mitadabajo)
              final = [xs !! i | i <- [mitadabajo + 1..(length xs)-1]]

-- devuelve los elementos
elemento (a, b, c) = b
izquierdo (a, b, c) = a
derecho (a, b, c) = c

-- dada una lista de 2^k - 1 da un arbol completo
indexed :: [a] -> ArbolBin a
indexed xs = dac Nil arbolDeUno sinElem arbolConHijos xs
        where arbolDeUno e = Bin Nil e Nil
              arbolConHijos orig i d = Bin i (elemento (partirEnTres orig)) d
              partido = partirEnTres xs
              sinElem xs = (izquierdo partido, derecho partido)

Esto compila, no estoy seguro si funciona o no porque no puedo hacer un show.

Es más fácil, en lugar de tomar el elemento del medio, tomar simplemente la cabeza y partir la cola de la lista que me pasan como parametro a la mitad.

Las funciones quedarian así

divide = \xs -> splitAt (length xs `div` 2) (tail xs)
combine = \xs arbolIzq arbolDer -> Bin arbolIzq (head xs) arbolDer

Ejercicio 2: Lambda cálculo tipado

Se desea extender el lengua je de calculo lambda tipado para soportar el tipo de las listas alternadas. Las listas alternadas son listas que contienen hasta 2 tipos de valores. Formalmente el nuevo tipo $list_{\sigma ,\tau }$ representara las listas que en los indices pares tienen elementos de tipo $\sigma$ y en los impares elementos de tipo $\tau$. Los indices se numeran empezando desde 0, desde la cabeza de la lista.

La sintaxis y la extension del sistema de tipos para la extension propuesta son las siguientes:

$M::=...\;|\;M:N\;|\;{\textrm {[\ ]}}\;|\;{\textrm {fold\ M\ base}}=N\;;\;rec_{\sigma }\;e_{1}\;r_{1}=O_{1}\;;\;rec_{\tau }\;e_{2}\;r_{2}=O_{2}$

$\sigma ::=...\;|\;list_{\sigma ,\tau }$

Por ejemplo, la lista 0 : true : [] es de tipo $list_{nat,bool}$ y la lista false : 1 : false : [] es de tipo $list_{bool,nat}$. Para poder observar y crear funciones sobre estas listas se introducira un fold nativo, pero en lugar de funciones como en Haskell se utilizaran expresiones con variables libres a llenar con los parametros. Dicho fold tendra un unico caso base y 2 casos recursivos, dependiendo de en que posicion de la lista se encuentre a cada paso de la recursion. En la expresion

${\textrm {fold\ M\ base}}=N\;;\;rec_{\sigma }\;e_{1}\;r_{1}=O_{1}\;;\;rec_{\tau }\;e_{2}\;r_{2}=O_{2}$

M sera la lista sobre la cual se hace la recursion, N lo que se debe retornar como caso base y los $O_{i}$ son los casos recursivos. Notar que las variables $e_{i}$ y $r_{i}$ pueden aparecer libres en $O_{i}$ y se deben reemplazar oportunamente por el elemento actual y el resultado recursivo respectivamente.

Ejercicio A

Introducir las reglas de tipado para la extension propuesta. Se admite que haya listas con mas de un tipo posible (por ejemplo la lista vacia).

Respuesta

${\frac {}{\Gamma \triangleright {\textrm {[\ ]}}:list_{\sigma ,\tau }}}$

${\frac {\Gamma \triangleright M:\tau \;\;\;\Gamma \triangleright N:list_{\sigma ,\tau }}{\Gamma \triangleright {\textrm {M:N}}:list_{\tau ,\sigma }}}$

${\frac {\Gamma \triangleright N:\alpha \;\;\;\Gamma \triangleright M:list_{\sigma ,\tau }\;\;\;\Gamma \cup \{e_{1}:\sigma ,r_{1}:\alpha \}\triangleright O_{1}:\alpha \;\;\;\Gamma \cup \{e_{2}:\tau ,r_{2}:\alpha \}\triangleright O_{2}:\alpha }{\Gamma \triangleright {\textrm {fold\ M\ base}}=N\;;\;rec_{\sigma }\;e_{1}\;r_{1}=O_{1}\;;\;rec_{\tau }\;e_{2}\;r_{2}=O_{2}:\alpha }}$

Ejercicio B

Dar formalmente la extension de los valores e introducir las reglas de semantica para la extension propuesta. No se deben utilizar en los axiomas de semantica sentencias de tipado (por ejemplo, no se puede pedir como precondicion que cierto termino tenga un tipo dado).

Respuesta

$V::=...\;|\;{\textrm {[\ ]}}\;|\;V_{1}:V_{2}$

${\frac {M\rightarrow M'}{M:N\rightarrow M':N}}$

${\frac {N\rightarrow N'}{V:N\rightarrow V:N'}}$

${\frac {M\rightarrow M'}{{\textrm {fold\ }}M{\textrm {\ base}}=N\;;\;...\rightarrow {\textrm {fold\ }}M'{\textrm {\ base}}=N\;;\;...}}$

${\frac {}{{\textrm {fold\ [\ ]\ base}}=N\;;\;...\rightarrow N}}$

${\frac {}{{\textrm {fold\ }}V:W{\textrm {\ base}}=N\;;\;rec_{\sigma }\ e_{1}\;r_{1}=O_{1}\;;\;rec_{\tau }\ e_{2}\;r_{2}=O_{2}\rightarrow O'}}$

donde

$O'=O_{1}\{e_{1}\leftarrow V,r_{1}\leftarrow ({\textrm {fold\ }}W{\textrm {\ base}}=N\;;\;rec_{\tau }\ e_{2}\;r_{2}=O_{2}\;;\;rec_{\sigma }\ e_{1}\;r_{1}=O_{1})\}$

Ejercicio 3: Inferencia de tipos

Utilizando el árbol de inferencia, inferir el tipo de las siguientes expresiones o demostrar que no son tipables. En cada paso donde se realice una unificación, mostrar el conjunto de ecuaciones a unificar y la sustitución obtenida como resultado de la misma.

Ejercicio A

$(\lambda x.\lambda y.y)(\lambda z.\lambda w.z)$

Respuesta: Es tipable, el resultado es: $t_{1}\rightarrow t_{1}$

Ejercicio B

$\lambda x.x(\lambda y.y\lambda z.x)$

Respuesta: No es tipable ya que la unificación daría un tipo infinito.

Ejercicio 4: Inferencia de tipos

Dar un algoritmo de inferencia similar al de calculo lambda que maneje la inferencia de tipos del mu calculo. El mu calculo es un lenguaje similar al calculo lambda con la siguiente sintaxis y sistema de tipos:

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

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

y las siguientes reglas de tipado:

${\frac {\Gamma \cup \{x_{i}:\sigma _{i}\;|\;1\leq i\leq n\}\triangleright M:\tau }{\Gamma \triangleright \mu x_{1},...,x_{n}.M:\{\sigma _{1},...,\sigma _{n}\}\rightarrow \tau }}$

${\frac {\Gamma \triangleright M:\{\sigma \}\rightarrow \tau \;\;\Gamma \triangleright N:\sigma }{\Gamma \triangleright M\#_{1}\;N:\tau }}$

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

Por ejemplo, la siguiente expresion (consideramos para el ejemplo mu calculo con booleanos y naturales, igual que como fue visto para calculo lambda):

$(\mu \;x\;y.Suc(x))\;\#_{2}\;true$

deberia tipar correctamente a

$\{Nat\}\rightarrow Nat$

Respuesta

Definimos:

$\mathbb {W} (\mu x_{1},...,x_{n}.U)=\Gamma '\triangleright \mu x_{1},...,x_{n}.M:\{\tau _{1},\dots ,\tau _{n}\}\rightarrow \sigma$

Dado:

$\mathbb {W} (U)=\Gamma _{1}\triangleright M:\sigma$

$\forall i,1\leq i\leq n,\tau _{i}={\begin{cases}\alpha _{i}&{\mbox{ si }}x_{i}:\alpha _{i}\in \Gamma _{1}\\t&{\mbox{ en caso contrario, donde }}t{\mbox{ es una nueva variable fresca}}\end{cases}}$

$\Gamma '=\Gamma _{1}-\{x_{1},...,x_{n}\}$

Definimos:

$\mathbb {W} (U\#_{i}V)=S\Gamma _{1}\cup S\Gamma _{2}\triangleright S(M\#_{i}N):S(\alpha )$

Dado:

$\mathbb {W} (U)=\Gamma _{1}\triangleright M:\sigma$

$\mathbb {W} (V)=\Gamma _{2}\triangleright N:\rho$

Sea t variable fresca

Sea $S=MGU\{\sigma =\{\tau _{1},\dots ,\tau _{i-1},\rho ,\tau _{i+1},\dots ,\tau _{n}\}\rightarrow t\}\cup \{\sigma _{1}=\sigma _{2}|x:\sigma _{1}\in \Gamma _{1},x:\sigma _{2}\in \Gamma _{2}\}$

$\alpha ={\begin{cases}\{\tau _{1},\dots ,\tau _{i-1},\tau _{i+1},\dots ,\tau _{n}\}\rightarrow t&{\mbox{ si }}n>1\\t&{\mbox{ si }}n=1\end{cases}}$

Nota: El problema de fondo acá es que dependemos de la unificación para saber el valor de n. Entonces, como nunca definimos cómo se modifica el algoritmo de unificación, queda medio vago esto de usar ese n.