Álgebra constructiva en Haskell

Álgebra constructiva en Haskell Facultad de Matemáticas Departamento de Ciencias de la Computación e Inteligencia Artificial Trabajo Fin de Grado Ángela González Martín 2 Agradecimientos A mis padres quiero agradecerles la ayuda y apoyo que me han dado durante esta bonita etapa. Siempre han estado para mí cuando más lo he necesitado, gracias por haberme facilitado el poder estudiar Matemáticas, por ayudarme en los momentos difíciles y por apoyarme en mis decisiones. A mi tutora María José, por toda la paciencia que ha tenido conmigo y la gran ayuda que me ha brindado para poder realizar este trabajo. Por último y no menos importante, a mi hermano, a todos mis amigos y todas las personas que son importantes para mí que han recorrido este camino conmigo. Ellos han hecho que haya sido una de las mejores experiencias. 3 El presente Trabajo Fin de Grado se ha realizado en el Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla. Supervisado por María José Hidalgo Doblado 4 Resumen El objetivo de este trabajo es representar las estructuras algebraicas en un lenguaje de programación funcional. Para ello, hemos usado Haskell. Mediante el uso de clases de tipos se han especificado las nociones de anillo, anillo conmutativo, dominio de integridad, cuerpo, ideal, anillo fuertemente discreto, anillo coherente y finalmente anillo fuertemente discreto y coherente. En este último es posible resolver sistemas de ecuaciones, para lo cual se ha desarrollado una librería de vectores y matrices cuyos elementos pertenecen a una estructura genérica (anillo, dominio de integridad o cuerpo). Además, mediante un proceso de instanciación se pueden obtener ejemplos concretos de las estructuras representadas. 5 Abstract The objective of this proyect is to represent the algebraic structures in a functional programming language. For this, we have maked use of Haskell. Through the use of type classes it has been specified the notion of ring, commutative ring, integral domain, field, ideal, strongly discrete ring, coherent ring and finally strongly discrete and coherent ring. In the last one it is possible to solve systems of equations, for which it has developed a library of vectors and matrices which elements are in a generic structure (ring, integral domain or field). Furthermore, through an instantiation process it can get specificed examples of the structures represented. 6 Esta obra está bajo una licencia Reconocimiento–NoComercial–CompartirIgual 2.5 Spain de Creative Commons. Se permite: copiar, distribuir y comunicar públicamente la obra hacer obras derivadas Bajo las condiciones siguientes: Reconocimiento. Debe reconocer los créditos de la obra de la manera especificada por el autor. No comercial. No puede utilizar esta obra para fines comerciales. Compartir bajo la misma licencia. Si altera o transforma esta obra, o genera una obra derivada, sólo puede distribuir la obra generada bajo una licencia idéntica a ésta. Al reutilizar o distribuir la obra, tiene que dejar bien claro los términos de la licencia de esta obra. Alguna de estas condiciones puede no aplicarse si se obtiene el permiso del titular de los derechos de autor. Esto es un resumen del texto legal (la licencia completa). Para ver una copia de esta licencia, visite http://creativecommons.org/licenses/by-nc-sa/2.5/es/ o envie una carta a Creative Commons, 559 Nathan Abbott Way, Stanford, California 94305, USA. Índice general Introducción 8 1 Programación funcional con Haskell 13 2 Teoría de Anillos en Haskell 17 2.1 Anillos ..................................... 17 2.2 Anillos Conmutativos ............................. 22 2.3 Dominio de integridad y Cuerpos ...................... 23 2.4 Ideales ...................................... 27 3 Vectores y Matrices 33 3.1 Vectores ..................................... 33 3.2 Matrices ..................................... 36 4 Anillos Coherentes 51 4.1 Anillos Fuertemente Discretos ........................ 51 4.2 Anillos Coherentes ............................... 52 4.3 Anillos Coherentes y Fuertemente Discretos ................ 61 A Como empezar con Emacs en Ubuntu 65 A.1 Instalar Ubuntu 16.04 junto a windows 10 ................. 65 A.2 Iniciar un Capítulo ............................... 67 A.3 Abreviaciones de Emacs ........................... 67 A.4 Push and Pull de Github con Emacs ..................... 69 Bibliografía 70 Indice de definiciones 71 7 8 Índice general Introducción Este trabajo tiene como objetivo implementar conceptos de álgebra constructiva en Haskell, desde la noción de anillo hasta la de anillo coherente. El camino a seguir consiste en desarrollar los siguientes puntos: Familiarización con las funciones predefinidas en Haskell. Aquí aportaremos las funciones básicas de Haskell con el fin de facilitar la lectura del código, pues muchas de ellas son utilizadas a lo largo del trabajo. Algunas de ellas las podemos encontrar en la librería Data.List de Haskell. Implementación de la teoría de anillos en Haskell. Introduciendo la noción de anillo, para posteriormente incluir los anillos conmutativos, dominio de integridad, cuerpos e ideales. Hemos definido los conceptos mediante programación funcional ( [1]y[7]) y teoría de tipos ( [2]y[9]). De tal forma, que mediante las instancias podemos trabajar con cualquier anillo en concreto, como el anillo de los enteros, Z. Para la elaboración de este capítulo se ha utilizado el material de la asignatura “Estructuras Algebraicas” del Departamento de Álgebra de la facultad de Matemáticas, “Tema 3: Anillos” ( [5]). También se ha utilizado la tesis “Constructive Algebra in Functional Programming and Type Theory” de Anders Mörtberg ( [6]). Librería de vectores y matrices sobre anillos en Haskell. Tomando como referencia la actual librería de matrices de la que Haskell dispone, Data.Matrix , junto con la tesis de Anders Mörtberg ( [6]). En este capítulo, comenzamos con las operaciones básicas entre matrices hasta poder aplicar el Método de Gauss, trabajando con vectores en forma de listas y matrices como listas de vectores sobre un anillo. Los conceptos sobre el método de Gauss-Jordan se encuentran en los apuntes de teoría “Sistemas de ecuaciones lineales” del Departamento de Álgebra ( [4]). Finalmente, incorporamos la teoría sobre anillos coherentes en Haskell. El objetivo de este capítulo es poder resolver sistemas de ecuaciones de la forma M~ X=~ b en anillos fuertemente discretos y coherentes. La primera sección del capítulo 9 16 Capítulo 1. Programación funcional con Haskell Capítulo 2 Teoría de Anillos en Haskell En este capítulo daremos una breve introducción a los conceptos de teoría de anillos en Haskell. Para ello haremos uso de los módulos. Un módulo de Haskell es una colección de funciones, tipos y clases de tipos relacionadas entre sí. En sentido amplio, un programa Haskell es una colección de módulos donde el módulo principal carga otros módulos y utiliza las funciones definidas en ellos. Así distribuiremos las secciones y partes del código que creeamos necesario en diferentes módulos. Nos centraremos principalmente en las notas sobre cómo definir los conceptos mediante programación funcional y teoría de tipos. 2.1. Anillos Comenzamos dando las primeras definiciones y propiedades básicas sobre anillos para posteriormente introducir los anillos conmutativos. Creamos el primer módulo TAH Antes de empezar tenemos que crear nuestro módulo. Todos tienen la misma estructura, se usa el comando de Haskell module seguido del nombre que le queramos dar al módulo. A continuación entre paréntesis introducimos todas las clases y funciones que vamos a definir y que queramos exportar cuando en otro fichero importemos este módulo, seguido del paréntesis escribimos where y finalmente importamos las librerías y módulos que vayamos a necesitar. Para importarlas usamos el comando import . Para nuestro primer módulo solo usaremos la conocida librería de Haskell Data.List 17 18 Capítulo 2. Teoría de Anillos en Haskell la cuál comprende las operaciones con listas, y Test.QuickCheck que contine las funciones para comprobar una propiedad e imprimir los resultados. module TAH ( Ring(..) , propAddAssoc, propAddIdentity, propAddInv, propAddComm , propMulAssoc, propMulIdentity, propRightDist, propLeftDist , propRing , (<->) , sumRing, productRing , (<^>), (~~), (<**) ) where import Data.List import Test.QuickCheck Comenzamos con la parte teórica, damos la definición de anillos: Definición 2.1.1. Un anillo es una terna (R,+,∗), donde R es un conjunto y +,∗son dos operaciones binarias +,∗:R×R→R, (llamadas usualmente suma y multiplicación) verificando lo siguiente: 1. Asociatividad de la suma: ∀a,b,c∈R.(a+b) + c=a+ (b+c) 2. Existencia del elemento neutro para la suma: ∃0∈R.∀a∈R. 0 +a=a+0=a 3. Existencia del inverso para la suma: ∀a∈R,∃b∈R.a+b=b+a=0 4. La suma es commutativa: ∀a,b∈R.a+b=b+a 5. Asociatividad de la multiplicación: ∀a,b,c∈R.(a∗b)∗c=a∗(b∗c) 6. Existencia del elemento neutro para la multiplicación: ∃1∈R.∀a∈R. 1 ∗a=a∗1=a 7. Propiedad distributiva a la izquierda de la multiplicación sobre la suma: ∀a,b,c∈R.a∗(b+c) = (a∗b) + (a∗c) 8. Propiedad distributiva a la derecha de la multiplicación sobre la suma: ∀a,b,c∈R.(a+b)∗c= (a∗c) + (b∗c) 2.1. Anillos 19 Una vez tenemos la teoría, pasamos a implementarlo en Haskell. Representaremos la noción de anillo en Haskell mediante una clase. Para ello, declaramos la clase Ring sobre un tipo a (es decir, a no está restringido) con las operaciones internas que denotaremos con los símbolos <+> y <**> (nótese que de esta forma no coinciden con ninguna operación previamente definida en Haskell). Representamos el elemento neutro de la suma mediante la constante zero y el de la multiplicación mediante la constante one . Asímismo, mediante la función neg representamos el elemento inverso para la suma, es decir, para cada elemento x del anillo, (neg x) representará el inverso de x respecto de la suma <+> . Todas ellas se concretarán para cada anillo particular. Mediante los operadores infixl e infixr se puede establecer el orden de precedencia (de 0 a 9) de una operación, así como la asociatividad de dicha operación ( infixl para asociatividad por la izquierda, infixr para asociatividad por la derecha e infix para no asociatividad). En este caso, las declaraciones ( infixl 6 <+> e infixl 7 <**> ) hacen referencia a la asociatividad por la izquierda de ambas operaciones, siendo 6 el nivel de precedencia de <+> y 7 el nivel de precedencia de <**> . infixl 6 <+> infixl 7 <**> class Show a => Ring a where (<+>) :: a -> a -> a (<**>) :: a -> a -> a neg :: a -> a zero :: a one :: a Una vez declarado el tipo y la signatura de las funciones, pasamos a implementar los axiomas de éste. En Haskell un tipo es como una etiqueta que posee toda expresión. Esta etiqueta nos dice a que categoría de objetos se ajusta la expresión. Todos los axiomas que tenemos que introducir tienen la misma estructura, reciben un tipo de la clase Ring y Eq para devolver elementos del tipo Bool y String . La clase Ring la acabamos de definir y la clase Eq es la clase de los tipos con igualdad. Cualquier tipo que tenga sentido comparar dos valores de ese tipo por igualdad debe ser miembro de la clase Eq . El tipo Bool devuelve un booleano con True y False , en nuestras funciones es necesario pues necesitamos que nos devuelva True si se veri- 20 Capítulo 2. Teoría de Anillos en Haskell fica el axioma y False en caso contrario. El tipo String es sinónimo del tipo [Char] . -- |1. Asociatividad de la suma. propAddAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) propAddAssoc a b c = ((a <+> b) <+> c == a <+> (b <+> c), "propAddAssoc") -- |2. Existencia del elemento neutro para la suma. propAddIdentity :: (Ring a, Eq a) => a -> (Bool,String) propAddIdentity a = (a <+> zero == a && zero <+> a == a, "propAddIdentity") -- |3. Existencia del inverso para la suma. propAddInv :: (Ring a, Eq a) => a -> (Bool,String) propAddInv a = (neg a <+> a == zero && a <+> neg a == zero, "propAddInv") -- |4. La suma es commutativa. propAddComm :: (Ring a, Eq a) => a -> a -> (Bool,String) propAddComm x y = (x <+> y == y <+> x, "propAddComm") -- |5. Asociatividad de la multiplicación. propMulAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) propMulAssoc a b c = ((a <**> b) <**> c == a <**> (b <**> c), "propMulAssoc") -- |6. Existencia del elemento neutro para la multiplicación. propMulIdentity :: (Ring a, Eq a) => a -> (Bool,String) propMulIdentity a = (one <**> a == a && a <**> one == a, "propMulIdentity") -- |7. Propiedad distributiva a la izquierda de la multiplicación -- sobre la suma. propRightDist :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) propRightDist a b c = ((a <+> b) <**> c == (a <**> c) <+> (b <**> c), "propRightDist") -- |8. Propiedad distributiva a la derecha de la multiplicación -- sobre la suma. propLeftDist :: (Ring a, Eq a) => a -> a -> a -> (Bool,String) propLeftDist a b c = (a <**> (b <+> c) == (a <**> b) <+> (a <**> c), "propLeftDist") Para saber si una terna (a,<+>,<**>) es un anillo definimos una propiedad que se encargue de comprobar que los axiomas anteriores se verifiquen, para cada caso particular de una instancia dada. La estructura que tiene es la siguiente: recibe un elemento de tipo Ring y Eq y devuelve un elemento de tipo Property , una función importada desde el módulo Test.QuickCheck . 2.1. Anillos 21 -- | Test para ver si se verifican los axiomas de un anillo. propRing :: (Ring a, Eq a) => a -> a -> a -> Property propRing a b c = whenFail (print errorMsg) cond where (cond,errorMsg) = propAddAssoc a b c &&& propAddIdentity a &&& propAddInv a &&& propAddComm a b &&& propMulAssoc a b c &&& propRightDist a b c &&& propLeftDist a b c &&& propMulIdentity a (False,x) &&& _ = (False,x) _ &&& (False,x) = (False,x) _ &&& _ = (True,"") Veamos algunos ejemplos de anillos. Para ello, mediante instancias, especificamos las operaciones que dotan al conjunto de estructura de anillo. Por ejemplo, el anillo de los números enteros Z, en Haskell es el tipo Integer , con la suma y la multiplicación. Ejemplo: -- | El anillo de los enteros con las operaciones usuales: instance Ring Integer where (<+>) = (+) (<**>) = (*) neg = negate zero = 0 one = 1 Se admite esta instancia porque se ha comprobado que se verifican los axiomas para ser un anillo. En caso contrario, proporcionaría un error. Veamos ahora cómo definir nuevas operaciones en un anillo a partir de las propias del anillo. En particular, vamos a definir la diferencia, suma de una lista, producto de una lista y potencia. Estas operaciones se heredan a las instancias de la clase anillo y, por tanto, no habría que volver a definirlas para cada anillo particular. En primer lugar, establecemos el orden de prioridad para los símbolos que vamos a utilizar para denotar las operaciones. infixl 8 <^> infixl 6 <-> infixl 4 ~~ infixl 7 <** -- | Diferencia. (<->) :: Ring a => a -> a -> a a <-> b = a <+> neg b 22 Capítulo 2. Teoría de Anillos en Haskell -- | Suma de una lista de elementos. sumRing :: Ring a => [a] -> a sumRing = foldr (<+>) zero -- | Producto de una lista de elementos. productRing :: Ring a => [a] -> a productRing = foldr (<**>) one -- | Potencia. (<^>) :: Ring a => a -> Integer -> a x <^> 0 = one x <^> y | y < 0 = error "<^>: La entrada debe ser positiva." | otherwise = x <**> x <^> (y-1) -- | Relación de semi-igualdad: dos elementos son semi-iguales si son -- iguales salvo el signo. (~~) :: (Ring a, Eq a) => a -> a -> Bool x ~~ y = x == y || neg x == y || x == neg y || neg x == neg y Finalmente hemos definimos la multiplicación de un entero por la derecha. La multiplicación de un entero por la izquierda se tiene debido a que la operación <+> es conmutativa. Esta función al igual que la anterior de potencia recibe un elemento de la clase Ring y devuelve un número entero, que es el tipo Integer . -- |Multiplicación de un entero por la derecha. (<**) :: Ring a => a -> Integer -> a _ <** 0 = zero x <** n | n > 0 = x <+> x <** (n-1) | otherwise = neg (x <** abs n) -- error "<**: Entrada Negativa." 2.2. Anillos Conmutativos Para espeficar los anillos commutativos crearemos un nuevo módulo en el que importaremos el módulo anterior, el nuevo módulo será TAHCommutative module TAHCommutative (module TAH , CommutRing(..) , propMulComm, propCommutRing ) where 2.3. Dominio de integridad y Cuerpos 23 import Test.QuickCheck import TAH En este módulo introducimos el concepto de anillo conmutativo. Aquí hemos importado el módulo TAH con el comando import , para poder usar las clases y funciones definidas en dicho módulo. Visto desde el punto de vista de la programación funcional,un anillo conmutativo es una subclase de la clase Ring . Solo necesitaremos una función para definirlo. Damos primero su definición. Definición 2.2.1. Un anillo conmutativo es un anillo (R,+,∗)en el que la operación de multiplicación ∗es conmutativa, es decir, ∀a,b∈R.a∗b=b∗a class (Show a, Ring a) => CommutRing a propMulComm :: (CommutRing a, Eq a) => a -> a -> Bool propMulComm a b = a <**> b == b <**> a Para saber si un anillo es commutativo definimos una propiedad que compruebe, en cada caso particular, que las operaciones concretas de una instancia verifiquen los axiomas para ser un anillo conmutativo y por consiguiente un anillo : -- | Test que comprueba si un anillo es commutativo. propCommutRing :: (CommutRing a, Eq a) => a -> a -> a -> Property propCommutRing a b c = if propMulComm a b then propRing a b c else whenFail (print "propMulComm") False El conjunto de los números enteros es un anillo conmutativo. Por tanto, añadiendo la instancia a la clase de anillos conmutativos, comprueba que se verifiquen las operaciones necesarias para ser un anillo conmutativo. instance CommutRing Integer 2.3. Dominio de integridad y Cuerpos Dada la noción de anillo conmutativo podemos hablar de estructuras algebraicas como dominio de integridad y cuerpo. Comenzamos por el módulo TAHIntegralDomain module TAHIntegralDomain (module TAHCommutative 24 Capítulo 2. Teoría de Anillos en Haskell , IntegralDomain , propZeroDivisors, propIntegralDomain ) where import Test.QuickCheck import TAHCommutative Para iniciar este módulo necesitamos importar el módulo TAHCommutative ya que vamos a definir los dominios de integridad sobre anillos conmutativos, por lo que la clase que vamos a definir parte de la clase CommutRing que como hemos definido antes es el tipo de los anillos conmutativos. Damos su definición. Definición 2.3.1. Dado un anillo (A,+,∗), un elemento a ∈A se dice que es un divisor de cero si existe b ∈A− {0}tal que a ∗b=0. Un anillo A se dice dominio de integridad, si el único divisor de cero es 0. Es decir, ∀a,b∈R.a∗b=0⇒a=0or b =0 -- | Definición de dominio de integridad. class CommutRing a => IntegralDomain a -- | Un dominio de integridad es un anillo cuyo único divisor -- de cero es 0. propZeroDivisors :: (IntegralDomain a, Eq a) => a -> a -> Bool propZeroDivisors a b = if a <**> b == zero then a == zero || b == zero else True Como ocurría con los axiomas de los anillos, la función propZeroDivisors requiere que los elementos que recibe sean de la clase de tipo IntegralDomain y de tipo Eq pues estamos definiendo operaciones en las que se tiene que dar una igualdad, y devuelva un valor booleano, por ello el elemento de salida es de tipo Bool . Para determinar si un anillo es un dominio de integridad usaremos la siguiente propiedad, esta tal y como ocurre con las anteriores propiedades, se encarga de comprobar que para cualquier instancia que demos se cumplan los axiomas que tiene que verificar, en este caso, para ser un dominio de integridad: propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property propIntegralDomain a b c = if propZeroDivisors a b then propCommutRing a b c else whenFail (print "propZeroDivisors") False El conjunto de los números enteros es un dominio de integridad. Mediante la instancia a la clase de dominio de integridad, comprueba que se verifiquen las operaciones 2.3. Dominio de integridad y Cuerpos 25 necesarias para ser un dominio de integridad. instance IntegralDomain Integer Ahora podemos implementar la especificación de la noción de cuerpo en el módulo TAHField module TAHField ( module TAHIntegralDomain , Field(inv) , propMulInv, propField , (</>) ) where import Test.QuickCheck import TAHIntegralDomain Para poder implementar la noción de cuerpo, necesitamos importar el módulo anterior TAHIntegralDomain , pues si una terna (A,+,∗)es un cuerpo también es dominio de integridad, y al definir la clase de cuerpo le imponemos la restricción de que sea un dominio de integridad. Veamos la definición teórica de cuerpo. Definición 2.3.2. Un cuerpo es un anillo de división conmutativo, es decir, un anillo conmutativo y unitario en el que todo elemento distinto de cero es invertible respecto del producto. Otra forma de definirlo es la siguiente, un cuerpo R es un dominio de integridad tal que para cada elemento a 6=0, existe un inverso a−1que verifica la igualdad: a−1a=1. Esta segunda definición es la que usaremos para la implementación. La primera definición es la más común a nivel de teoría algebraica, y para aquellos familiarizados con conceptos básicos de álgebra, conocen la definición de cuerpo como la primera que hemos dado. En Haskell especificamos el inverso de cada elemento mediante la función inv . La función propMulInv esta restringida a la clase de tipo Field pues requerimos que sea cuerpo y al tipo Eq pues se tiene que dar la igualdad. -- | Definición de cuerpo. class IntegralDomain a => Field a where inv :: a -> a -- | Propiedad de los inversos. propMulInv :: (Field a, Eq a) => a -> Bool 32 Capítulo 2. Teoría de Anillos en Haskell --(<0>,[[0,0]],[[0,0]]) Capítulo 3 Vectores y Matrices En este capítulo implementaremos los vectores y matrices como listas para poder usarlas en los módulos siguientes. En Haskell existen ya estas librerías pero solo podemos usarlas si nos restringimos al tipo numérico. Por ello, crearemos este módulo con el fin de generalizar los conceptos para anillos sobre cualquier tipo a. 3.1. Vectores Antes de introducir las matrices tenemos que especificar ciertas operaciones y funciones sobre los vectores, pues las filas de las matrices serán vectores, así tendremos la matriz como lista de listas. Damos los conceptos necesarios en el módulo TAHVector module TAHVector ( Vector(Vec) , unVec, lengthVec , sumVec, mulVec ) where import Control.Monad (liftM) import Test.QuickCheck import TAHField Para comenzar este módulo, necesitaremos hacer uso de librerías de Haskell como Control.Monad para utilizar ciertas funciones que nos ayuden a construir nuestros vectores. Daremos más detalle cuando la utilicemos. Comenzamos por implementar las nociones básicas de los vectores. Creamos un 33 34 Capítulo 3. Vectores y Matrices nuevo tipo para definir un vector, usaremos las listas para trabajr con los vectores en Haskell. Daremos también una función para generar vectores de forma aleatoria, para poder comprobar resultados mediante QuickCheck . -- | Vectores. newtype Vector r = Vec [r] deriving (Eq) instance Show r => Show (Vector r) where show (Vec vs) = show vs -- Generar un vector de longitud 1-10. instance Arbitrary r => Arbitrary (Vector r) where arbitrary = do n <- choose (1,10) :: Gen Int liftM Vec $ gen n where gen 0 = return [] gen n = do x <- arbitrary xs <- gen (n-1) return (x:xs) Explicamos brevemente algunas de las funciones utilizadas en el generador de vectores. Con choose se elige de forma aleatoria un número (en nuestro caso, entre 1 y 10) para establecer la longitud del vector. Con gen generamos elementos aleatorios del tipo Int y la lista obtenida la transformamos en tipo Vector con la función liftM . Damos la función que muestra el vector en forma de lista y la que mide la longitud de un vector en ese formato. Acompañamos de ejemplos para mostrar los resultados que se obtienen. unVec :: Vector r -> [r] unVec (Vec vs) = vs lengthVec :: Vector r -> Int lengthVec = length . unVec -- | Ejemplos: --> unVec (Vec [2,3]) -- [2,3] --> lengthVec (Vec [3,4,5]) -- 3 Para trabajar con vectores, haremos uso de la clase de tipos Functor de Haskell. Esta clase de tipos está implementada de la siguiente forma: 3.1. Vectores 35 -- class Functor f where -- fmap :: (a -> b) -> f a -> f b Define una función, fmap , y no proporciona ninguna implementación por defecto. El tipo de fmap es similar al tipo de map . Aquí, f no es un tipo concreto, sino un constructor de tipos que toma un tipo como parámetro. Vemos que fmap toma una función de un tipo a otro, un funtor aplicado a un tipo y devuelve otro funtor aplicado con el otro tipo. En nuestro caso crearemos una instancia con la clase de tipos Functor sobre el constructor Vector con el objetivo de aplicar una función f sobre un vector. Definiremos la función (fmap f) de forma que devuelva un vector con la función f aplicada a cada componente del vector. instance Functor Vector where fmap f = Vec . map f . unVec Veamos las operaciones de suma y multiplicación de vectores sobre anillos, para ello restringimos a los anillos conmutativos de forma general. La multiplicación de vectores es el producto escalar de ambos. Añadimos unos ejemplos sobre los números enteros. sumVec:: Ring a => Vector a -> Vector a -> Vector a sumVec (Vec xs) (Vec ys) | length xs == length ys = Vec (zipWith (<+>) xs ys) | otherwise = error "Los vectores tienen dimensiones diferentes" mulVec:: Ring a => Vector a -> Vector a -> a mulVec (Vec xs) (Vec ys) | length xs == length ys = foldr (<+>) zero $ zipWith (<**>) xs ys | otherwise = error "Los vectores tienen dimensiones diferentes" -- | Ejemplos: --> sumVec (Vec [2,3]) (Vec [4,5]) -- [6,8] --> mulVec (Vec [2,3]) (Vec [4,5]) -- 23 36 Capítulo 3. Vectores y Matrices 3.2. Matrices Una vez dadas las funciones y operaciones de los vectores podemos comenzar a implementar las matrices, notesé que cada fila o columna de una matriz puede verse como un vector. Nuestra idea es dar las matrices como una lista de vectores de forma que cada vector será una fila de la matriz. El objetivo de esta sección es implementar el método de Gauss-Jordan con el fin de poder resolver sistemas de la forma Ax =b. Lo vemos en el módulo TAHMatrix module TAHMatrix ( Matrix(M), matrix , matrixToVector, vectorToMatrix, unMVec, unM, (!!!) , identity, propLeftIdentity, propRightIdentity , mulM, addM, transpose, isSquareMatrix, dimension , scale, swap, pivot , addRow, subRow, addCol, subCol , findPivot, forwardElim, gaussElim, gaussElimCorrect ) where import qualified Data.List as L import Control.Monad (liftM) import Control.Arrow hiding ((<+>)) import Test.QuickCheck import TAHField import TAHVector Antes de comenzar, hemos importado algunas librerías necesarias para construir las matrices. Entre ellas utilizaremos Control.Arrow , de ella tenemos que excluir la suma (<+>) pues nosotros utilizamos la definida en anillos. Declaramos el nuevo tipo de matrices, la representación de la matriz viene dada en forma de lista de vectores, donde cada vector de la lista representa una fila de la matriz. Daremos también una instancia para que se puedan mostrar. Así como un generador de matrices aleatorio, similar al utilizado en vectores, con el fin de poder comprobar resultados mediante QuickCheck . newtype Matrix r = M [Vector r] deriving (Eq) 3.2. Matrices 37 instance Show r => Show (Matrix r) where show xs = case unlines (map show (unMVec xs)) of [] -> "[]" xs -> init xs ++ "\n" -- Generar matrices con a lo sumo 10 filas. instance Arbitrary r => Arbitrary (Matrix r) where arbitrary = do n <- choose (1,10) :: Gen Int m <- choose (1,10) :: Gen Int xs <- sequence [ liftM Vec (gen n) | _ <- [1..m]] return (M xs) where gen 0 = return [] gen n = do x <- arbitrary xs <- gen (n-1) return (x:xs) Una vez implementado el tipo de las matrices vamos a definir la función para construir una matriz de dimensión m×na partir de una lista de listas, de forma que cada lista es una fila de la matriz (todas de la misma longitud) y la longitud de una lista es el número de columnas. Vamos a dar una función para que devuelva la matriz de la forma en que visualmente la vemos, es decir una fila debajo de la otra. -- | Matriz mxn. matrix :: [[r]] -> Matrix r matrix xs = let m = fromIntegral $ length xs n = fromIntegral $ length (head xs) in if length (filter (\x -> fromIntegral (length x) == n) xs) == length xs then M (map Vec xs) else error "La dimensión del vector es distinta al resto" Las siguientes funciones son para mostrar una matriz como lista de vectores, y aplicar funciones con este formato sobre ella. Pasar de matrices a vectores y viceversa, así como una función para obtener el elemento en la posición (i,j). -- | Mostrar la matriz como lista de vectores. unM :: Matrix r -> [Vector r] unM (M xs) = xs -- Ejemplo: -- > unM (M [Vec [2,3], Vec [3,4]]) -- [[2,3],[3,4]] -- | Aplicamos la función 'unM' a cada vector de la lista. unMVec :: Matrix r -> [[r]] 38 Capítulo 3. Vectores y Matrices unMVec = map unVec . unM -- Ejemplo: -- > unMVec (M [Vec [2,3], Vec [3,4]]) -- [[2,3],[3,4]] -- | De vector a matriz. vectorToMatrix :: Vector r -> Matrix r vectorToMatrix = matrix . (:[]) . unVec -- Ejemplo: -- > vectorToMatrix (Vec [2,3,4]) -- [2,3,4] -- | De matriz a vector. matrixToVector :: Matrix r -> Vector r matrixToVector m | fst (dimension m) == 1 = head (unM m) | otherwise = error "No pueden tener dimensiones distintas" -- Ejemplos: -- > matrixToVector (M [Vec [2,3], Vec [4,5]]) -- *** Exception: No pueden tener dimensiones distintas -- > matrixToVector (M [Vec [2,3]]) -- [2,3] -- | Obtener el elemento de la posición (i+1,j+1). (!!!) :: Matrix a -> (Int,Int) -> a m !!! (i,j) | i >= 0 && i < rows && j >= 0 && j < cols = unMVec m !! i !! j | otherwise = error "!!!: Fuera de los límetes" where (rows,cols) = dimension m -- Ejemplos: -- > (M [Vec [2,3,4], Vec [4,5,6], Vec [7,8,9]]) !!! (2,3) -- *** Exception: !!!: Fuera de los límetes -- > (M [Vec [2,3,4], Vec [4,5,6], Vec [7,8,9]]) !!! (1,2) -- 6 -- > (M [Vec [2,3,4], Vec [4,5,6], Vec [7,8,9]]) !!! (0,1) -- 3 Utilizando las funciones anteriores podemos implementar propiedades y operaciones con las matrices. Daremos la dimensión de la matriz, una función que compruebe si la matriz es cuadrada, es decir, que el número de filas coincide con el número de columnas. Y la función para transponer una matriz, es decir, pasar las filas a columnas. Para esta última, utilizaremos la función transpose de la librería Data.List que se aplica sobre listas de forma que agrupa los elementos para que las listas que son 3.2. Matrices 39 filas estén en la posición de la columna correspondiente. -- | Dimensión de la matriz. dimension :: Matrix r -> (Int, Int) dimension (M xs) | null xs = (0,0) | otherwise = (length xs, length (unVec (head xs))) -- Ejemplo: -- > dimension (M [Vec [2,3,4], Vec [4,5,6], Vec [7,8,9]]) -- (3,3) -- | Comprobar si una matriz es cuadrada. isSquareMatrix :: Matrix r -> Bool isSquareMatrix (M xs) = all (== l) (map lengthVec xs) where l = length xs -- Ejemplo: -- > isSquareMatrix (M [Vec [2,3,4], Vec [4,5,6], Vec [7,8,9]]) -- True -- > isSquareMatrix (M [Vec [2,3,4], Vec [4,5,6]]) -- False -- | Transponer la matriz. transpose :: Matrix r -> Matrix r transpose (M xs) = matrix (L.transpose (map unVec xs)) -- Ejemplo: -- > transpose (M [Vec [2,3,4], Vec [4,5,6]]) -- [2,4] -- [3,5] -- [4,6] Recordamos que la suma de matrices da una matriz cuyas entradas son la suma de las entradas correspondientes de las matrices a sumar. Para esta suma lo haremos mediante suma de listas ya que utilizaremos la función matrix para mostrar la matriz correspondiente y esta recibe como argumento de entrada una lista de listas. Por otro lado la multiplicación de matrices recordamos que consiste en multiplicar cada fila de la primera matriz por cada columna de la segunda matriz, obteniendo así un elemento en la entrada correspondiente a la fila y columna. Aquí si podemos utilizar la operación mulVec entre vectores pues devuelve un valor que no es un vector, por tanto obtenemos una lista de vectores. Recordamos que para poder realizar multiplicaciones entre matrices el número de columnas de la primera matriz tiene que ser igual al número de filas de la segunda matriz. -- | Suma de matrices. 40 Capítulo 3. Vectores y Matrices addM :: Ring r => Matrix r -> Matrix r -> Matrix r addM (M xs) (M ys) | dimension (M xs) == dimension (M ys) = m | otherwise = error "Las dimensiones de las matrices son distintas" where m = matrix (zipWith (zipWith (<+>)) (map unVec xs) (map unVec ys)) -- Ejemplo: -- > addM (M [Vec [2,3,4], Vec [4,5,6]]) (M [Vec [1,0,2], Vec [1,2,3]]) -- [3,3,6] -- [5,7,9] -- > addM (M [Vec [2,3,4], Vec [4,5,6]]) (M [Vec [1,0,2]]) -- *** Exception: Las dimensiones de las matrices son distintas -- | Multiplicación de matrices. mulM :: Ring r => Matrix r -> Matrix r -> Matrix r mulM (M xs) (M ys) | snd (dimension (M xs)) == fst (dimension (M ys)) = m | otherwise = error "La dimensión de colunmas y filas es distinta" where m = matrix [ [mulVec x y | y <- unM (transpose (M ys)) ] | x <- unM (M xs) ] -- Ejemplo: -- > mulM (M [Vec [2,3], Vec [4,5]]) (M [Vec [1,0,2], Vec [1,2,3]]) -- [5,6,13] -- [9,10,23] -- > mulM (M [Vec [2,3,4], Vec [4,5,6]]) (M [Vec [1,0,2], Vec [1,2,3]]) -- *** Exception: La dimensión de colunmas y filas es distinta Del mismo modo que para vectores, para matrices volveremos a utilizar la clase de tipos Functor para establecer matrices en forma de listas. instance Functor Matrix where fmap f = M . map (fmap f) . unM Veamos un ejemplo sobre los números enteros de (fmap f) , sumar 2 a una matriz: -- > fmap (<+> 2) (M [Vec [2,3], Vec [4,5]]) -- [4,5] -- [6,7] Introducimos las propiedades básicas de la matriz identidad. Estas estarán restringidas a la clase de dominio de integridad, IntegralDomain . 3.2. Matrices 41 -- | Construcción de la matriz identidad nxn. identity :: IntegralDomain r => Int -> Matrix r identity n = matrix (xs 0) where xs x | x == n = [] | otherwise = (replicate x zero ++ [one] ++ replicate (n-x-1) zero) : xs (x+1) -- Ejemplo: -- > identity 3 -- [1,0,0] -- [0,1,0] -- [0,0,1] -- Propiedades de la multiplicación a izquierda y derecha de la -- matriz identidad. propLeftIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool propLeftIdentity a = a == identity n `mulM` a where n = fst (dimension a) propRightIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool propRightIdentity a = a == a `mulM` identity m where m = snd (dimension a) A continuación vamos a trabajar con matrices sobre anillos conmutativos, al igual que hicimos con los vectores. Realizaremos operaciones entre filas y columnas, y veremos que estas operaciones no afectan a la dimensión de la matriz. Hacemos esta restricción debido a que en el siguiente capítulo necesitaremos estas operaciones con matrices y estaremos restringidos a anillos conmutativos. Damos una breve descripción de la primera operación. El objetivo es multiplicar una fila por un escalar, de forma que la matriz obtenida tenga la fila que queramos modificar como el resultado de multiplicar esta fila por un número o escalar, quedando el resto de filas sin modificar. Los argumentos de entrada serán la matriz, el número de la fila que queremos modificar menos 1 (pues la función (!! r) de la librería Data.List selecciona el elemento r+1 de la lista, pues es un índice y comienza en 0). Comprobaremos que esta operación no afecta a la dimensión, pues la dimensión de la matriz resultante es la misma que la primera matriz. -- | Multiplicar una fila por un escalar en la matriz. scaleMatrix :: CommutRing a => Matrix a -> Int -> a -> Matrix a scaleMatrix m r s | 0 <= r && r < rows = matrix $ take r m' ++ map (s <**>) (m' !! r) : drop (r+1) m' 48 Capítulo 3. Vectores y Matrices --> forwardElim (M [Vec [1,0,2], Vec [2,1,-3], Vec [4,1,8]],Vec [4,5,6]) --([1.0,0.0,2.0] --[0.0,1.0,-7.0] --[0.0,0.0,1.0] --,[4.0,-3.0,-1.0]) En segundo lugar aplicamos el paso de Jordan que consiste en obtener ceros por encima de la diagonal. Para aplicar el método de Gauss-Jordan es necesario aplicar antes el paso de Gauss y después el de Jordan. -- | Realizar el paso "Jordan" en la eliminación de Gauss-Jordan. Esto -- es hacer que cada elemento encima de la diagonal sea cero. jordan :: (Field a, Eq a) => (Matrix a, Vector a) -> (Matrix a, Vector a) jordan (m, Vec ys) = case L.unzip (jordan' (zip (unMVec m) ys) (r-1)) of (a,b) -> (matrix a, Vec b) where (r,_) = dimension m jordan' [] _ = [] jordan' xs c = jordan' [ (take c x ++ zero : drop (c+1) x, v <-> x !! c <**> snd (last xs)) | (x,v) <- init xs ] (c-1) ++ [last xs] --Ejemplos: --jordan (M [Vec [1,0,2], Vec [2,1,-3], Vec [4,1,8]],Vec [4,5,6]) --([1.0,0.0,0.0] --[2.0,1.0,0.0] --[4.0,1.0,8.0] --,[-8.0,23.0,6.0]) -- --jordan (M [Vec [1,0,2], Vec [0,1,-7], Vec [0,0,1]], Vec [4.0,-3.0,-1.0]) --([1.0,0.0,0.0] --[0.0,1.0,0.0] --[0.0,0.0,1.0] --,[6.0,-10.0,-1.0]) Finalmente, podemos realizar el método de Gauss-Jordan, con el objetivo de resolver un sistema de ecuaciones de la forma A~ x=~ b. Primero obtenemos la matriz con solo la diagonal que es la obtenida tras aplicar Gauss-Jordan esto lo obtenemos con la función que denotaremos gaussElim . La última función que denotaremos gaussElimCorrect , recibe la partición de la ma- 3.2. Matrices 49 triz Ay el vector columna~ b. Con ella comprobamos dos cosas. La primera que la dimensión de las filas de la matriz Acoincida con la dimensión del vector~ by que A sea una matriz cuadrada. Una vez se cumple esto lo siguiente que comprueba es que el vector que se obtiene de gaussElim al multiplicarlo por la matriz Acoincide con el vector~ b. -- | Eliminación por Gauss-Jordan: Dados A y b resuelve Ax=b. gaussElim :: (Field a, Eq a, Show a) => (Matrix a, Vector a) -> (Matrix a, Vector a) gaussElim = jordan . forwardElim gaussElimCorrect :: (Field a, Eq a, Arbitrary a, Show a) => (Matrix a, Vector a) -> Property gaussElimCorrect m@(a,b) = fst (dimension a) == lengthVec b && isSquareMatrix a ==> matrixToVector (transpose (a `mulM` transpose (M [snd (gaussElim m)]))) == b --Ejemplo: --> gaussElim (M [Vec [1,0,2], Vec [2,1,-3], Vec [4,1,8]],Vec [4,5,6]) --([1.0,0.0,0.0] --[0.0,1.0,0.0] --[0.0,0.0,1.0] --,[6.0,-10.0,-1.0]) --> gaussElim (M [Vec [2,7,3], Vec [1,3,4], Vec [1,4,3]],Vec [-7,3,-2]) --([1.0,0.0,0.0] --[-0.0,1.0,0.0] --[0.0,0.0,1.0] --,[4.0,-3.0,2.0]) 50 Capítulo 3. Vectores y Matrices Capítulo 4 Anillos Coherentes El objetivo de este capítulo será ver cuando un anillo es coherente y fuertemente discreto. Gracias a esto podremos resolver sistemas de ecuaciones sobre estos anillos. Antes de comenzar, introduciremos la noción de anillo fuertemente discreto. 4.1. Anillos Fuertemente Discretos En esta breve sección mostraremos la noción de anillo discreto y fuertemente discreto, lo vemos en el módulo TAHStronglyDiscrete module TAHStronglyDiscrete ( StronglyDiscrete(member) , propStronglyDiscrete ) where import TAHCommutative import TAHIdeal Para desarrollar esta sección, importamos los módulos TAHConmutative y TAHIdeal . Veamos antes unas definiciones teóricas. Definición 4.1.1. Un anillo se llama discreto si la igualdad es decidible. Todos los anillos que consideremos serán discretos. Pero hay muchos ejemplos de anillos que no son discretos. Por ejemplo, Rno es discreto ya que no es posible decidir si dos números irracionales son iguales en tiempo finito. Definición 4.1.2. Un anillo es fuertemente discreto si la pertenencia a un ideal es decidible. 51 52 Capítulo 4. Anillos Coherentes Para introducir este concepto definimos una clase restringida a la clase de tipo Ring: class Ring a => StronglyDiscrete a where member :: a -> Ideal a -> Maybe [a] El objetivo de este método es decidir si un elemento del anillo pertene al ideal, por ello hacemos uso del constructor (Maybe [a]) . En el caso de que no pertenezca al ideal, member devolverá Nothing . Por otro lado, si un elemento pertenece a un ideal, significa que podemos escribir dicho elemento mediante una combinación lineal de los generadores del ideal. Por ello, si el elemento pertenece al ideal, member nos devolverá la lista con los coeficientes de los generadores del ideal al que el elemento pertenece. Para verificar que una especificación concreta de member es correcta definimos una función que denotaremos (propStronglyDiscrete x id@(Id xs)) , esta devolverá un booleano, True cuando member haya funcionado bien y False cuando no haya devuel- to lo esperado. En caso de que no pertenezca al ideal y devuelva Nothing significa que funciona correctamente luego obtendremos True . Si x pertenece al ideal generado por xs entonces comprobará que la lista de coeficientes que member ha devuelto al multiplicarla por la lista de generadores del ideal, xs , la suma resultante es x y entonces devolverá True . propStronglyDiscrete :: (CommutRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool propStronglyDiscrete x id@(Id xs) = case member x id of Just as -> x == sumRing (zipWith (<**>) xs as) && length xs == length as Nothing -> True 4.2. Anillos Coherentes En esta sección, nos ayudaremos del módulo de vectores y matrices creado en el capítulo anterior para construir, en Haskell, la noción de anillo coherente con el objetivo de poder resolver sistemas de ecuaciones. Lo vemos en el módulo TAHCoherent module TAHCoherent ( Coherent(solve) , propCoherent, isSolution , solveMxN, propSolveMxN , solveWithIntersection ) where 4.2. Anillos Coherentes 53 import Test.QuickCheck import TAHIntegralDomain import TAHIdeal import TAHStronglyDiscrete import TAHVector import TAHMatrix Definición 4.2.1. Un anillo R es coherente si dado un vector ~ m∈R1×nexiste una matriz L∈Rn×rpara r ∈Ntal que ~ mL =~ 0y ~ m~ X=0⇔ ∃ ~ Y∈Rr×1tal que ~ X=L~ Y esto es, m1m2· · · mn      l11 l12 · · · l1r l21 l22 · · · l2r . . .. . ..... . . ln1ln2· · · lnr       =0· · · 01×ry m1m2· · · mn      x1 x2 . . . xn       =0⇔ ∃       y1 y2 . . . yr       tal que       x1 x2 . . . xn       =      l11 l12 · · · l1r l21 l22 · · · l2r . . .. . ..... . . ln1ln2· · · lnr             y1 y2 . . . yr       De esta forma es posible calcular las soluciones de un sistema de ecuaciones en un anillo coherente. El vector ~ mes solución del sistema homogéneo y la matriz Lnos proporciona un conjunto de generadores finito de las soluciones del sistema. De esta forma, podemos obtener todas las posibles soluciones del sistema. La propiedad de la coherencia es bastante difícil de implementar en Haskell. El con- 54 Capítulo 4. Anillos Coherentes tenido que se puede implementar es que es posible calcular la matriz Ldada ~ mtal que ~ mL =0. En esta sección todos los anillos de los que partimos son dominios de integridad, por lo que al construir la clase de los anillos coherentes haremos una restricción a la clase de IntegralDomain . Introducimos la clase de anillos coherentes: class IntegralDomain a => Coherent a where solve :: Vector a -> Matrix a Al igual que ocurría con member en el anterior capítulo, aquí solve es una función que no tiene una definición concreta. El objetivo de esta función es que dado un vector ~ m∈Rndevuelva una matriz L∈Rn×rde forma que al multiplicar ambos el vector resultante sea un vector fila de ceros. Para verificar que una definición concreta de solve es correcta especificamos unas funciones para realizar dicha comprobación. La función que denotaremos propCoherent es la encargada de comprobar que la multiplicación de ~ mpor Lsea nula. Para ello, se ayuda de una segunda función que denotaremos por isSolution , esta comprueba que el vector que se obtiene tras la multiplicación de ~ mL es un vector de ceros. -- | Test para comprobar que la multiplicación del vector M por la matriz -- encontrada por solve (la matriz L) sea un vector de ceros. isSolution :: (CommutRing a, Eq a) => Matrix a -> Matrix a -> Bool isSolution m sol = all (==zero) (concat (unMVec (m `mulM` sol))) propCoherent :: (Coherent a, Eq a) => Vector a -> Bool propCoherent m = isSolution (vectorToMatrix m) (solve m) Empezaremos por resolver sistemas de ecuaciones homogéneos sobre un anillo coherente. Nuestro objetivo es encontrar todas las posibles soluciones del sistema homogéneo, solo que esta vez tenemos una matriz My no un vector. Proposición 4.2.1. En un anillo coherente R es posible resolver un sistema M~ X=~ 0donde 4.2. Anillos Coherentes 55 M∈Rr×ny~ X∈Rn×1. Es decir,       m11 m12 · · · m1n m21 m22 · · · m2n . . .. . ..... . . mr1mr2· · · mrn             x1 x2 . . . xn       =    0 . . . 0    r×1 Prueba 4.2.1. Sean ~ mi∈R1×n,~ mi=mi1· · · min las filas de M. Por coherencia es posible resolver ~ m1~ X=0y obtener un L1∈Rn×p1tal que m11 · · · m1n      x1 x2 . . . xn       =0⇔ ∃       y1 y2 . . . yp1       tal que       x1 x2 . . . xn       =      l1(11)l1(12)· · · l1(1p1) l1(21)l1(22)· · · l1(2p1) . . .. . ..... . . l1(n1)l1(n2)· · · l1(np1)             y1 y2 . . . yp1       Si imponemos, ~ m2~ X=0, como ~ X=L1~ Y⇒~ m2L1~ Y=0. Por coherencia sobre ~ Y existe L2∈Rp1×p2tal que ~ m2L1~ Y=0⇔ ∃ ~ Z∈Rp2×1tal que ~ Y=L2~ Z . Por tanto, nos queda que (~ X=L1(n×p1)~ Y(p1×1) ~ Y=L2(p1×p2)~ Z(p2×1) ⇒~ X=L1(n×p1)L2(p1×p2)~ Z(p2×1) Iterando este método la solución ~ X=L1L2· · · Lr~ Z con Li∈Rpi−1×pi, p0=n y ~ Z∈ Rpm×1puede ser calculada. La proposición anterior nos muestra la forma de resolver mediante recursión un sistema M~ X=~ 0, veamos como hacerlo en Haskell. Siguiendo la prueba de la proposición anterior, comenzamos a aplicar coherencia con la primera fila de la matriz My así vamos obteniendo por coherencia una nueva matriz en cada iteración hasta obtener la solución del sistema de ecuaciones. Mediante la función solveMxN calcula la matriz obtenida por recursión L1L2· · · Lr. Con una segunda función, que denotaremos propSolveMxN comprobaremos que la matriz obtenida por solveMxN al multiplicarla 56 Capítulo 4. Anillos Coherentes por la matriz dada Mes solución del sistema homogéneo es decir el resultado de la multiplicación es un vector de ceros. solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a solveMxN (M (l:ls)) = solveMxN' (solve l) ls where solveMxN' :: (Coherent a, Eq a) => Matrix a -> [Vector a] -> Matrix a solveMxN' m [] = m solveMxN' m1 (x:xs) = if isSolution (vectorToMatrix x) m1 then solveMxN' m1 xs else solveMxN' (m1 `mulM` m2) xs where m2 = solve (matrixToVector (mulM (vectorToMatrix x) m1)) -- |Test para comprobar que esta especificación de solve devuelve -- un vector de ceros. propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool propSolveMxN m = isSolution m (solveMxN m) Ahora consideraremos la intersección de dos ideales finitamente generados en un anillo coherente. Esto es necesario para poder resolver más adelante sistemas utilizando la intersección entre ideales. Proposición 4.2.2. La intersección de dos ideales finitamente generados en un anillo coherente R está finitamente generada. Prueba 4.2.2. Sean I =<a1,· · · ,an>y J =<b1,· · · ,bm>dos ideales finitamente generados en R. Consideramos el sistema AX −BY =0, donde A =(a1· · · an)y B =(b1· · · bm) son vectores filas. Como el anillo es coherente, entonces es posible calcular un número finito de generadores {(X1,Y1),· · · ,(Xp,Yp)}de la solución. Esto es, AX1=BY1 . . . AXp=BYp y si (x1,· · · ,xn),(y1,· · · ,ym)verifican A    x1 . . . xn     =B    y1 . . . ym     (4.2) 4.2. Anillos Coherentes 57 Entonces se tiene, ∃λ1,· · · ,λp:    x1 . . . xn     =λ1X1+· · · +λpXp(4.3) ∃µ1,· · · ,µp:    y1 . . . ym     =µ1Y1+· · · +µpYp(4.4) Si z ∈I∩J⇒ ∃ α1,· · · ,αn,β1,· · · ,βm∈R tales que z=α1a1+· · · +αnan=β1b1+· · · +βmbm ⇒(a1,· · · ,an)    α1 . . . αn     =(b1,· · · ,bm)    β1 . . . βm     son soluciones del sistema (4.2). De (4.2),(4.3)y(4.4) se tiene que (a1,· · · ,an)λ1X1+· · · +λpXp=(b1,· · · ,bm)µ1Y1+· · · +µpYp =λ1AX1+· · · +λpAXp=µ1BY1+· · · +µpBYp Por tanto, un conjunto de generadores para la intersección es {AX1,· · · ,AXp}y otro conjunto de generadores es {BY1,· · · ,BYp}. A continuación daremos una proposición importante en la teoría de anillos coherentes, con ella podemos probar si un anillo Res coherente. Proposición 4.2.3. Si R es un dominio de integridad tal que la intersección de dos ideales finitamente generados está finitamente generada, entonces R es coherente. Prueba 4.2.3. Lo probaremos mediante inducción en la longitud del sistema a resolver. Primero consideramos ax =0. Aquí la solución es trivial, pues R es un dominio de integridad, por lo que a 6=0, por tanto se tiene que x =0. Suponemos cierto que es posible resolver un sistema en (n−1)variables y consideramos el caso con n ≥2variables: a1x1+· · · +anxn=0 64 Capítulo 4. Anillos Coherentes Nothing -> True Apéndice A Como empezar con Emacs en Ubuntu En este capítulo se hace una breve explicación de conceptos básicos para empezar a redactar un documento a LaTeX en Emacs y con Haskell a la vez, así como ir actualizando los archivos junto con la plataforma Github. Comenzaremos explicando como realizar la instalación de Ubuntu 16.04 en un PC con windows 10. A.1. Instalar Ubuntu 16.04 junto a windows 10 Para realizar la instalación de Ubuntu junto a windows necesitaremos los siguientes programas: Rufus-2.17 Ubuntu 16.04 También necesitaremos un pen drive para usarlo de instalador. Paso 1: Descargamos Ubuntu 16.04 y rufus-2.17 desde sus respectivas web (o enlaces dados anteriormente). Necesitamos saber que tipo tiene nuestro disco duro, esto lo podemos ver haciendo click derecho sobre el icono de windows (abajo izquierda) y le damos a administrador de equipos ->administrador de discos, y nos aparecerá nuestro disco duro con todas sus subparticiones internas, en el general nos pondrá si es NTFS o MBR. 65 66 Apéndice A. Como empezar con Emacs en Ubuntu Paso 2: •Conectamos el pen al PC y abrimos el programa rufus, el propio programa reconocerá el pen, sino en la pestaña de dispositivo marcamos el pen. •En Tipo de partición si nuestro disco es NTFS marcamos GPT para UEFI, en caso contrario uno de los otros dos MBR. •En la parte de opciones de formateo marcamos (aunque deben de venir marcadas): Formateo rápido •Crear disco de arranque con ->seleccionamos imagen ISO y hacemos click en el icono de la derecha para adjuntar la imagen ISO de Ubuntu que hemos descargado anteriormente. •Añadir etiquetas extendidas e iconos. •Seleccionamos empezar. Paso 3: Dejamos el pen conectado al PC y reiniciamos el ordenador, al reiniciar justo antes de que cargue pulsamos F2 (o F1 según el PC) para acceder a la bios del PC y aqui nos vamos a la zona de arranque de cada sistema (esto cada bios es diferente). Tenemos que colocar el pen en la primera posición, que en esta debe estar windows, de esta forma iniciamos con el pen y comenzamos a instalar Ubuntu. Seguimos los pasos que el programa de instalación nos indica, solo tenemos que marcar España cuando nos lo pida y dar el espacio que queramos a Ubuntu (con unos 40 GB es suficiente), el propio programa se encarga de hacer la partición del disco duro. Paso 4: Una vez instalado Ubuntu, nos vamos al icono naranjita que se llama software de Ubuntu y actualizamos. Tras realizar todos estos pasos, cuando iniciemos el PC nos debe dar a elegir entre iniciar con Ubuntu o con Windows 10. Recomiendo buscar en youtube un video tutorial de como instalar Ubuntu junto a windows 10. A.2. Iniciar un Capítulo 67 A.2. Iniciar un Capítulo El editor de Emacs podemos descargarlo de su página web, la instalación es muy sencilla y guiada. Del mismo modo, instalamos Haskell 8.0.2. Una vez tenemos ambos programas instalados, procedemos a iniciar un capítulo en Haskell literario. Paso 1: Abrimos el directorio desde Emacs con Ctrl+x+d y accedemos a la carpeta de texto para crear el archivo nuevo .tex sin espacios. Aquí escribiremos la introducción a nuestro capítulo y secciones. Desde este fichero .tex se importarán los módulos. Paso 2: Hacemos lo mismo pero en la carpeta código y guardamos el archivo con la abreviatura que hemos usado en el .tex, el archivo lo guardamos como .lhs para tener ahí el código necesario de Haskell. Estos serán los módulos donde desarrollaremos las secciones con Haskell literario, es decir, escribiremos a Latex y a su vez tendremos el código de Haskell. Paso 3: Al acabar el capitulo hay que añadir el capítulo al resto del trabajo. Para ello, nos vamos al archivo que contiene todo el trabajo que en nuestro caso se llama ’TFG.tex’ , importante coger el de la extensión .tex, nos vamos a la zona donde incluimos los capitulos y usamos el comando de LaTeX con el nombre que le dimos en la carpeta de texto: include{’nombre sin el .tex’} A.3. Abreviaciones de Emacs La tecla ctrl se denominara C y la tecla alt M, son las teclas mas utilizadas, pues bien ahora explicamos los atajos más importantes y seguiremos la misma nomenclatura de la guía para las teclas: ctrl es llamada C y alt M. 68 Apéndice A. Como empezar con Emacs en Ubuntu Para abrir o crear un archivo: C+x+C+f Para guardar un archivo: C+x+C+s Para guardar un archivo (guardar como): C+x+C+w Si abriste mas de un archivo puedes recorrerlos diferentes buffers con C+x+←o→ Emacs se divide y maneja en buffers y puedes ver varios buffers a la vez (los buffers son como una especie de ventanas). Para tener 2 buffers horizontales: C+x+2 Para tener 2 buffers verticales: C+x+3 Para cambiar el puntero a otro buffer: C+x+o Para tener un solo buffer: C+x+1 Para cerrar un buffer: C+x+k Si por ejemplo nos equivocamos en un atajo podemos cancelarlo con: C+g Para cerrar emacs basta con: A.4. Push and Pull de Github con Emacs 69 C+x+C+C Para suspenderlo: C+z A.4. Push and Pull de Github con Emacs Vamos a mostrar como subir y actualizar los archivos en la web de Github desde la Consola (o Terminal). Lo primero que debemos hacer es abrir la Consola: Ctrl+Alt+T Escribimos los siguientes comandos en orden para subir los archivos: cd ’directorio de la carpeta en la que se encuentran las subcarpetas de código y texto’ ejemplo: cd Escritorio/AlgebraConEnHaskell/ git add . (de esta forma seleccionamos todo) git commit -m ’nombre del cambio que hemos hecho’ git push origin master A continuación, nos pedirá el nombre de usuario de GitHub, lo ponemos y seguidamente nos pedirá la contraseña, al ponerla se subirán los archivos a la plataforma de GitHub. Para descargar los archivos hacemos lo mismo cambiando el último paso por: git pull origin master 70 Apéndice A. Como empezar con Emacs en Ubuntu Bibliografía [1] J. Alonso. Temas de programación funcional. Technical report, Univ. de Sevilla, 2015. [2] J. Alonso. Tipos y clases en Haskell. Technical report, Univ. de Sevilla, 2016. [3] T. Coquand. Coherent Ring. Technical report, University of Gothenburg, 2010. [4] M. Gago. Sistemas de ecuaciones lineales. Technical report, Univ. de Sevilla, 2015. [5] J. González-Meneses. Tema 3: Anillos. Technical report, Univ. de Sevilla, 2015. [6] A. Mörtberg. “Constructive Algebra in Functional Programming and Type Theory”. Tesis de máster, University of Gothenburg, 2010. [7] G. Hutton. “Programming in Haskell”. Cambridge University Press, 2016. [8] A. Serrano. “Beginning in Haskell”. Utrecht University, 2014. [9] “¡Aprende haskell por el bien de todos!”. Technical report, aprendehaskell.es, 2018 [10] Haskell Language. haskell.org, 2018 71 Índice alfabético <-> ,21 </> ,26 Mult. por la derecha (<**) ,22 Posición (i+1,j+1) ,37 Potencia ,21 Relación de semi-igualdad ,21 addCol ,43 addId ,30 addM ,39 addRow ,43 dimension ,39 fE ,46 findPivot ,45 forwardElim ,46 fromId ,29 gaussElimCorrect ,49 gaussElim ,49 identity ,40 isPrincipal ,29 isSameIdeal ,31 isSolutionB ,62 isSolution ,54 isSquareMatrix ,39 jordan ,48 lengthVec ,34 matrixToVector ,37 matrix ,37 mulId ,30 mulM ,39 mulVec ,35 pivot ,45 productRing ,21 propAddAssoc ,20 propAddComm ,20 propAddIdentity ,20 propAddInv ,20 propAddRowDimension ,43 propCoherent ,54 propCommutRing ,23 propField ,26 propIntegralDomain ,24 propLeftDist ,20 propLeftIdentity ,40 propMulComm ,23 propMulIdentity ,20 propMulInv ,25 propRightDist ,20 propRightIdentity ,40 propRing ,20 propScaleDimension ,41 propSolveGeneralEquation ,62 propSolveGeneral ,63 propSolveMxN ,56 propStronglyDiscrete ,52 propSwapDimension ,42 propSwapIdentity ,42 propZeroDivisors ,24 scaleMatrix ,41 solveGeneralEquation ,62 solveGeneral ,62 solveMxN ,56 solveWithIntersection ,59 subCol ,43 subRow ,43 72 Índice alfabético 73 sumRing ,21 sumVec ,35 swap ,42 transpose ,39 unMVec ,37 unM ,37 unVec ,34 vectorToMatrix ,37 zeroIdealWitnesses ,31 zeroIdeal ,28