En clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones de ejercicios de evaluación perezosa y listas infinitas de la 11ª relación.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2016: Ejercicios de evaluación perezosa y listas infinitas en Haskell (1)”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha ecplicado el uso de las libretías HLint y Trace.
La librería HLint se instala ejecutando en una consola
|
1 |
cabal install hlint |
Para explicar el uso de HLint se considera el programa ej1.hs en el que está definida la suma de una lista de números y cuyo contenido es
|
1 2 3 |
suma :: [Int] -> Int suma [] = 0 suma (x:xs) = x + suma xs |
para analizarlo, se ejecuta en una consola
|
1 2 3 4 5 6 7 8 9 |
tmp> hlint ej.hs ej.hs:2:1: Warning: Use foldr Found: suma [] = 0 suma (x : xs) = x + suma xs Why not: suma xs = foldr (+) 0 xs 1 suggestion |
Siguiendo la sugerencia, cambiamos el contenido del programa ej1.hs y queda
|
1 2 |
suma :: [Int] -> Int suma xs = foldr (+) 0 xs |
Lo volvemos a analizar con HLint
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
tmp> hlint ej1.hs ej1.hs:2:1: Error: Eta reduce Found: suma xs = foldr (+) 0 xs Why not: suma = foldr (+) 0 ej1.hs:2:11: Error: Use sum Found: foldr (+) 0 Why not: sum 2 suggestions |
Con lo que finalmente el programa queda
|
1 2 |
suma :: [Int] -> Int suma = sum |
y al analizarlo
|
1 2 |
tmp> hlint ej1.hs No suggestions |
El segundo ejemplo que se explicó es en un programa con acumulador. El programa está en el fichero ej2.hs cuyo contenido es
|
1 2 3 4 |
suma :: [Int] -> Int suma xs = aux 0 xs where aux y [] = y aux y (x:xs) = aux (y+x) xs |
Lo analizamos con HLint
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
tmp> hlint ej2.hs ej2.hs:2:1: Error: Eta reduce Found: suma xs = aux 0 xs Why not: suma = aux 0 ej2.hs:3:9: Warning: Use foldl Found: aux y [] = y aux y (x : xs) = aux (y + x) xs Why not: aux y xs = foldl (+) y xs 2 suggestions |
Al incorporar las 2 sugerencias a ej2.hs el programa queda como sigue
|
1 2 3 |
suma :: [Int] -> Int suma = aux 0 where aux y xs = foldl (+) y xs |
Lo volvemos a analizar con HLint
|
1 2 3 4 5 6 7 8 |
tmp> hlint ej2.hs ej2.hs:3:9: Error: Eta reduce Found: aux y xs = foldl (+) y xs Why not: aux = foldl (+) 1 suggestion |
a incorporar la sugerencia a ej2.hs cuyo contenido queda como sigue
|
1 2 3 |
suma :: [Int] -> Int suma = aux 0 where aux = foldl (+) |
Lo vovemos a analizar con HLint
|
1 2 |
tmp> hlint ej2.hs No suggestions |
Aunque no ha dado ninguna sugerencia, podemos eliminar la dunción auxiliar aux quedando el contenido de ej2.hs como sigue
|
1 2 |
suma :: [Int] -> Int suma = foldl (+) 0 |
Lo analizamos con HLint
|
1 2 3 4 5 6 7 8 |
tmp> hlint ej2.hs ej2.hs:2:8: Error: Use sum Found: foldl (+) 0 Why not: sum 1 suggestion |
Con lo que el program final se reduce a
|
1 2 |
suma :: [Int] -> Int suma = sum |
Para explicar la librería Trace volvemos a considerar la 2ª definición de la suma de los elemntos de una lista; es decir, la versión inicial del ej2.hs
|
1 2 3 4 |
suma :: [Int] -> Int suma xs = aux 0 xs where aux y [] = y aux y (x:xs) = aux (y+x) xs |
Para usar la librería Trace hauy que importarla añadiendo al principio del fichero la línea
|
1 |
import Debug.Trace |
Como la función recursiva es aux, para seguir su traza le añadimos como primera ecuación la siguiente.
|
1 |
aux y xs | trace ("aux " ++ show y ++ " " ++ show xs) False = undefined |
Con estos cambios, el contenido del fichero es
|
1 2 3 4 5 6 7 |
import Debug.Trace suma :: [Int] -> Int suma xs = aux 0 xs where aux y xs | trace ("aux " ++ show y ++ " " ++ show xs) False = undefined aux y [] = y aux y (x:xs) = aux (y+x) xs |
Al evaluarlo
|
1 2 3 4 5 6 |
λ> suma [3,2,4] aux 0 [3,2,4] aux 3 [2,4] aux 5 [4] aux 9 [] 9 |
se observa la traza. La cadena de la traza se puede construir con la función printf de la librería Printf como se muestra a continuación
|
1 2 3 4 5 6 7 8 |
import Debug.Trace import Text.Printf (printf) suma :: [Int] -> Int suma xs = aux 0 xs where aux y xs | trace (printf "aux %2d %s" y (show xs)) False = undefined aux y [] = y aux y (x:xs) = aux (y+x) xs |
en donde se ha ajustado el ancho de la la columna del acumulador a 2 (mediante %2d) como se ve en la evaluación
|
1 2 3 4 5 6 |
λ> suma [3,2,7] aux 0 [3,2,7] aux 3 [2,7] aux 5 [7] aux 12 [] 12 |
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la evaluación perezosa en Haskell. Se han visto la estrategias de evaluación perezosa e impaciente, se han comparado respecto de la terminación y el número de pasos necesarios en las computaciones, se ha aplicado a la computación con estructuras infinitas y se han visto casos en los que se aumenta la eficiencia con evaluación estricta.
Como ejemplo, se ha estudiado el cálculo de los números primos mediante la criba de Erastótenes.
Los apuntes correspondientes a la clase son
En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 5ª relación de ejercicios sobre eliminación de elementos duplicados de listas en Isabelle/HOL.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2016: Ejercicios de eliminación de duplicados en Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.
La teoría utilizada es la siguiente
Read More “RA2016: Razonamiento sobre árboles y bosques en Isabelle/HOL”