En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos el problema de las reinas (consistente en colocar N reinas en un tablero de dimensiones N por N de forma que no se encuentren más de una en la misma línea: horizontal, vertical o diagonal).
Los apuntes correspondientes a la clase son
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos desarrollado un programa en Haskell para resolver los problemas aritméticos del concurso Cifras y letras que consisten en dada una sucesión de números naturales y un número objetivo, intentar construir una expresión cuyo valor es el objetivo combinando los números de la sucesión usando suma, resta, multiplicación, división y paréntesis. Además, cada número de la sucesión puede usarse como máximo una vez y todos los números, incluyendo los resultados intermedios tienen que ser enteros positivos (1,2,3,…).
Por ejemplo, dada la sucesión 1, 3, 7, 10, 25, 50 y el objetivo 765, una solución es (1+50)x(25−10). Para el problema anterior existen 780 soluciones. En cambio, con la sucesión anterior y el objetivo 831, no hay solución.
Se empieza formalizando el problema y definiendo una función para reconcer las soluciones. A continuación, se presentan tres soluciones: la primera por fuerza bruta, la segunda mediante generación y evaluación y la tercera con simplificaciones algebraicas. Se termina con una comparación de las tres soluciones.
Los apuntes correspondientes a la clase son
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalized linear algebra over elementary divisor rings in Coq.
Sus autores son
Su resumen es
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bézout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension ≤1 and well-founded strict divisibility.
El trabajo se ha publicado en Logical Methods in Computer Science (Volume 12, Issue 2).
El código de las correspondientes teorías en Coq se encuentra aquí.
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 |