Primer Parcial 1er Cuat 2008 (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.

Definimos la funcion generate, que genera listas en base a un predicado y una funcion, de la siguiente manera:

generate :: ([a] -> Bool) -> ([a] -> a) -> [a]  
generate stop next = generateFrom stop next [] 

generateFrom:: ([a] -> Bool) -> ([a] -> a) -> [a] -> [a] 
generateFrom stop next xs | stop xs = xs 
                        | otherwise = generateFrom stop next (xs ++ [next xs]) 

Ejercicio A

Usando generate, escribir generateMaybe:: ([a] ->Maybe a) ->[a], que funciona de manera similar a generate, excepto que en lugar de recibir por separado el predicado y la funcion generadora, toma una funcion que devuelve un tipo Maybe. Si el resultado es Nothing, generateMaybe para de generar y si es Just a encola el elemento a y continua. Por ejemplo,

generateMaybe (\xs ->if (length xs) <3 then Just 1 else Nothing)

devuelve [1,1,1].

Respuesta

generateMaybe f = generate (\x -> isNothing (f x)) (\x -> fromJust (f x))
where isnothing x = (x == Nothing)
      fromJust (Just a) = a

Ejercicio B

Usando generate definir generateMult :: ([a] ->[a]) ->[a], que debe funcionar de manera similar a generate, excepto que toma una funcion f que devuelve una lista de elementos a ser encolados. Si la lista es vacia, el procedimiento se debe detener, si no, se deben encolar todos los elementos en el orden en el que fueron devueltos por f y continuar. Por ejemplo,

generateMult (\xs ->if (length xs) <3 then [1,2] else [])

devuelve [1,2,1,2].

Respuesta

generateMult f = juntar (generate stop next)
where stop xs = (f xs) == []
      next xs = f (juntar xs)
      juntar xs = foldr (++) [] xs

Ejercicio C

Definir iterateN :: Int ->(a ->a) ->a ->[a] utilizando alguno de los items anteriores. iterateN toma un entero n, una funcion f y un elemento inicial x y devuelve la lista [x, f x, f (f x), ..., f ( ...(f x) ...)] de longitud n.

Respuesta

iterateN n f x = generate stop next
where stop xs = (length xs) == n
      next xs = if (xs == []) then x else f (last xs)

Nota: last es una función del preludio.

Ejercicio D

Utilizando alguno de los items anteriores, reescribir la funcion del prelude de Haskell map :: (a ->b) ->[a] ->[b].

Respuesta

map f xs = generate stop next
where stop ys = (length xs) == (length ys)
      next ys = f (xs !! (length ys))

Ejercicio 2: Lambda cálculo tipado

En este ejercicio introduciremos pattern matching al calculo lambda tipado. Para eso nos basaremos en el calculo lambda con arboles binarios, como fue visto en clase, con el mismo conjunto de tipos:

$\sigma ::=Bool\;|\;AB_{\sigma }\;|\;\sigma _{1}\rightarrow \sigma _{2}$

Vamos a trabajar con el siguiente conjunto de términos M y patrones P :

$M::=x\;|\;true\;|\;false\;|\;nil_{\sigma }\;|\;Bin(M_{1},M_{2},M_{3})\;|\;\lambda x:\sigma .M\;|\;M_{1}\ M_{2}\;|\;match\ M_{1}\ with\ P\ in\ M$

$P::=x\;|\;true\;|\;false\;|\;nil_{\sigma }\;|\;Bin(P_{1},P_{2},P_{3})$

en donde $M,M_{1},M_{2}{\textrm {\ y\ }}M_{3}$ son terminos, x es una variable y $P,P_{1},P_{2}{\textrm {\ y\ }}P3$ son patrones. Las reglas de tipado para los terminos usuales del calculo lambda (es decir, para cualquier termino distinto de match) son las vistas en clase, y vamos a usar esas mismas reglas para tipar a los patrones P . Ademas, un patron no puede tener variables repetidas, y esa restriccion se va a imponer en las reglas de tipado de la expresion match.

De forma equivalente al pattern matching de Haskell, si P es un patron, y M y N son términos, la construcción match M with P in N intenta hacer coincidir el valor de M con P. Esta construcción liga en N todas las ocurrencias de variables de P , asocia las variables de P con subexpresiones de M, y luego reemplaza en N las variables ligadas por P por las subexpresiones correspondientes. La idea es que un patrón de tipo σ coincida con términos de tipo σ. Los siguientes son ejemplos donde los patrones coinciden, y en donde se muestra la expresión a la que reducen:

1. $match\ true\ with\ true\ in\ (\lambda x:Bool.x)\rightarrow \lambda x:Bool.x$
2. $match\ Bin(nil_{Bool},true,nil_{Bool})\ with\ Bin(x,y,z)\ in\ x\rightarrow nil_{Bool}$
3. $match\ (\lambda x:AB_{Bool}.Bin(nil_{Bool},true,x))\ nil_{Bool}\ with$$Bin(x,y,nil_{Bool})\ in\ (\lambda x:Bool.x)\ y\rightarrow true$

Siguiendo con los ejemplos, la expresiones:

1. $match\ false\ with\ true\ in\ (\lambda x:Bool.x)$ no coincide (es decir, la expresion se indefine), aunque esta bien tipada
2. $match\ nil_{Bool}\ with\ true\ in\ \lambda x:Bool.x$ no esta bien tipada
3. $match\ nil_{Bool}\ with\ Bin(x,x,x)\ intrue$ no esta bien tipada por tener variables repetidas en el patron
4. $match\ Bin(nil_{Bool},true,z)\ with\ Bin(x,true,y))\ in\ x$ no reduce, porque M no es (ni reduce a) un valor.

Ejercicio A

Escribir las reglas de tipado necesarias para tipar la construccion match. Recordar que un patron no puede tener variables repetidas, y para imponer esa restriccion se puede suponer definido el predicado sinVarRepetidas(t), donde t es cualquier termino o patron del calculo lambda.

Respuesta

${\frac {{\textrm {sinVarRep}}(P)\;\;\;\Gamma \triangleright M_{1}:\alpha \;\;\;x_{i}:\sigma _{i}\triangleright P:\alpha \;\;\;\Gamma \cup \{x_{i}:\sigma _{i}\}\triangleright M_{2}:\tau }{\Gamma \triangleright {\textrm {match}}\ M_{1}\ {\textrm {with}}\ P\ {\textrm {in}}\ M_{2}:\tau }}$

donde $x_{i}\in FV(P)$.

Ejercicio B

Decidir si los valores de este cálculo se ven modificados con respecto a los del cálculo original, y en ese caso dar formalmente su extensión. Definir las reglas semánticas de a un paso para la extensión propuesta, de manera tal que el calculo sea determinístico.

Respuesta

${\frac {M_{1}\rightarrow M_{1}'}{{\textrm {match}}\ M_{1}\ {\textrm {with}}\ P\ {\textrm {in}}\ M_{2}\rightarrow {\textrm {match}}\ M_{1}'\ {\textrm {with}}\ P\ {\textrm {in}}\ M_{2}}}$

${\frac {}{{\textrm {match}}\ V\ {\textrm {with}}\ x\ {\textrm {in}}\ M_{2}\rightarrow M_{2}\{x\leftarrow V\}}}$

${\frac {}{{\textrm {match}}\ T\ {\textrm {with}}\ T\ {\textrm {in}}\ M\rightarrow M}}$

con $T\in \{true,false,nil_{\sigma }\}$

${\frac {{\textrm {match}}\ V_{1}\ {\textrm {with}}\ P_{1}\ {\textrm {in}}\ M_{2}\rightarrow M_{2}}{{\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}\rightarrow T'}}$

con $T'={\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}'$

${\frac {\forall x\in FV(P_{1})\Rightarrow x\ \not \in \ FV(M_{2})\;\;\;{\textrm {match}}\ V_{2}\ {\textrm {with}}\ P_{2}\ {\textrm {in}}\ M_{2}\rightarrow M_{2}}{{\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}\rightarrow T'}}$

con $T'={\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}'$

${\frac {\forall x\in FV(P_{1}),y\in FV(P_{2})\Rightarrow x,y\ \not \in \ FV(M_{2})\;\;\;{\textrm {match}}\ V_{3}\ {\textrm {with}}\ P_{3}\ {\textrm {in}}\ M_{2}\rightarrow M_{2}}{{\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}\rightarrow T'}}$

con $T'={\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}'$

${\frac {\forall x_{i}\in FV(P_{i})\Rightarrow x_{i}\ \not \in \ FV(M_{2})}{{\textrm {match}}\ Bin(V_{1},V_{2},V_{3})\ {\textrm {with}}\ Bin(P_{1},P_{2},P_{3})\ {\textrm {in}}\ M_{2}\rightarrow M_{2}}}$

Los valores no se modifican, se agregan formas normales que no son valores.

Ejercicio 3: Inferencia de tipos

La siguiente extension al calculo lambda soporta el manejo de listas de elementos. La sintaxis, el sistema de tipos y las reglas de tipado son los siguientes:

$M::=\dots \;|\;nil_{\sigma }\;|\;M:N\;|\;{\textrm {case}}\ M\ {\textrm {of}}\ \{nil\rightarrow P\;|\;x:y\rightarrow Q\}$

$\sigma ::=\dots \;|\;[\sigma ]$

${\frac {}{\Gamma \triangleright nil_{\sigma }:[\sigma ]}}$

${\frac {\Gamma \triangleright M:\sigma \;\;\;\Gamma \triangleright N:[\sigma ]}{\Gamma \triangleright M:N:[\sigma ]}}$

${\frac {\Gamma \triangleright M:[\sigma ]\;\;\;\Gamma \triangleright P:\tau \;\;\;\Gamma \cup \{x:\sigma ,y:[\sigma ]\}\triangleright Q:\tau }{\Gamma \triangleright {\textrm {case}}\ M\ {\textrm {of}}\ \{nil\rightarrow P\;|\;x:y\rightarrow Q\}:\tau }}$

Se pide modificar el algoritmo de inferencia de tipos visto en clase para soportar el tipado del obser vador case y el constructor $nil_{\sigma }$ . Suponer que el algoritmo ya esta correctamente extendido para el constructor M:N . Tener en cuenta que el algoritmo recibe como entrada una expresion sin anotaciones de tipos y debe devolver un juicio de tipado. Por ejemplo, al recibir nil debe devolver $\emptyset \triangleright nil_{s}:[s]$, con s una variable de tipo.

Respuesta

Definimos:

$\mathbb {W} (nil)=_{def}\emptyset \triangleright nil_{s}:[s]$

Sean:

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

$\mathbb {W} (P)=\Gamma _{2}\triangleright P':\beta$

$\mathbb {W} (Q)=\Gamma _{3}\triangleright Q':\gamma$

$S=MGU\{\beta =\gamma \}\cup \{\alpha =[\tau ]\}\cup C_{1}\cup C_{2}\cup C_{3}\cup C_{4}$

donde

$C_{1}=\{\sigma _{1}=\sigma _{2}\;|\;v:\sigma _{1}\in \Gamma _{i}\;\wedge \;v:\sigma _{2}\in \Gamma _{j},1\leq i,j\leq 3,v\neq x,v\neq y\}$

siendo "v" una variable cualquiera de los conjuntos y "x" e "y" fijas.

$C_{2}=\{\sigma _{1}=\sigma _{2}\;|\;x:\sigma _{1}\in \Gamma _{i}\;\wedge \;x:\sigma _{2}\in \Gamma _{j}\ \lor \ y:\sigma _{1}\in \Gamma _{i}\;\wedge \;y:\sigma _{2}\in \Gamma _{j},1\leq i,j\leq 2\}$

siendo "x" e "y" fijas.

$C_{3}=\{\tau =\sigma \;|\;x:\sigma \in \Gamma _{3}\}$

siendo "x" fija.

$C_{4}=\{[\tau ]=\sigma \;|\;y:\sigma \in \Gamma _{3}\}$

siendo "y" fija.

Entonces:

$\mathbb {W} ({\textrm {case}}\ M\ {\textrm {of}}\ \{nil\rightarrow P\;|\;x:y\rightarrow Q\})=_{def}$ $S\Gamma _{1}\cup S\Gamma _{2}\cup S(\Gamma _{3}-\{x,y\})\triangleright S({\textrm {case}}\ M'\ {\textrm {of}}\ \{nil\rightarrow P'\;|\;x:y\rightarrow Q'\}):S\gamma$