I1M2012: División y factorización de polinomios mediante la regla de Ruffini en Haskell

PorJosé A. Alonso

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los 6 primeros ejercicios de la relación 25. El objetivo de la relación es implementar la regla de Ruffini y sus aplicaciones utilizando las implementaciones del TAD de polinomio estudiadas en el tema 21.

En los ejercicios se usan las siguientes librerías:

  • PolRepTDA: Implementación de los polinomios mediante tipos de datos algebraicos.
  • PolRepDispersa: Implementación de los polinomios mediante listas dispersas.
  • PolRepDensa: Implementación de los polinomios mediante listas densas.
  • PolOperaciones: Operaciones con el TAD de los polinomios.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: División y factorización de polinomios mediante la regla de Ruffini en Haskell”

I1M2012: Operaciones con el TAD de los polinomios en Haskell (2)

PorJosé A. Alonso

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha continuado la resolución de los ejercicios de la relación 24. El objetivo de esta relación es ampliar el conjunto de operaciones
sobre polinomios definidas utilizando las implementaciones del TAD de
polinomio estudiadas en el tema 21. Además, en algunos ejemplos de usan polinomios con coeficientes racionales. En Haskell, el número racional x/y se representa por x%y. El TAD de los números racionales está definido en el módulo Data.Ratio.

En los ejercicios se usan las siguientes librerías, estudiadas en el tema 21,

  • PolRepTDA: Implementación de los polinomios mediante tipos de datos algebraicos.
  • PolRepDispersa: Implementación de los polinomios mediante listas dispersas.
  • PolRepDensa: Implementación de los polinomios mediante listas densas.
  • PolOperaciones: Operaciones con el TAD de los polinomios.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Operaciones con el TAD de los polinomios en Haskell (2)”

Reseña: A constructive theory of regular languages in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado A constructive theory of regular languages in Coq.

Sus autores son Christian Doczkal, Jan-Oliver Kaiser y Gert Smolka (de la Univ. de Sarre (en alemán: Saarland), Alemania).

Su resumen es

We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect’s support for finite types and graphs.

El código de las correspondientes teorías en Coq se encuentra aquí.

Reseña: A formal proof of Kruskal’s tree theorem in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado A formal proof of Kruskal’s tree theorem in Isabelle/HOL.

Su autor es Christian Sternagel (del JAIST, Japón).

Su resumen es

We give the first formalization of Kruskal’s tree theorem in a proof assistant – the closure of a long-standing challenge. More concretely, we present our Isabelle/HOL development of Nash-Williams’ minimal bad sequence argument for proving the tree theorem. Along the way, we discuss proofs of Dickson’s lemma and Higman’s lemma; and close all gaps in the original proofs.

El código con las correspondiente teorías en Isabelle/HOL se encuentra aquí.

I1M2012: El TAD (tipo abstracto de datos) de las tablas en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla (array en inglés y tableau en francés) es una colección de elementos (valores) a los que se accede mediante sus índices.

El contenido de la clase ha sido el siguiente:

  • la signatura del TAD de las tablas;
  • las propiedades del TAD de las tablas;
  • las implementaciones, en Haskell, de las tablas mediante funciones, listas de asociación y matrices y
  • la comprobación con QuickCheck de sus propiedades.

Read More “I1M2012: El TAD (tipo abstracto de datos) de las tablas en Haskell”